A sound and complete proof theory for propositional logical contingencies (Q2425353)

The authors call a propositional formula logically contingent if it is satisfiable and also falsifiable. Letting LC be the set of such formulas, they give a sound and complete axiomatic system for LC. It consists of two parts: the first is a set of rules for logically equivalent transformations, like replace \(\neg\neg A\) by \(A\), and the second is for contingency proper, e.g. (i) \(\vdash p\) where \(p\) is a sentence letter, (ii) if \(\vdash A\) then \(\vdash\neg A\), and (iii) if \(\vdash A\) then \(\vdash(A\wedge p)\vee (B\wedge\neg p)\). Completeness follows from the proof that truth tables can be handled by these axioms and rules. The authors point out that LC is an NP-complete set which is disjoint from two co-NP sets of logically true and logically false formulas. They also point out that LC in predicate calculus is not axiomatizable because of undecidability of validity. What kind of quantification rules are appopriate for LC is a project they leave for the future. \{The reviewer wonders what the situation is in intuitionism. Contingency in terms of Kripke models looks like an interesting subject.\}