Some explanations needed about Negation in Gentzen's Natural Deduction rules

cs.stackexchange https://cs.stackexchange.com/questions/101693

  •  05-11-2019
  •  | 
  •  

سؤال

I'm beginning to have an understanding thanks to some videos relating to "Proposition as Types". But, I don't come from a theoretical CS background, so maybe I'm blocked probably a bit by notation...

Given that I have understood, Conjunction, Disjunction, Implication,

I'm stumbling on Negation:

intro:
[A]
 /\
--- 
¬ A

elim:
A ¬A    /\
----   ---- .
 /\     D

It comes from an extract of the Gentzen paper during a P. Wadler talk Proposition as Types, and I'm stuck by the meaning of the symbol resembling /\. What is this symbol called, and what is the meaning ?

Moreover, I have no clue about that D (which was not introduced) and . in:

 /\
---- . 
 D

Is it anything related to _|_ bottom in Haskell, or else the Void empty type?

All those missing pieces makes me unable to grasp the meaning and how to apply these rules.

EDIT: I was also having difficulties with the Universal Introduction rule and this video covers the topic.

لا يوجد حل صحيح

مرخصة بموجب: CC-BY-SA مع الإسناد
لا تنتمي إلى cs.stackexchange
scroll top