CUT-SIMULATION AND IMPREDICATIVITY
CUT-SIMULATION AND IMPREDICATIVITY
复制标题
DOI：
10.2168/lmcs-5(1:6)2009
复制
发表时间：
2009-01-01
影响因子：
0.6
通讯作者：
Kohlhase, Michael
中科院分区：
文献类型：
--
作者：
Benzmueller, Christoph;Brown, Chad E.;Kohlhase, Michael
我们研究了非谓词（高阶）逻辑中的割消除和割模拟。我们说明，添加简单的公理，如莱布尼茨方程的演算不可断言的逻辑-在我们的情况下，经典类型理论的微积分-就像添加削减。这一现象同样适用于布尔和函数外延性、归纳、选择和描述等重要公理。这就要求微积分的发展，这些原则是内置的，而不是被公理化处理。
We investigate cut-elimination and cut-simulation in impredicative (higher-order) logics. We illustrate that adding simple axioms such as Leibniz equations to a calculus for an impredicative logic - in our case a sequent calculus for classical type theory - is like adding cut. The phenomenon equally applies to prominent axioms like Boolean- and functional extensionality, induction, choice, and description. This calls for the development of calculi where these principles are built-in instead of being treated axiomatically.