Paradox regained: Life beyond Gödel’s shadow
Bhupinder Singh Anand
(A copy of this paper can be downloaded as a .pdf file from http://arXiv.org/abs/math/0201307.)
Gödel’s explicit thesis was
that his undecidable formula
GUS
is a well-formed, well-defined proposition
in any formalisation of Intuitive
Arithmetic IA in which the Axioms and Rules of Inference are recursively
definable. His implicit thesis was that GUS is not formally inconsistent in
any such system.
I consider a constructive, and
intuitionistically unobjectionable, formalisation PP of IA in which the Axioms and Rules of Inference
are recursively
definable. I argue that, although Gödel’s proposition GUS is a well-formed formula in PP, it is
an ill-defined proposition
that formally reflects the “Liar” paradox in PP.
I argue that the introduction
of “formal truth”
and “PP-provability” values to selected propositions of IA through
PP
leads to the collapse of the Gödelian
argument advanced by J.R.Lucas, Roger Penrose and others.
CONTENTS
Intuitive truth - a paradigm
shift
Implicit influence of Gödel's Platonism
Gödel’s Theorems and
"formal (logical) truth"
Non-verifiable assertions
implicit in Gödel’s formal system
1. Introduction
1.1. An intellectual
challenge for the 21st century: Gödel in a wider perspective
1.2. Gödel’s
Undecidability Theorem and its consequences
1.3. The
"Liar" paradox
1.4. The Russell
paradox
1.5. Creation
through definition
2.1. Intuitive
Arithmetic and the formal system PP
2.2. The alphabet
S of the sub-language PP of IA
2.4.
Quantification and “formal
truth” in PP:
nailing an ambiguity
3.1. Is there a
“Liar” expression in IA?
3.2. Provability in PP
3.3. Recursive
functions in IA
3.4. A
representation lemma of Hilbert and Bernays
3.5. Are recursive
functions “consistent”?
3.6.
Gödel-numbering
3.7. Gödel’s
Self-reference Lemma
3.8. Hilbert
& Bernays Representation Lemma
3.9. The
undecidable “Gödel” proposition in PP
4. Beyond
Gödel
4.1. “Formal truth” and
“provability”
as formally assigned values
4.2.
Effectiveness of a language
4.3. Collapse of
the “Gödelian” argument
4.4. Constructive
“provability”
4.5. Paradox regained:
“Constructive
Provability” and the “Gödelian” proposition
4.6. Beyond
Gödel’s shadow
5. Basis of
Gödel’s conclusions
5.1. Intuitive
Arithmetic and Peano’s
Arithmetic
5.4. Significant
features of PP
and PA
5.5. Generalisation:
Gödel’s rule of “Extrapolation”
5.6. Gödel's
undecidable formula
GUS
5.8. Well-formed,
well-defined formulas
of Gödel's formal system of standard PA
6. Questioning
Gödel’s conclusions
6.1. GDL(x) is well-defined in PA, but not necessarily in any interpretation M
6.2. GUS is
well-formed and well-defined, but Gödel's reasoning is non-constructive
6.3. Intuitive Arithmetic IA is not a model
of PA
6.4. Generalisation
as a Rule of Inference is intuitionistically questionable
6.5. A
non-constructive interpretation of Generalisation
7. Conclusions
Author’s preface
Intuitive truth - a paradigm
shift
The alternative consequences of
Godel’s reasoning developed in this paper (and in its roots) involve a significant
paradigm shift in the philosophical basis of our perception of the nature of Intuitive
Knowledge, and more particularly of the concept of factual, or intuitive truth.
By Intuitive Knowledge I
refer loosely to that body of pro-active knowledge that stems directly from our
conscious states, in contrast to our reactive Instinctive Knowledge,
which stems from, and lies within, our sub-conscious and unconscious states.
This preface is intended to
highlight the wider significance of an issue that may otherwise lie in
obscurity due to the specialised nature of the subject. My thesis is that the
influence, on our current modes of thought, of the interpretations, and
conclusions, drawn from Gödel’s original paper (Gödel 1931) may have a wider,
multi-disciplinary, element that is not obvious from an appreciation of its
purely logical and mathematical import.
Implicit influence of Gödel’s
Platonism
I
argue that the roots of this influence may be traced to implicitly Platonistic
elements that underlie classical first order predicate calculus PA,
which is based essentially on the formal
system defined by Gödel in his
(1931) paper. Loosely speaking Gödel, who was an
explicitly strong Platonist, assumed the existence of a world of ideals that could
objectively be referred to for arbitrating which of our assumptions or
premises, when formally expressed in a rigorously constructed scientific
language, were “intuitively true”, and which were “intuitively false”, under interpretation.
Now
one may, of course, argue reasonably - as Gödel does - in
Platonistic terms and define "intuitive truths" as characteristics of
"relationships" that are assumed to "exist" in some
"absolute" sense (that is, even in the absence of any
"perceiver") between the "objects" of an external
"ontology" (both of which are also taken to "exist" in
some "absolute" sense).
I
argue, however, for an alternative view of "relationships" as
belonging to "perceptions" that we consciously “construct” and
selectively “assign” to abstract "objects" (that themselves are
conceptual "constructs") of an abstract "ontology" (that
is similarly a conceptual "construct").
In
other words, I argue that each "perception" can reasonably be assumed
to be an abstract “construct" based on a unique, one-of-a-kind,
never-to-be-repeated consciousness of an “experience”. "Intuitive
truth" is then, essentially, a “constructed”, space-time-localised,
“factual truth”. It corresponds to a "subjectively” constructed
characteristic of the “expression” of individually constructed
"perceptions". Loosely speaking, it corresponds to a characteristic
of the way we construct an “expression” for that which we select as common to a
series of "subjective perceptions", rather than to a characteristic
that we “discover” of an "objectively" observed "something".
My
brief against Platonism, when rooted in scientific ways of thought, is that it
could permit us to “logically” validate our subjective “intuitive” perceptions
as being reflective of some “absolute Truth” that “must be” of universal
“significance” in a Utopian, Platonistic world.
Gödel's Theorems and "formal (logical) truth"
The
view of Gödel's Theorems that I attempt to
present is that they are essentially concerned with the effectiveness of our ability
to “communicate” the abstractions that we intellectually "construct"
on the basis of our “individualistic” sensory perceptions. They thus have to do
with the efficiency and effectiveness of our language of communication, and
involve the concept of “logical truth”, or "formal truth" (the two
terms are used synonymously in this paper).
I
argue that, in formal languages, a selected set of "axiomatic truths"
is expressed as a set of Axioms (or Axiom schemas). The selection
criteria is that the Axioms are readily accepted by any
"perceiver" as faithfully reflecting some "significant"
"factual truths" pertaining to the expression of abstract
"constructed" elements of the "constructed" ontology under
consideration as “perceived” and “conceived” also by the “perceiver”.
For
the most basic, and intuitive, of our scientific languages, namely Number
Theory or our Intuitive Arithmetic of the natural numbers, I take
the commonly accepted selection of such "axiomatic truths" as the set
of Peano's Postulates,
first expressed in semi-axiomatic format by Dedekind (1901).
I
consider that the challenge in any such theory is then to find a suitable set
of Rules of Inference by which we can assign unique "formal (logical) truth" values to as many
well-formed propositions
of the theory as possible that are not Axioms.
I
argue that the concept of "formal (logical)
truths" is thus merely the result of the application of a set of Rules
of Inference for assigning such “formal (logical) truth” values to
various “logical” permutations and combinations of "axiomatic truths"
as (finite and infinite) compound assertions (which ideally should
not introduce any new "axiomatic truths" that are not already
implicit within the Axioms).
I
argue that the Rules of Inference of any specific language should
include not only the familiar “Rules of Inference” that we define for
the language, but also the logical Axioms that, strictly speaking, should
be considered equally as being part of the Rules of Inference of the
language.
I
argue that he significance of "formal (logical) truths" lies
in our experience that the "factual (intuitive) truths" of our
"perceptions" can generally be corresponded in a communicable
language with a high degree of correlation to the "formal (logical)
truths" of the language. The large body of our “factual (intuitive)
truths” may thus also be viewed as “intuitively constructed” permutations and
combinations of a smaller, ideally finite, set of "factual (intuitive)
truths".
This
appears to suggest that the "significance" to us (and possibly to
any intelligence whose evolution is based on communication) of any set of
"factual (intuitive) truths" may be proportional to the body
of "formal (logical) truths" that can be inferred by various
“logical” combinations and permutations of the "axiomatic truths"
that can be distilled from the particular set of “factual (intuitive)
truths”.
I
argue that the significance of Gödel's Theorems lies in
the fact that they are derived in a system of Axioms where the Rules
of Inference lead to a particularly rich body of expressions that can be
assigned "formal (logical) truth” values under various interpretations of the symbols of
the theory.
Non-verifiable assertions
implicit in Gödel’s formal system
I
argue, however, that a major feature of Gödel’s
formal system is that the chosen Rules of Inference are non-constructive, in
the sense that they also assign, implicitly and sweepingly, non-verifiable
"formal (logical) truth” values under interpretation in some models to
various expressions. Thus the system, in a sense, postulates "formally (logically)
true" expressions under some interpretation that cannot be
correlated, even in principle, to any "factual (intuitive)
truths" of a human "perception".
In
(Anand
2001), I highlight this non-intuitive aspect of Gödel's choice of Rules of Inference, and suggest
more intuitive, constructive, Rules of Inference that would make our
formal systems of Arithmetic more faithfully representative of our Intuitive
Arithmetic.
One
of the consequences of using constructive Rules of Inference is that the
reasoning by which Godel concludes that the formal “Gödel” proposition,
which translates loosely as “The ‘Gödel’ proposition is not ‘provable’”, is intuitively true
collapses. In this paper, I define a formalisation of Intuitive Arithmetic
in which Gödel’s argument leads to a
contradiction. In effect, we are faced with the expected reflection of the
"Liar" sentence, namely "The 'Liar' sentence is a lie", in
constructive formal theories.
However,
I argue that this is not necessarily the drawback that it appears to be at
first sight. In fact such contradictions both encourage and discipline us in
our use of rich and creative languages. They force us to focus on devising
rules by which we can recognise well-formed formulas of the theory that need to be
treated as ill-defined propositions
(in the sense that there is no way a unique "formal (logical)
truth" value can be assigned to the well-formed formula by the Rules of Inference of the
theory). I thus offer the thesis that “consistency” may be treated in any theory
as the specification for determining which well-formed formulas qualify as well-defined propositions.
I
argue that, in a sense, what Gödel’s
reasoning actually accomplishes is best viewed as an “illusion”, where a
"constructive" argument successfully masks a
"non-constructive" premise.
The
significance of this is that if an “illusion-prone” logical system forms the
bedrock of all scientific thought and discourse, then attendant conflicts and
controversies must inevitably follow "illusory", if not outright
"hallucinatory", "perceptions" rooted in non-constructive
thought.
To
the extent that the foundations of our scientific thought can visibly be seen
to be increasingly influencing, and impacting on, the way we
"perceive", "conceive", "express",
"communicate" and "act" in every sphere of human activity,
any logic that provides a theoretical legitimacy to "illusory
perceptions" as having a possible validity in a non-verifiable universe
that "exists" in some "absolute" sense can be held
qualitatively accountable in some measure for reinforcing the kind of
"perception" that leads to unresolvable confrontations arising out of
"extra-logical" consequences of non-constructive theories.
(The
development of systems of Artificial Intelligence, which so far have not shown
any marked susceptibility to Gödelian
"illusions", may, however, force consideration of formal systems that
are more self-disciplined in their faithfulness to our intuitively constructive
aspects that can be verified and duplicated mechanically.)
In
this paper I aim to highlight the implicit assumptions that, I argue, underlie
the formal structure of our current formal system of logic.
Truth: I argue, albeit implicitly, against the concept of “intuitive truth”
as something a priori that is to be discovered, and which can be captured only
partially through formal structures. In other words, I argue against the
concept that “provable” formulas in any formal
system can be corresponded 1-1 to a proper subset of the “intuitively true” propositions under
any “interpretation” of the formal system.
Formal truth: My thesis is that “formal (logical) truth” is
a characteristic that we choose to attribute, as something of commonly
communicable, intellectual, “significance”, to our assertions through
meta-rules of assignment that we call our logical Rules of Inference (by
definition, these lie outside the language).
Significance: I hold we choose these rules in order to
intellectually communicate the essence of “factual (intuitive) truths”
that we also choose to intuitively construct as “significant”, individualistic,
abstract concepts.
Factual truth: I hold that “factual truths”, or “intuitive truths”,
belong to our consciously constructed intuitive “perceptions”, just as “formal
(logical) truth” belongs to our consciously constructed intellectual
systems (languages) of communication.
Consciousness: I hold that “factual (intuitive) truth” does
not “exist” outside “consciousness”. Thus there is no “factual (intuitive)
truth” in the absence of conscious intuitive “perception”, just as there is no
“formal (logical) truth” in the absence of conscious intellectual
“communication”.
Axiomatic truth: I hold that “axiomatic truths” are “factual (intuitive)
truths” that we choose to express within a language of communication in order
to create a common link between the body of our intuitively constructed
“factual (intuitive) truths”, and the body of our intellectually
constructed “formal (logical) truths”.
Rules of Inference: I hold that our Rules of Inference and Logical
Axioms are what we select as the means of intellectually constructing the
body of our “formal (logical) truths”, just as our Intuition is
what we rely on for intuitively constructing the body of our “factual (intuitive)
truths”.
Inductive truth: I further hold that “inductive (extra-logical)
truth” is, loosely speaking, an individualistic, non-experiential,
non-verifiable, extrapolation of “formal (logical) truth” - built around
both qualified, and individually preferred, generalisations of “formal (logical)
truth”.
Interpretation: I argue against the thesis
that a formal system can be meaningfully viewed in isolation, separately from
an intended interpretation. I argue that, given a set of
“axiomatic truths”, it is our Rules of Inference that determine “formal
(logical) truth” values in any interpretation.
Model: Thus I argue (Anand
2001, Section_4) that an interpretation can be a model of
two formal systems that have identical primitive symbols, identical rules of
construction for well-formed formulas, and identical
sets of “axiomatic truths”, but distinctly different, contradictory, “logical”
consequences.
Communication: My thesis is that it is through our system of formal
languages that we, on the one hand, constructively assign “formal (logical)
truths” (and provability) and, on the other, non-constructively assign
selected characteristics of non-verifiable “inductive (extra-logical)
truths” (through qualified generalisation), to elements of the language
in an effort to correspond these to specific “factual (intuitive)
truths” of our intuitively constructed individual perceptions whose
“significance” we desire to communicate.
Uniqueness: I suggest that there can be no commonly verifiable
non-standard model. Each such must differ in some essentials perceived uniquely
only by each perceiver who is, in effect, both the architect and builder of the
model.
Bhupinder
Singh Anand Friday,
15 February 2002
Paradox regained: Life beyond Gödel’s shadow
1. Introduction
1.1. An intellectual challenge for the 21st
century: Gödel in a wider perspective
One of the intellectual challenges
inherited from the last century is that of interpreting Gödel’s assertions of
formal undecidability within a wider, intuitively acceptable, perspective.
Given his formal premises, Gödel’s
formal reasoning and its formal consequences (Gödel 1931) are
logically irrefutable. However, there is no similarly unequivocal
interpretation of his reasoning, or of his conclusions.
I argue elsewhere (Anand 2001), in greater detail, the
thesis that differing perceptions of the interpretation of Gödel’s reasoning
and conclusions arise because the system of standard Peano’s Arithmetic, essentially
formulated by Gödel (1931, pp.9), is only one - and perhaps not the most representative
- of several significantly differing systems that can be defined to formalise
our system of Intuitive Arithmetic IA
of the natural “counting” numbers (which we take to be the Arithmetic based
on an intuitive interpretation of Dedekind’s formulation of Peano’s
Postulates[1]).
(Another thesis would be that
Gödel’s formal system itself is open to significantly differing
interpretations.)
In this paper I outline in more
general terms a constructive, and intuitionistically unobjectionable,
formalisation PP
of IA
in which the Axioms
and Rules of Inference
are recursively
definable. I argue that, although Gödel’s undecidable sentence GUS is a
well-formed formula
in PP,
it is an ill-defined
formal proposition[2] that formally reflects the “Liar” paradox
in PP.
1.2. Gödel’s Undecidability Theorem and its consequences
Usually referred to loosely as
“Gödel's Theorems", these assertions are the outcome of Gödel's attempt to
construct a formal language for faithfully expressing our Intuitive Arithmetic IA of the
natural numbers.
The ideal source for assessing
Gödel’s intent and the significance of the wealth of concepts introduced by him
in the course of his attempt is still, albeit arguably, his seminal paper “On
formally undecidable propositions of Principia Mathematica and related systems
I”, accessible on the web in an English translation by B. Meltzer (Gödel 1931).
However, with the advantage of
hindsight, my thesis in this paper is that the essence of Gödel’s reasoning,
its formal consequences, and its wider implications, are better viewed today in
a somewhat different context.
1.3. The "Liar" paradox
Around 2000 years back, Greek
philosophers discussed the paradox of ambiguous self-reference within ordinary
language. This arises if we postulate a ‘Liar’ expression, which reads as
"The ‘Liar’ proposition is a lie", as a valid proposition within the
language in which the expression is constructed. Clearly, the "Liar"
proposition is true if and only if it is a lie!
Now the grammar of an ordinary
language governs the construction of words and propositions of the language for
use as a means of general unrestricted communication. It obviously does not
contain the specification necessary to prohibit the creation by definition of
such vague, or ill-defined, self-referential expressions as that of the “Liar”.
Though these may have the formal form of propositions, they appear devoid of
the “communicative content”, or “meaning”, that we intuitively expect
propositions to have.
We conclude that the well-defined
"Liar" expression cannot be a well-defined "Liar"
proposition in a “consistent”
language. So we may either treat the language as inherently “inconsistent”, or
conclude that the language is deficient in its ability to identify well-defined
expressions that are ill-defined, or “meaningless”, propositions.
Considered primarily a linguistic
anomaly, the paradox does, however, focus attention on the issue:
When may
we treat a well-formed expression as a well-defined proposition, without fear
of contradiction?
1.4. The Russell paradox
The “Liar” paradox gained in
significance when, in 1901, Bertrand Russell discovered a similarly paradoxical
expression within Set Theory. Loosely speaking, he defined a set, which we may
name "Russell", as the set whose elements are all, and only, those
sets of the Theory that do not belong to themselves. Clearly, if it can be
expressed within the Theory, then the set "Russell" belongs to itself
if and only if it does not belong to itself!
Again, the Axioms and
logical Rules of Inference of the Theory - which governed the
construction of sets for use in a more restricted and precise language of
mathematical communication - did not contain the specification necessary to
satisfactorily prohibit the creation by definition of vague, ill-defined, or inconsistent
entities such as the “Russell” set that could be expressed within the language
of the Theory, but apparently harboured concealed concepts involving unruly
infinite sets.
Here too, we conclude from the
contradiction that introduction of the well-defined "Russell"
expression cannot yield a well-defined "Russell" set in a consistent Set
Theory. So, again, we may either treat any Theory admitting such sets as
inherently inconsistent,
or conclude that such a Theory is deficient in its ability to identify
well-defined expressions that yield ill-defined "sets".
Viewed as a reflection on the
soundness of the foundations of mathematics, Russell's paradox focuses on the
issue:
When may
we introduce entities through definition into our mathematical languages,
without fear of contradiction?
1.5. Creation through definition
We note that definitions are
essentially arbitrary assignments of convenient names within a language, or
theory, for expressing complex reasoning in a compact and easier-to-grasp form.
The paradoxes indicate that
unrestricted definitions, particularly those that involve self-reference, may
admit well-formed expressions within the language, or theory, which lead to an inconsistency.
Clearly such expressions must be considered as ill-defined elements within the
language, or theory. It follows that a language, or theory, that admits such
well-formed expressions as representing well-defined elements cannot
uncritically be assumed consistent.
2. Formal systems
2.1. Intuitive
Arithmetic IA and the formal
system PP
A natural question arises whether
the simplest, and most intuitive, of our mathematical theories also admit such
expressions. We consider, for instance, the Intuitive Arithmetic IA of the natural “counting”
numbers. The following Axioms -
based on what are termed as Peano's
Postulates, and expressed formally in a sub-language PP of IA as defined below - are commonly
taken to be “formally
true” representations of some of the most “intuitively true”
assertions of IA[3]:
(By “PP”, we
shall henceforth mean “the sub-language PP of IA”.)
(PP1)
(Ax)|=PP
~(0 = (x+1))
(Intuitive
interpretation:
Adding 1 to any natural number expressible in PP never yields 0.)
(PP2)
(Ax)(Ay)|=PP ~(x=y) => ~((x+1) = (y+1))
(Intuitive
interpretation:
Adding 1 to each of two different natural numbers expressible in PP yields
two different natural numbers that are expressible in PP.)
(PP3)
(Ax)|=PP (x+0) = x
(Intuitive
interpretation:
Adding 0 to a natural number that is expressible in PP yields the same natural number.)
(PP4)
(Ax)(Ay)|=PP (x+(y+1)) = ((x+y)+1)
(Intuitive
interpretation:
Adding 1 to a natural number that is expressible in PP, and then adding another natural
number that is expressible in PP to the sum, yields the same natural
number that is expressible in PP as is obtained by adding the two
natural number that are expressible in PP first, and then adding 1 to their
sum; in other words addition is an “associative” operation over the natural
numbers expressible in PP.)
(PP5)
(Ax)|=PP (x*0) = 0
(Intuitive
interpretation:
Multiplying a natural number expressible in PP by 0 yields 0.)
(PP6)
(Ax)(Ay)|=PP (x*(y+1)) = ((x*y)+x)
(Intuitive
interpretation:
Adding 1 to a natural number that is expressible in PP, and then multiplying the sum by a
second natural number that is expressible in PP, yields the same natural number that
is expressible in PP
as is obtained by multiplying the two natural number that are expressible in PP first, and
then adding the second natural number that is expressible in PP to
their product; in other words multiplication is a “distributive” operation over
“addition” for the natural numbers expressible in PP.)
2.2. The alphabet S of the sub-language PP of IA
The characteristic feature of
these selected “assertions”, which are taken to express the most intuitive
arithmetical truths of IA symbolically, is that they are
expressed using only a limited alphabet S, containing the arithmetical
symbols “+” (addition) and “*” (multiplication) only, apart from
the meta-logical and logical symbols “|=PP” (It is “formally true” in
PP
that), “~”(not), “=>” (implies), “=” (equals),
“&” (and), “v” (or),
“(Ax)” (for all x), “(Ex)” (there exists x), “x, y, ...” (variables), “a, b, c, ...” (constants),
“0” (zero), “1” (one), and the two parentheses “(“, “)”.
The (ontological) domain
over which the finite set of variables “x, y, ...” range is
taken, in IA,
to be the intuitively non-terminating series “0, 1, 2, 3, ...” of natural “counting” numbers and, in PP, the
non-terminating formal series expressing the
natural numbers in PP
as the numerals
“0, 0+1, (0+1)+1, ((0+1)+1)+1, ...”.
2.4. Quantification and “formal truth” in PP : nailing an ambiguity
Thus each of (PP1)
to (PP6) symbolically assigns a “formal (logical) truth” value in PP to a
countable infinity of arithmetical “propositions” of IA. In
other words, assuming the expression, including the meta-logical symbol “|=PP”,
is a well-formed “propositional formula”
by the rules for the formation of well-formed “propositional formulas” of PP, the
well-formed formula
to the right of the meta-logical symbol “|=PP” is asserted as a “formally true” proposition in PP for any
given set of finite values of the variables contained in it.
Clearly, a crucial characteristic
of the language PP,
as defined above, is that all formulas
containing quantifiers necessarily contain the “formally true” meta-logical symbol “|=PP”
immediately after the quantifier. This reflects the intention that, in PP, the
quantifiers “(Ax)” and “(Ex)”
should indeed “quantify” the “formal
truth” of the expression “F(x)” over a specific domain in order to yield a
well-defined expression that has the symbolic form of a “proposition”. Thus all formal propositions
of PP
that contain quantifiers are meta-assertions under interpretation.
I argue further that “(Ax)|=PP F(x)” is intended to formally represent the intuitive
meta-assertion that “F(x) is ‘formally
true’ in PP
for all values of x that are
expressible in PP”.
I therefore adopt the expanded form to highlight the significance of the
intended meta-assertion (or negation) of the compound “formal truth”,
involved in “(Ax)|=PP F(x)”, when we intend to adjoin “(Ax)” to “F(x)” in PP.
The two Rules of Inference
in PP,
for deriving propositions
in PP
that are “logical” consequences of the above Postulates, are Modus
Ponens and Induction.
(PPR1) Modus
Ponens: From “(Ax)|=PP
F(x)” and “(Ax)|=PP (F(x) => G(x))” we may conclude “(Ax)|=PP G(x)”.
(Intuitive interpretation:
If F(x) is “formally true”
for all natural numbers x
expressible in PP,
and G(x) is “formally true” whenever F(x) is “formally true” for any natural number x expressible in PP, then G(x) is “formally true”
for all natural numbers x expressible
in PP.)
(PPR2) Induction:
From “|=PP F(0)” and “(Ax)|=PP (F(x) => F(x+1))” we may conclude “(Ax)|=PP F(x)”.
(Intuitive interpretation:
If F(0) is “formally
true”, and F(x+1) is “formally
true” whenever F(x) is “formally
true” for any natural number x expressible in PP, then F(x) is “formally true”
for all natural numbers x
expressible in PP.)
3. Gödel’s reasoning
3.1. Is there a “Liar” expression in IA?
Around 1930, Gödel considered
whether the “Liar” expression, "The ‘Liar’ proposition is a lie",
would be “reflected” formally in PP by asserting an arithmetical “Gödel”
proposition
that is “equivalent”, loosely speaking, to the assertion “The ‘Gödel’ proposition is not
‘provable’”.
What Gödel had noticed, with
remarkable insight, was that terms such as “well-formed formula”[4], “well-formed proposition” and “proof sequence” could be
formally defined in the language of PP. He therefore argued that he could express
meta-assertions about PP
such as “ ‘F(x)’ is a
well-formed formula
in PP”,
“ ‘(Ax)|=PP F(x)’ is a well-formed proposition in PP”, “ ‘F(x)’ is a ‘provable’ formula in PP”, “ ‘(Ax)|=PP F(x)’ is a ‘provable’ proposition in PP” and “The ‘Gödel’ proposition is not
‘provable’ in PP”,
amongst others, as equivalent arithmetical propositions in PP.
3.2. Provability
in PP
The essence of Gödel’s argument,
when applied to PP,
is that we can define a proposition
P of IA
as “PP-provable” if and only if there is a finite
“proof sequence” consisting of propositions
of PP
each of which is either a “formally
true” axiom (PP1-6),
or a “formally true”
immediate consequence of the preceding “formally true” propositions by the Rules of Inference
(PPR1-2),
and where P is the final proposition in the sequence.
The “PP-provable”
propositions
are thus characterised by the fact that they are all expressed as “well-formed propositions”,
such as “(Ax)|=PP F(x)”, using only a small set of primitive, undefined
symbols of the alphabet S.
Clearly, the Axioms
(PP1-6)
are all “PP-provable”
propositions.
3.3. Recursive
functions in PP
The significance of the alphabet S selected for expressing “PP-provable” propositions is that many significant arithmetical functions of IA such as “n!” (factorial), “m^n” (exponential), “m/n” (division), “n is a prime number”, amongst others, are defined recursively