Complementary Logics for Classical Propositional Languages

This note presents a simple axiomatic system by means of which exactly those sentences can be derived that are rated non-tautologous in classical propositional logic. Since the logic is decidable, there exist of course many algorithms that do the job, e.g. using semantic tableaux or refutation trees. However, a formulation in terms of axioms and rules of inference is by no means a straightforward task, as these must be of a most non-standard non-classical sort. For instance, axioms cannot be axiom schemata and standard substitution rules cannot hold, since a non-tautology may well become tautologous upon substitution. Moreover, the system must be paraconsistent, i.e. such as to allow derivation of sentences with opposite truth values. The system presented here provides, I think, a rather nice way of dealing with these difficulties. Since tautologous sentences are also axiomatizable, the outcome is an exhaustive characterization of the logic of classical propositional languages in purely syntactic terms. The picture can then be completed by developing related systems axiomatizing classical contradictions, contingencies, non-contradictions