Finite sets, mappings, cardinals, and arithmetic in intuitionistic NF
Michael Beeson
TL;DR
This work develops a constructive infrastructure for finite mathematics inside intuitionistic NF (iNF), addressing foundational questions like the finiteness of finite cardinals and the existence of infinity under intuitionistic logic. The author adapts Rosser–Specker’s developments by introducing separable subsets and separable power sets, enabling constructive definitions of FINITE, Frege cardinals, and cardinal arithmetic in iNF. Key contributions include a robust treatment of Finite sets with decidable equality, the Frege-style notion of finite cardinals, a constructive order on cardinals, and the adoption of P_s(X) for power-set-like constructions, culminating in a coherent theory of exponentiation (2^m) within iNF. The results lay groundwork for Bishop-style constructive mathematics in NF, and the Lean-verified proofs provide a verified substrate for further investigations into constructive NF and its arithmetic.
Abstract
NF set theory using intuitionistic logic is called iNF. We develop the theories of finite sets and their power sets and mappings, finite cardinals and their ordering, cardinal exponentiation, addition, and multiplication. We follow Rosser and Specker with appropriate constructive modifications, especially replacing ``arbitrary subset'' by ``separable subset'' in the definitions of exponentiation and order. It is not known whether iNF proves that the set of finite cardinals is infinite, so the whole development must allow for the possibility that there is a maximum integer; arithmetical computations might ``overflow'' as in a computer or odometer, and theorems about them must be carefully stated to allow for this possibility. The work presented here is intended as a substrate for further investigations of iNF, including the development of Bishop-style constructive mathematics in iNF.