Why no morphisms from the contradictory proposition to the inconsistent context? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-22T13:31:28Z http://mathoverflow.net/feeds/question/88380 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/88380/why-no-morphisms-from-the-contradictory-proposition-to-the-inconsistent-context Why no morphisms from the contradictory proposition to the inconsistent context? Russell O'Connor 2012-02-13T21:44:41Z 2012-02-14T07:24:59Z <p>Consider Higher order predicate logic over dependent type theory (DPL) as defined in Chapter 11 of B. Jacobs's book "Categorical Logic and Type Theory" (though I think this question applies to first-order predicate logic too).</p> <p>In the category $\mathbb{P}$ of propositions-in-dependent-type-contexts, an object is a well formed proposition $\Gamma \vdash \varphi:Prop$ and a morphism $(\Gamma \vdash \varphi:Prop) \rightarrow (\Delta \vdash \psi : Prop)$ consists of a context morphism $\vec{M} : \Gamma \rightarrow \Delta$ such that $\Gamma | \varphi \vdash \phi(\vec{M})$ is derivable. This category $\mathbb{P}$ is fibred over the category of dependent type contexts $\mathbb{C}$ via $(\Gamma \vdash \varphi:Prop) \mapsto \Gamma$.</p> <p>Consider the "contradictory proposition" object, $A$, in $\mathbb{P}$ which I define as $\emptyset \vdash \perp : Prop$ and the "inconsistent context" object, $B$, which I define as $x : 0 \vdash \top:Prop$ (where $0$ is the empty type).</p> <p>I would expect $A$ and $B$ to be isomorphic in $\mathbb{P}$ since both objects seems equally void to me in the sense that neither appear to have any models, i.e. there are no morphisms from the terminal object, $1 := \emptyset \vdash \top : Prop$, to either $A$ or $B$. But, of course, $A$ and $B$ cannot be isomorphic since a morphism from $A$ to $B$ entails the existence of a context morphism $M : \emptyset \rightarrow x : 0$ which would imply that the void type is inhabited.</p> <p>Can someone assuage my concerns about $A$ and $B$ being equally void yet not isomorphic?</p> http://mathoverflow.net/questions/88380/why-no-morphisms-from-the-contradictory-proposition-to-the-inconsistent-context/88391#88391 Answer by Ulrik Buchholtz for Why no morphisms from the contradictory proposition to the inconsistent context? Ulrik Buchholtz 2012-02-14T00:36:08Z 2012-02-14T00:36:08Z <p>I'm not sure what you mean by the individual propositional objects having models or not.</p> <p>In any case, as you said, as morphism in $\mathbb P$ simply <em>is</em> a context morphism compatible with the preordering. So $A$ and $B$ are definitely not isomorphic in $\mathbb P$. In a model, $A$ is the initial subobject of the terminal object, while $B$ is the terminal subobject of the initial object (taking models in subobject fibrations for simplicity), and an isomorphism of these subobjects would restrict to an isomorphism of the initial object with the terminal object.</p> http://mathoverflow.net/questions/88380/why-no-morphisms-from-the-contradictory-proposition-to-the-inconsistent-context/88407#88407 Answer by Andrej Bauer for Why no morphisms from the contradictory proposition to the inconsistent context? Andrej Bauer 2012-02-14T07:24:59Z 2012-02-14T07:24:59Z <p>My understanding of the situation is that you have to correctly understand what the morphisms do. A geometric picture might be helpful.</p> <p>Let us interpret a context $\Gamma = x_1 : A_1, \ldots, x_n : A_n$ as a cartesian product $|\Gamma|$ of topological spaces. A proposition in a context $\Gamma \vdash \phi$ is interpreted as a subspace of a cartesian product $|\phi| \subseteq |\Gamma|$. I think the confusion arises if you think of a morphism $M : (\Gamma \vdash \phi) \to (\Delta \vdash \psi)$ as a continuous map $|\phi| \to |\psi|$, which it is <em>not</em>. It is an <em>ambient</em> map, i.e, a continuous map $|\Gamma| \to |\Delta|$ which also happens to map $|\phi| \to |\psi|$. Now it is clear that even though $|\phi|$ and $|\psi|$ may be homeomorphic as spaces, the may be embedded in $|\Gamma|$ and $|\Delta|$ in wildly different way (the wild Cantor sets come to mind), so it won't be possible to extend a homeomorphism between them to an ambient map.</p> <p>In your example, we are comparing $\emptyset$ as a subspace of $\emptyset$ versus $\emptyset$ as a subspace of $1$. Even though the two empty subspaces are homeomorphic, there is no ambient map taking the latter to the former.</p>