Results 1 to 6 of 6

Math Help - Proof theory: example of an existence proof of a proof?

  1. #1
    Member
    Joined
    Aug 2010
    Posts
    130

    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.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,530
    Thanks
    774
    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.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Member
    Joined
    Aug 2010
    Posts
    130

    Excellent example, thanks; yes, please, more details

    Quote Originally Posted by emakarov View Post
    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.

    Quote Originally Posted by emakarov View Post
    The thing hat comes to mind is the Henkin's proof of completeness.
    Thanks! Perfect example.

    Quote Originally Posted by emakarov View Post
    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?
    Follow Math Help Forum on Facebook and Google+

  4. #4
    Senior Member
    Joined
    Feb 2010
    Posts
    466
    Thanks
    4
    Quote Originally Posted by emakarov View Post
    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).
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Senior Member
    Joined
    Feb 2010
    Posts
    466
    Thanks
    4
    Quote Originally Posted by nomadreid View Post
    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.
    Follow Math Help Forum on Facebook and Google+

  6. #6
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,530
    Thanks
    774
    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 \Delta_0 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 \exists x.\,f(x, y) = 0, i.e., a \Sigma_1 (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 \forall x, y.\,x=y\lor x\ne y is provable. (This is done by induction first on x and then on y.) Therefore, one can prove \forall x,y.\,\neg\neg x=y\to x=y, 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 \text{PA}\vdash A implies \text{HA}\vdash A^g where A^g is the result of the translation. Therefore, if \text{PA}\vdash \text{Prov}(n), then \text{HA}\vdash\neg\neg\exists x.\,f(x,n)=0.

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

    Since \bot does not play a special role and \text{HA}\vdash((\exists x.\,f(x,y)=0)\to\bot)\to\bot, we can substitute \exists x.\,f(x,y)=0 for \bot and get a proof of \exists x.\,f(x,y)=0 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 (\neg\neg A)^g, which is \neg\neg A^g, implies A^g, 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 \Pi_2 formula, i.e., formulas of the form \forall x\exists y.\,A(x,y) where A is \Delta_0. 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.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Replies: 15
    Last Post: July 16th 2011, 12:22 PM
  2. [SOLVED] Existence proof
    Posted in the Number Theory Forum
    Replies: 6
    Last Post: September 23rd 2010, 09:18 AM
  3. existence proof, how to start?
    Posted in the Trigonometry Forum
    Replies: 1
    Last Post: April 12th 2010, 09:34 PM
  4. proof of existence of z in x < z < y
    Posted in the Differential Geometry Forum
    Replies: 3
    Last Post: May 24th 2009, 10:54 AM
  5. existence of proof in connection to x^2 = y^2 mod n
    Posted in the Number Theory Forum
    Replies: 2
    Last Post: November 13th 2008, 04:24 PM

Search Tags


/mathhelpforum @mathhelpforum