User talk:Lord Farin/Tableau Proof Rules

Quick question: how (if at all) does one use definitions in a tableau proof? For instance, how does one use set union notation? One can use sequent introduction or some such to bring in the axiom of union, but that in itself doesn't allow the use of the term union, or the notation for it. --Dfeuer (talk) 09:25, 11 March 2013 (UTC)

Presently tableaux are only used in the empty signature (i.e. bare logic). In any other case, such notation would formally require to enlarge the signature by a symbol and impose an axiom that specifies its definition in terms of the language one started with. This is hardly the place to discuss this, though. My talk page would be a more appropriate place. — Lord_Farin (talk) 09:31, 11 March 2013 (UTC)

The "Tableau proof" presentation is required only for propositional / predicate logic when using the "Natural Deduction" approach to proving logical theorems. For presentation of conventional mathematics (including set theory), the usual technique (as has already been demonstrated to work perfectly adequately over the last 4+ years) is appropriate. As always, I do not believe there is any advantage to redesigning our presentational paradigms without an extremely good argument in its favour. --prime mover (talk) 09:57, 11 March 2013 (UTC)

If you disagree, take a look at http://us.metamath.org/ and navigate around. They've taken the tableau method way beyond its readability limit, to the point of numbing impracticality. — Lord_Farin (talk) 10:13, 11 March 2013 (UTC)