Philosophy of Mathematics

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.

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.

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$.

References

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