Constructivism, Choice, and the Ethics of Decision

by Leandro Caniglia

Transitioning from classical mathematics to Homotopy Type Theory requires adopting a constructive, intuitionistic mindset. In this framework, the Law of Excluded Middle is not a universal truth but a specific axiom that must be explicitly added if classical logic is desired. This shift forces us to reevaluate foundational principles, particularly the Axiom of Choice.

In classical Zermelo-Fraenkel set theory (ZFC), the Axiom of Choice is highly permissive, allowing for arbitrary selections from collections without requiring a specific constructible rule. From the perspective of decision theory, this models a pure “choice”—a capricious, unreflective action taken without a comparative analysis of consequences or alternative paths.

Type theory is far more cautious. It fundamentally rejects arbitrary, unfounded choices. Instead, it demands that every selection be accompanied by a witness or a structural justification. By chaining these justifications together, what emerges is a formalized criterion. In this framework, because an unjustified choice is syntactically impossible to express, it becomes a truism that every choice is actually a reasoned “decision”.

This distinction carries unexpected philosophical weight. It enforces a kind of intellectual accountability, demanding that we do not make selections blindly but rather justify our steps constructively, taking full responsibility for the mathematical consequences they provoke.