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

[Dmytro Taranovsky]

This posting addresses some of the comments made by Timothy Chow.

The set of arithmetical sentences that is unassailably known to human
mathematicians is not closed under logical implication.  There are
plenty of wonderful theorems and even tautologies left to be
discovered.  The set (let us call it S) of arithmetical sentences that
human civilization is capable of knowing might satisfy better closure
conditions; although, even here, some believe that human civilization
will have access only to a limited amount of computational power and
memory, and will never have the list of all tautologies that involve
less than 2^1000 symbols.  Assuming, however, that S is closed under
logical implication (and is consistent and includes Robinson's
arithmetic Q), then S is non-recursive but may be recursively
enumerable.

Every instance of P->Con(P) (where P can be any arithmetical sentence)
is presumably in S.  If T is a recursive subset of S, then Con(T) is
true.  However, conceivably, we will never know Con(T) because at every
finite instant of time we will have confirmed only finitely many
instances of T and may not have realized that all instances of T are
true (or even consistent).  Conceivably, there is an algorithmic
limitation to human arithmetical knowledge, but we will never learn of
that limitation; and any attempt to scan human brain for the algorithms
it uses will lead to a program that either captures only a part of human
arithmetical abilities or produces, as human brains sometimes do, false
arithmetical statements.

Incompleteness of deductive systems is a general phenomenon that depends
only on sufficient expressibility of the language (including sufficient
closure conditions on what is expressible in the language), basic
deductive ability, consistency, and the expression of the provability
predicate in the language.

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.  The relevant provability
predicate is not expressible as a Sigma-0-1 sentence, and all true
Pi-0-1 sentences are in the theory.  However, the relevant provability
predicate is expressible as a Sigma-0-2 sentence, so the theory fails to
include some true Pi-0-2 sentences.

Sincerely,
Dmytro Taranovsky