nLab synthetic mathematics

Contents

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Mathematics

Contents

Idea

In “synthetic” approaches to the formulation of theories in mathematics the emphasis is on axioms that directly capture the core aspects of the intended structures, in contrast to more traditional “analytic” approaches where axioms are used to encode some basic substrate out of which everything else is then built analytically.

analyticsynthetic
structures built out of “point-set”-substrateaxioms imposed on the available types

Often the “synthetic approach” is just referred to as “axiomatic”. For instance model categories were introduced as “axiomatic homotopy theory” and indeed they may be regarded as providing a synthetic axiomatization of homotopy theory, which is not based on (but does subsume) the traditional “point-set model” provided by topological spaces.

Examples

Alternatively one may set up synthetic differential geometry via axioms for differential cohesion.

Relation to constructivism

Synthetic approaches are naturally compatible with constructive mathematics/intuitionistic mathematics, but synthetic mathematics is about a different issue than constructivism. For instance even most constructive proof assistants in existence have in their libraries defined basic mathematics concepts, such as topological spaces, in the traditional analytic way.

Relation to computer science

There is at least some similarity between synthetic mathematics and domain specific embedded programming languages, see for instance (Hudak 98, section 3.2). In (Hudak 98, figure 2) this shows aspects of a real-world DSL for “geometric region analysis” embedded in Haskell which under the relation between type theory and category theory/computational trinitarianism one immediately recognizes as a fragment of synthetic geometry.

Philosophical arguments

Proving an arithmetic result in Peano arithmetic, or more generally a statement in an appropriate axiomatic theory, ensures axiomatic purity (a notion of purity of methods?) as defined by Lehet (2021).

Moreover, such proofs are certain to be valid because of the nature of the fundamental objects considered, as captured by the axioms of the theory, and not by accident because of their particular construction in such and such a system.

References

General

See also

Synthetic homotopy theory

Discussion of synthetic homotopy theory (typically understood as homotopy type theory):

Via cubical type theory:

Last revised on October 7, 2024 at 15:18:10. See the history of this page for a list of all contributions to it.