Re: [isabelle] The presentation of Goedel's First Incompleteness Theorem by Lawrence C. Paulson (and others)



Ken,

I email this to you also, to try and be civilized, but you shouldn't email me back. I'm happy to let Popescu and Kumar finish it all.

But you did address this to me. I stated my rules, but rules require the use of discretion, or being ignored and broken.

If you don't diss the team on the team's turf, in a way that makes me feel I should defend the team, and you don't address emails to me, there's no reason for me to keep showing up.

To try and add some concrete value, I include a base 10 datatype that's bijective with 'nat':

https://gist.github.com/GezzMC/125ce3352966ec7f7e6c

I did that based on Num.thy, by Florian Haftmann and Brian Huffman. For the proofs, I brute forced them with a combination of 'auto', 'induct', and Sledgehammer. I've never before or since been willing to wait so long on Sledgehammer.

I suppose I should tie that into this thread.

I think I'm starting to remember its purpose for here.

We can consider any person an archetype of some class of people. An archetype at hand is Larry Paulson, and you're another archetype. To call myself an archetype, that would mean I'm (willing to admit I'm) full of myself.

*NO FANBOY, NO LOYALTY*

In this thread of emails (made up of multiple subject lines), Larry Paulson is getting mentioned a lot, and I'm defending him.

I could say, "And obviously, Larry Paulson doesn't need me to defend him". It's not the need. I think it's the value of someone knowing that their stuff is getting used.

The gist link also shows that something is being looked at and used. However, it also reflects that Isabelle/HOL isn't some perfect work where I'm saying, "I have a testimony for the world. Isabelle? Pure bliss, all the time, 24/7."

Where's the base 10 type? Where are the vectors? And don't tell me to look outside of 'Complex_Main'.

Criticism? Absolutely, to show I'm no fanboy, but in the end, it happens to be that Isabelle/HOL is good, as far as I can tell.

*ISABELLE/HOL: HAVE YOU, KEN, AND JAMES MEYER EVEN USED IT?*

This falls under the "if you're so smart" category.

I've always considered that I would need a better understanding of logic to work at the "meta-logic" or "metalanguage" level. Briefly here, you challenge the top dogs at the meta-logic level, but nothing I've seen indicates that you have any decent ability to use Isabelle/HOL. Shouldn't a smart person be able to blow through the easy stuff?

Previously, I kept James Meyer out of this, who was in your first address list. In reviewing your emails, I paid more attention to your reference to him, particularly to his remark about Paulson. Based on that, I then looked at Meyer's PDF on his site. Keep that in mind.

*MISUNDERSTANDING? NO, NON-VERBOSENESS*

You say this time:

On 12/22/2015 3:03 AM, Ken Kubota wrote:
There has been a misunderstanding. I claimed neither that Isabelle is
inconsistent nor the contrary.

Context is everything. You suggested that the foundation of Isabelle is shaky, and warned everyone that it could be inconsistent, all while bringing attention to your own work.

There was no misunderstanding on my part, only a lack of verboseness, and a lack of completely covering my tail.

*ISABELLE/HOL: HAVE YOU, JAMES, AND KEN KUBOTA EVEN USED IT?*

First, a little comedic relief.

A logician, a 2nd logician, and a 3rd logician were in a bar looking at their shoes. The first logician said, "I have concluded that when I send a long-winded email to the FOM mailing list, most likely, most of the email is not read". The 2nd and 3rd logicians just kept looking at their shoes. Not because they were stereotypical nerds, but because the choices had been, while the 1st logician was speaking, between logic or shoes, shoes or logic, logic and shoes, shoes and logic, not shoes and not logic, not(shoes and logic), and so forth, duplicates allowed. So, clearly, if not shoes and not logic is not an option, shoes are more interesting than logic any day, even to logicians.

*ISABELLE/HOL: HAVE YOU, KEN, AND MEYER EVEN USED IT?*

You referenced Meyer in your first email:

On 12/7/2015 10:35 AM, Ken Kubota wrote:
Independently, James R. Meyer has raised the same concern: "[T]he result, as
for Åwierczkowski's proof, is an illogical confusion of meta-language and the
language of HF. [...] Paulson does not include any computer code that proves
that this cannot result in an illogical confusion of meta-language and
object[ ]language." [Meyer, 2015, p. 11]

I did a search, and the PDF is this:

http://www.jamesrmeyer.com/pdfs/ff_swierczkowski.pdf

I'll get the links out of the way, and provide Paulson's:

http://afp.sourceforge.net/entries/Incompleteness.shtml

Here's a pertinent quote, page 11, including a pertinent phrase, "computer code":

Paulson does not include any computer code that proves that this cannot result in an illogical confusion of meta-language and object-language. Of course, it would be a simple matter to change the computer code to apply a different notation for HF sets and meta-language sets, but clearly the reason that was not done was because the proof could not proceed without that common notation
  for HF and the meta-language.

Paulsonâs computer assisted proof follows ÂSwierczkowskiâs proof in including the assumption that such common notation cannot result in a loss of independence of the meta-language and the object-language, and that it cannot result in an illogical confusion of meta-language and object-language. This assumption is not stated anywhere either in Paulsonâs description or in his computer code, but if it is a fully formal proof (as Paulson claims his proof to be) then that assumption should not be implicit but should be an explicit statement, and included as part of the computer code.

I will speak for Larry Paulson here, which is meant as a joke, to the extent that it is a joke.

Larry Paulson gets slightly irritated, at most, when people take pot shots at his work, but he gets downright furious when "source", as what's in a THY, is called "computer code".

Language is where I have and could get argumentative with Larry Paulson. In the end, I recognize what's important, and I try to conform with their vocabulary, when I'm operating on their domain.

Now the point. Meyer's use of "computer code" indicates that he has never used Isabelle/HOL in a meaningful way.

You have also said nothing to indicate that you've used Isabelle/HOL in a meaningful way.

I have used it now for 3.5 years. There is no "changing" things in some casual sense, as with programming languages.

The axioms are enforced, all the time. Surface changes to notation only get you a different look, for the same thing.

*SEMANTICS, MONOLITHICISTS LIKE ME DON'T NEED IT*

You're a purist? With the help of this thread, I have new labels for myself: concretist and monolithicist.

You're all caught up in "meta" and "object". Larry Paulson could have chosen lots of things to call what he calls "meta-logic" and "object-logic", like "little-logic" and "big-logic".

Personally, I think he should have chosen "I-be-the-man-logic" and "I-be-the-beggar-for-axioms-logic".

Ultimately, there's a monolithic logic. It is what is it. It is to you what you want it to be. It is to Larry Paulson what Larry Paulson wants it to be. Semantics aren't required for it to do what it does. Bits and bytes, highs and lows don't need semantics.

Goedel's First Incompleteness Theorem, whether anyone (as opposed to the machine) thinks it's been implemented in Isabelle (Nominal2 it looks like, whatever that is), has no bearing on whether it can be proved that "True = False", which, concretely, should bring a lot of things into sharp focus, when what's being used is a boolean logic like HOL.

(NOTE: Take the good and leave the bad, anywhere in this email.)

*MY EXPERIENCE, INTUITION, SO FAR SO GOOD*

When I've tried to prove things that aren't true, after seeing the light, because Isabelle/HOL wouldn't prove them, it has always ended up making sense.

Likewise with what I've proved true, like with the base 10 datatype above. It ends up making intuitive sense.

Assuming the consistency of Nominal2, whatever that is, I'll boldly say, based upon my experience with Isabelle/HOL, that what Larry Paulson proved is true, in that particular logic.

As to the meaning of what he proved, I don't even care. I care that "True ~= False". That's 13 characters, with the spaces, and even now, I'm calling for more neurons to help me out.

There's no burden in knowing very little. I always get to over perform. Please see my base 10 datatype above. True art? It's ugly, just a means to the next step.

Regards,
GB


On 12/22/2015 3:03 AM, Ken Kubota wrote:
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
	>  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 deduction
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'
	>  a<->   >  PfP "a"

cannot be a metatheorem either, since both ways of dealing with it, either
semantically (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 level
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'
	>  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 not
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







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.