[FOM] Reflection Principles and Proof Speed-up

[Aatu Koskensilta]

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