# calculus of natural deduction

1. What is the most natural formulation (without contexts) of the $\leftrightarrow$-introduction? Maybe $\begin{array}{c} A\rightarrow B \quad B \rightarrow A\\ \hline\hline A\leftrightarrow B \end{array}$?

2. Why is not $A$ allowed to be dependent of a formula in which $x$ is a free variable (exception: $A$ is dependent of $\varphi(x)$) in the $\exists$-elimination-rule $\begin{array}{c} \exists x(\varphi(x)) \quad \varphi(x)\vdash A\\ \hline A \end{array}$?

$A\vdash B$ means the same as

$[A]$

$\ \ \vdots$

$\ B$

• If $A\vdash B$, $B\vdash A$, we say that $A\equiv B$. If $A\to B$, $B\to A$, we say $A\leftrightarrow B$. Is it what you mean? – Michael Galuza Jul 9 '15 at 11:54
• Yes. ------------------------------ – asdfusername Jul 9 '15 at 11:58

For 1) : NO. The "standard" approach with Natural Deduction is to use only one connective per rule :

$$\frac{\begin{array}{ccc} [A]&&[B]\\ \vdots&&\vdots\\ B&&A \end{array}}{A \leftrightarrow B}$$

Often, mainly for typoghrapical reasons, we may write it as :

$$\frac{\begin{array}{ccc} A \vdash B &&B \vdash A \end{array}}{A \leftrightarrow B}$$

but in this way we can "loose" the information about the discharge of the assumptions.

For 2), you have to recall the restriction :

$x$ is not free in $A$, or in a hypothesis of the subderivation of $A$, other than $\varphi(x)$,

and that, with the application of $\exists$-elim rule, you have to discharge the "temporary" assumption $\varphi(x)$.

Consider the following example :

1) $\exists x (x=0)$ --- premise

2) $x=0$ --- temporary assumption [a] for $\exists$-elim : it is the $\varphi(x)$ of the rule

3) $x=0$ --- from 2) : invalid ! it is the $A$ of the rule, but it has $x$ free, where $x$ is already free in $\varphi(x)$

4) $x=0$ --- from 1), 2) and 3) by $\exists$-elim, discharging [a]

5) $\forall x (x=0)$ --- from 4) by $\forall$-intro : no open assumptions with $x$ free.

Thus, we have derived the invalid :

$\exists x (x=0) \vdash \forall x(x=0)$.

Regarding the part of the proviso : $x$ is not free in a hypothesis of the subderivation of $A$, other than $\varphi(x)$, consider :

1) $\exists x (x=0)$ --- premise

2) $x=0$ --- assumed [a] for $\exists$-elim

3) $\exists x (x=1)$ --- premise

4) $x=1$ --- assumed [b] for $\exists$-elim

5) $x=0 \land x=1$ --- from 2) and 4) by $\land$-intro

6) $\exists x (x=0 \land x=1)$ --- from 5) by $\exists$-intro

7) $\exists x (x=0 \land x=1)$ --- from 1), 2) and 6) by $\exists$-elim, discharging [a] : invalid ! there is still the open assumption [b] with $x$ free in this sub-derivation.

Thus, we have derived the invalid :

$\exists x (x=0), \exists x (x=1) \vdash \exists x (x=0 \land x=1)$.

• And why is this more natural than $\begin{array}{c} A\rightarrow B \quad B \rightarrow A\\ \hline\hline A\leftrightarrow B \end{array}$ (except the fact that my rule is using another connective but that hasn't to do with natural or not)? – asdfusername Jul 9 '15 at 12:11
• @asdfusername - Peter Smith has already answered you in this post. – Mauro ALLEGRANZA Jul 9 '15 at 12:18
• No, he hasn't!! – asdfusername Jul 9 '15 at 12:21
• The argument "A rule should not contain more than one connective" is bullshit. In a natural deduction calculus one can alway use all the usual connectives. Otherwise it wouldn't be a natural deduction calculus. – asdfusername Jul 9 '15 at 12:25
• @asdfusername - This is not what the "founders" of Nat Ded thinked ... See e.g. Dag Prawitz, Natural Deduction : A Proof-Theoretical Study (1965), but of course you can stay with your own ideas, and define a bran new, "not bullshit", super-Natural Deduction system. – Mauro ALLEGRANZA Jul 9 '15 at 12:33