Ken Kubota

2015-12-22 10:58:29 UTC

Dear Gottfried Barrow,

There has been a misunderstanding. I claimed neither that Isabelle is

inconsistent nor the contrary.

However, a proof of Paulson's claimed theorem 'proved_iff_proved_PfP' is not

available in axiomatic (Hilbert-style) deductive systems, because in

Hilbert-style systems this claimed theorem cannot even be expressed, since it

does not contain well-formed formulae only. Therefore this claimed theorem is

not a mathematical theorem or metatheorem. For now, please allow me to focus on

this single point.

This can be demonstrated easily by looking at the structure of the claimed

theorem 'proved_iff_proved_PfP' available at

http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 21)

http://www.owlofminerva.net/files/Goedel_I_Extended.pdf (p. 19)

which can be written

{} > a <-> {} > PfP "a"

if we use '>' for the deduction symbol (turnstile) and '"' for the Goedel

encoding quotes, and simplified without change of meaning to

Now, recalling the quotes by Alonzo Church and Peter B. Andrews available at

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00018.html

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00042.html

in an axiomatic (Hilbert-style) deductive system, the claimed theorem

'proved_iff_proved_PfP' could be either a theorem (a theorem of the object

language) or a metatheorem (a theorem of the mathematical meta-language).

Case 1 (theorem of the object language, language level 1):

As a trivial example for a theorem of the object language, we shall use

(T & T) = T

usually written

symbol (turnstile) in order to express that '(T & T) = T' is a theorem.

In this notation it has, like all theorems of the object language of Q0,

exactly one occurrence of the deduction symbol (turnstile).

Hence, the claimed theorem 'proved_iff_proved_PfP', having two occurrences,

cannot be a theorem of the object language.

Case 2 (theorem of the meta-language, language level 2):

As a trivial example for a theorem of the meta-language, we shall use

If H > A and H > A => B, then H > B.

presented in [Andrews, 2002, p. 224 (5224 = Modus Ponens)], expressing that if

there is a proof of A (from the set of hypotheses H) and a proof of A => B

(from H), then there is a proof of B (from H).

Note that this example shows some of the typical formal criteria of a

metatheorem:

1. Multiple occurrences of the deduction symbol (turnstile).

2. Use of syntactical variables (denoted by bold letters in the works of both

Church and Andrews).

3. Use of the informal words "If" and "then" instead of logical symbols in the

meta-language (according to Church's proposal).

It should be emphasized that metatheorems in proofs can always be replaced by

the proof of the concrete theorems (the syntactical or schematic variable

instantiated) when carrying out the proof, such that metatheorems are actually

not necessary (but reveal properties of the object language that help finding

proofs).

In the notation of Isabelle (natural deduction) this metatheorem would be

expressed by

[H > A; H > A => B] --> H > B

and, if we would add subscripts for the language levels, by

[H >1 A; H >1 A => B] -->2 H >1 B

So metatheorems infer from theorems of the object language (language level 1)

to another theorem of the object language, and this relation between theorems

of the object language is expressed at a higher level: the meta-language

(language level 2).

But the claimed theorem 'proved_iff_proved_PfP'

semantically (subcase a) or syntactically (subcase b), fail.

Case 2 Subcase a (semantically):

In the claimed theorem 'proved_iff_proved_PfP'

by its meaning, itself a metatheorem, not a theorem of the object language, and

we would have some kind of meta-metatheorem like

restrictions and nevertheless proceed further, then from a theorem of the

object language a theorem of the meta-language could be inferred and vice

versa, which would again violate language level restrictions, as for example a

metatheorem would be added to the list of theorems of the object language and

treated as such, leading to a confusion of language levels.

This is, in principle, the construction of the proofs of Andrews and Rautenberg

[cf. Kubota, 2013], in which 'proved_iff_proved_PfP' is used as an implicit

rule, not as a proven theorem/metatheorem. Of course, they both fail also

simply by not providing a proof using syntactical means only.

Case 2 Subcase b (syntactically):

In Paulson's claimed theorem 'proved_iff_proved_PfP'

But the Goedel encoding in Paulson's proof is implemented by the use of means

which are not available in the object language (i.e., in mathematics).

According to Paulson at

http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 16)

"[i]t is essential to remember that Gödel encodings are terms (having type tm),

not sets or numbers. [...] First, we must define codes for de Bruijn terms and

formulas.

function quot_dbtm :: "dbtm -> tm"

where

"quot_dbtm DBZero = Zero"

[...]"

Paulson's definition goes beyond the use of purely mathematical means. After

the introduction of the definition of quot_dbtm, it is used as follows:

"We finally obtain facts such as the following:

lemma quot_Zero: "'Zero' = Zero"

[...]"

But with its purely syntactical means the object language cannot explicitly

