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.


$$ \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?

  • 2
    $\begingroup$ 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! $\endgroup$
    – chi
    Sep 22 '17 at 19:08
  • $\begingroup$ @chi perfect. good to know i have reasons to learn. $\endgroup$
    – Jason Hu
    Sep 22 '17 at 19:19

looks entirely identity function to me, which can definitely be inhabited by a closed term

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!

  • $\begingroup$ you are right. i should sleep good before reading things. $\endgroup$
    – Jason Hu
    Sep 21 '17 at 21:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.