Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory

Topic: LEM in HoTT

Leopold Schlicht (Aug 11 2021 at 10:53):

The HoTT book defines the law of excluded middle as follows (see page 113):
$\mathsf{LEM} := \prod_{A\colon\mathcal U}(\mathsf{isProp}(A)\to(A+\neg A))$
This means: every mere proposition is decidable. However, this is stronger than what I personally consider LEM to be, namely the statement that every mere proposition is merely true or false:
$\mathsf{LEM}' := \prod_{A\colon\mathcal U}(\mathsf{isProp}(A)\to \lVert(A+\neg A)\rVert_{-1})$

1. Why doesn't the HoTT book consider this version of LEM?
2. Is $\mathsf{LEM}'$ a good candidate for a framework in which classical logic and constructive logic can coexist, in the sense that one can use both modes in parallel? What I have in mind is the following: when one wants to reason classically, one uses truncated logic. $\mathsf{LEM}'$ then allows one to use the law of excluded middle on the truncated level (in which one just makes mere assertions). On the other hand, if one wants to make pure, constructive assertions (with computational content), then one uses untruncated logic (i.e., the pure propositions-as-types interpretation without $\lVert\cdots\rVert_{-1}$-ing). For this to be possible it must be the case that assuming $\mathsf{LEM}'$ somehow doesn't destroy the computational meaning of the untruncated layer, i.e., it should still be possible to extract an algorithm from each term of an untruncated statement of the form $\prod_{n\colon\mathbb N}\,\sum_{m\in\mathbb N}.\, P(m,n)$. Is this true?
3. Quite unrelated to 1. and 2.: what are some examples of applications of truncated logic (except in the statements of LEM and AC)? (If the truncated logic is constructive, just as untruncated logic, there seems to be no real advantage of using truncated logic instead of untruncated logic, since the latter yields algorithms. Of course, sometimes one has to use truncated logic in subformulas in order to get the intended meaning, as in the statements of LEM and AC, but here I'm talking more about the overall structure of the statement: why should one formulate a statement as $\forall n\in\mathbb N.\, \exists m\in\mathbb N.\, P(m,n)$ if one can just as well construct a term of $\prod_{n\colon\mathbb N}\,\sum_{m\in\mathbb N}.\, P(m,n)$?)
4. Also quite unrelated to 1. and 2.: Theorem 8.10.1 in the HoTT book states that there is a $k$ such that for all $n\geq 3$, $\pi_{n+1}(\mathbb S^n)=\mathbb Z_k$. The proof doesn't use LEM and AC, but it uses univalence and higher inductive types. Now that there's stuff like cubical Agda, is it possible to execute the proof of Theorem 8.10.1? (I don't know whether cubical Agda yields a computational interpretation of both univalence and higher inductive types.) Are there other examples of theorems of this kind, possibly admitting completely new results of calculations of homotopy groups?

Tom de Jong (Aug 11 2021 at 11:05):

I haven't looked in detail at items 3 and 4 yet, but I can tell you that LEM and LEM' are equivalent. It will be a nice exercise to prove this yourself. (Hint: prove that $A + \lnot A$ is a proposition when $A$ is.)

Tom de Jong (Aug 11 2021 at 11:08):

RE Item 3: What if for every $x : X$ there are multiple (possibly infinitely many) $y : Y$ such that $P(x,y)$ holds? You're not always in the position where you can/want to make a choice. I'll try to think of some concrete examples.

Tom de Jong (Aug 11 2021 at 11:11):

RE Item 4: I'm not an expert on Cubical Agda, but it does support univalence and (most?) higher inductive types, certainly spheres. Since each $n$ has a unique $k$, you can actually prove the formulation with $\Sigma_{k}$ and Cubical Agda should be able to calculate it for each $n$ (giving enough time and memory). I don't think this has led to completely new results though, but someone else should know a lot more about that topic.

Reid Barton (Aug 11 2021 at 11:16):

In item 2, it sounds like you're talking about something more like (for example) Lean's type theory, which has a separate Prop with no computational content, and instead calls $\mathsf{isProp}$ subsingleton, and $||-||_{-1}$ trunc (constructed as the quotient by the always-true relation).

Reid Barton (Aug 11 2021 at 11:23):

For item 4, also see https://thehighergeometer.wordpress.com/2018/06/29/trying-to-compute-bruneries-number/

James Wood (Aug 11 2021 at 11:56):

There's a whole zoo of notions of irrelevance, and I don't think there's any alternative to studying each one carefully. There are h-props, as in HoTT, which say that all inhabitants are substitutable with each other. Then there are s-props (strict propositions), as in Lean and Agda's Prop and Coq's SProp, which have all open inhabitants identified, and only interact with computation by dismissing impossible cases. Additionally, there is erasure, where types can genuinely have multiple distinct closed inhabitants, but there is a guarantee that no information from them is needed when computing with closed terms (i.e, in a compiled program). If you want to preserve computational meaning, you first have to decide which notion of computation (open or closed) to preserve.

Leopold Schlicht (Aug 11 2021 at 14:35):

5. Is there another framework in which classical logic and constructive logic can coexist in the sense of question 2. (so that one can use LEM at the "mere" layer without destroying executability of proofs at the "pure" layer)?

Mike Shulman (Aug 11 2021 at 17:16):

Item 4 is one of the open problems in HoTT. In principle, we know that cubical type theories can compute the "Brunerie number", since it's been proven that they satisfy canonicity (and even normalization). But no one has yet managed to implement a cubical type theory and actually perform the computation using available time and memory constraints.

Mike Shulman (Aug 11 2021 at 17:18):

Leopold Schlicht said:

5. Is there another framework in which classical logic and constructive logic can coexist in the sense of question 2. (so that one can use LEM at the "mere" layer without destroying executability of proofs at the "pure" layer)?

One answer is that double-negation is a modality. Thus, you always can use LEM while "reasoning in that modality". Of course, the resulting logic won't interact with types quite the way you're used to, e.g. it won't satisfy function comprehension.

Mike Shulman (Aug 11 2021 at 17:21):

Re 3, it happens often that we want truncated logic when defining subobjects of a given object. For instance, in defining the dedekind reals we would get the wrong answer if we formulated the axioms of a cut using untruncated logic. Similarly, the classifying space $B\mathrm{Aut}(X)$ can be defined as $\sum_{Y:\mathcal{U}} \Vert X=Y\Vert$, whereas the untruncated version $\sum_{Y:\mathcal{U}} (X=Y)$ is contractible.

Mike Shulman (Aug 11 2021 at 17:21):

Another place where truncation is necessary is in formulating nonclassical continuity principles, although that's roughly similar to its usage in LEM and AC.

Tom de Jong (Aug 12 2021 at 07:14):

Re 3 again and similar to Mike Shulman's point above: Assuming univalence, the circle $\mathbb S^1$ satisfies $\Pi_{x,y : \mathbb S^1} \|x=y\|$ but not $\Pi_{x,y:\mathbb S^1} (x=y)$.

Leopold Schlicht (Aug 12 2021 at 08:58):

Thanks for all the answers! :-)