Definition talk:Tableau Proof/Natural Deduction

Wider context

Ben-Ari introduces a tableau proof method for the Gentzen system I put up yesterday. It occurred to me that the presentational technique is not limited to natural deduction, only to the extent one can conveniently write the expressions on a single line.

Therefore, I have created a tentative adaptation of this page, situated at Definition:Tableau Proof (Formal Systems). As far as I'm concerned, it can replace this page entirely, but perhaps you think there should be subpages on the new page, one per proof system using it.

At the very least, it's a step forward, unlocking more proof systems for the future. In the near future, I will also be adding a Hilbert-style system, which will bring the total of rigorous proof systems to four, the others being natural deduction and tableau proofs. It gets easier when the structure is in place and the process has become modular.

TL; DR: Progress! — Lord_Farin (talk) 10:45, 29 March 2014 (UTC)

I need to go away and think about all this ... as you see, I'm making similar progress on some of the messy bits in complex analysis at the moment and I don't want to lose the thread.

Incidentally, I have Proof Theory by Takeuti on the book pile (a veritable avalanche of books has recently arrived in my collection and I haven't had a chance to really open it yet) and this appears to use Gentzen's approach.

As I say, I will take the time to revisit all this in due course. Carry on with your stuff, and when it's bedded down I can incorporate the approaches I have studied and see whether it can be further generalised. --prime mover (talk) 22:46, 29 March 2014 (UTC)

Will do. For now, I'll let the pages coexist. — Lord_Farin (talk) 22:58, 29 March 2014 (UTC)

Including the various proof metastructures as subpages, transcluded, sounds like the way to go; but the parts of those subpages which actually appears on this page should be minimised as much as possible, so as to allow this page to be kept relatively compact.

As for replacing this with that, I'm on it. --prime mover (talk) 09:42, 30 March 2014 (UTC)

I have migrated Definition:Tableau Proof/Natural Deduction to Definition:Tableau Proof (Formal Systems) and moved all the links as appropriate. I have left Definition:Tableau Proof (Natural Deduction) and everything that links to it (it's part of a template anyway), redirecting it to Definition:Tableau Proof (Formal Systems), with a view to pointing it to something more specific in due course, once we have generated some instance-specific subpages of Definition:Tableau Proof (Formal Systems).

Hope this is okay -- incidentally I found a mistake in the Lemmon links which I was then able to fix, so that's good. --prime mover (talk) 09:57, 30 March 2014 (UTC)

The current form suffices for now; we'll look into improving the coverage of specific approaches in due time. Perhaps a subpage/subsection simply listing the proof systems using tableau proofs would suffice, with each system definition page containing the specific details for writing the proofs -- kind of like the ND instance is currently set up. — Lord_Farin (talk) 14:36, 30 March 2014 (UTC)