Syntactical truth predicates for second order arithmetic
Loïc Colson, Serge Grigorieff · Journal of Symbolic Logic · 2001
Abstract We introduce a notion ofsyntactical truth predicate(s.t.p.) for the second order arithmeticPA2. An s.t.p. is a setTof closed formulas such that: (i)T(t=u) if and only if the closed first order termstanduare convertible, i.e., have the same value in the standard interpretation (ii)T(A→B) if and only if (T(A) ⇒T(B)) (iii)T(∀xA) if and only if (T(A[x←t]) for any closed first order termt) (iv)T(∀X A) if and only if (T(A[X← ∆]) for any closed set definition ∆ = {x∣D(x)}). S.t.p.'s can be seen as a counterpart to Tarski's notion of (model-theoretical)validityand have main model properties. In particular, their existence is equivalent to the existence of anω-model ofPA2, this fact being provable inPA2with arithmetical comprehension only.