The language $L_A(\Finv)$ is formed by adding the quantifier $\Finv x$ , "few x", to the infinitary logic L A on an admissible set A. A complete axiomatization is obtained for models whose universe is the set of ordinals of A and where $\Finv x$ is interpreted as there exist A-finitely many x. For well-behaved A, every consistent sentence has a model with an A-recursive diagram. A principal tool is forcing for $L_A(\Finv)$.

A notion of finitary inductively presented (f.i.p.) logic is proposed here, which includes all syntactically described logics (formal systems)met in practice. A f.i.p. theory FS0 is set up which is universal for all f.i.p. logics; though formulated as a theory of functions and classes of expressions, FS0 is a conservative extension of PRA. The aims of this work are (i)conceptual, (ii)pedagogical and (iii)practical. The system FS0 serves under (i)and (ii)as a theoretical framework for the formalization of metamathematics. The general approach (...) may be used under (iii)for the computer implementation of logics. In all cases, the work aims to make the details manageable in a natural and direct way. (shrink)

Mancosu, P., Generalizing classical and effective model theory in theories of operations and classes, Annas of Pure and Applied Logic 52 249-308 . In this paper I propose a family of theories of operations and classes with the aim of developing abstract versions of model-theoretic results. The systems are closely related to those introduced and already used by Feferman for developing his program of ‘explicit mathematics’. The theories in question are two-sorted, with one kind of variable for individuals and the (...) other for classes. The individual variables range over a domain closed under pairing and containing, among other things, natural numbers and operations.All the theories used assume a common group of axioms that insure that the individuals in the domain satisfy the conditions for a partial combinatory algebra with pairing. We also assume a class of natural numbers and a class induction axiom on . Finally there are various class existence axioms. I work mainly with three theories, FMT0, FMT and FMTΩ, which differ from each other both in their class existence axioms as well as in some further applicative axioms.These theories have various interpretations in which every object is explicitly presented by some means of definition as well as classical, or ‘standard’, set-theoretical interpretation. The systems are formulated in a flexible general language which can be used to prove abstract theorems of mathematics , thereby generalizing recursive, hyperarithmetic and admissible versions of classical mathematics.The aim of my work is to give an abstract development of portions of model theory in the afore-mentioned theories, in a way to look as much as possible like classical mathematics. Thus, FMT0 generalizes portions of countable and recursive model theory; FMT further generalizes portions of countable and hyperarithmetical model theory and finally FMTΩ provides a generalization of the classical L-completeness theorem and of an admissible version of L-completeness due to Bruce and Keisler. This continues the development of the program mentioned above, originating with Feferman. (shrink)

The language $L_A$ is formed by adding the quantifier $\Finv x$ , "few x", to the infinitary logic L A on an admissible set A. A complete axiomatization is obtained for models whose universe is the set of ordinals of A and where $\Finv x$ is interpreted as there exist A-finitely many x. For well-behaved A, every consistent sentence has a model with an A-recursive diagram. A principal tool is forcing for $L_A$.