Relevant harmony

被引:3
作者
Francez, Nissim [1 ]
机构
[1] Technion Israel Inst Technol, Dept Comp Sci, IL-32000 Haifa, Israel
关键词
Relevant logic; derivation-composition; harmony; stability; proof-theoretic semantics;
D O I
10.1093/logcom/ext026
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
After reviewing the basic definitions of harmony and stability, two of the central concepts in Proof-Theoretic Semantics, the paper considers the implicational fragment of the relevant logic R (Anderson&Belnap), under a labelled natural deduction (ND) system, where the labels keep track of 'use' of assumptions. Thereby, no assumption is discharged that has not been used. It is shown that the ND is not closed under composition of derivations using its standard definition, thereby prohibiting Prawitz's detour removal reductions, hence failing harmony. Arevised definition of derivation composition is proposed, under which the ND system *is* closed, allowing reductions and reenabling harmony (and stability).
引用
收藏
页码:235 / 245
页数:11
相关论文
共 17 条
[1]  
[Anonymous], ELECT NOTES THEORETI
[2]  
[Anonymous], 1975, ENTAILMENT
[3]  
Belnap Nuel., 1962, Analysis, V22, P130, DOI DOI 10.1093/ANALYS/22.6.130
[4]   A modal analysis of staged computation [J].
Davies, R ;
Pfenning, F .
JOURNAL OF THE ACM, 2001, 48 (03) :555-604
[5]  
Dummett MA., 1991, LOGICAL BASIS METAPH
[6]  
Hindley J. R., 1997, BASIC SIMPLE TYPE TH
[7]  
Mares E. D., 2004, Relevant Logic: A Philosophical Interpretation
[8]   Relevance and Conjunction [J].
Mares, Edwin D. .
JOURNAL OF LOGIC AND COMPUTATION, 2012, 22 (01) :7-21
[9]  
Momigliano A., 2002, ACM T COMPUT LOG, V3, P1
[10]  
Pfenning F., 2001, Mathematical Structures in Computer Science, V11, P511, DOI 10.1017/S0960129501003322