reason about its own properties directly.

Propositions in Andrews' logic Q0 have type 'o' (Boolean truth values), and one

could define a function 'foo': o -> o, o -> i, or o -> nat (with nat = (o(oi))

= (i -> o) -> o; natural numbers as "equivalence classes of sets of

individuals" [Andrews, 2002, p. 260]), etc.

But since a type "tm" (for term) does not exist in Q0 [cf. Andrews, 2002, p.

210] or R0, one cannot define a mathematical function 'quot_dbtm': dbtm -> tm.

Of course, there are rules for construing well-formed formulae (wffs), but

these (in R0 hardcoded) rules are used implicitly for construing wffs and are

not part (are not theorems) of the object language itself.

Explicit meta-reasoning as with lemma 'quot_Zero' might extend (and, hence,

violate) the object language, as it actually introduces new rules of inference

to the object language, which again may be considered as a confusion of

language levels.

Type "tm" (for term) is a notion of the (technical) meta-language, but not a

mathematical type. Therefore the function 'quot_dbtm' (type: dbtm -> tm) is not

a mathematical well-formed formula (wff), subsequently the Goedel encoding

function ('" "') and the Goedel encoding of proposition 'a' ('"a"') are not

either, and hence the right-hand side (PfP "a") is not a wff and therefore not

a proposition. Finally,

PfP "a"

or

'proved_iff_proved_PfP'

Obviously the (technical) meta-language and the object language in Isabelle are

not strictly separated, since the type "tm" (for term) is treated as a

mathematical type in the construction of wffs of the object language, which is

not mathematically safe. Mathematically, a proposition has only type 'o'

(Boolean truth values), but not a type "tm" (for term).

All definitions of Q0 are only shorthands for established wffs. In my R0

implementation, a definition label added to a wff is used for input (parsing)

and output (display) only, and remains irrelevant for syntactical inference and

can be removed or replaced at any time. This means that a definition label for

Goedel encodings (in this case the quotation marks) must represent a

mathematical well-formed formula (wff) when used in 'proved_iff_proved_PfP',

which may be a function with a mathematical type as input (domain) type such as

the type of truth values (type: o -> *), but not with types of the

meta-language as input (domain) type (type: dbtm -> *, or tm -> *), as this

violates the rules for construing mathematical wffs [cf. Andrews, 2002, p. 211].

Of course, one could introduce Goedel numbering in order to arithmetize the

object language and reason about the Goedel numbers. But the reasoning would

then be restricted to these Goedel numbers, and there would be no possibility

to relate these Goedel numbers directly to theorems of the object language as

done in the claimed theorem 'proved_iff_proved_PfP'

definable with purely mathematical means of the object language (e.g., in R0).

Since the proposition 'a' has only type 'o' (Boolean truth values), the logical

arithmetic is not stronger than propositional calculus, ruling out Goedel

encodings requiring a type "tm".

The concept of the Goedel encoding function generally violates the type

restrictions for construing mathematical wffs, as with the type of truth values

as input (domain) type there would be only two different Goedel numbers.

As in other claimed proofs, non-mathematical means are used in order to

establish a relation between the object language (proposition 'a') and the

meta-language (its provability: PfP "a") as the translation mechanism between

both language levels necessary for the self-reference part of the antinomy,

since Goedel's antinomy is construed across language levels. Note that the

antinomy seems to cause inconsistency in axiomatic (Hilbert-style) deductive

systems, but not necessarily in natural deduction [cf. Kubota, 2015, p. 14].

References

Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type

Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London:

Kluwer Academic Publishers. ISBN 1-4020-0763-9. DOI: 10.1007/978-94-015-9934-4.

Kubota, Ken (2013), On Some Doubts Concerning the Formal Correctness of Gödel's

Incompleteness Theorem. Berlin: Owl of Minerva Press. ISBN 978-3-943334-04-3.

DOI: 10.4444/100.101. See: http://dx.doi.org/10.4444/100.101

Kubota, Ken (2015), Gödel Revisited. Some More Doubts Concerning the Formal

Correctness of Gödel's Incompleteness Theorem. Berlin: Owl of Minerva Press.

ISBN 978-3-943334-06-7. DOI: 10.4444/100.102. See:

http://dx.doi.org/10.4444/100.102

____________________

Ken Kubota

doi: 10.4444/100

http://dx.doi.org/10.4444/100

There has been a misunderstanding. I claimed neither that Isabelle is

inconsistent nor the contrary.

However, a proof of Paulson's claimed theorem 'proved_iff_proved_PfP' is not

available in axiomatic (Hilbert-style) deductive systems, because in

Hilbert-style systems this claimed theorem cannot even be expressed, since it

does not contain well-formed formulae only. Therefore this claimed theorem is

not a mathematical theorem or metatheorem. For now, please allow me to focus on

this single point.

This can be demonstrated easily by looking at the structure of the claimed

theorem 'proved_iff_proved_PfP' available at

http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 21)

