一句话：在可计算泛函理论 TCF 中定义公式与谓词的强否定，并证明其关键逻辑性质与构造性数学适用性。
本文研究如何在可计算泛函理论 TCF（Plotkin PCF 与 Gödel 系统 T 的常见扩展）中融入强否定。作者同时定义公式 A 的强否定 A^N 和谓词 P 的强否定 P^N，并将归纳谓词与余归纳谓词的强否定作为特例。文中证明了强否定下 Ex falso quodlibet 与双重否定消去的相应版本，引入紧公式（由其强否定的弱否定所蕴含的公式）及相对紧公式。通过若干案例与例子，作者展示该定义的自然性，并论证 TCF 可作为 Bishop 式构造性数学的形式系统。
We incorporate strong negation in the theory of computable functionals TCF, a common extension of Plotkin's PCF and G\"{o}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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{KoppP25,
title = {Strong negation in the theory of computable functionals TCF},
author = {Nils Köpp and Iosif Petrakis},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 2},
year = {2025},
doi = {10.46298/lmcs-21(2:1)2025}
}