Logic & Programming

In a constructive context, such as the multi-sorted first order arithmetic theory TCF adopted in the paper, usual negation — also called “weak” negation in the paper — does not in general satisfy the De Morgan laws involving disjunction and the existential quantifier.

The paper is a systematic study of adding “strong” negation to TCF, negation that is defined by the De Morgan laws. The new system still does not in general satisfy De Morgan laws, however it does so for certain important classes of formulas defined in the paper (SP, PP, NP, FP). The authors also define strong implication, following the idea of Rasiowa (or perhaps of Godel's Dialectica interpretation) as a pair of a proof of the implication and a refutation of the contraposition.

The paper argues for the convenience of the new extended system TCF for formalizing constructive real analysis. It also contains a review of the research history of strong negation going back to the first half of the twentieth century. Finally, TCF being the base of the Minlog proof assistant, the present work allows to extend Minlog to the new theory.

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net