[FOM] Reflection Principles and Proof Speed-up

Aatu Koskensilta aatu.koskensilta at xortec.fi
Sun Jun 3 08:25:41 EDT 2007

Richard Heck wrote:
> Certainly by L"ob's theorem, if any axiomatic system S (of sufficient
> strength, etc) proves all instances of Bew_S('A') --> A, then S is 
> inconsistent. But formulating such a system isn't entirely trivial. Take 
> PA. If we add the instances of Bew_{PA}('A') --> A, then we don't have 
> PA anymore. So what is needed is going to be some kind of 
> diagonalization: We want a system PA* that adds to PA precisely the 
> instances of: Bew_{PA*}('A') --> A. I'm sure this can be done, but, as I 
> said, it doesn't seem trivial.

Nothing but a trivial application of the recursion theorem is needed. 
The axioms of the desired theory T will be recognized by a recursive 
function f(x) with index e, where f(x) is defined by

 f(x) = 1 if x is the code of an axiom of PA or a code of "Prov_e('A') 
--> A"
 f(x) = 0 otherwise

where Prov_e('A') is the formalisation of "A is derivable from the set 
of sentences recognized by the recursive function with index e".

> As for Nuprl, I don't know if it satisfies this condition or not, seeing 
> how I'd never heard of it before.

My impression is that reflection is invoked in Nuprl when adding a 
tactic. That is, in order to add a proof tactic to the system, one 
proves, in the unextended system, that the tactic is sound, and invokes 
reflection to conclude proofs using the tactic are acceptable. I would 
guess this amounts to just iterating the addition of (local?) reflection 
any finite number over the base theory.

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