4/26 Applying Loeb's proof to prl.
Let A1..An|- B iff there is a proof of >>B with premises >>A1..>>An.
Let A1..An|-k B iff there is a k-level proof of >>B with premises >>A1..>>An.
Note |-k is monotonic in k. Also, since uses of reflection can be eliminated
from premiseless proofs, |- B iff |-0 B iff |-k B.
Let Der(s;l;e) be the type family used in the reflection rule to represent
the proofs of level unrep(e), goal unrep(s), premises unrep(l).
Let Pk be \x.Der([>>x];nil;`k').
Let Q be a term, such as \x.Sigma i:N.Der([>>x];nil;i), representing
premiseless provability.
Note that |- A and the inhabitation of Pk`A' and Q`A' are equivalent.
Our reflection rule implies that Pk`A'|-j A when k>B';`>>A';`k'), and further |- Pk`A'->Pk`B',
since filling in premises of a k-proof with k-proofs gives a k-proof.
We must show (but not here) that there are valid primitive rules which can be
included such that Pk and Q are proof-predicates-ala-Loeb.
For us, such a proof predicate will be any term B in Term->U0 such that
1) |- A implies |- B`A',
2) |- B`A'->B`B`A'' (this is the hard part),
3) if |- B`A->C' then |- B`A'->B`C'.
Loeb's result is that for any A such that |- B`A'->A, |- A.
Here is his method. Pick a term C such that |- C<->(B`C'->A).
Then |- B`[C->B`C'->A]' hence(3) |- B`C'->B`B`C''->B`A' .
By (2) |- B`C'->B`B`C'' hence |- B`C'->B`A'.
So, if |- B`A'->A
then |- B`C'->A, hence(by choice of C) |- C, then |- B`C' and |- A.
We assume all our primitive rules, hence all our proofs, are valid.
Since we want to show the non-provability of various truths and
non-derivability of various rules of inference, we need only
consider certain values for A as used above, viz. *, Q`*', and Pk`*'
where * is void, and so unprovable.
a) Pk`*'->* and Q`*'->* are inhabited but not provable since
that would imply (by Loeb) the provability of *.
b) Not( Q`*'|- * ), so stratification of reflection is necessary, since
if Q`*'|- * then |- Q`Q`*''->Q`*' hence(Loeb) |- Q`*' then |- *.
b') Not( Pk`*'|-k * ), so k-reflection is not derivable at level k, since
if Pk`*'|-k * then |- Pk`Pk`*''->Pk`*' hence(Loeb) |- Pk`*' then |- *.
c) [Pi x:Term. Q(x)->P0(x)] is inhabited, i.e., we can specify
a method for elimination of reflection rules, but we cannot
prove this, or any interesting subcases.
Not |- Q`*'->Pj`*' since that would violate (b):
Pj`*'|- * by reflection; so |- Q`*'->Pj`*'
would imply Q`*'|- Pj`*' by modus ponens,
which would imply Q`*'|- *.
c') Not |- Pk`*'->Pj`*' when jPj`*' would
imply Pk`*'|-0 Pj`*' by modus ponens,
hence(monot) Pk`*'|-k Pj`*' and so Pk`*'|-k *.
January 2001
Here is a fixed point construction required for Loeb's thm for Nuprl.
We'll construct a term C such that C = [B`C'=>A] in Type.
This follows the method of our reflection paper for a similar construction,
bottom p6-top p7. (Adapted from Goedel)
Let `x' be a metanotation for a standard rep of a term,
ergo, for any term x, `x' reps x.
Let Rep(t) be an operator in Nuprl that represents this standard rep function,
i.e., if t reps r then Rep(t) reps `r'.
So, for any term x, Rep(`x') reps `x'.
Let AP(a;b) be an operator in Nuprl representing application-formation,
i.e., if a reps c and b reps d then AP(a;b) reps c(d).
Assume A in Type.
Assume B(t) in Type (t in Term).
Let k be the term \i.B(AP(i;Rep(i)))=>A
k(`k') = [B(AP(`k';Rep(`k')))=>A] in Type, by evaluation.
AP(`k';Rep(`k')) reps k(`k')
since `k' reps k and Rep(`k') reps `k',
But also `k(`k')' reps k(`k'), so AP(`k';Rep(`k')) = `k(`k')' in Term.
Hence, B(AP(`k';Rep(`k'))) = B(`k(`k')') in Type
so
k(`k') = [B`k(`k')'=>A] in Type