Tonk-A Full Mathematical Solution
Tonk-A Full Mathematical Solution
复制标题
Tonk-完整的数学解决方案
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
A. Avron
中科院分区：
文献类型：
--
作者：
A. Avron
从[12]开始，有一个很长的传统（例如[9，10]），根据这个传统，连接词的意义是由与之相关的引入和消除规则决定的。这一论点的支持者通常想到某种理想类型的自然演绎系统（在下面的第3节中解释）。不幸的是，处理经典否定已经需要不属于那种类型的规则。这个问题可以在多结论Gentzen型系统（也是在[12]中首次引入）的框架中解决，其中代替引入和消除规则的是左引入规则和右引入规则。连接词的意义是由其引入（和消除）规则给出的论点受到了Prior在[13]中的强烈挑战。在那篇论文中，他介绍了他著名的“连接词”Tonk（下面用T表示）。这个“连接词”有两个理想类型的规则。引入规则允许从φ推断φT。消元法则允许从φT <$推导出<$。在Tonk的存在下，每一个公式都可以从任何其他公式推导出来，使得由任何包括这个“连接符”的系统所“定义”的“逻辑”变得微不足道。普赖尔的论文已经清楚地表明，并不是每一个“理想的”引入和消除规则的组合都可以用来定义一个连接词。应该对这套规则施加一些限制。贝尔纳普在他著名的[6]中确实提出了这样一个约束：连接符的规则应该是保守的，在这个意义上，如果T φ可以使用它们导出，并且T φ中不出现连接符，那么T φ也可以不使用连接符的规则导出。这种解决Tonk问题的方法至少有两个问题：
There is a long tradition (See e.g. [9, 10]) starting from [12], according to which the meaning of a connective is determined by the introduction and elimination rules which are associated with it. The supporters of this thesis usually have in mind natural deduction systems of a certain ideal type (explained in Section 3 below). Unfortunately, already the handling of classical negation requires rules which are not of that type. This problem can be solved in the framework of multiple-conclusion Gentzen-type systems (also first introduced in [12]), where instead of introduction and elimination rules there are left introduction rules and right introduction rules. The thesis according to which the meaning of a connective is given by its introduction (and elimination) rules was strongly challenged by Prior in [13]. In that paper he introduced his famous “connective” Tonk (denoted below by T ). This “connective” has two rules of the ideal type. The introduction rule allows to infer φTψ from φ. The elimination rule allows to infer ψ from φTψ. In the presence of Tonk every formula can be derived from any other formula, making trivial the “logic” which is “defined” by any system which includes this “connective”. Prior’s paper has made it clear that not every combination of “ideal” introduction and elimination rules can be used for defining a connective. Some constraints should be imposed on the set of rules. Such a constraint was indeed suggested by Belnap in his famous [6]: the rules for a connective ⋄ should be conservative, in the sense that if T ⊢ φ is derivable using them, and ⋄ does not occur in T ∪ φ, then T ⊢ φ can also be derived without using the rules for ⋄. This solution to the Tonk problem has at least two problematic aspects: