\input zb-basic
\input zb-ioport
\iteman{io-port 04127199}
\itemau{Corsi, Giovanna}
\itemti{A cut-free calculus for Dummett's LC quantified.}
\itemso{Z. Math. Logik Grundlagen Math. 35, No.4, 289-301 (1989).}
\itemab
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.
\itemrv{G.E.Mints}
\itemcc{}
\itemut{cut-elimination; Gentzen-type system; Dummett's LC; intuitionistic predicate calculus; many-succedent sequents}
\itemli{doi:10.1002/malq.19890350402}
\end