27
$\begingroup$

I am looking for a closed statement (i.e. not depending on any parameter objects) which is true in the internal logic of the topos of simplicial sets, but is not an intuitionistic tautology. Ideally, I would like it to be a simple universal statement of propositional logic (e.g. "for all propositions P, Q, and R, blah blah", like LEM or de Morgan's law).

(To clarify: this has nothing to do with higher topoi or homotopy type theory; it's purely a question about ordinary 1-categorical 1-topos theory.)

$\endgroup$
  • $\begingroup$ My guess is that any purely propositional statement true in this topos will be an intuitionist tautology. Perhaps Markov's principle will meet your needs? (See en.wikipedia.org/wiki/Markov's_principle.) It is so close to being an intuitionist tautology that it probably holds in this topos, though I don't know the topos well enough to check easily. Translating to find out what the principle says about simplicial sets would be interesting. $\endgroup$ – Matt F. Mar 11 '14 at 3:32
  • $\begingroup$ What objects may I refer to? $\endgroup$ – Andrej Bauer Mar 11 '14 at 6:02
  • 1
    $\begingroup$ @MattF. Markov's principle indeed holds in $\mathbf{sSet}$ (assuming the ambient logic is classical): the natural numbers object is basically a copy of the usual natural numbers, and its subobjects are precisely the subsets in the usual sense. Similarly, $\mathbf{sSet}$ satisfies countable choice (if the ambient logic does). $\endgroup$ – Zhen Lin Mar 11 '14 at 9:15
  • 1
    $\begingroup$ The only subobjects of 1 are 0 and 1, up to isomorphism, so I think a suitable form of LEM should hold. $\endgroup$ – aws Mar 11 '14 at 9:20
  • 2
    $\begingroup$ @aws LEM holds for the closed terms in the language of Heyting algebras... but that's a triviality. Note that $\mathbf{sSet}$ is not a boolean topos. $\endgroup$ – Zhen Lin Mar 11 '14 at 18:00
26
$\begingroup$

Short answer: the Kreisel-Putnam axiom $(\lnot p \to (q \lor r)) \to ((\lnot p \to q) \lor (\lnot p \to r))$ is not an intuitionistic tautology but it is valid for any subobjects of an object in the topos of simplicial sets.

The longer answer relies on an interesting characterization of the subobject classifier $\Omega$ of the topos of simplicial sets. (Thanks to Zhen Lin for helping me explain this characterization.) Sieves on $[n]$ in $\Delta$ can be identified with (possibly empty) abstract simplicial complexes $A$ with vertices drawn from $[n] = \{0,\ldots,n\}$. The sieve corresponding to $A$ consists of all order preserving maps $f:[m]\to[n]$ such that $\{f(0),\dots,f(m)\} \in A$. So, for each $n$, $\Omega(n)$ can be identified with the set of all such abstract simplicial complexes and for $g:[m]\to[n]$, $\Omega(g):\Omega(n)\to\Omega(m)$ takes each $A \in \Omega(n)$ to $B = \{x \subseteq [m] : \{g(i) \mid i \in x\} \in A\}$.

Interestingly, the lattice of abstract simplicial complexes on $[n]$ (with intersection and union) is the free distributive lattice $D_{n+1}$ on $n+1$ generators with a free top element (but no free bottom element though it still has a bottom element). Every finite bounded distributive lattice is a Heyting algebra by defining implication via $$(p \to q) \equiv \bigvee \{r \mid p \land r \leq q\},$$ where the big join makes sense since there are only finitely many possibilities for $r$. The logical operators $\land,\lor,\to:\Omega\times\Omega\to\Omega$ can be computed pointwise using the Heyting algebra structure of $D_{n+1}$. In other words, ${\land}(n):\Omega(n)\times\Omega(n)\to\Omega(n)$ takes each pair of abstract simplicial complexes $A_n,B_n$ on $[n]$ to $A_n \cap B_n$, and similarly for $\lor$ and $\to$. Thus any propositional formula which is true in $D_{n+1}$ for every $n$ will be valid for generalized truth values in the topos of simplicial sets. I don't know a simple characterization of this logic but it at least satisfies the Kreisel-Putnam axiom.

To verify the Kreisel-Putnam axiom in $D_{n+1}$, suppose $P$, $Q$, $R$ are abstract simplicial complexes over $[n]$. Note that $\lnot P$ consists of all nonempty $x \subseteq [n]$ that are disjoint from every element of $P$. If nonempty, which is the interesting case, this simplicial complex has a maximal element that I will denote $z$. Now $\lnot P \to (Q \lor R)$ consists of all $x \subseteq [n]$ such that $x \cap z \in Q \cup R$. Since $\lnot P \to Q$ (resp. $\lnot P \to R$) similarly consist of all $x \subseteq [n]$ such that $x \cap z \in Q$ (resp. $x \cap z \in R$), we see that $\lnot P \to (Q \lor R)$ and $(\lnot P \to Q) \lor (\lnot P \to R)$ correspond to the same abstract simplicial complexes.

$\endgroup$
  • $\begingroup$ I'm slightly confused by your statement about sieves. Surely what you mean is that a sieve on $[n]$ can be identified with an abstract simplicial complex with vertices drawn from $\{ 0, \ldots, n \}$? $\endgroup$ – Zhen Lin Mar 11 '14 at 18:25
  • $\begingroup$ No, what I meant was that an $n$-simplex of $\Omega$ (= generalised element of $\Omega$ with domain of variation $\Delta^n$) is a sieve on $[n]$, hence can be identified with etc.; in particular global elements of $\Omega$ are just sieves on $[0]$. I'm not sure what you mean by "element of $\Omega$" without qualification. $\endgroup$ – Zhen Lin Mar 11 '14 at 18:36
  • $\begingroup$ @ZhenLin: Right, I wasn't giving a full characterization of $\Omega$ since I also left out the functoriality conditions. Sorry for the confusion. Feel free to suggest better wording. $\endgroup$ – François G. Dorais Mar 11 '14 at 18:45
  • 1
    $\begingroup$ @FrançoisG.Dorais I think I agree with everything now, except for the claim that $\Omega (n)$ is a free distributive lattice. By my count, $\Omega (0)$ has 2 elements, $\Omega (1)$ has 5 elements, and $\Omega (2)$ has 19 elements. This is one less than what OEIS says free distributive lattices should have. $\endgroup$ – Zhen Lin Mar 11 '14 at 23:01
  • 1
    $\begingroup$ @ZhenLin: You're right! There is a free top but no free bottom. So it's the free distributive lattice with a free top or the free bounded distributive lattice without the free bottom. So the count is off by one whichever way you think about it... $\endgroup$ – François G. Dorais Mar 11 '14 at 23:08
9
$\begingroup$

Francois's answer is exactly what I was looking for. I just want to record a different proof of the same fact, that the Kreisel-Putnam axiom $(\neg p \Rightarrow (q\vee r)) \Rightarrow ((\neg p \Rightarrow q) \vee (\neg p \Rightarrow r))$ holds in $\mathbf{sSet}$.

First note that for simplicial subsets $A,B\subseteq X$, the Heyting implication $(A\Rightarrow B)\subseteq X$ is (of course) the largest simplicial subset of $X$ whose intersection with $A$ is contained in $B$, and that this admits the following inductive description: an $n$-simplex of $X$ lies in $A\Rightarrow B$ iff (1) all of its faces lie in $(A\Rightarrow B)_{n-1}$ and (2) it is either in $B_n$ or not in $A_n$. (When $n=0$ the first condition is vacuous, so $(A\Rightarrow B)_0 = (X_0 \setminus A_0)\cup B_0$.)

In particular, $(\neg A)_n$ consists of the $n$-simplices of $X$ all of whose faces lie in $(\neg A)_{n-1}$ and which are not in $A_n$. But since $A$ is a simplicial subset, if $n>0$ the second condition is implied by the first: if all (indeed, any) of the faces of an $n$-simplex lie in $\neg A$, they do not lie in $A$, and so the $n$-simplex cannot be in $A$ either. Thus, $\neg A$ is the full simplicial subset on the vertices of $X$ not in $A$; "full" means that it contains a simplex as soon as it contains its vertices.

Now I claim that $(A\Rightarrow (Q\cup R)) = ((A\Rightarrow Q) \cup (A\rightarrow R))$ holds whenever $A$ is full (hence in particular when $A=\neg P$). It suffices to show the left-to-right containment. Since this is certainly true on 0-simplices, we inductively assume it true on $(n-1)$-simplices, and let $x\in (A\Rightarrow (Q\cup R)_n$. By assumption either $x\in Q_n$ or $x\in R_n$ or $x\notin A_n$. The first two cases are trivial, so suppose $x\notin A_n$.

Since $A$ is full, $x\notin A_n$ means that some vertex $v$ of $x$ is not in $A$. By induction, the unique $(n-1)$-dimensional face of $x$ not containing $v$, call it $y$, must be either in $A\Rightarrow Q$ or $A\Rightarrow R$; WLOG say it is in $A\Rightarrow Q$.

Now we can prove by induction on $k$ that every $k$-dimensional face of $x$ is also in $A\Rightarrow Q$. Any such face must either be a face of $y$, in which case it is in $A\Rightarrow Q$ since $y$ is, or else contain $v$. In the latter case, it cannot be in $A$ since $v$ is not in $A$, so it is in $A\Rightarrow Q$ as soon as all its faces are, and this follows by the inductive hypothesis. Therefore, every face of $x$ is in $A\Rightarrow Q$, hence so is $x$.

$\endgroup$
9
$\begingroup$

I will augment François Dorais’s answer with an exact identification of the propositional logic.

Let $D_n$ be the free distributive lattice with a top, considered as a finite Heyting algebra. Algebras are a nuisance to work with, so let us compute the dual Kripke frame $F_n$, which validates the same formulas, but is much smaller and simpler. Since we are dealing with a finite algebra, the elements of $F_n$ are just the $\lor$-irreducible (which entails $\bot$-irreducible, i.e., nonzero) elements of $D_n$, ordered upside down.

If $\{x_i:i\in[n]\}$ is the set of free generators, each element of $D_n$ can be written in a disjunctive normal form $$a=\bigvee_{i\in I}\bigwedge_{j\in J_i}x_j,$$ where $J_i\subseteq[n]$, $I\ne\varnothing$, and $\{J_i:i\in I\}$ is an antichain. Clearly, if $a$ is $\lor$-irreducible, we must have $|I|=1$, thus $a$ is of the form $$a_J=\bigwedge_{j\in J}x_j$$ for some $J\subseteq[n]$. Moreover, we must have $J\ne[n]$ so that $a_J\ne\bot$. Conversely, it is not difficult to check that all $a_J$ with $J\ne[n]$ are indeed $\lor$-irreducible. Since $$a_J\le a_{J'}\iff J\supseteq J',$$ $F_n$ is just the powerset Boolean algebra without top: $$F_n\simeq\langle\mathcal P([n])\smallsetminus\{[n]\},{\subseteq}\rangle.$$ These Kripke frames are known as Medvedev frames, and the logic defined by $\{F_n:n\in\mathbb N\}$ is Medvedev’s logic (aka logic of finite problems), denoted LM or ML, based on Medvedev [1]. See e.g. Chagrov&Zakharyaschev [2,§2.9]. Thus, the logic of $\{D_n:n\in\mathbb N\}$ is also Medvedev’s logic.

Despite its seemingly simple definition, this logic is shrouded in mystery: it is particularly scandalous that half a century after its discovery, it is still an open problem if the logic is recursively axiomatizable. Let me just mention that apart from the Kreisel–Putnam axiom $$(\neg p\to q\lor r)\to(\neg p\to q)\lor(\neg p\to r),$$ Medvedev’s logic is also known to include Scott’s axiom $$((\neg\neg p\to p)\to p\lor\neg p)\to\neg\neg p\lor\neg p,$$ and an axiom identified by Andrews (reported in Gabbay [3]), which in fact implies both the Kreisel–Putnam and Scott axioms: $$((\neg p\to q)\to r\lor s)\to(p\to r)\lor(q\to s).$$ On the other hand, Medvedev’s logic is included in the logic of weak excluded middle $\mathrm{KC}=\mathrm{IPC}+(\neg p\lor\neg\neg p)$.

Medvedev’s logic has many interesting properties. In particular, it is the largest logic with the disjunction property that extends Kreisel–Putnam logic (Levin [4], Maksimova [5], cf. [2,Thm. 15.18]), and it is the only known superintuitionistic logic that simultaneously has the disjunction property and is structurally complete (Prucnal [6,7]).

References:

[1] Yuriĭ T. Medvedev: Finite problems. Doklady Akademii Nauk SSSR 142 (1962), no. 5, pp. 1015–1018, http://mi.mathnet.ru/eng/dan26117 (in Russian). English translation: Soviet Mathematics, Doklady 3 (1962), pp. 227–230.

[2] Alexander Chagrov and Michael Zakharyaschev: Modal logic. Oxford Logic Guides vol. 35, Oxford University Press, 1997.

[3] Dov Gabbay: Semantical investigations in Heyting’s intuitionistic logic. Synthese Library vol. 148, Springer, 1981, doi: 10.1007/978-94-017-2977-2.

[4] Leonid A. Levin: Some syntactic theorems on the calculus of finite problems of Yu. T. Medvedev. Doklady Akademii Nauk SSSR 185 (1969), no. 1, pp. 32–33, http://mi.mathnet.ru/eng/dan34473 (in Russian). English translation: Soviet Mathematics, Doklady 10 (1969), 288–290.

[5] Larisa L. Maksimova: On maximal intermediate logics with the disjunction property. Studia Logica 45 (1986), no. 1, pp. 69–75, doi: BF01881550.

[6] Tadeusz Prucnal: Structural completeness of Medvedev’s propositional calculus. Reports on Mathematical Logic 6 (1976), pp. 103–105.

[7] Tadeusz Prucnal: On two problems of Harvey Friedman. Studia Logica 38 (1979), no. 3, pp. 247–262, doi: 10.1007/BF00405383.

$\endgroup$
  • $\begingroup$ Can you recommend some sort of survey on this Medvedev logic? Or perhaps a metareference which would include references to the various facts you mentioned? I would love to know more. $\endgroup$ – Gro-Tsen Apr 5 at 22:11
  • 1
    $\begingroup$ @Gro-Tsen I don’t know of a survey. There is some information in Chagrov and Zakharyaschev (spread throughout the book, which unfortunately does not have a good index), and anyway, I included a few references in the answer. $\endgroup$ – Emil Jeřábek Apr 8 at 14:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.