[FOM] Re: Lucas, Penrose, and the Church-Kleene ordinal

[Timothy Y. Chow]

Dmytro Taranovsky <dmytro at mit.edu> wrote:
> The set of arithmetical sentences that is unassailably known to human
> mathematicians is not closed under logical implication.

Indeed, I was careful never to assume this in my treatment.

> For example, Theory(Q plus all true Pi-0-1 sentences) is the minimal S
> that contains Q, closed under logical implication, and includes Con(T)
> whenever T is a code (under reasonable coding;  note that there are
> non-provably equivalent claims of consistency of the same set of
> sentences) of a recursive subset of S.

Hmmm...does this assertion of yours confirm or contradict what I said 
about w_1^CK?

Tim