04127199

j

04127199 Corsi, Giovanna A cut-free calculus for Dummett's LC quantified. Z. Math. Logik Grundlagen Math. 35, No.4, 289-301 (1989). 1989 VEB Deutscher Verlag der Wissenschaften, Berlin EN cut-elimination Gentzen-type system Dummett's LC intuitionistic predicate calculus many-succedent sequents

doi:10.1002/malq.19890350402

Dummett's LC is the result of adding (A$\to B)\vee (B\to A)$ to the intuitionistic predicate calculus. The Gentzen-type formulation considered here deals with many-succedent sequents. All rules except those for $\to$, $\forall$ in the succedent have the usual intuitionistic form (valid also in the many-succedent case). The only specific rule allows to infer a sequent with succedent consisting of several formulas beginning with implication or general quantifier from the set of all premisses of the corresponding classical rule applied (bottom up) to each of these formulas. For example $X\Rightarrow (A\to B)$, (C$\to D)$, $\forall yBy$ is inferred from three premisses: X,Y$\Rightarrow B$, $C\to D$, $\forall yBy$; X,C$\Rightarrow A\to B, D$, $\forall yBy$; $X\Rightarrow A\to B$, $C\to D$, Ba. Cutelimination is done by induction on rank and cut-degree. So the only non-invertible rule of the system is weakening used for dropping atomic and existential formulas to make the application of the ($\to,\forall)$-rule possible. The problem of completeness (for connected Kripke models with nested domains) stated in the paper has now been solved by the author in the positive. G.E.Mints