*Subject*: Re: [isabelle] The presentation of Goedel's First Incompleteness Theorem by Lawrence C. Paulson (and others)*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Wed, 23 Dec 2015 06:36:02 +1100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <2D14D352-3D4D-4FDE-ABA4-0168BF6E04F3@kenkubota.de>*References*: <2D14D352-3D4D-4FDE-ABA4-0168BF6E04F3@kenkubota.de>*Sender*: ramana.kumar at gmail.com

Hi Ken, There are a few points in your email where I believe what you are saying is simply mistaken. I have pointed a couple of them out below. On 22 December 2015 at 20:03, Ken Kubota <mail at kenkubota.de> wrote: > 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, That is incorrect. (PfP "a") is an object-language statement. I think you may have been confused by what it represents. Indeed, the only reason you want to claim it is a metatheorem is because of "its meaning". But if you simply ignore its meaning, it is clearly and syntactically an object-level statement. If you disagree, I press you to argue your point further and concentrate only on this example until we can clear up the disagreement about this point. > 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. > The type "tm" is not a primitive type, but it can be defined, just as you defined "nat" above. Paulson defined the type before using it. It is incorrect to say that the type "tm" does not exist in Q0, if we allow Q0 type definitions.

**References**:

- Previous by Date: [isabelle] yet another AFP entry: Algebraic Numbers in Isabelle/HOL
- Next by Date: Re: [isabelle] The presentation of Goedel's First Incompleteness Theorem by Lawrence C. Paulson (and others)
- Previous by Thread: Re: [isabelle] The presentation of Goedel's First Incompleteness Theorem by Lawrence C. Paulson (and others)
- Next by Thread: Re: [isabelle] The presentation of Goedel's First Incompleteness Theorem by Lawrence C. Paulson (and others)
- Cl-isabelle-users December 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list