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.