Finite sets, mappings, cardinals, and arithmetic in intuitionistic New Foundations
Michael Beeson
math.LO
Mar 31, 2021 · v7
TL;DR
All proofs about finite sets, cardinals, and arithmetic in intuitionistic NF were machine-checked in Lean without using Mathlib's classical library.
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.
Problem
Intuitionistic New Foundations (iNF) lacks a developed basic infrastructure. It is open whether iNF proves the set of finite cardinals is infinite, so any development must allow for a possible maximum integer.
Approach
The paper develops finite sets, separable power sets, mappings, finite Frege cardinals, their ordering, and cardinal exponentiation, addition, and multiplication. It follows Rosser and Specker, with constructive modifications such as replacing arbitrary subsets by separable subsets. Arithmetic is defined so that overflow yields the empty set. All proofs were checked in the Lean proof assistant.
Results
A Lean-checked foundation of definitions and theorems for iNF, including associativity and commutativity of addition for all sets and constructive analogues of Specker's lemmas. It is intended as a basis for further work, including Bishop-style constructive mathematics in iNF.
