0

Context: I've been reading through the Dover English translation of Godel's paper "On Formally Undecidable Propositions of Principia Mathematica and Related Systems".

It seems the key to producing Godel formulas is the generalization operation, such as the formula "17 Gen r". Without generalization, it seems impossible to create an unprovable formula.

Looking through the axioms and proof schema earlier in the paper, I did not see any that would allow introduction of generalization. This suggests to me that many generalized formula are unprovable in Godel's system in the sense that any proof of a generalized formula would require another generalized formula as a premise. Assuming there's no infinite regress, then working backwards means we end up with a primal generalized formula which has no proof, since there is no precursor generalized formula. Unless there is a "super generalized formula" that can prove most other generalized formula, which seems implausible, this means there are loads and loads of unprovable generalized formula.

In which case, "17 Gen r" is not particularly notable in being unprovable, except for the fact that we can interpret it as saying "this formula is unprovable" and consequently more formally prove its unprovability.

Am I missing something here?

yters
  • 35
  • 1
    Generalization rule is part of the underlying logic: we need it (or some equivalent) in order to have a sound and complete proof system for predicate logic. – Mauro ALLEGRANZA Dec 16 '22 at 07:29
  • Is it possible to infer |- P(y) without some sort of universal quantification on the left of the turnstile? From the example in the article, it looks like the generalization rule requires a prior generalization in the set of formula to the left of the turnstile, just as my question assumes. – yters Dec 16 '22 at 07:50
  • Details of original GIT proof are relevant for understanding the "diagonal" technique used. You can see this post regarding the formal system used, this post regarding godel numebring. – Mauro ALLEGRANZA Dec 16 '22 at 09:06
  • See also this one regarding formulas and this one regarding proofs. – Mauro ALLEGRANZA Dec 16 '22 at 09:06
  • 1
    The details of G's proof system are in ch.2. page 45 of Dover reprint you can find the two rules of inference: "a formula $c$ is called an immediate consequence of $a$ and $b$, if $a$ is the formula $(\lnot b) \lor c$ [i.e. $b \to c$; this is Modus Ponens], and an immediate consequence of $a$, if $c$ is the formula $v \Pi (a)$ [i.e. $(\forall x)a$], where $v$ denotes any given variable [and this is Generalization]." – Mauro ALLEGRANZA Dec 16 '22 at 09:49
  • "Is it possible to infer $\vdash P(y)$ without some sort of universal quantification on the left of the turnstile?" Yes; see Ax.I.1 $\lnot (f x_1=0)$, one of original Peano axioms. Applying Gen to it we get $x_1 \Pi (\lnot (f x_1=0))$ corresponding to modern: $(\forall x_1)\lnot (s(x_1=0))$. – Mauro ALLEGRANZA Dec 16 '22 at 10:10
  • 1
    IMO you are misunderstanding what the author is trying to do... IF the formal system F for arithmetic is consistent, there are lots of formulas that are not provable: e.g. $\forall x (x=1)$. What the author is doing is to build a formula G of formal system F such that - if the system is consistent - then both G and not-G are unprovable, contrary to our expectation that the system F is sufficient to derive all true facts about arithmetic. – Mauro ALLEGRANZA Dec 16 '22 at 10:58
  • @MauroALLEGRANZA aha, yes I see that on page 45, thanks! – yters Dec 16 '22 at 11:06

0 Answers0