Description

• Title:
  Does the Implication Elimination Rule Need a Minor Premise?
• Creator:
  Francez, Nissim
• Description:
  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.
• Object availability:
  free access
• Rights:
  Prawa autorskie (c) 2017 Logic and Logical Philosophy
• Date:
  2017.07.21
• Type:
  info:eu-repo/semantics/article;
  info:eu-repo/semantics/publishedVersion
• Language:
  English
• Source:
  Logic and Logical Philosophy; Vol. 27 No. 3 (2018): September; 351-373;
  Logic and Logical Philosophy; Tom 27 Nr 3 (2018): September; 351-373;
  2300-9802;
  1425-3305
• Format:
  application/pdf
• Publisher:
  Uniwersytet Mikołaja Kopernika w Toruniu
• Relation: https://apcz.umk.pl/LLP/article/view/LLP.2017.019/12527
• Subject:
  natural deduction;
  NJ;
  proof-theoretic semantics;
  grounds for assertion;
  term assignment;
  03A99
• Identifier: https://apcz.umk.pl/LLP/article/view/LLP.2017.019
• Data provider:
  Akademicka Platforma Czasopism
• Can I use it?:
  seek permission
• Type:
  text