Here Z is Zermelo’s set theory of 1908, as later formulated: full separation, but no replacement or collection among its axioms. PROVI was presented in lectures in Cambridge in 2010 and later published with improvements by Nathan Bowler, and is, I claim, the weakest subsystem of ZF to support a recognisable theory of set forcing: PROV is PROVI shorn of its axiom of infinity. The provident sets are the transitive non-empty models of PROV. The talk will begin with a presentation of PROV, and then discuss more recent applications and problems: in particular an answer in the system Z + PROV to a question posed by Eugene Wesley in 1972 will be sketched, and two proofs (fallacious, I hope) of 0 = 1 will be given, one using my slim models of Z and the other applying the Spector–Gandy theorem to certain models of PROVI. These “proofs”, when re-interpreted, supply some arguments of Reverse Mathematics.
- Logic Seminar