Skip to main content
3 of 10
fixed after Zhen Lin's comment
François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233

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 in the topos of simplicial sets.

The longer answer relies on an interesting characterization of the subobject classifier of the topos sSet. Elements of $\Omega$ can be identified with sequences $(S_n)$ where each $S_n$ is a (possibly empty) abstract simplicial complex with vertices drawn from $[n] = \{0,\ldots,n\}$. (The sieve corresponding to $S_n$ consists of all order preserving maps $f:[m]\to[n]$ such that $\{f(0),\dots,f(m)\} \in S_n$.) Meets and joins are just coordinatewise intersections and unions. One can then define implication via $$p \to q \equiv \bigvee\{ r \mid p \land r \leq q\},$$ where the big disjuction makes sense since, for each coordinate, there are only finitely many choices of abstract simplicial complexes on $[n]$.

Interestingly, the lattice of abstract simplicial complexes on $[n]$ is the free bounded distributive lattice $D_{n+1}$ on $n+1$ generators. Every finite bounded distributive lattice is a Heyting algebra for the reason explained above. Thus the propositional tautologies in sSet are precisely those that are valid in all $D_{n+1}$, seen as Heyting algebras. I don't know a simple characterization of all such tautologies.

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 $x \subseteq [n]$ that are disjoint from every element of $P$. If nonempty (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.

François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233