Not quite. Not "For all Godel numbers p," but instead, for all x, x being any natural number. Some xs will be ps, most not. Them that aren't won't be (encode) a proof, and them that are also won't be a proof. — tim wood
Sorry, that was actually a typo. Nevertheless this exchange perhaps serves as a useful reminder that
any number represents a legitimate theorem relative to the provability-predicate of
some Godel-numbering system.
Furthermore, for
any provability predicate Prov('X','S') interpreted as saying 'X' encodes a proof of 'S', it isn't actually knowable which numbers represent legitimate proofs, due the possibility that Peano-arthmetic is inconsistent and proves absurdity, together with Godel's second incompleteness theorem which forbids the possibility of PA representing it's own consistency. Neither humans nor God can ever claim knowledge of PA's consistency, for all we can have are proofs of consistency relative to the consistency of other systems, which begs the question.
Of course, it is standard practice to explicitly state consistency as an assumption when we informally interpret PA and discussing incompleteness, so your remark is valid, after a bit of clarification. My political agenda here is actually concerned with how to interpret PA
without assuming consistency, in light of Godel's results. For there are arguably many conceptual benefits to be had by dropping the consistency assumption, that demonstrate the fundamentally empirically contigent, vague and indeterminate nature of logic and mathematics that is better understood as being
a posteriori in nature.
Incompleteness is the result of unlimited universal quantification in Peano's axiom of induction, that takes us from the non-controversial constructive semantics of quantifier-free Primitive Recursive Arithmetic that represents the predictably terminating algorithms, to the controversial non-constructive interpretations of PA that represents every possible algorithm. Logic should therefore replace the simplistic sign of universal quantification for a richer collection of signs that distinguishes the different use-cases of the original sign, whilst also making explicit the relation of the Axiom of choice to universal quantification. David Hilbert in fact did use a system closer to this, called the epsilon-calculus during his attempts to prove consistency, and it is in fact making a come back.
And the universal quantifier is both part of the proof, and proved separately within the proof. — tim wood
Consider universal quantification over the negative-provability predicate in PA, that is informally interpreted as saying " For
every 'S', 'S' doesn't prove 'G' ".
We know for a fact that this has no syntactical expression in PA, since if PA is consistent then the statement isn't decidable (via the Diagonalization lemma) and if PA is inconsistent then PA is unsound and has no interpretation whatsoever. We also know that for any
particular 'S' and 'G', PA
can decide whether or not 'S' derives 'G'.
Therefore the universal quantifier above
cannot have the ordinary meaning of
every, which ought to have been the central conclusion of Godel's incompleteness theorem. In stark contrast to the commonly accepted idea that Godels' sentence is self-referential with definite meaning.
So we have two choices. Either we stick to our a priori philosophical concepts and abandon mathematical logic and it's physical embodiment as being an unsuitable language for expressing and justifying philosophical truth. Or we revise our philosophical intuitions to match what PA and its physical embodiment can and cannot express. I'm saying the latter.
I read this as your taking exception to the use of existential (i.e., existential and universal) quantifiers unless it/they "abbreviate an independent proof of the fact concerned...". So, if I say x>3 is true for all x greater than three, this is neither true nor valid, subject to a proof of the "for all"? — tim wood
This is acceptable, because the contradiction it expresses can be represented without universal quantifiers. It is analogous to having a function that by design terminates, and that converts an arbitrary number into a number or another arbitrary number. the conflation of
all with
arbitrary is perhaps the central source of controversy and misunderstanding in logic.