http://www.owlofminerva.net/files/Goedel_I_Extended.pdf (p. 19)

which can be written

{} > a <-> {} > PfP "a"

if we use '>' for the deduction symbol (turnstile) and '"' for the Goedel

encoding quotes, and simplified without change of meaning to

a <-> > PfP "a"

expressing that 'a' is a theorem if and only if there is a proof of 'a'.Now, recalling the quotes by Alonzo Church and Peter B. Andrews available at

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00018.html

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00042.html

in an axiomatic (Hilbert-style) deductive system, the claimed theorem

'proved_iff_proved_PfP' could be either a theorem (a theorem of the object

language) or a metatheorem (a theorem of the mathematical meta-language).

Case 1 (theorem of the object language, language level 1):

As a trivial example for a theorem of the object language, we shall use

(T & T) = T

usually written

(T & T) = T

as presented in [Andrews, 2002, p. 220 (5211)], with the preceding deductionsymbol (turnstile) in order to express that '(T & T) = T' is a theorem.

In this notation it has, like all theorems of the object language of Q0,

exactly one occurrence of the deduction symbol (turnstile).

Hence, the claimed theorem 'proved_iff_proved_PfP', having two occurrences,

cannot be a theorem of the object language.

Case 2 (theorem of the meta-language, language level 2):

As a trivial example for a theorem of the meta-language, we shall use

If H > A and H > A => B, then H > B.

presented in [Andrews, 2002, p. 224 (5224 = Modus Ponens)], expressing that if

there is a proof of A (from the set of hypotheses H) and a proof of A => B

(from H), then there is a proof of B (from H).

Note that this example shows some of the typical formal criteria of a

metatheorem:

1. Multiple occurrences of the deduction symbol (turnstile).

2. Use of syntactical variables (denoted by bold letters in the works of both

Church and Andrews).

3. Use of the informal words "If" and "then" instead of logical symbols in the

meta-language (according to Church's proposal).

It should be emphasized that metatheorems in proofs can always be replaced by

the proof of the concrete theorems (the syntactical or schematic variable

instantiated) when carrying out the proof, such that metatheorems are actually

not necessary (but reveal properties of the object language that help finding

proofs).

In the notation of Isabelle (natural deduction) this metatheorem would be

expressed by

[H > A; H > A => B] --> H > B

and, if we would add subscripts for the language levels, by

[H >1 A; H >1 A => B] -->2 H >1 B

So metatheorems infer from theorems of the object language (language level 1)

to another theorem of the object language, and this relation between theorems

of the object language is expressed at a higher level: the meta-language

(language level 2).

But the claimed theorem 'proved_iff_proved_PfP'

a <-> > PfP "a"

cannot be a metatheorem either, since both ways of dealing with it, eithersemantically (subcase a) or syntactically (subcase b), fail.

Case 2 Subcase a (semantically):

In the claimed theorem 'proved_iff_proved_PfP'

a <-> > PfP "a"

the right-hand side (PfP "a"), expressing the provability of theorem 'a', is,by its meaning, itself a metatheorem, not a theorem of the object language, and

we would have some kind of meta-metatheorem like

1 a <->3 >2 PfP "a"

If we ignore the fact that his meta-metatheorem violates the language levelrestrictions and nevertheless proceed further, then from a theorem of the

object language a theorem of the meta-language could be inferred and vice

versa, which would again violate language level restrictions, as for example a

metatheorem would be added to the list of theorems of the object language and

treated as such, leading to a confusion of language levels.

This is, in principle, the construction of the proofs of Andrews and Rautenberg

[cf. Kubota, 2013], in which 'proved_iff_proved_PfP' is used as an implicit

rule, not as a proven theorem/metatheorem. Of course, they both fail also

simply by not providing a proof using syntactical means only.

Case 2 Subcase b (syntactically):

In Paulson's claimed theorem 'proved_iff_proved_PfP'

a <-> > PfP "a"

the right-hand side (PfP "a") needs to be a well-formed formula.But the Goedel encoding in Paulson's proof is implemented by the use of means

which are not available in the object language (i.e., in mathematics).

According to Paulson at

http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 16)

"[i]t is essential to remember that Gödel encodings are terms (having type tm),

not sets or numbers. [...] First, we must define codes for de Bruijn terms and

formulas.

function quot_dbtm :: "dbtm -> tm"

where

"quot_dbtm DBZero = Zero"

[...]"

Paulson's definition goes beyond the use of purely mathematical means. After

the introduction of the definition of quot_dbtm, it is used as follows:

