Chapter 4                                                                 Index                                                                 Chapter 6

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 5.  Gödel’s argument for undecidable propositions

Contents

 

5.0.  Introduction

5.1.  Every recursive function can be constructively represented in any Arithmetic

5.2.  Every representation of a recursive function has a unique Gödel-number

5.3.  Gödel’s recursive definition of provability

5.4.  Gödel’s Turing-computable q(x, y)

5.5.  Gödel’s constructive self-reference lemma

5.6.  Hilbert and Bernay’s representation lemma

5.7.  The Gödelian premise

5.8.  G$ is not provable

5.9.  ~G$ is not provable

5.10.  The essence of Gödel’s reasoning

5.11.  Gödel’s undecidable proposition GUS

5.12.  Gödel’s reasoning in PA

5.13.  Gödel’s reasoning does not establish his conclusions in most Arithmetics

5.14.  The Palimpsest syndrome in standard PA : Overview of the argument

5.15.  The Extended Representation Lemma

5.16.  The Palimpsest syndrome in standard PA : The proof

5.17.  Conclusion

5.0.  Introduction

We have argued in this paper that though Gödel’s reasoning for the formal undecidability of true propositions is valid in all the above systems of Arithmetic, the inferences that can be validly drawn from it depend on the choice of the particular system.

We now highlight the conditional nature of Gödel’s conclusions in a general Arithmetic GA.

We also argue that Gödel’s undecidable formulas have the form of palimpsests that translate as ill-defined sentences in every interpretation

5.1.  Every recursive function can be constructively represented in any Arithmetic

We note that, by a lemma of Hilbert and Bernays, if f(x, y) is a recursive function, then it can be constructively represented in GA by the well-formed formula F(x1, x2, x3), as defined in §2.2 above.

Specifically, this means that, in any of the above systems, we can construct Turing machines to verify that, for every set of natural numbers k, m, n, if f(k, m) = n then:

(i)      GA proves: F(k, m, n).

(ii)     GA proves: (Az)(~(z=n) => ~F(k, m, z)).

5.2.  Every representation of a recursive function has a unique Gödel-number

Since every recursive function, by definition, is built up from only a finite number of recursive functions of lower rank, we can further construct a Turing machine so that F(x1, x2, x3) can be expressed in only the primitive symbols of GA, and so uniquely coded and Gödel-numbered by some natural number F#.

5.3.  Gödel’s recursive definition of provability

Such a process of coding allows us, following Gödel, to define a recursive arithmetic relation prf(x, y), constructed out of 44 'simpler' recursive arithmetic functions and relations (Gödel 1931 p182), such that prf(x, y) is constructively true if and only if x is the Gödel-number of a finite proof sequence X in GA for some well-formed formula Y in GA whose Gödel-number is y.

In other words, for any given natural numbers k, m, we can construct a Turing machine T(prf(k, m)) to write out the finite expression of GA whose Gödel-number is k, check if this is a valid proof sequence of GA, extract the last element of the sequence, and check if the Gödel-number of this element is m, returning the value T(prf(k, m))=0 if prf(k, m) is true and 1 if prf(k, m) is false.

5.4.  Gödel’s Turing-computable q(x, y)

We can now define a Turing-computable function q(x, y) which is true if and only if x is the Gödel-number of a well-formed formula K(z) of GA with a single free variable z, and y is the Gödel-number of a proof of K(x) in GA.

In other words, given any numbers K#, M#, we can establish a Turing machine T(K#, M#) which will decode K# to yield the string K$ of GA, check if K$ is a well-formed formula in GA of the form K(z), decode and check if the string M$ is a valid proof sequence in GA, and then check if the last well-formed formula of the sequence is K(K#).

