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.

$\endgroup$
  • $\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$ – Aristu Dec 17 '18 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 Dec 18 '18 at 23:00
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.

$\endgroup$
  • 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 Dec 17 '18 at 22:02
  • $\begingroup$ @StephaneRolland I've edited my answer to address what I think is your first rule $\endgroup$ – Aristu Dec 18 '18 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 Dec 18 '18 at 7:20
  • 1
    $\begingroup$ Glad I could be of help $\endgroup$ – Aristu Dec 18 '18 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 Dec 19 '18 at 2:08

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.