论文标题
部分可观测时空混沌系统的无模型预测
Puzzles of Existential Generalisation from Type-theoretic Perspective
论文作者
论文摘要
本文解决了与存在概括的规则有关的几个难题（例如）。从简单类型理论的角度来解决这些难题的解决方案，我将（例如）与修改的存在量化器引入规则区分开，该规则可从（例如）衍生。这两种规则通常都是混淆的，两者都被认为是原始的，但是我表明（例如）本身是从适当的存在量化器引入的规则中衍生的。此外，后一个规则在处理总和和部分功能的逻辑系统中必须是原始的，因为通用量词和存在的量词在其中不可互定。部署了适当的自然扣除额。当前的逻辑系统比本作者最近提出和应用的系统更简单。它利用了对替代的适当定义，该定义不仅能够处理高阶量化，还可以（超级）强度上下文处理。
The present paper addresses several puzzles related to the Rule of Existential Generalization, (EG). In solution to these puzzles from the viewpoint of simple type theory, I distinguish (EG) from a modified Rule of Existential Quantifier Introduction which is derivable from (EG). Both these rules are often confused and both are considered as primitive but I show that (EG) itself is derivable from the proper Rule of Existential Quantifier Introduction. Moreover, the latter rule must be primitive in logical systems that treat both total and partial functions, for the universal and the existential quantifiers are not interdefinable in them. An appropriate natural deduction for such a system is deployed. The present logical system is simpler than the system recently proposed and applied by the present author. It utilises an adequate definition of substitution which is capable of handling not only a higher-order quantification, but also (hyper)intensional contexts.
