Talk:Proof theory

From Wikipedia, the free encyclopedia

WikiProject Mathematics
Mathematics Portal
This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.
Mathematics rating: B Class High Priority  Field: Foundations, logic, and set theory
This article has been reviewed by the Version 1.0 Editorial Team.

Contents

[edit] Taku's merge suggestion

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:

--Markus[sorry, currently no login]

[edit] 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)

[edit] Questionable prehistory

Deleted the following (sorry, forgot to put an edit summary):

That represents the position as of about 1940 onwards. The subject of proof theory has a significant if somewhat opaque prehistory as metamathematics, the proposed theory under development since the start of the twentieth century, which was, for a generation, under the influence of David Hilbert. The aim of a convincing consistency proof for mathematics was not to be realised, for reasons only later understood: proof theory can only sweep the metaphysical dust into tidier heaps under carpets with more attractive patterns. Hilbert's ideas seem to have been based on an analogy, in fact false, with the elimination theory of algebraic geometry familiar to him from his early work in algebra. The real insights of proof theory, such as cut-elimination and the isolation of the structural rules, were not to come from this direction.

There's already a history section. This "prehistory" looks like a one-sided attack and definitely doesn't belong in the introduction.

[edit] IF logic and proof theory

IF logic, as far as I know, admits of a proof-theoretic characterization using e.g. a natural deduction calculus. In fact, in several articles he gives modified definitions for quantifier intelim rules. However, it does not admit of a complete characterization, or if it does, then not a finitely axiomatizable one.

Since IF logic is equivalent to the Sigma-1-1 fragment, all properties of the latter carry over to the former. Nortexoid 20:44, 5 May 2006 (UTC)

[edit] Looking for citation

Where is proof theory described as one of the four pillars of foundations of mathematics?

[edit] Math rating B+

The later summary sections get shorter and shorter. The history section could use an inline citation to a published history of the field. A section describing current work in the area would round out the coverage, which is currently mostly historical. CMummert 14:19, 25 October 2006 (UTC)

I looked up what a class B article is. This may very well be in need of improvement. Be that as it may, I wish to express my thanks to the people who have written what there is today. I am completely uninitiated in the subject and found the article both informative and fascinating. Elmer 21:53, 09 March 2008 (Central Time)

[edit] Proposed merge

I've proposed that logic system be merged into this article (proof theory) or one of its subarticles. To the extent that there's something there in logic-system, it's an abstraction or example (depending on the precise structure) of a formal proof system. — Arthur Rubin | (talk) 19:53, 16 November 2006 (UTC)

Withdrawing merge request. A better target has been found. — Arthur Rubin | (talk) 15:43, 17 November 2006 (UTC)