We incorporate strong negation in the theory of computable functionals TCF, a common extension of Plotkin’s PCF and Goedel’s system T, by defining simultaneously strong negation of a formula and strong negation 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.
Strong negation in the theory of computable functionals TCF
Petrakis, Iosif
2025-01-01
Abstract
We incorporate strong negation in the theory of computable functionals TCF, a common extension of Plotkin’s PCF and Goedel’s system T, by defining simultaneously strong negation of a formula and strong negation 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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
