The logic of the weak excluded middle
a case study of proof-search
pp. 95-116
in: Rossella Lupacchini, Giovanna Corsi (eds), Deduction, computation, experiment, Berlin, Springer, 2008Abstract
The logic J of the weak excluded middle, known also as Jankov's logic, is an extension of the intuitionistic logic obtained by adding the schema ¬A⋁¬¬A. This logic, we believe, 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? It is a well known result [4] that Lemma 1. (Hosoi) If a wff A contains the propositional letters p 1,...,p n then A is a theorem of J iff (¬p 1 ⋁ ¬¬p 1) ⋀ ⋯ ⋀ (¬p n ⋁ ¬¬p n ) → A is a theorem of the intuitionistic logic.