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


$ \ \ \vdots$

$ \ B$

  • $\begingroup$ 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? $\endgroup$ – Michael Galuza Jul 9 '15 at 11:54
  • $\begingroup$ Yes. ------------------------------ $\endgroup$ – 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)$.

  • $\begingroup$ 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)? $\endgroup$ – asdfusername Jul 9 '15 at 12:11
  • $\begingroup$ @asdfusername - Peter Smith has already answered you in this post. $\endgroup$ – Mauro ALLEGRANZA Jul 9 '15 at 12:18
  • $\begingroup$ No, he hasn't!! $\endgroup$ – asdfusername Jul 9 '15 at 12:21
  • $\begingroup$ 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. $\endgroup$ – asdfusername Jul 9 '15 at 12:25
  • 1
    $\begingroup$ @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. $\endgroup$ – Mauro ALLEGRANZA Jul 9 '15 at 12:33

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.