# David Corfield negative facts

nForum discussion

### Negative fact

From here

A fact … is taken to be some kind of existent in the world… . But … can it really be a fact in the world that there is no hippopotamus in the room? This sounds like an absence of a fact, and an absence is nothing at all. (2007, 46)

Form the dependent sum – ‘Hippopotamus in the room’, then its bracket type – ‘There is a hippo in the room’. Then [There is a hippo in the room, 0] = There is no hippo in the room, a perfectly good proposition. Taking $El$, this is ‘Fact that there is no hippo in the room’. So a term of this type is a function taking a witness of there being a hippo in the room to a term of the empty type. That doesn’t sound like an absence.

[Something like, a hippo being present in this room, then in view of sizes, I would see something if I scan the room as I have, but I dont.]

(Mike) A fact that there is no hippopotamus is not the absence of a fact. There’s no reason that “fact that not” should be the same as “not fact that”, any more than “proof that not” is the same as “not proof that”. A constructivist point of view may be helpful; saying that we can’t prove or assert something is not the same as saying that we can prove it false or deny it. And as you pointed out, the type-theoretic perspective bears that out; a “fact than not” is a real thing, a reason why the truth of such a statement would be contradictory. (One might also bring in the occasional constructive necessity for “positive” versions of facts that are classically negative, e.g. apartness.)

### Conditional fact

Negative facts taken constructively are conditional facts, $A \to B$, the fact that $A$ implies $B$.

Is ${\Vert A \Vert} \to {\Vert B\Vert}$ the same as $\Vert A\to B\Vert$? And in general, I’m pretty sure the answer is no, although I don’t have a counterexample off the top of my head. However, it is true if $B$ is already a proposition (such as $0$), since in that case we have ${\Vert B \Vert} = B$ and ${\Vert A\to B\Vert} = (A \to B)$, and the universal property of truncation $({\Vert A\Vert} \to B) = (A\to B)$.

$({\Vert A \Vert} \to {\Vert B \Vert}) = {\Vert A\to B\Vert}$ is equivalent to the propositional axiom of choice, ${\Vert ({\Vert A\Vert} \to A)\Vert}$. In particular, it is implied by LEM, hence holds in $\infty Gpd$ and any slice of it; but it fails for instance if the world’s simplest AC fails.

Last revised on April 16, 2021 at 05:48:26. See the history of this page for a list of all contributions to it.