"We finally obtain facts such as the following:

lemma quot_Zero: "'Zero' = Zero"

[...]"

But with its purely syntactical means the object language cannot explicitly

reason about its own properties directly.

Propositions in Andrews' logic Q0 have type 'o' (Boolean truth values), and one

could define a function 'foo': o -> o, o -> i, or o -> nat (with nat = (o(oi))

= (i -> o) -> o; natural numbers as "equivalence classes of sets of

individuals" [Andrews, 2002, p. 260]), etc.

But since a type "tm" (for term) does not exist in Q0 [cf. Andrews, 2002, p.

210] or R0, one cannot define a mathematical function 'quot_dbtm': dbtm -> tm.

Of course, there are rules for construing well-formed formulae (wffs), but

these (in R0 hardcoded) rules are used implicitly for construing wffs and are

not part (are not theorems) of the object language itself.

Explicit meta-reasoning as with lemma 'quot_Zero' might extend (and, hence,

violate) the object language, as it actually introduces new rules of inference

to the object language, which again may be considered as a confusion of

language levels.

Type "tm" (for term) is a notion of the (technical) meta-language, but not a

mathematical type. Therefore the function 'quot_dbtm' (type: dbtm -> tm) is not

a mathematical well-formed formula (wff), subsequently the Goedel encoding

function ('" "') and the Goedel encoding of proposition 'a' ('"a"') are not

either, and hence the right-hand side (PfP "a") is not a wff and therefore not

a proposition. Finally,

PfP "a"

or

PfP "a"

cannot be a theorem, and for this reason the claimed theorem'proved_iff_proved_PfP'

a <-> > PfP "a"

cannot be a metatheorem.Obviously the (technical) meta-language and the object language in Isabelle are

not strictly separated, since the type "tm" (for term) is treated as a

mathematical type in the construction of wffs of the object language, which is

not mathematically safe. Mathematically, a proposition has only type 'o'

(Boolean truth values), but not a type "tm" (for term).

All definitions of Q0 are only shorthands for established wffs. In my R0

implementation, a definition label added to a wff is used for input (parsing)

and output (display) only, and remains irrelevant for syntactical inference and

can be removed or replaced at any time. This means that a definition label for

Goedel encodings (in this case the quotation marks) must represent a

mathematical well-formed formula (wff) when used in 'proved_iff_proved_PfP',

which may be a function with a mathematical type as input (domain) type such as

the type of truth values (type: o -> *), but not with types of the

meta-language as input (domain) type (type: dbtm -> *, or tm -> *), as this

violates the rules for construing mathematical wffs [cf. Andrews, 2002, p. 211].

Of course, one could introduce Goedel numbering in order to arithmetize the

object language and reason about the Goedel numbers. But the reasoning would

then be restricted to these Goedel numbers, and there would be no possibility

to relate these Goedel numbers directly to theorems of the object language as

done in the claimed theorem 'proved_iff_proved_PfP'

a <-> > PfP "a"

since the Goedel encodings in Paulson's proof (requiring a type "tm") are notdefinable with purely mathematical means of the object language (e.g., in R0).

Since the proposition 'a' has only type 'o' (Boolean truth values), the logical

arithmetic is not stronger than propositional calculus, ruling out Goedel

encodings requiring a type "tm".

The concept of the Goedel encoding function generally violates the type

restrictions for construing mathematical wffs, as with the type of truth values

as input (domain) type there would be only two different Goedel numbers.

As in other claimed proofs, non-mathematical means are used in order to

establish a relation between the object language (proposition 'a') and the

meta-language (its provability: PfP "a") as the translation mechanism between

both language levels necessary for the self-reference part of the antinomy,

since Goedel's antinomy is construed across language levels. Note that the

antinomy seems to cause inconsistency in axiomatic (Hilbert-style) deductive

systems, but not necessarily in natural deduction [cf. Kubota, 2015, p. 14].

References

Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type

Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London:

Kluwer Academic Publishers. ISBN 1-4020-0763-9. DOI: 10.1007/978-94-015-9934-4.

Kubota, Ken (2013), On Some Doubts Concerning the Formal Correctness of Gödel's

Incompleteness Theorem. Berlin: Owl of Minerva Press. ISBN 978-3-943334-04-3.

DOI: 10.4444/100.101. See: http://dx.doi.org/10.4444/100.101

Kubota, Ken (2015), Gödel Revisited. Some More Doubts Concerning the Formal

Correctness of Gödel's Incompleteness Theorem. Berlin: Owl of Minerva Press.

ISBN 978-3-943334-06-7. DOI: 10.4444/100.102. See:

http://dx.doi.org/10.4444/100.102

____________________

Ken Kubota

doi: 10.4444/100

http://dx.doi.org/10.4444/100