◄
Chapter
3 ◄
Index Chapter
5 ►
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 4. Are there stronger omega-constructive
systems of first order Arithmetic?
Contents
4.0. Introduction
4.1. An omega-constructive first order
Arithmetic
4.2. omega-PA
4.3. Some features of omega-PA
4.4. The difference between PA and omega-PA
4.5. omega1-PA
4.6. The conflict with model theory
4.7. Introducing the omega-Specification
rule of inference
4.8. A yet stronger omega-calculus : omega2-PA
4.9. The Generalisation rule of inference
holds for omega2-PA
4.10. We cannot infer Gödel’s
conclusions from his reasoning in omega2-PA
4.11. Does Gödel’s reasoning hold even when his conclusions do not?
In this fourth section we begin by
briefly reviewing the main arguments of the earlier sections.
We then consider whether, and how,
we may strengthen omega-PA.
We use Parikh’s form of the Kreisel-Parson’s conjecture to constructively
qualify quantification.
This now allows a constructive formal system to refer to selective properties of non-constructive
elements under interpretation
We finally construct a strong
omega2-PA, and show
that the axioms,
interpretations
and models
of strong omega2-PA, and the axioms, interpretations
and models
of PA,
are identical, but have significantly different consequences.
We conclude that the formal undecidability
of Arithmetical propositions
that are true
under interpretation
is a characteristic
not of any relations that are Platonistically inherent in any Arithmetic
of the natural numbers,
but of the particular formalisation
chosen to represent the Arithmetic.
4.1. An omega-constructive
first order Arithmetic
We
argued in §1
and §2
that an omega-constructive system of Arithmetic is inconsistent
with standard first
order predicate calculus PA with strong
Generalisation.
In §3 we defined omega-PA, where we
eliminated the closed Induction axiom schema A(10) of PA,
and replaced the strong Generalisation rule of inference
I(ii) of PA
by the weaker omega-Constructivity rule of inference
I(iii).
4.3. Some
features of omega-PA
We then argued that every model of PA
is a model
of omega-PA.
We argued further that every primitive
recursive function cannot be strongly represented in omega-PA.
We also argued that omega-PA is intuitively a more natural and constructive
formal system
of Peano’s Arithmetic than PA.
We argued that Gödel’s
reasoning does not establish the existence of undecidable propositions in omega-PA, which are
true
under interpretation,
in a constructive
and intuitionistically
unobjectionable way, as he intended (Gödel p189).
4.4. The
difference between PA and omega-PA
We argued in §3.15
that the essential difference between PA
and omega-PA lay in their respective meta-assertions
about the nature and scope of the valid consequences amongst the elements of
the domain of each system under interpretation.
We then posed the question: Can we
strengthen omega-PA so that every model of a stronger omega-PA is a model of PA?
If we now add the closed Induction axiom schema A(10) to omega-PA, we arrive at a stronger, yet still constructive,
formal system
of Peano Arithmetic, omega1-PA.
omega1-PA is thus axioms A(1) to A(11) 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).
Thus PA
and omega1-PA have
identical axioms,
with identical interpretations
and models. Prima facie, though, omega1-PA
is an intuitively more natural and constructive formalisation of Peano’s Arithmetic
than PA.
Since the assumption that every recursive function
can be strongly represented in any system of Arithmetic with the omega-Constructivity
rule of inference
I(iii) leads
to inconsistency
in the system, it follows that Gödel’s reasoning does not hold in any interpretation
of omega1-PA.
Further, although omega1-PA now proves the closed Induction axiom schema A(11), in the absence
of the strong Generalisation rule of inference
I(ii) of PA,
we still cannot conclude either of:
omega1-PA proves:
‘Closed Induction’ => ‘Open Induction’
holds in omega1-PA
‘Open Induction’
holds in omega1-PA =>
omega1-PA
proves: ‘Closed Induction’
whereas in PA
we have both:
PA proves:
‘Closed Induction’ =>
‘Open Induction’
holds in PA
‘Open Induction’
holds in PA => PA proves: ‘Closed Induction’
4.6. The
conflict with model theory
Now, although PA and omega1-PA
have identical axioms,
with identical interpretations
and models,
the difference in their rules
of inference yield differing consequences amongst the well-formed formulas of the two formal systems,
and hence amongst corresponding statements under interpretation.
The difference is reflected in the
fact that Cantor’s transfinite
ordinal Arithmetic CA is not a model of PA, since:
However, in omega1-PA, we have
that, as in omega-PA:
~(omega1-PA proves: (Ax)(x+1 = 1+x)).
Further, in the absence of strong
Generalisation, all the theorems of omega1-PA
translate into true
statements, in Cantor’s transfinite
ordinal-Arithmetic CA, about only the sub-domain
N of natural
numbers.
Thus CA is a model of omega1-PA.
This appears
to conflict with the implicit Platonistic
thesis that it is the axioms
of a formal system
that essentially determine
the logical consequences in the interpretation.
4.7.
Introducing the omega-Specification rule of inference
Can we
strengthen omega1-PA further?
We consider introducing Parikh’s form
of the Kreisel-Parson’s
conjecture in omega1-PA as a means
for specifying essentially the conditions under which the closure of a provable, open,
well-formed formula in omega1-PA yields a provable,
closed, well-formed formula of omega1-PA:
I(iv) omega-Specification:
(Ax)F(x) is provable
in PA if, for each natural number n, there is a proof in PA of F(n), and its Gödel-number is less than some natural number k that is independent of n.
4.8. A yet
stronger omega-calculus : omega2-PA
We thus arrive at a yet stronger, constructive,
formulation of the first order predicate calculus, omega2-calculus.
omega2-PA is now the axioms A(1) to A(11) 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), the omega-Constructivity
rule of inference
I(iii) and the
omega-Specification
rule of inference
I(iv).
Thus PA and omega1-PA, omega2-PA all have
identical axioms,
with identical interpretations
and models. Again, omega2-PA appears
intuitively a more natural and constructive formalisation of Peano’s Arithmetic
than PA.
We note that, as in PA, we now have that:
omega2-PA proves:
(Ax)(x+1 = 1+x)
So, like PA, omega2-PA too does
not admit Cantor’s transfinite
ordinals in any model.
Thus, though omega2-PA and omega1-PA are both constructive
and have identical axioms,
these too have significantly different logical consequences, highlighting again the
apparent conflict with the implicit Platonistic thesis that it is the axioms of a formal system
that essentially determine
the logical consequences.
4.9. The Generalisation
rule of inference holds for omega2-PA
We note that, in omega2-PA, as in PA, the strong
Generalisation rule
of inference I(ii) holds, since we now have the meta-equivalence:
omega2-PA proves:
F(x) <=>
omega2-PA proves: (Ax)F(x)
It follows that, in omega2-PA, as in PA, we have:
omega2-PA proves:
‘Closed Induction’ <=> ‘Open Induction’
holds in omega2-PA
4.10. We
cannot infer Gödel’s
conclusions from his reasoning in omega2-PA
However, omega2-PA
retains the constructive
and intuitionistically
unobjectionable nature inherited from omega-PA.
Thus, in sharp contrast to PA, omega2-PA does not
admit the strong representation of
every recursive
function, and so Gödel’s reasoning establishing the existence of undecidable propositions
cannot be carried out in omega2-PA.
This follows from the fact that, if f(x, y) is a recursive function
that is represented
by a omega2-PA well-formed formula F(x, y, z), then the formal provability of (E1x3)F(k, m, x3) is the intuitive assertion (cf. §2.9)
that, for any given natural
numbers k and m, we can always construct some (non-unique)
pair of natural numbers
u, v such that
the Beta-function
β(u, v, i) represents the
first m terms, i.e. f'(k, 0), f'(k, 1), ... , f'(k, m), that are common to every primitive recursive function such as f'(x1, x2) that is
formally represented by F(x1, x2, x3).
To
prove this for any given F(x1, x2, x3), and given natural
numbers
k and m, we can determine a suitable Turing
machine that will actually construct the sequence f'(k, 0), f'(k, 1), ... , f'(k, m) uniquely in order to verify the assertion.
Clearly we can choose a k such that the number of terms in the above sequence,
and so the Gödel-number
of any Turing-computable proof, exceeds
any given natural
number k1.
It follows that, in omega2-PA, we cannot
assume that if the Gödel-number
of a proof
of:
(E1x3)F(x1, x2, x3)
is less than a given natural number k1, then
the Gödel-number
of a proof
of:
(E1x3)F(x+1, x2, x3)
will also not exceed k1.
We cannot thus assume that:
omega2-PA proves:
(E1x3)F(x1, x2, x3) =>
(E1x3)F(x+1, x2, x3).
Hence we cannot assume that the
argument of §2.13 will establish strong representability for every recursive function
F(x1, x2, x3), as is necessary for Gödel’s reasoning to hold.
In fact, since the assumption that
every recursive
function can be strongly represented in any system of Arithmetic with the omega-Constructivity
rule of inference
I(iii) leads
to inconsistency
in the system, it follows that Gödel’s conclusions do not logically follow from his
reasoning in any interpretation
of omega2-PA.
We once more have the apparent conflict with
the implicit Platonistic
thesis that it is the axioms
of a formal system
that essentially determine
the logical consequences in the interpretation.
4.11. Does Gödel’s reasoning hold even when his conclusions do not?
The
question arises: When can we infer Gödel’s conclusions
from his reasoning?
◄ Index
◄ Contents ◄ Chapter 1 ◄ Chapter 2
◄ Chapter 3 ▲ Chapter
4 Chapter 5 ► Conclusions
► Web_links ►
(Updated : Friday 11th January 2002 2:35:51 AM by re@alixcomsi.com)
References
Burbanks, Andrew. (e-seminar)
Fast-Growing Functions and Unprovable Theorems.
<Home page : http://www.maths.bris.ac.uk/~maadb/>
<Seminar
: http://www.maths.bris.ac.uk/~maadb/research/seminars/online/fgfut/index.html>
<Ord’ls
: http://www.maths.bris.ac.uk/~maadb/research/seminars/online/fgfut/fgfut09.html>
Davis, M (ed.). 1965. The
Undecidable. Raven Press, New York.