This idea of a recursive definition of strong negation is applied here to the formal theory of computable functionals
\(\mathrm {TCF}\) , developed mainly by Schwichtenberg in [1]}. \(\mathrm {TCF}\)  is a
common extension of Plotkin's PCF and Gödel's system T, it uses, in contrast to Scott's LCF,
non-flat free algebras as semantical domains for the base types, and for higher types its intended model consists
of the computable functions on partial continuous objects (see [1]}, Chapter 7).
Furthermore, it accommodates inductively and coinductively defined predicates and its underlying logic is minimal.
\(\mathrm {TCF}\)  is the theoretical base of the proof assistant Minlog [3]} with which the extraction of computational
content of formalised proofs is made possible. A significant feature of \(\mathrm {TCF}\)  is its relation to \(\mathrm {CM}\) , as
many parts of \(\mathrm {BISH}\)  have already been formalised in \(\mathrm {TCF}\)  and implemented
in Minlog (see e.g., [4]}, [5]}, [6]}).
