论文标题
可计算功能理论的强烈否定tcf
Strong negation in the theory of computable functionals TCF
论文作者
论文摘要
我们将强烈的否定纳入了可计算函数的理论中，这是Plotkin的PCF和Gödel的系统$ \ MathBf {T} $的共同扩展，通过同时定义强大的否定$ a^{\ MATHBF {n}} $ formula $ a $ a $ a $ a $ p^$ p^$ p^$ pexpe $ p premaula formula作为后者的一种特殊情况，我们对TCF的感应和共同感应谓词有很大的否定。我们证明了falso Quodlibet的适当版本，并在TCF中进行了强烈否定的双重否定。我们介绍了TCF的所谓紧密公式，即由于其强烈否定和相对紧密的配方所隐含的公式。我们介绍了各种案例研究和示例，这些案例和示例揭示了我们对TCF强烈否定的定义的自然性，并证明将TCF用作主教风格的建设性数学很大一部分的正式系统是合理的。
We incorporate strong negation in the theory of computable functionals TCF, a common extension of Plotkin's PCF and Gödel's system $\mathbf{T}$, by defining simultaneously strong negation $A^{\mathbf{N}}$ of a formula $A$ and strong negation $P^{\mathbf{N}}$ of a predicate $P$ in TCF. As a special case of the latter, we get strong negation of an inductive and a coinductive predicate of TCF. We prove appropriate versions of the Ex falso quodlibet and of double negation elimination for strong negation in TCF. We introduce the so-called tight formulas of TCF i.e., formulas implied by the weak negation of their strong negation, and the relative tight formulas. We present various case-studies and examples, which reveal the naturality of our definition of strong negation in TCF and justify the use of TCF as a formal system for a large part of Bishop-style constructive mathematics.
