Proof-Theoretic Functional Completeness for the Connexive Logic C

TL;DR

This paper establishes the functional completeness of connectives in the non-trivial negation inconsistent connexive logic C using proof-theoretic methods that incorporate bilateralist and connexive perspectives on inference and refutation.

Contribution

It introduces a proof-theoretic approach to demonstrate functional completeness in connexive logic C, considering strong negation and bilateralist inference.

Findings

Proves functional completeness for connectives in logic C

Develops a bilateral proof system for refutations

Adapts refutation concepts to connexive logic

Abstract

We show the functional completeness for the connectives of the non-trivial negation inconsistent logic C by using a well-established method implementing purely proof-theoretic notions only. Firstly, given that C contains a strong negation, expressing a notion of direct refutation, the proof needs to be applied in a bilateralist way in that not only higher-order rule schemata for proofs but also for refutations need to be considered. Secondly, given that C is a connexive logic we need to take a connexive understanding of inference as a basis, leading to a different conception of (higher-order) refutation than is usually employed.