[FOM] Reflection Principles and Proof Speed-up

Aatu Koskensilta aatu.koskensilta at xortec.fi
Sat Jun 9 14:26:03 EDT 2007

Ilya Tsindlekht wrote:
> It seems one can use the same technic as in construction of Goedel's
> indecidable statement: take sentence which says 'PA + sentence obtained
> from sentence with Goedel number N by substituting N for 'N' proves A ->
> A' and then substitute its Goedel number for N.

You seem to have in mind adding to PA the fixed point A of
"Prov_(PA+x)('P') --> P" and considering the theory PA + A. Alas,
this doesn't work, since the reflection schema is not reducible to
any finite number of its instances -- there is no single sentence
"Prov_(PA+A)('P') --> P". I don't know how to get a set of statements
A with the property that the axioms of PA are in A, and for every P,
"Prov_A('P') --> P" is in A, without using the recursion theorem.

Aatu Koskensilta (aatu.koskensilta at xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

More information about the FOM mailing list