Syntactical and semantical properties of simple type theory
Syntactical and semantical properties of simple type theory
复制标题
简单类型理论的句法和语义特性
DOI：
10.2307/2963525
复制
发表时间：
1960
影响因子：
0.6
通讯作者：
Kurt Schütte
中科院分区：
文献类型：
--
作者：
Kurt Schütte
在我的论文[10]中，我介绍了一阶谓词演算中逻辑公式的句法概念“正部分”和“负部分”。这些概念使得在类似于 Gentzen 推理规则的推理规则上建立逻辑系统成为可能，但不使用“顺序”概念，也不需要 Gentzen 结构推理规则。基于正负部分的几个形式系统的证明理论研究发表在[11]中。在本文中，我考虑了简单类型理论的类似形式系统。 “严格可导性”的语法概念来自于[10]中的形式系统，通过从一阶谓词演算到高阶谓词演算的公理和推理规则的推广，以及通过 λ 符号添加集合抽象的推理规则，它允许我们从格式良好的公式形成任意类型的集合表达式。
In my paper [10] I introduced the syntactical concepts “positive part” and “negative part” of logical formulas in first-order predicate calculus. These concepts make it possible to establish logical systems on inference rules similar to Gentzen's inference rules but without using the concept “sequent” and without needing Gentzen's structural inference rules. Proof-theoretical investigations of several formal systems based on positive and negative parts are published in [11]. In this paper I consider a similar formal system of simple type theory. A syntactical concept of “strict derivability” results from the formal system in [10] by generalization of the axioms and inference rules from first to higher-order predicate calculus and by addition of inference rules for set abstraction by means of a λ-symbol which allows us to form set expressions of arbitrary types from well-formed formulas.