A logic of abstraction related to finite constructive number classes (Q910401)

We present a sequence \(\{V_ n:\) \(n\in \omega \}\) of formal systems, which are based on type free abstraction principles and extensions of standard (classical) logic. The main result is a lower bound on the proof theoretic strength of the \(V_ n's:\) \(V_ 0\) can interpret Peano Arithmetic and each \(V_{n+1}\) contains the theory \(ID_{n+1}({\mathcal O})\) of the first \(n+1\) constructive number classes. We produce a model of \(V_{<\omega}:=\cup \{V_ n:\) \(n\in \omega \}\) and this ensures consistency. \(V_ 0\) contains: (i) first order classical logic with equality; (ii) an abstraction operator \(\{\) :\(\}\) and a predication relation \(\in\), which are connected by a suitable abstraction principle; (iii) a specific logic for a new unary sentential operator T. TA should be read as `A is internally true' \((=\) valid according to a semantical schema related to supervaluations). In \(V_ 0\) predication corresponds to internal truth and we require a weakening of Frege's principle (SAP): T(\(\forall u(u\in \{x:A)\leftrightarrow TA(x/u))\). Nevertheless \(V_ 0\) can give an independent logical foundation to elementary reasoning about natural numbers (in contrast to the type free systems of Feferman, Aczel). However, \({\mathbb{N}}\) is not definite, i.e. not \(V_ 0\vdash \neg a\in {\mathbb{N}}\to T\neg a\in {\mathbb{N}}\). This fact suggests to introduce internal truth and predication of higher level (say of level 1 if T, \(\in\) are assigned conventionally level 0). Concretely, we assume that every statement about level 0, say TA, becomes internally true or internally false at level 1. If we lift to level 1 the principles of the ground level, we are led to a new system \(V_ 1\) of type free abstraction, which can define \({\mathcal O}_ 1\), the property of being a constructive ordinal, and prove the transfinite induction schema for \({\mathcal O}_ 1\). Not surprisingly, \({\mathcal O}_ 1\) is not a definite property in \(V_ 1\) and this forces the creation of a new abstraction level. The procedure is uniform and it leads to a hierarchy \(V_ 0,V_ 1,V_ 2,..\). of theories of type free abstraction which are strictly tied up with iterated generalized induction principles. Indeed we achieve a rather natural type free framework which easily jumps up to \(\Pi^ 1_ 1\)-analysis with the axiom of induction on numbers.