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$ Feb 4 '14 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$ Feb 4 '14 at 16:56
  • $\begingroup$ For the tutorial of this site, see the guideline $\endgroup$ Feb 4 '14 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$ Feb 4 '14 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$ Feb 4 '14 at 20:21

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.


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.