Axioms Change the Mathematics You Can Build

Classical logic accepts the law of excluded middle: a proposition or its negation holds. Intuitionistic logic asks for a construction before accepting many existence claims. Choice principles select elements from families of sets. Univalent Foundations gives equivalence a foundational role in equality.

Each decision changes what counts as a proof and which transformations remain valid. It can also change the computational content that a proof assistant extracts from a theorem.

Compare Consequences, Not Schools

Foundational debates become productive when they leave labels behind and compare a concrete theorem under different axioms. The comparison can trace construction, excluded middle, choice, and the effect of univalence on equivalent structures.

Putnam’s classical arguments and constructive programs deserve the same exact reading: trace each starting rule into the mathematics it enables. The result gives researchers a working map across foundations instead of an allegiance to one vocabulary.

Make the Starting Rules Visible

Choose a familiar result and formalize it twice. The differences will reveal more than a general debate ever can. They show how logic shapes existence, how proof shapes computation, and which foundation best serves the problem at hand.