Skip to main content
MathOverflow

Return to Answer

added 853 characters in body
Source Link
user13113
user13113

For the purposes of doing classical physics where you've defined a (topological) state space, or at least hypothesized one without actually constructing one, then a particularly appealing construction is the topos of sheaves on state space.

The internal language of this topos allows you precisely express various ideas I've seen thrown about based on 'physical intuition'.

For example, the idea that "physical variables don't have exact values" can be expressed by observing you can have an internal real number (i.e. some real-valued physical observable) $X$ with the property that $X = r$ is identically false for every ordinary real number $r$. In fact, this is a typical property for internal real numbers to have; $X = r$ will always be identically false unless there is some open subset $U$ of state space on which $U$ is constant.

For the purposes of doing classical physics where you've defined a (topological) state space, or at least hypothesized one without actually constructing one, then a particularly appealing construction is the topos of sheaves on state space.

The internal language of this topos allows you precisely express various ideas I've seen thrown about based on 'physical intuition'.

For example, the idea that "physical variables don't have exact values" can be expressed by observing you can have an internal real number (i.e. some real-valued physical observable) $X$ with the property that $X = r$ is identically false for every ordinary real number $r$. In fact, this is a typical property for internal real numbers to have; $X = r$ will always be identically false unless there is some open subset $U$ of state space on which $U$ is constant.

Source Link
user13113
user13113

In ZF, you can explicitly define a well-ordering of the entire constructible universe — so the axiom of choice is the theorem of choice if you reject the existence of noncosntructible sets (i.e. adopt the axiom of constructibility).

You can even get the axiom of choice as a theorem or even a triviality in somewhat more constructive settings. For example, given a family of types $X_\alpha$, the translation of the proposition $\forall \alpha \exists x : x \in X_\alpha$ into dependent type theory via the propositions-as-types paradigm is precisely the type of choice functions for the family, and so the assertion that this proposition is true is literally the same thing as specifying a choice function.

In a universe without the excluded middle, one distinguishes between the set $\Omega$ of truth values and the set $\{ \bot, \top \}$ consisting of false and true. While predicates are generally $\Omega$-valued, one still likes to find $\{ \bot, \top \}$-valued predicates where one can, since they are nicer to work with.

One can appreciate this sort of idea even in a purely classical context. For example, consider the category of topological spaces.

If $S = \{ \bot, \top \} $ is a two-point space, define an "S-valued predicate" on a space $X$ to mean a continuous function $f : X \to S$. Any such function has a corresponding subspace $f^{-1}(\{\top\}) \subseteq X$.

If $S$ has the indiscrete topology, then $S$-valued predicate are the same thing as functions $X \to \{ \bot, \top \}$, so these are just boolean predicates on the points of $X$.

If $S$ is the Sierpinski space and $\top$ is the open point, then $S$-valued predicates correspond to open subspaces of $X$, and thus describe some sort of "open property" that respects the topology of the space. Alternatively, taking $\top$ to be the closed point gives a notion of a "closed" property.

If $S$ has the discrete topology, then $S$-valued predicates on a space $X$ correspond to a property on the connected components of $X$. While these predicates are less common, they tell you something very strong about the space.

My general philosophy on these things is very heavily influenced by the idea of an internal language — in particular the internal language of a topos, or more general categories.

So, while you might want to do some work in some weaker setting, the most expedient approach to the foundations is:

  • Formalize of abstract mathematics in the way that's easiest to do work in
  • Using this convenient ambient mathematical setting, define/construct the types of universes you want to work in, and develop their theory
  • Flesh out the internal language of this universe

As an example, you mention an interest in "intuitionistic type theory" — it turns out, for example, that (intuitionistic) dependent type theories = locally cartesian closed categories. If you also insist on a type of truth values, you get precisely the notion of "elementary topos".