Provident sets and rudimentary set forcing

A. R. D. Mathias¹

¹ Professeur émérite, ERMIT, Université de la Réunion Address for correspondence: Albert-Ludwigs-Universität Freiburg Mathematisches Institut Abt. f. Mathematische Logik Eckerstrasse 1 D-79104 Freiburg, Germany

Fundamenta Mathematicae, Tome 230 (2015) no. 2, pp. 99-148.

Résumé

Using the theory of rudimentary recursion and provident sets expounded in [MB], we give a treatment of set forcing appropriate for working over models of a theory PROVI which may plausibly claim to be the weakest set theory supporting a smooth theory of set forcing, and of which the minimal model is Jensen's $J_\omega$. Much of the development is rudimentary or at worst given by rudimentary recursions with parameter the notion of forcing under consideration. Our development eschews the power set axiom. We show that the forcing relation for $\dot\varDelta_0 $ wffs is propagated through our hierarchies by a rudimentary function, and we show that the construction of names for the values of rudimentary and rudimentarily recursive functions is similarly propagated. Our main result is that a set-generic extension of a provident set is provident.

Détail

DOI : 10.4064/fm230-2-1

Keywords: using theory rudimentary recursion provident sets expounded treatment set forcing appropriate working models theory provi which may plausibly claim weakest set theory supporting smooth theory set forcing which minimal model jensens omega much development rudimentary worst given rudimentary recursions parameter notion forcing under consideration development eschews power set axiom forcing relation dot vardelta wffs propagated through hierarchies rudimentary function construction names values rudimentary rudimentarily recursive functions similarly propagated main result set generic extension provident set provident