NATURAL DEDUCTION FOR BI-CONNEXIVE LOGIC AND A TWO-SORTED TYPED lambda-CALCULUS

The bi-connexive propositional logic 2C is being introduced, which contains a connexive implication and a connexive co-implication that is in a certain sense dual to the connexive implication. The system 2C is a connexive variant of the bi-intuitionistic logic 2Int and contains a primitive strong negation. In both systems a relation of provability is supplemented with a certain relation of dual provability. Whereas entailment as the semantic counterpart of provability preserves support of truth from the premises to the conclusion of an inference, dual entailment as the semantic counterpart of dual provability preserves falsity from the premises to the conclusion of an inference. The strong negation that is added to the language of 2Int to obtain the system 2C internalizes falsification with respect to provability and it internalizes verification with respect to dual provability. This tight relation between verification, falsification, and strong negation allows one to see the dual of provability as disprovability. After introducing a natural deduction proof system, N2C, and a relational semantics for 2C, a two-sorted typed lambda-calculus, 2 lambda, is presented that can be used to encode derivations in N2C. In particular, the {implication, coimplication, strong negation}-fragment of 2C receives an encoding that makes use of functional application, functional abstraction, and certain sort/type-shift operations.