2021/03/31 by Michael Beeson, Beeson, Michael
Computer Science · Mathematics · #03A05 #03E70 #Algebra over a field #Arithmetic function #Computability, Logic, AI Algorithms #Computer science #Constructive #Discrete mathematics #Exponentiation #FOS: Mathematics #Finite set #Integer (computer science) #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics #Pure mathematics #Set (abstract data type) #Set theory #Universal set
paper · pdf · doi:10.48550/arxiv.2104.00506
openalex publication_date 2021/03/31 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.