Mattias Wikström: IpC2 as a Foundation of Mathematics

Supervisor: Peter LeFanu Lumsdaine

Abstract: This paper discusses quantified intuitionistic propositional logic (IpC2) and suggests that it may be able to serve as a simple and yet powerful foundation of mathematics. The logic is understood topologically, as a theory for reasoning about parts of objects, and it is shown how it has the expressive power for saying how the parts of an object with finitely many parts are structured. It is shown how a conventional first-order theory (whose logic may be classical logic, intuitionistic logic, or minimal logic) for reasoning about parthood can be translated into IpC2. The paper also shows how IpC2 allows us to define a description operator, further highlighting the power of IpC2, and it is shown how the operator in question is related to well-known definitions of conjunctions, disjunctions, and the existential quantifier out of implication and the universal quantifier. The paper suggests three ways in which IpC2 may be extended with existence axioms, a topic that matters for any foundation of mathematics. The existence axioms in question turn out to be related to three different fragments of IpC2 which are also discussed in the paper, fragments where quantifiers are restricted from above and/or below.