The Logic of the Weak Excluded Middle: a Case Study of Proof-Search

The logic of the weak excluded middle, known also as Jankov's logic, is an extension of the intuitionistic logic obtained by adding the schema "not A or not not A". This logic offers a good case study for some metatheoretical properties: Is there a cut-free calculus for this logic? Is it analytic? Is there a proof-search procedure that answers the question whether a formula is a theorem or not, and if not, does it give us a strategy to build a countermodel? We answer these quetsions by presenting a calculus, SJC, with the following metatheoretical properties: 1. Proof.search is performed by a single tree. 2. proof.search always terminates since never enters into loops, thanks to the a fortiori rule. 3. there is no need of back-tracking thanks to the rules push and pop. 4. SJC-proofs satisfy the sub-formula property 5. SJC-proofs are cut free. 6. If proof search in SJC fails we get a kripke countermodel based on a ocnvergent frame