Nelson E. Predicative arithmetic (Princeton, 1986)(T)(201s)_MAml

Home / lib / M_Mathematics / MA_Algebra / MAml_Mathematical logic /

Nelson E. Predicative arithmetic (Princeton, 1986)(T)(201s)_MAml_.djvu

Size 1.1Mb
Date Jul 28, 2003

SEMIBOUNDED REPLACEMENT
SBRD! {{x, y) : x £ a & minK D} = /<->/ is a function &
Dom / = о & Vx(x G a —» (miny D)|,[/(x)]), otherwise f — 1,
even if D is unbounded, since the uniqueness condition holds...
Suppose 1 < j < Ln y' and define
D\ = (B'(j)) * Cy'(j)(iW(;)~S'(y + 1))) * C" * CX0(u0*X0)) *
D'KM(u0*X0,X0,y'(j)) * Cy'(j)(uo*y'(j))) * (B'(j + 1))...
This is a Unitary but impredicative consistency proof for Q*; the se-
semantic element in the proof enters in the usual proof that Q is consistent,
which involves the assumption that superexponentiation is total...