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
/\ ---- . 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.