# How come identity encodes absurdity

From P5 in this paper: https://hal.inria.fr/hal-01094195/file/CIC.pdf

Using this purely functional part, it is possible to encode many int eresting notions. For instance ∀ C : Prop , C is a logical proposition (a term of type Prop ) which encodes absurdity ( ⊥ ) : there is no closed term of type ∀ C : Prop , C (so no proof of ⊥ without hypothesis) and also from a proof t of ∀ C : Prop , C one can build a proof t C of an arbitrary proposition C so the natural deduction rule for eliminating ⊥ is derivable in the logic.

where

$$\forall C: Prop, C$$

looks entirely identity function to me, which can definitely be inhabited by a closed term. Why the author said it encodes absurdity?

If I were to encode absurdity, I would do

$$\exists P: Prop, P \to \forall Q:Prop, Q$$

That is, there exists a proposition which derives everything. From category theoretic perspective, it's precisely how the initial object is defined, which can encode absurdity with no doubt.

Did I misread it in a terrible wrong way that the author was actually right? How about my encoding, does it make sense to you?

• Also note that your encoding of absurdity... actually encodes truth! Indeed, we can take $P$ to be $\forall Q:Prop.\ Q$ and prove the resulting trivial implication. Indeed, there does exist a proposition that derives everything: the false proposition! – chi Sep 22 '17 at 19:08
• @chi perfect. good to know i have reasons to learn. – Jason Hu Sep 22 '17 at 19:19

A proof of $\forall C : Prop, C$ is a function from an arbitrary proposition to its proof. Since a proposition isn't a proof, an identity function is not a function from propositions to proofs.
The identity function (or rather, a function returning the identity function on proofs of $C$) corresponds instead to the proof of $\forall C : Prop, C \to C$. That's even the example on the beginning of page 3!