1
$\begingroup$

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.

Improve this question
$\endgroup$
2
  • $\begingroup$ Hello, cs.stackexchange supports MathJax, so you can type the inferences rules in a more readable manner, take a look at answer here for some examples on how it could look like. $\endgroup$
    – Schonfinkel
    Commented Dec 17, 2018 at 21:25
  • 1
    $\begingroup$ As a side note, the symbol that appears in the slides ($\curlywedge$) is the one originally used by Gentzen in the thirties. We now mostly use $\bot$, as in Aristu's answer. $\endgroup$
    – cody
    Commented Dec 18, 2018 at 23:00

1 Answer 1

Reset to default
1
$\begingroup$

I'm guessing your first rule is:

\begin{align*} &[A]\\ &~~\vdots\\ &~\bot\\ &\overline{\lnot A}\qquad (I\lnot) \end{align*}

This means that in order to derive $\lnot A$ one must first assume $A$ (that is $[A]$) and derive a contradiction ($\bot$), the dots between mean a finite number of steps.

$$ \frac{A \quad \lnot A}{D} \qquad (E\lnot) $$

This latter rule with $D$ seems to be ex falso quodlibet, since:

$$ \frac{A \quad \lnot A}{\bot} \qquad (E\lnot) $$

therefore:

$$ \frac{\bot}{D} $$

it says that you can derive anything (some $D$) from a contradiction.

Those $(I\circ)$ and $(E\circ)$, where $\circ$ is some operation mean Introduction-Elimination rules. In Gentzen's formulations all rules come in pairs.

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ With what you say, I now think the first introduction rule can be read as: if assuming A we get bottom _|_ , then A is False. Your statement about the elimination rule is powerful... That: if we take something False as input, we can conclude whatever... It's powerful as a conclusion. $\endgroup$
    – Stephane Rolland
    Commented Dec 17, 2018 at 22:02
  • $\begingroup$ @StephaneRolland I've edited my answer to address what I think is your first rule $\endgroup$
    – Schonfinkel
    Commented Dec 18, 2018 at 1:09
  • $\begingroup$ Exactly. But I see it now as : cannot provide an evidence for the proof, rather than contradiction in saying it is false. The Void type for expressing the idea of contradiction seems (now) clearer for me: there are no value encoding the existence of the proof. $\endgroup$
    – Stephane Rolland
    Commented Dec 18, 2018 at 7:20
  • 1
    $\begingroup$ Glad I could be of help $\endgroup$
    – Schonfinkel
    Commented Dec 18, 2018 at 15:31
  • 1
    $\begingroup$ @Aristu $\bot$ is a symbol commonly used for the bottom element of a lattice or, more generally, a partial order. Falsity is the bottom element of the lattice of truth values, while in denotational semantics (particularly using domain theory) the diverging computation is the bottom element of the information ordering. Diverging computations don't correspond to contradictions. They are not even at the same level in that a contradiction is a kind of formula while program (diverging or otherwise) corresponds to a proof. $\endgroup$
    – Derek Elkins left SE
    Commented Dec 19, 2018 at 2:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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