Philosophy of Mathematics

Traditional Schools

Platonism

Asserts mathematical objects exist independently of human thought in an abstract realm. Statements are objectively true or false regardless of provability.

• Logic: Classical ($P\vee \neg P$ holds universally).
• Infinity: Accepts actual infinity.

Formalism

Views mathematics as a game of symbol manipulation according to syntactic rules, devoid of intrinsic meaning.

• Logic: Usually classical, derived from axiomatic consistency.
• Infinity: Treated as an ideal element to secure consistency of finite mathematics.

Intuitionism

Asserts mathematics is a creation of the human mind. Truth equals provability via mental construction.

• Logic: Intuitionistic (Rejects $P\vee \neg P$ and $\neg \neg P\to P$ without witness).
• Infinity: Accepts potential infinity; rejects actual infinity as a completed totality.

Constructive Approaches

Brouwerian Intuitionism

Founded by L.E.J. Brouwer. A metaphysical stance where mathematics is a languageless activity of the mind based on the intuition of time.

• Ontology: Objects exist only if mentally constructed.
• Logic: Rejects LEM. The continuum is non-atomistic and constructed via choice sequences.
• Continuity: All functions $f:\mathbb{R}\to \mathbb{R}$ are continuous.

Bishop-Style Constructivism (BISH)

Founded by Errett Bishop. A pragmatic approach aiming to preserve numerical meaning without metaphysical reliance on a creative subject.

• Philosophy: Mathematics must have computational content. To prove $\exists xP(x)$, one must provide an algorithm to compute $x$ and show it satisfies $P$.
• Compatibility: Designed to be a proper subsystem of classical mathematics.

Finitism

A stricter restriction accepting only objects and operations constructible in a finite number of steps.

• Strict Finitism: Rejects natural numbers not practically computable.
• Classical Finitism: Accepts potential infinity of $\mathbb{N}$ but quantifiers range only over finite domains.

Logical Semantics

The BHK Interpretation

The Brouwer-Heyting-Kolmogorov (BHK) interpretation provides the informal semantics for intuitionistic logic, equating truth with the existence of a proof-object.

For propositions $A,B$:

• $A\wedge B$: A pair $(a,b)$ where $a$ proves $A$ and $b$ proves $B$.
• $A\vee B$: A pair $(i,p)$ where $i\in \{0,1\}$. If $i=0$, $p$ proves $A$; if $i=1$, $p$ proves $B$.
• $A\to B$: A construction $f$ that transforms any proof $x$ of $A$ into a proof $f(x)$ of $B$.
• $\exists x\in S,P(x)$: A pair $(w,p)$ where $w$ is a witness in $S$ and $p$ proves $P(w)$.
• $\forall x\in S,P(x)$: A function mapping each $x\in S$ to a proof of $P(x)$.
• $\neg A$: Defined as $A\to \perp$.

Formalization

Martin-Löf Type Theory

Per Martin-Löf formalized the BHK interpretation via the Propositions-as-Types correspondence.

Judgements vs Propositions

We distinguish between the judgement (meta-level) and the proposition (object level).

1. $A\text{ type}$
2. $A=B$
3. $a:A$
4. $a=b:A$

Canonical Forms

Logic	Type Theory	Construction
$\forall x\in A,P(x)$	${\Pi }_{(x:A)}P(x)$	Dependent Function
$\exists x\in A,P(x)$	${\Sigma }_{(x:A)}P(x)$	Dependent Pair
$A\wedge B$	$A\times B$	Product
$A\vee B$	$A\uplus B$	Coproduct
$a{=}_{A}b$	${\text{Id}}_A(a,b)$	Identity Type

Homotopy Type Theory

Extends Martin-Löf Type Theory with the Univalence Axiom, treating isomorphic structures as equal.

• Constructive View: Cubical Type Theory provides computational content for Univalence via dimension variables and Glue types, restoring canonicity.

References

• bishop1967-constructive
• brouwer1981-lectures
• heyting1956-intuitionism
• martinlof1984-itt
• troelstra1988-constructivism