If so, it establishes that q(K#, M#) is true; if not, it establishes that q(K#, M#) is false.

5.5.  Gödel’s constructive self-reference lemma

Hence the constructive self reference involved in Gödel's argument is:

q(K#, M#) is true <=> M$ is a proof in GA of some well-formed formula K(K#) of GA.

5.6.  Hilbert and Bernay’s representation lemma

Now, by §5.1, since q(x, y) is recursive, there is a well-formed formula Q(x, y) of GA such that, for any natural numbers K#, M#:

(i)      q(K#, M#) is true => Q(K#, M#) is provable in GA, and

(ii)     q(K#, M#) is false => ~Q(K#, M#) is provable in GA.

5.7.  The Gödelian premise

We assume now that the well-formed formula P$ given by (Ay)(~Q(x, y)), and the well-formed formula G$ given by (Ay)(~Q(P#, y)), are well-formed formulas of a simply consistent GA.

5.8.  G$ is not provable

Assuming G$ is provable in GA, let M$ be the proof of (Ay)(~Q(P#, y)) in GA.

We then have that q(P#, M#) is true by definition.

Hence Q(P#, M#) is provable in GA, and so (Ey)Q(P#, y) is provable in GA.

Hence ~(Ay)(~Q(P#, y)) is provable in GA, i.e. ~G$ is provable in GA

We conclude that (Ay)(~Q(P#, y)) is not provable in GA if GA is simply consistent, i.e. G$ is not provable in GA if GA is simply consistent

5.9.  ~G$ is not provable

Assuming ~G$ is provable in GA, it follows that G$ is not provable in GA if GA is simply consistent.

Hence q(P#, y) is false for all y.

It follows that ~Q(P#, y) is provable in GA for all y.

So, in every interpretation of GA, ~Q(P#, y) translates as a true proposition for all y.

However, since ~G$ is provable in GA, then ~(Ay)(~Q(P#, y)) is provable in GA.

We then have the contradiction, in every interpretation of GA, that Q(P#, M#) translates as true for some M#, thus implying that GA is inconsistent.

We conclude that ~G$ is not provable in GA if GA is simply consistent.

5.10.  The essence of Gödel’s reasoning

What we have above is that, if G$ is a well-formed formula in GA, then:

(i)      [(GA proves: G$)  =>  (GA proves: ~G$)]  =>  ~(GA proves: G$)

(ii)     [(GA proves: ~G$)  =>  (Every interpretation of GA is inconsistent)]  =>  ~(GA proves: ~G$)

5.11.  Gödel’s undecidable proposition GUS

We consider now the well-formed formula G$ of GA, given by (Ay)(~Q(P#, y)), under interpretation.

We argue below, in §5.14, that if (Ay)(~Q(P#, y)) translates as a false sentence under any interpretation, then Q(P#, L#) translates as a true assertion for some L$.

However, we then have the contradiction that (Ay)(~Q(P#, y)) translates as a true sentence under the interpretation.

We conclude that, if G$ is a well-formed formula in GA, then G$ translates into a true proposition in every interpretation of GA, even though both the well-formed formulas G$ and ~G$ are not provable in GA, i.e. in every interpretation of GA, G$ yields a Gödelian, formally undecidable but true, proposition GUS.

5.12.  Gödel’s reasoning in PA

Since, by §2.13, the well-formed formula F(x1, x2, x3) is well-defined in PA for any primitive recursive function f(x, y), the above reasoning yields Gödel’s proof of undecidability as a non-trivial assertion in PA.

5.13.  Gödel’s reasoning does not establish his conclusions in most Arithmetics

However, in all the other systems of Arithmetic defined above, Gödel’s reasoning does not establish his conclusions significantly since the well-formed formula F(x1, x2, x3) is not obviously well-defined in these systems for every primitive recursive function f(x, y).

In systems of Arithmetic with an omega-constructive rule, in particular, the assumption §5.7 yields the meta-inconsistency:

(i)      [(GA proves: G$)  =>  (GA proves: ~G$)]  =>  ~(GA proves: G$)

(ii)     [~(GA proves: G$)  =>  (GA proves: G$)]  =>  (GA proves: G$)

Ipso facto, both G$ and ~G$ are not well-defined, well-formed formulas in any systems of Arithmetic with an omega-constructive rule.[1]

They are thus trivially unprovable, and Gödel’s formally undecidable proposition GUS trivially true, in every interpretation of a system of Arithmetic with an omega-constructive rule.

5.14.  The Palimpsest syndrome in standard PA : Overview of the argument

We now argue that GUS essentially formalises the Liar sentence in standard PA by means of a “palimpsest”.[2]

We argue that, by virtue of its roots in the finite construction, through Gödel-numbering, of the primitive recursive relation q(P#, y), every interpretation of Gödel’s undecidable formula (Ay)(~Q(P#, y)) can constructively be well-defined over the entire domain of any interpretation M in such a way that it is equivalent to the assertion:

"For all y, the formula Y, whose Gödel-number is y, is not the interpretation of a finite proof sequence in standard PA for the formula (Ay)(~Q(P#, y)), whose Gödel-number is P#, from the given set Axm of recursively defined axioms, and the given set Inf of recursively defined rules of inference, of standard PA."

If standard PA is assumed consistent, this means either that the sentence (Ay)(~Q(P#*, y)) (where P#* is the interpretation in M of the numeral P#) can be interpreted as true in every interpretation M of standard PA (since the set Axm of axioms, and set Inf of rules of inference, of Gödel’s formal system of standard PA, are defined recursively), or the expression (Ay)(~Q(P#*, y)) treated as an ill-defined sentence in every M under interpretation.

In other words, even if (Ay)(~Q(P#, y)) is a well-defined formula in standard PA, there can be no consistent, non-standard model M of standard PA in which its interpretation (Ay)(~Q(P#*, y)) is uniquely false.

(The latter would imply the contradiction that we can write out a finite proof sequence in standard PA for the unprovable formula (Ay)(~Q(P#, y)) using only the given set Axm of axioms and the given set Inf of rules of inference of standard PA.)

By virtue of Gödel’s completeness theorem for first order predicate calculus, it then follows that even if, like Russell's paradoxical set, the formula (Ay)(~Q(P#, y)) appears to be a valid construction in standard PA, it must translate as an ill-defined sentence under every interpretation.

In other words, there is an essential element in the definition of the formula (Ay)(~Q(P#, y)) such that, as in the case of the Liar sentence, we cannot constructively ascribe, or even non-constructively assume, either truth or falsity to/for the sentence (Ay)(~Q(P#*, y)) in an interpretation without inconsistency.

It is a moot point whether we choose to treat (Ay)(~Q(P#*, y)) as an ill-defined “sentence” in every interpretation, or to treat standard PA as an inconsistent system.

5.15.  The Extended Representation Lemma

To give the argument in detail, we note the following meta-properties of recursive arithmetical relations f(y) where, if M is any interpretation of standard PA then, for all natural numbers n, and their representations n and interpretations n* in standard PA and M respectively:

f(n) is true in the standard interpretation

=> F(n) is provable in standard PA

=> F(n*) is true in the interpretation M

f(n) is false in the standard interpretation

=> ~F(n) is provable in standard PA

=> F(n*) is false in the interpretation M

From this we conclude that, for every natural number n:

f(n) is true in the standard interpretation  <=>  F(n*) is true in the interpretation M

If we extend the definition of f(x) in the standard interpretation SI so that f(x) is false if x is not a natural number, then we have the Extended Representation meta-Lemma for recursive arithmetical functions f(x):

  f(x) is true in the standard interpretation  <=>  F(x) is true in the interpretation M

5.16.  The Palimpsest syndrome in standard PA : The proof

We note that Gödel’s undecidable formula ~(Ay)(~Q(P#, y)) now translates as a well-defined sentence over the entire domain of any interpretation M.

The significance of the Extended Representation meta-Lemma is that, by virtue of Goedel’s original definition of the primitive recursive relation q(P#, y) - involving only finite Gödel-numbers of finite sets of well-formed, well-defined finite formulas and finite proof sequences of standard PA - its representation Q(P#, y) in standard PA is well-defined only over the denumerable domain of the numerals n in standard PA, corresponding to the denumerable natural numbers n.[3]

It follows that, in any interpretation M of standard PA, the sentence ~(Ay)(~Q(P#*, y)) - which is equivalent to the assertion (Ey)Q(P#*, y) - is well-defined if and only if the relation Q(P#*, a*) is satisfied for some value a* in the domain of M that is an interpretation of some numeral a of standard PA. However, we cannot conclude from this that Q(P#*, a*) is well-defined - and so decidable - for every value a* in the domain of M that is not an interpretation of some numeral a of standard PA.

This lacuna is now filled by the Extended Representation meta-Lemma, which ensures that the range over which the relation Q(P#*, a*) is well-defined covers the entire domain of M, and that Q(P#*, a*) is not satisfied by any value a* in the domain of M that is not an interpretation of some numeral a of standard PA.

This follows immediately since (Ay)(~Q(P#*, y)) in M is now equivalent to:

"For all y, the formula Y, whose Gödel-number is y, is not the interpretation in M of a finite proof sequence in standard PA for the formula (Ay)(~Q(P#, y)), whose Gödel-number is P#, from the given set Axm of recursively defined axioms, and the given set Inf of recursively defined rules of inference, of standard PA."

In other words, the sentence ~(Ay)(~Q(P#*, y)) is well-defined in M, and Q(P#*, a*) is necessarily false for all values a* in the domain of M that are not interpretations of some numeral a of standard PA.

(The argument here is that the relation Q(x, y) can always be well-defined in every interpretation M of standard PA in such a way that it mirrors the “palimpsest” that is embedded in the definition of the relation q(x, y) of the standard interpretation SI.)

We thus argue that there is no interpretation in which the formula ~(Ay)(~Q(P#, y)) of standard PA uniquely translates as a well-defined sentence ~(Ay)(~Q(P#*, y)) that can be true for some value a* in the domain of M that is not an interpretations of some numeral a of standard PA.

Hence the truth of the sentence ~(Ay)(~Q(P#*, y)) in any interpretation M of standard PA can always be defined so as to imply the truth of Q(P#*, n*) for some n* in M, where n* is the interpretation of the numeral n in M.

This, of course, implies the truth of q(P#, n) for some natural number n in the standard interpretation SI by the Extended Representation meta-Lemma. This in turn, by Gödel’s Self-reference Lemma for q(P#, y), implies that n is a proof of the sentence (Ay)(~Q(P#, y)) in standard PA, contradicting the unprovability of the formula (Ay)(~Q(P#, y)) in standard PA.

Hence the sentence ~(Ay)(~Q(P#*, y)) can be falsified in every interpretation M of standard PA, so that the sentence (Ay)(~Q(P#*, y)) is true in every interpretation M of standard PA.

However, by Gödel’s completeness theorem for first order predicate logic, this again implies that the formula (Ay)(~Q(P#, y)) is provable in standard PA.

5.17.  Conclusion

The contradiction establishes that, if standard PA is consistent, then Gödel’s undecidable formulas, (Ay)(~Q(P#, y)) and ~(Ay)(~Q(P#, y)), translate as ill-defined sentences under interpretation[4].

Index           Contents           Chapter 1          Chapter 2

Chapter 3         Chapter  4           Chapter 5           Conclusions           Web_links

(Updated : Friday 11th January 2002 2:37:10 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.

<Home page : http://www.cs.nyu.edu/cs/faculty/davism/>

 

Franzén, Torkel. Provability and Truth.

< Home page : http://www.sm.luth.se/~torkel/>

<See also remarks : http://www.sm.luth.se/~torkel/eget/godel/system.html>

<See also remarks : http://www.sm.luth.se/~torkel/eget/thesis/chapter5.html>

 

Friedman, Harvey. 1997. Unprovable theorems in discrete mathematics.

<Unprovable : http://www.math.berkeley.edu/~ribet/Colloquium/friedman.html>

 

Gödel, Kurt. 1931. On formally undecidable propositions of Principia Mathematica and related systems I. Also in M. Davis (ed.). 1965. The Undecidable. Raven Press, New York.

<1931 Paper : http://www.ddc.net/ygg/etext/godel/godel3.htm>

<Formal system : http://www.ddc.net/ygg/etext/godel/godel3.htm - 15>

<Reducibility : http://www.ddc.net/ygg/etext/godel/godel3.htm - AXIOM-IV>

<Comprehension : http://www.ddc.net/ygg/etext/godel/godel3.htm - AXIOM-IV>

<See remarks on p190/191 : http://www.ddc.net/ygg/etext/godel/godel3.htm - 16>

<Recursive definitions : http://www.ddc.net/ygg/etext/godel/godel3.htm - DEF1>

< Beta-function : http://www.ddc.net/ygg/etext/godel/godel3.htm - LEMMA1>

< See remarks on p189 : http://www.ddc.net/ygg/etext/godel/godel3.htm - 16>

<Eqn. 8.1 : http://www.ddc.net/ygg/etext/godel/godel3.htm - EQ8.1>

<Axiom IV : http://www.ddc.net/ygg/etext/godel/godel3.htm - AXIOM-IV>

<Footnote 48a : http://www.ddc.net/ygg/etext/godel/godel3.htm - 48a>

<cf. Recursive definition #17 : http://www.ddc.net/ygg/etext/godel/godel3.htm - DEF17>

<cf. Proposition V : http://www.ddc.net/ygg/etext/godel/godel3.htm#PROP-V>

 

Gödel, Kurt. 1934. On undecidable propositions of formal mathematical systems. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York.

 

Lucas, J. R. The Gödelian argument.

<Home page : http://users.ox.ac.uk/~jrlucas/>

<Gödelian argument : http://www.leaderu.com/truth/2truth08.html>

 

Mendelson, Elliott. 1964. Introduction to Mathematical Logic. Van Norstrand, Princeton. 

<Home page : http://sard.math.qc.edu/Web/Faculty/mendelso.htm>

 

Parikh, Rohit. 1973. On the length of proofs. In Trans. AMS, 177, 29-36

<Home page : http://www.sci.brooklyn.cuny.edu/cis/parikh/>

 

Parsons, Charles D. 1995. Platonism and mathematical intuition in Kurt Gödel's thought. In The Bulletin of Symbolic Logic, Volume 1, Issue 1, March 1995.

<1995 Article : http://www.math.ucla.edu/~asl/bsl/0101-toc.htm>

 

Peregrin, Jaroslav. 1997. Language and its Models: Is Model Theory a Theory of Semantics?

< cf. also Models : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/models-html.html>

<cf. also Quantifier : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node8.html>

<cf. also Basis : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node5.html>

< cf. also Consequence : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node11.html>

< cf. also Truth : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node3.html>

< cf. also Language :  http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node2.html>

 

Podnieks, Karlis. 2001. Around Goedel's Theorem.

<Home page : http://www.ltn.lv/~podnieks/index.html>

<Around Goedel’s Theorem : http://www.ltn.lv/~podnieks/gt.html>

<Goedel's Incompleteness Theorem : http://www.ltn.lv/~podnieks/gt5.html - BM5_3>

<Standard first order Arithmetic PA : http://www.ltn.lv/~podnieks/gt3.html - BM3>

<Formula-number : http://www.ltn.lv/~podnieks/gt5.html - BM5_2>

<Decode : http://www.ltn.lv/~podnieks/gt5.html - BM5_2>

<Representation theorem : http://www.ltn.lv/~podnieks/gt3.html - BM3_3>

<Platonism : http://www.ltn.lv/~podnieks/gt1.html>

<Self-reference lemma : http://www.ltn.lv/~podnieks/gt5.html - BM5_2>

 

Rosmaita, Brian J. Minds, machines, and metamathematics: constraints on the mathematical objection to mechanism.

<Article : http://www.personal.kent.edu/~brosmait/apa96.html>

---

Web resources

 

Free On-line Dictionary of Computing.

<Dictionary : http://www.nightflight.com/foldoc/>

<cf. constructive : http://lgxserve.ciseca.uniba.it/lei/foldop/foldoc.cgi?query=constructive>

<Simply consistent : http://www.swif.uniba.it/lei/foldop/foldoc.cgi?simple+consistency>

<Infinite : http://www.swif.uniba.it/lei/foldop/foldoc.cgi?query=infinite&action=Search>

<Generalisation : http://www.swif.uniba.it/lei/foldop/foldoc.cgi?generalization>

<Converse : http://lgxserve.ciseca.uniba.it/lei/foldop/foldoc.cgi?query=converse>

<Turing machine : http://www.swif.uniba.it/lei/foldop/foldoc.cgi?query=turing>

<Artificial Int. : http://www.swif.uniba.it/lei/foldop/foldoc.cgi?query=AI&action=Search>

<Range : http://www.nightflight.com/foldoc-bin/foldoc.cgi?query=range>

<Cmprhn. axiom : http://ase.isu.edu/ase01_07/ase01_07/bookcase/ref_sh/foldoc/99/8.htm>

<ZF set theory : http://ase.isu.edu/ase01_07/ase01_07/bookcase/ref_sh/foldoc/35/122.htm>

<Mapping : http://www.swif.uniba.it/lei/foldop/foldoc.cgi?query=mapping&action=Search>

 

Free On-line Dictionary of Philosophy.

<Dictionary : http://www.swif.uniba.it/lei/foldop/>

 

Glossary of First-Order Logic.

<Glossary : http://www.earlham.edu/~peters/courses/logsys/glossary.htm>

<First order : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - fot>

<Predicate calculus : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - pl>

<Arithmetic : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - arithmetic>

<Omega : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - omegacom>

<Formula : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - formalsystem>

<Domain : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - domain>

<Set : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - set>

<Natural numbers : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - naturals>

<Numeral : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - numeral>

<Compound : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - compoundprop>

<cf. Meta... : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - metalanguage>

<Intrprttn. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - interpretation>

<Equivalent : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - equivalence>

<Omega-comp. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - omegacom>

<Free variable : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - freevar>

<Consequence : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - syncon>

<Proof sequence : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - proof>

<Denum. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - denumerableset>

<Rcrsv. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - recursivefunction>

<Frml sys. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - formallanguage>

<Cptbl. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - computablefunction>

<Standard model : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - model>

<Set theory : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - settheory>

<Closure : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - closure>

<Model : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - model>

<Std. set theory : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - settheory>

<Epimenides : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - enumset>

<Russell : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - russellparadox>

<Gödel-number : http://www.earlham.edu/~peters/courses/logsys/glossary.htm#gnumbering>

<Well-formed formula : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - wff>

<Rprsntn. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - repfunction>

<Proposition : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - proposition>

<Predicate : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - powerset>

<Rules of inf. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - rulesinf>

<Total fn. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - totalfunction>

<Satisfaction : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - satisfaction>

<Axioms : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - axioms>

<Function : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - function>

<Dcdbl : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - decidablesystem>

<Transfinite : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - totalfunction>

<Exstnc. pr. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - existenceproof>

<Cnst. pr. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - constructiveproof>

<Implication : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - implication>

<Completeness : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - completeness>

 

Internet Encyclopedia of Philosophy

<Antinomies : http://www.utm.edu/research/iep/p/par-log.htm>

 

Larry Hauser’s Mostly Modern Philosophical Glossary.

<Glossary : http://members.aol.com/lshauser2/lexicon.html>

<True : http://members.aol.com/lshauser2/lexicon.html - truth>

 

MacTutor History of Mathematics archive

<Home page :  http://www-groups.dcs.st-and.ac.uk/~history/>

<Kurt Gödel :  http://www-groups.dcs.st-and.ac.uk/~history/Mathematicians/Godel.html >

 

MathPages

<MathPages : http://www.mathpages.com/home/>

 

Stanford Encyclopedia of Philosophy.

<Encyclopedia : http://setis.library.usyd.edu.au/stanford/archives/win1997/contents.html>

<Vagueness : http://setis.library.usyd.edu.au/stanford/archives/win1997/entries/vagueness/>

<cf. also Non-constructive : http://plato.stanford.edu/entries/mathematics-constructive/ - 2>

<Intuitionistically : http://plato.stanford.edu/entries/logic-intuitionistic/>

<Principia : http://plato.stanford.edu/entries/principia-mathematica/>

<cf. also Constructive : http://plato.stanford.edu/entries/mathematics-constructive/ - 1>

<cf. also Platonism : http://plato.stanford.edu/entries/mathphil-indis/ - 1>

 

Web Dictionary of Cybernetics and Systems

<Dictionary : http://pespmc1.vub.ac.be/ASC/indexASC.html>

<Isomorphism : http://pespmc1.vub.ac.be/ASC/ISOMORPHISM.html>

 

xrefer

<Home page : http://www.xrefer.com/>

<Axiom of reducibility :  http://www.xrefer.com/entry/553361>

<cf. Formalism : http://www.xrefer.com/entry/552091>



[1]  We note that Russell’s anomalous set R, defined by {x | x is a member of R’, ‘x is not a member of x’} as the set of all sets that are not members of themselves, can also be expressed in terms of the primitive symbols of an axiomatic set theory S. However, the assumption that the well-formed formulasR is a member of R’ and ‘R is not a member of R’ are well-defined, well-formed formulas of S is inconsistent with the axioms of S.

 

[2]  The intention here is to translate the formula ‘(Ay)(~Q(P#, y))’ from standard PA into English in order to argue the point that the truth of this assertion, under any interpretation, does not depend on the interpretation into which it is translated, but on the truth of a factual assertion, pertaining to standard PA specifically, that is embedded in the formula ‘(Ay)(~Q(P#, y))’ itself in the form of a “palimpsest”.

 

For example, albeit at an explicit level, the statement “The English word ‘tree’ contains four letters of the English alphabet” must remain true no matter into which language - standard PA, Sanskrit, sign-language etc. - it is translated; it contains an assertion of fact that cannot be altered by the language into which it is translated.

 

If the destination-language contains the source-language, then it may indeed be able to determine the truth of factual assertions such as the above. If not, such assertions would be factually undecidable, at least until enough of the source-language is suitably adjoined.

 

The thesis here is that every interpretation of Gödel’s formal system of standard PA in another language implicitly preserves the logical content of “named” entities; moreover, it subsumes standard PA and so contains the necessary wherewithal to determine the truth or falsity of factual assertions pertaining to the formal system of standard PA.

 

[3]  The central issue in these papers actually concerns the relationship of the formally represented elements to the elements that they seek to represent. Thus, if standard PA is to serve as the formal representation of intuitive arithmetic IA, then the questions that must be addressed are whether every element of intuitive arithmetic IA is represented in standard PA, and whether there are elements of standard PA that are not reflected in intuitive arithmetic IA.

 

If we assume that our intuitive arithmetic IA is what we define as the standard interpretation SI of standard PA, then the question is whether every element of the standard interpretation SI is represented in standard PA, and whether there are elements of standard PA that are not reflected in the standard interpretation SI.

 

In the former case, standard PA must be judged as inadequate to our intent; in the latter, as containing elements extraneous to our intent.

 

Applying the same measure to the representation of, say, a function f(x) of the standard interpretation SI by some formula F(x, y) of standard PA, it follows that if f(x) is an intuitively well-defined function, then F(x, y) too must be a well-defined representation, i.e. F(x, y) cannot be considered to represent f(x) in some respects only, but must be taken to represent it entirely.

 

We argue that Gödel’s interpretation of undecidability actually violates this basic integrity. It implies that the truth of some propositions cannot be reflected in the formalisation, whilst the undecidability of some formulas cannot be reflected in the assertions that they represent.

 

We argue that this interpretation is subjective, and that a more objective interpretation implies that the undecidability of some formulas in standard PA reflects assertions in the standard interpretation SI that cannot be ascribed any truth-value, and are thus ill-defined assertions similar to the Liar sentence, and not true sentences as concluded by Gödel.

 

[4]  The cause of such ill-definedness apparently lies in the formal definition of Q(x, y) as the representation of q(x, y) in standard PA through use of the Gödel Beta function. By definition, Q(x, y) thus represents, in standard PA, an infinity of “recursive” functions of every interpretation (cf. §2.9).

 

Hence the PA provability of Q(k, m) may be intuitively viewed as corresponding, in any interpretation M, to the intuitive assertion that, for any interpretations k* and m* in M of the numerals k and m, we can always construct some (non-unique) pair of values u*, v* such that we can define a “Beta-functionβ*(u*, v*, i) in M that represents the first m* terms, i.e. q'(k*, 0*), q'(k*, 1*), ... , q'(k*, m*), which are common to an infinity of “primitive recursive relations” of M, such as q'(x, y), that are formally represented in PA by Q(x, y)..

 

Clearly, in this view, the provability of the formula Q(x, y) for variable x and y does not interpret similarly into a unique, well-defined proposition that can be asserted as true in M. It follows that the provability of ~Q(x, y) in PA interprets as a true proposition in M by virtue of its ill-definedness (i.e. although we may not intuitively assert an ill-defined proposition as true in M, we may yet assert that it is not a true proposition in M).

Index           Chapter 5          Bibliography          Web_links

(Updated : Friday 11th January 2002 2:38:02 AM by re@alixcomsi.com)