Mathematics

Study of shape, structure and quantity.

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

Link to original