Definition: A deduction is in normal form if there is no formula which is a conclusion of an introduction rule and the main premise of the elimination rule of the same connective.

So, in a natural deduction system, one can normalize a proof that contains an introduction rule of a connective followed right after by the elimination rule of the same connective. Here, I have the opposite. First two elimination rules and then the introduction rule of the same connective.


By this definition, the above deduction is in normal form. But still, it can be reduced to a simpler deduction (the trivial A∧B). It seems correct to me, that we can reduce it to just the axiom $A\wedge B$. But how, since the structure of the deduction doesn't have a pair of rules that could be eliminated?

For whoever cannot see the image on the post, I'll give a description of the deduction depicted in it.

(1): $A\wedge B\vdash A$ (by conjunction elimination)

(2): $A\wedge B\vdash B$ (by conjunction elimination, again)

(3): $A, B\vdash A\wedge B$ (by conjunction introduction on (1) and (2))

  • $\begingroup$ I'm not able to read the link. It is much easier for the "potential answerers" if you type in the formulas. $\endgroup$ Commented Feb 4, 2014 at 16:26
  • $\begingroup$ You can download Latex symbols from the web for the symbols, used the tutorial of this site and last (without saving) edit a question/answer with the formula you need and copy them ... $\endgroup$ Commented Feb 4, 2014 at 16:56
  • $\begingroup$ For the tutorial of this site, see the guideline $\endgroup$ Commented Feb 4, 2014 at 17:13
  • $\begingroup$ I think that (3) is wrong; it must be like : $A, B \vdash A \land B$. If your tree is made by two branch: the first one ending with (1) and the second one with (2), and after them you use again (with $A$ and $B$ as premisses) $\land$-I, why you need it ? Of course, we must see what we have on top of (1) and (2), but if what you need is really $A \land B$ and you have already on branch (1), I think you can use that only... $\endgroup$ Commented Feb 4, 2014 at 17:57
  • $\begingroup$ Now I read it - simply "cut" the right branch (for example) and avoid the "detour" from $A \land B$ to $A \land B$ through $A$. $\endgroup$ Commented Feb 4, 2014 at 20:21

1 Answer 1


By the Curry-Howard isomorphism, the deduction in question corresponds exactly to an $\eta$-reduction of $\lambda$-calculus.

Unfortunately, the books for proof theory that I have, don't mention this class of reduction rules.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .