Talk: Proof theory

From open-encyclopedia.com - the free encyclopedia.

I think we should merge proof theory and proof (math) because to me they seem the same thing, but I am not sure enough to do that. Any though? -- Taku 00:26 2 Jun 2003 (UTC)

Hmm, careful. While I have no clue about the subject, it seems like Proof theory is a sort of meta- discussion about proofs. I'd leave it. Evercat 00:28 2 Jun 2003 (UTC)

I mean the definition of them can vary; mathematical proof is a formal proof in math while proof theory is the study of proof. I mean I guess I am not sure after all. I will leave this for more knowledgable people. -- Taku 05:01 2 Jun 2003 (UTC)

They are different fields, one is an area of study in logic (including mathematical logic), the other is a tool used by mathematicians. There's much less overlap between the two fields than one might think. ---- Charles Stewart 09:12, 16 Aug 2004 (UTC)

I have changed a lot in this entry [and its vicinity] but tried to preserve most of the old information as well. I hope I have been able to clarify some of the above concerns. I think proof theory deserves much more information and I will try (if time permits) to add additional pages on the subject: the sequent calculus LK, the related system NK (there is some page on natural deduction---lets see), (NJ, LJ may be included in intuitionistic logic), once the notions of sequent calculus are explained, substructural logics can be added. A note on cut-elimination would also be nice... OK, thats all about it. -- Markus[sorry, currently no login] 23 Jun 2003

I'm not sure I agree in detail with the changes. I'll think about it. I do agree that some technical proof theory has a clarifying effect.

Charles Matthews 19:20 23 Jun 2003 (UTC)

Yes, I suppose details are always left to improve. In case the main direction of this entry is OK, I think improvements should not be a matter of much discussion. I also would like some more detailed historical background including how Russels Paradox and the foundational crisis in mathematics made people think about purely formal proofs for mathematical statements, and how this had to be given up due to Gödels findings on incompleteness. Maybe someone knows about this issues in detail? -- Markus[sorry, currently no login] 24 Jun 2003

There's a fair amount here about that already, spread over pages like naive set theory, Russell's paradox, Gottlob Frege, symbolic logic, philosophy of mathematics. As you say, there is pre-Gödel and there is post-.

Charles Matthews 12:02 24 Jun 2003 (UTC)

Of course you are right. It is just that these issues influenced proof theory quite a lot and in fact Gödels incompleteness is a theorem of proof theory. Maybe one could have some pointers. Surely not the main concern at the moment... -- Markus[sorry, currently no login] 18:16 24 Jun 2003 (UTC)

Newly created pages:

• sequent
• rule of inference
• sequent calculus (very extensive and hopefully helpful)

--Markus[sorry, currently no login]

Informal use?

I've deleted the following section:

More informally , the term proof theory is also used (in logic classes, for example) to refer to a concrete calculus. For example, one may state that there is no proof theory for second-order logic, meaning that there is no syntactical calculus for this logic that simultaneously (1) is sound, and (2) is complete, and (3) is decidable (admits a proof-checking algorithm). First-order logic and many logics "below" admit a proof theory.

because, while it documents a standard usage, it is perfectly comprehensible formally. ---- Charles Stewart 18:34, 25 Aug 2004 (UTC)