一个简化的改进型自由变量框架：将Hilbert的epsilon作为非确定性承诺选择的算子
A Simplified and Improved Free-Variable Framework for Hilbert's epsilon as an Operator of Indefinite Committed Choice
AI总结：
本文提出了一个改进的二值逻辑自由变量框架，仅保留两种自由变量类型，其表达与求解能力超越标准一阶及高阶模态逻辑，并直接支持Fermat的descente infinie，同时为Hilbert的epsilon提出了支持归约式证明搜索的新选择算子语义。
摘要：
自由变量在数学和计算机科学中频繁出现，其语义往往是临时的且不断变化的。我们提出了用于二值逻辑的自由变量框架的最新版本，其功能得到了适当改进，仅保留了两种自由变量（而非三种）：隐式全称量化变量和隐式存在量化变量，现在分别简称为“free atoms”和“free variables”。我们框架的量化表达能力和问题求解能力超越了标准一阶甚至高阶模态逻辑，并直接支持Fermat的descente infinie。借助该改进版框架，我们现在也能对Henkin量化进行建模，既不使用量词（绑定符），也不进行类型提升（Skolemization）。我们为Hilbert的epsilon提出了一种作为选择算子的新语义，具有以下特征：我们避免了过度规约（如右唯一性），但允许非确定性选择、承诺选择和经典逻辑。此外，我们对epsilon的语义能够最优地支持归约式证明搜索。
英文摘要：
Free variables occur frequently in mathematics and computer science with ad hoc and altering semantics. We present the most recent version of our free-variable framework for two-valued logics with properly improved functionality, but only two kinds of free variables left (instead of three): implicitly universally and implicitly existentially quantified ones, now simply called "free atoms" and "free variables", respectively. The quantificational expressiveness and the problem-solving facilities of our framework exceed standard first-order and even higher-order modal logics, and directly support Fermat's descente infinie. With the improved version of our framework, we can now model also Henkin quantification, neither using quantifiers (binders) nor raising (Skolemization). We propose a new semantics for Hilbert's epsilon as a choice operator with the following features: We avoid overspecification (such as right-uniqueness), but admit indefinite choice, committed choice, and classical logics. Moreover, our semantics for the epsilon supports reductive proof search optimally.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
