Thread: Proof theory: example of an existence proof of a proof?

I would like an example of a sentence S whereby the statement Prov_T("S") has a non-constructive proof, where Prov_T("S") means "There exists a proof (in the system T) of the codification (e.g. Gödel number) of S."

That is, non-constructive existence proofs (whereby it is proven that an object with given properties exists without exhibiting the object itself) are common, but the ones I know about are not about (codifications of) proofs. I would like to be able to have a proof A that there is a proof B about something non-tautological. Of course, to be rigorous, one would further codify to bring it all onto one level, but an example with A and B being on two different levels is acceptable.

Thanks.

I would like to be able to have a proof A that there is a proof B about something non-tautological.

Every mathematical theorem is a tautology

The thing hat comes to mind is the Henkin's proof of completeness. One can formalize the semantics of, say, propositional logic, in Peano arithmetic and prove completeness by showing that if a formula is not derivable, then there exists a countermodel. Under the assumption that the formula is a tautology, this will yield a nonconstructive proof that the formula is derivable. It is probably possible to do this not only for propositional logic, but for some fragments of first-order logic, such as for formulas with at most n nested alternating quantifiers.

Note, by the way, that any proof of Prov_T("S") is not essentially nonconstructive because there is an algorithm (Gödel–Gentzen negative translation) that turns any such proof into a constructive one. Please ask if you need more details about this.

Originally Posted by emakarov

Every mathematical theorem is a tautology

This depends on your definition of theorem. I consider, say, the Continuum Hypothesis as a valid but not tautological theorem, while you might require the full statement "L |= CH" as the theorem.

Originally Posted by emakarov

The thing hat comes to mind is the Henkin's proof of completeness.

Thanks! Perfect example.

Originally Posted by emakarov

Note, by the way, that any proof of Prov_T("S") is not essentially nonconstructive because there is an algorithm (Gödel–Gentzen negative translation) that turns any such proof into a constructive one. Please ask if you need more details about this.

Interesting. I will take you up on your offer of more details, as the Wiki link does not give the proof. I would like to see the proof before I see it as an algorithm. The double-negation method in Glivenko's theorem is an algorithm, but this is only valid for propositions without quantifiers, whereas the provability formula has the existence quantifier. Therefore there must be something more to the proof of Gödel–Gentzen for Peano. Do you have a link for this proof?

Originally Posted by emakarov

Every mathematical theorem is a tautology

Even in the sense of 'tautology' as 'logically valid formula' (not necessarily restricted to logically valid formulas whose validity may be shown by mere sentential structure), it is not the case that every mathematical theorem is a tautology. Not even the non-logical axioms of set theory are logically valid. Indeed, by definition, any non-logical axiom is not logically valid, thus there are theorems of such systems (ones that have non-logical axioms) that are not logically valid (starting even with the non-logical axioms themselves).

Originally Posted by nomadreid

This depends on your definition of theorem. I consider, say, the Continuum Hypothesis as a valid but not tautological theorem

In the sense of 'theorem' in mathematical logic, EVERY formula is a theorem of some system or another.

This is some promised details about Gödel–Gentzen negative translation.

Let's start by noting that the relation Proof(x, y), which means that x is (the code of) a proof of a formula (with the code) y, is primitive recursive. This means that its characteristic function is primitive recursive, and it also means that it can be written as a formula of Peano Arithmetic, i.e., a formula that has only bounded quantifiers. Actually, the latter fact is very tedious to show, so I prefer working with the version of PA that has functional symbols and defining equations for all primitive recursive functions, not only addition and multiplication. Then Proof(x, y) can be represented as f(x, y) = 0 for some primitive recursive function f. Therefore, Prov(y) is , i.e., a (i.e., existential) formula.

Gödel-Gentzen translation puts double negation in front of existential quantifiers, disjunctions, and atomic formulas, i.e., equalities. Actually, equalities are decidable in both Peano and Heyting (i.e., intuitionistic Peano) arithmetic (HA), which means that is provable. (This is done by induction first on x and then on y.) Therefore, one can prove , so the version of the translation where atomic formulas are unchanged is equivalent to Gödel-Gentzen translation (i.e., the resulting formulas are provably equivalent).

The correctness theorem for the translation says that implies where is the result of the translation. Therefore, if , then .

In fact, is derived already in minimal logic, which is like intuitionistic but without the axiom for every P. Thus, the symbol does not play any special role in minimal logic. (Here I may be a little fuzzy about the axioms of PA since, say uses . It can probably be replaced by the schema for every P.)

Since does not play a special role and , we can substitute for and get a proof of in minimal logic.

Proving the translation correctness theorem is pretty straightforward by induction on derivation because the translation commutes with most connectives. One has to prove a lemma that , which is , implies , by induction on A, in order to handle the double negation elimination rule.

Instead of Gödel-Gentzen translation, one can also use Kuroda translation, which is a generalization of the procedure used in Glivenko's theorem to first-order logic. Kuroda translation inserts double negation after the universal quantifiers and before the whole formula, but its target is intuitionistic, not minimal logic.

All this is called conservativity of PA over HA for formula, i.e., formulas of the form where A is . It is a well-known result due to Georg Kreisel and Harvey Friedman.

I'll try to send you a message with an excerpt from Troelstra and van Dalen book that I have as well as my thesis.

Some sources:

Friedman, Harvey. 1978. Classically and intuitionistically provably recursive functions. In D.S. Scott and G.H. Müller, eds., Higher Set Theory, volume 669 of Lecture Notes in Mathematics, pp. 21–27. Springer-Verlag.
The first syntactic proof of conservativity of PA over HA for Pi_2 formulas.

Daniel Leivant: Syntactic Translations and Provably Recursive Functions. J. Symb. Log. 50(3): 682-688 (1985)
Syntactic proof of conservativity of classical over constructive logic for a wide class of formulas.

Troelstra, Anne S. and Dirk van Dalen. 1988. Constructivism in Mathematics, volume 121 of Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam.
Especially volume 1, sections 2.3, 3, 5. In particular, repeats Leivan't results above.

Troelstra, Anne S. and Helmut Schwichtenberg. 2000. Basic Proof Theory.
Cambridge University Press, 2nd edition.
Has description and proofs concerning Gödel-Gentzen and Kuroda translations.