[FOM] Reflection Principles and Proof Speed-up

[Aatu Koskensilta]

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