A Note on Harmony |
| |
Authors: | Nissim Francez Roy Dyckhoff |
| |
Institution: | 1.The Technion,Department of Computer Science,Haifa,Israel;2.School of Computer Science,University of St Andrews,Scotland,UK |
| |
Abstract: | In the proof-theoretic semantics approach to meaning, harmony, requiring a balance between introduction-rules (I-rules) and elimination rules (E-rules) within a meaning conferring natural-deduction
proof-system, is a central notion. In this paper, we consider two notions of harmony that were proposed in the literature:
1. GE-harmony, requiring a certain form of the E-rules, given the form of the I-rules. 2. Local intrinsic harmony: imposes the existence of certain transformations of derivations, known as reduction and expansion. We propose a construction of the E-rules (in GE-form) from given I-rules, and prove that the constructed rules satisfy also local intrinsic harmony.
The construction is based on a classification of I-rules, and constitute an implementation to Gentzen’s (and Pawitz’) remark,
that E-rules can be “read off” I-rules. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|