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

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> 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

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

> 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.

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