@article{Francez_2017, title={Does the Implication Elimination Rule Need a Minor Premise?}, volume={27}, url={https://apcz.umk.pl/LLP/article/view/LLP.2017.019}, DOI={10.12775/LLP.2017.019}, abstractNote={<p>The paper introduces NJ g , a variant of Gentzen’s NJ natural deduction system, in which the implication elimination rule has no minor premise. The NJ g -systems extends traditional ND-system with a new kind of action in derivations, assumption incorporation, a kind of dual to the assumption discharge action. As a result, the implication (I/E)-rules are invertible and, almost by definition, harmonious and stable, a major condition imposed by proof-theoretic semantics on ND-systems to qualify as meaning-conferring. There is also a proof-term assignment to NJ g -derivations, materialising the Curry-Howard correspondence for this system.</p>}, number={3}, journal={Logic and Logical Philosophy}, author={Francez, Nissim}, year={2017}, month={Jul.}, pages={351–373} }