Strong negation in the theory of computable functionals TCF
Nils Köpp, Iosif Petrakis
TL;DR
This work extends the theory of computable functionals ($\mathrm{TCF}$) by defining a recursive strong negation $A^{\mathbf{N}}$ for formulas and $P^{\mathbf{N}}$ for predicates, and it further extends this to inductive and coinductive predicates. It develops key logical properties, notably EfQ and double-negation-elimination variants, introduces tight and relative-tight formulas, and presents case studies illustrating the naturality and usefulness of strong negation in Bishop-style constructive mathematics. The results establish $\mathrm{TCF}$ as a viable formal framework for constructive mathematics, compatible with Minlog, while highlighting the duality between induction and coinduction and pointing to future work on incorporating dependencies. These contributions provide both foundational and practical tools for formalizing constructive reasoning with explicit refutations and strong negation in a computable setting.
Abstract
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.