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