[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