The aim of this p~per is to provide ~ decision procedure for Dummett's logic/)U, such that wi~h any given formula will be associated either a proof in a sequent calculus eqwiv~len* to ZC or a finite linear Kripke counr
In [2] Sonobe gives an axiomatization of the intermediate propositioha! c~lculus LC [1] in ~ sequent calculus and proves the cut elimination theorem for it. Let us call this calculus D. The cut elimination theorem for D does not provide an effective procedure for deciding whether a given sequent is provable in D or not. In the present paper we describe how to build for each sequent M:N a reduction tree A such that, if closed, it can be transformed into a proof of M:N in D, while if not closed, it contuins a path P which is a finite linear Kripke eountermodel of M:N.
The language of/), JS, contains an infinite list of sentence letters p, ~, 2.~, ..., the symbol of falsehood _L, the connectives ^ (and), v (or), -~ (if ... then) and the auxiliary symbols (,). There is no primitive symbo for negation, and -la =~ia-+ _[_. We use a, fl, 7 as metavariables for formulas, which ~re defined in the usual way; the letters M, _A r, P, Q1 designate finite sets (possibly empty) of formulas.