◄
Chapter
2 ◄
Index Chapter
4 ►
Beyond
Gödel
Simply
consistent constructive systems of first order Peano’s Arithmetic that do not
yield undecidable propositions by Gödel’s reasoning
(A compiled copy of Chapters 1 to 6 can be downloaded as a .pdf file from http://arxiv.org/abs/math/0201059.)
Chapter
3. Is there an
omega-constructive first order Arithmetic?
Contents
3.0. Introduction
3.1. The primitive symbols of a general first
order predicate calculus K
3.2. The logical axioms of K
3.3. The rules of inference of K
3.4. Gödel’s formal system PA
3.5. General Arithmetics: weak-GA
3.6. General Arithmetics: strong-GA
3.7. Peano Arithmetics : weak-PA
3.8. Peano Arithmetics : standard PA
3.9. Closed Induction implies open
Induction in PA
3.10. Can PA admit models of transfinite
ordinals?
3.11. omega-constructive first order
Arithmetics
3.12. omega-constructive Arithmetic : omega-GA
3.13. The omega-constructive Peano
Arithmetic : omega-PA
3.14. Every model of PA is a model of omega-PA
3.15. The essential difference between PA
and omega-PA
3.16. Can omega-PA admit models of
transfinite ordinals?
3.17. Can we strengthen omega-PA
In this third section we formally
construct and briefly examine various
systems of first
order Arithmetic.
We argue that we cannot use Gödel’s reasoning to prove that every primitive
recursive function (Mendelson p120) can be strongly
represented formally
in all such systems. Hence it does not universally establish the existence of undecidable propositions
that are true
under interpretation.
We finally construct an omega-constructive system
of first order
Arithmetic,
omega-PA, where we
replace the non-constructive
closed Induction axiom schema by
a constructive,
open Induction
axiom schema.
We base omega-PA on a modified first order predicate calculus where we
replace the strong Generalisation
rule of inference
I(ii) by a weaker
omega-Constructivity
rule of inference
I(iii).
We show that every model of standard PA is a model of omega-PA. We show
further that every primitive recursive function cannot be strongly
represented formally
in omega-PA if it is simply consistent.
So, in omega-PA, Gödel’s
reasoning does not establish the existence of undecidable propositions that are true
under interpretation.
We
argue in this, and the next, section that Gödel mistakenly concluded (Gödel p190-191) that the existence of undecidable propositions
that are true
under interpretation
must follow from his reasoning in all the above formal systems of Arithmetic.
We
begin by reviewing in detail Mendelson’s definition (p103) of the system PA. This is essentially the formal system
in which Gödel constructed his undecidable propositions.
3.1. The primitive symbols of a general first
order predicate calculus K
The system PA is based on a
particularisation of the general first order predicate calculus K whose primitive
symbols are (Mendelson
p57):
'~' (not), '=>' (implies),
'(' (left parenthesis), ')' (right parenthesis), ',' (comma),
'x1, x2, ...' (denumerably
many individual variables), 'A(n, j), (n, j >= 1)'
(denumerably
many predicate
letters), 'f(n, j), (n, j >= 1)'
(denumerably
many function
letters), and 'ai,
(i>= 1)' (denumerably many constants).
The logical axioms of K are:
K(1) A
=> (B => A)
K(2) (A
=> (B => C)) => ((A => B)
=> (A => C))
K(3) (~B
=> ~A) => ((~B => A) => B)
K(4) (Axi)A(xi) => A(t), if A(xi) is a well-formed formula of K and t is a term of K free for xi in A(xi).
K(5) (Axi)(A => B) => (A
=> (A => (Axi)B) if A is a well-formed formula of K containing
no free occurences of xi.
3.3. The rules of inference of K
The rules of inference of K are:
I(i) Modus
Ponens: B follows from A and A
=> B.
I(ii) Strong
Generalisation: (Axi)A
follows from A.
3.4. Gödel’s formal
system PA
The particular system of first order predicate
calculus that Mendelson uses (p103), to develop Gödel's
reasoning in a formal
first order Arithmetic,
contains:
A(i) a single predicate
letter 'A' to represent equality A(t, s) between
the terms t and s, which we express as ‘t=s’;
A(ii) one
individual constant 'a' which we
write as ‘0’;
A(iii) three function
letters f, g and h to represent,
respectively, the successor of ‘t’, which we write as ‘t'’, addition, which we write as ‘t+s’, and
multiplication, which we write as ‘t.s’.
The axioms of Arithmetic
that Gödel
considered were Dedekind's axioms
for number theory, known as Peano's Postulates, which are essentially as below
(not necessarily independent):
A(1) (x1 = x2) =>
((x1 = x3) => (x2 = x3)
A(2) (x1 = x2) => (x1' = x2')
A(3) 0 ¹ x1'
A(4) (x1' = x2') => (x1 = x2)
A(5) (x1 + 0) = 0
A(6) (x1 + x2') = (x1 + x2)'
A(7) x1.0 = 0
A(8) x1. x2' = (x1. x2) + x1
A(9) (x1 ¹ 0) => (Ex2)(x1 = x2')
and the two meta-axiom schemas (more accurately,
rules of inference) of closed and open Induction:
A(10) For any wff F(x) of PA, from (F(0) and (Ax)(F(x)) => F(x')), we may conclude (Ax)F(x)
A(11) For any wff F(x) of PA, from (F(0) and (F(x)) => F(x')) we may conclude F(x)
3.5. General Arithmetics : weak-GA
If we eliminate strong Generalisation
I(ii), closed
Induction A(10) and open Induction A(11) from PA, we obtain
a weak first order
general Arithmetic,
weak-GA.
Weak-GA is thus
the axioms A(1) to A(9) of first order Arithmetic,
as specified in §3.4,
added to a first order
predicate calculus A(i) to A(iii), as specified in §3.4, with only the Modus Ponens
rule of inference
I(i).
Since all axioms of weak-GA are provable in PA, every interpretation and model of PA is an interpretation and model of weak-GA.
However,
in the absence of strong
Generalisation I(ii), and closed Induction A(10), the argument
of §2.13,
establishing the strong
representability of every recursive function, cannot be carried out
in weak-GA.
So, in weak-GA, Gödel’s reasoning does not establish the existence of undecidable propositions
that are true
under interpretation.
3.6. General Arithmetics : strong-GA
If we strengthen weak-GA by adding
the strong
Generalisation rule
of inference I(ii), we
arrive at a stronger first order general Arithmetic, strong-GA.
Strong-GA is thus
the axioms A(1) to A(9) of first order Arithmetic,
as specified in §3.4,
added to a first order
predicate calculus A(i) to A(iii), as specified in §3.4, with both the Modus Ponens
rule of inference
I(i) and the strong Generalisation
rule of inference
I(ii).
Since all axioms of strong-GA are provable in PA, every interpretation and model of PA is an interpretation and model of strong-GA.
However, in the absence of closed Induction A(10), the argument
of §2.13,
establishing the strong
representability of every recursive function, still cannot be carried
out in strong-GA.
So, in strong-GA, Gödel’s reasoning does not establish the existence of undecidable propositions
that are true
under interpretation.
3.7. Peano Arithmetics : weak-PA
If we add closed Induction A(10) to weak-GA, we arrive
at a weak first order Peano Arithmetic, weak-PA.
Weak-PA is thus
the axioms A(1) to A(10) of first order Arithmetic,
as specified in §3.4,
added to a first order
predicate calculus A(i) to A(iii), as specified in §3.4, with only the Modus Ponens
rule of inference
I(i).
Since all axioms of weak-PA are provable in PA, every interpretation and model of PA is an interpretation and model of weak-PA.
However, in the absence of strong Generalisation
I(ii), the
argument of §2.13, which establishes the strong representability
of every recursive
function, cannot be carried out in weak-PA.
Hence, in weak-PA also, Gödel’s reasoning does not establish the existence of undecidable propositions
that are true
under interpretation.
We note also that it is not
obvious whether weak-PA proves weak-Induction
A(11).
3.8. Peano Arithmetics : Standard PA
We arrive at the standard first order Peano
Arithmetic, standard PA, used by Gödel,
when we add strong
Generalisation I(ii) to weak-PA.
Standard PA
is thus the axioms
A(1) to A(10) of first order Arithmetic,
as specified in §3.4,
added to a first order
predicate calculus A(i) to A(iii), as specified in §3.4, with both the rules of inference,
Modus Ponens
I(i), and strong Generalisation
I(ii).
Since standard PA establishes the strong representability of
every recursive
function, we are now able to formally derive Gödel’s
undecidable propositions in
standard PA.
However, as we have argued in the earlier
sections, strong representability now
admits closed well-formed formulas that refer to
totalities, under interpretation,
which are not reflected in the intuitive Arithmetic that is intended to be formalised by standard PA.
3.9. Closed
Induction implies open Induction in PA
We note that, in standard PA, closed
Induction A(10) implies
open Induction A(11).
Thus, from the closed
Induction axiom schema A(10) in standard PA:
Standard PA proves:
(F(0) &
Standard PA proves: (Ax)(F(x) => F(x+1)))
=>
Standard PA proves: (Ax)F(x)
we have that if:
Standard PA proves:
F(0) & Standard PA proves: F(x) => F(x+1)
then:
Standard PA proves:
F(x) =>
F(x+1)
Standard PA proves:
(Ax)(F(x) => F(x+1))
... Gen
Standard PA proves:
F(0) &
Standard PA proves: (Ax)(F(x) => F(x+1))
Standard PA proves:
(Ax)F(x)
Standard PA proves:
F(x)
We thus have that:
Standard PA proves:
F(0) &
Standard PA proves: (F(x) => F(x+1)))
=> Standard PA proves: F(x)
Hence standard PA proves the open Induction axiom schema A(11), and so PA and standard PA are
identical.
3.10. Can PA
admit models of transfinite ordinals?
Now we note that:
It follows that Cantor’s transfinite ordinal-Arithmetic CA, in which omega is a term
for which we have that “omega +1” is not equal to “1+ omega”,
is not a model
of PA.
3.11. omega-constructive first order
Arithmetics
We next define a range of omega-constructive first order
systems of Arithmetic,
by introducing an intuitionistically
unobjectionable omega-Constructivity rule of inference:
I(iii) omega-Constructivity:
From [“x
is a numeral” => F(x)] we may
conclude (Ax)F(x).
Since “x
is a numeral” is recursively definable, we note that I(iii) is a
recursively definable rule of inference that is equivalent to the concept of omega-constructivity introduced
in “Chapter 1. First order Arithmetic is not
omega-constructive”.
3.12. omega-constructive
Arithmetic : omega-GA
If we strengthen weak-GA by adding
the omega-Constructivity rule of inference I(iii), we
arrive at a formal
system of constructive
omega-GA.
omega-GA is thus
the axioms A(1) to A(9) of first order Arithmetic,
as specified in §3.4,
added to a first order
predicate calculus A(i) to A(iii), as specified in §3.4, along with the Modus Ponens
rule of inference
I(i) and the omega-Constructivity
rule of inference
I(iii).
Since all axioms of omega-GA are provable in PA, every interpretation
and model of
PA is an interpretation and model of omega-GA.
Also, in the absence of strong Generalisation
I(ii), and closed Induction A(10), the argument
of §2.13,
establishing the strong representability of
every recursive
function, cannot be carried out in omega-GA.
However,
as we have shown in the earlier section, “Chapter 1. First order Arithmetic is not
omega-constructive”, in any system
of Arithmetic
with the omega-Constructivity
rule of inference
I(iii), the
assumption that every recursive
function can be strongly represented leads to
inconsistency
in the system.
Hence, in omega-GA, Gödel’s reasoning does not establish the