Dummett's logic LC quantified, Q-LC, is shown to be characterized by the extended frame (Q+, <,D), where Q+ is the set of non-negative rational numbers, _< is the numerical relation "less or equal then" and D is the domain function such that for all v, w E Q+, D~ r ~ and if v < w, then Do C Dw. Moreover, simple completeneSS proofs of extensions of Q-LC are given.
The Logic Q-LC Q-LC is the logic obtained by adding to the intuitionistic predicate calculus IPC the axiom schema (a ~ fl V fl ~ a). It has been an Open problem for a long time if Q-/C were complete or not. By a generalization of the method of diagrams, first introduced by S. Kripke in [6] and developed for modal logics by K. Fine in [5], it is possible to solve it positively and in a very simple and natural way.
The language L of Q-/C is a first-order intuitionistic language such that _L E L and ~(~ =dr c~ ~ _L. By '% a" we mean that a is a theorem of Q-LC.
LEMMA 1.1 The following are theorems of Q-LC: ~(z---')~ 7(~'))], whe,~ ~ does not occur in (,~ ~ #). "7(~)], wh~re ~ does not occur i~ (~ ~ 9). V;',~(~V V~(~(~') ~ ~(~)), where ~ do~s not occur in ~(~.) ~ "~(~) and ~ does not occur in c~( ~.
(d) V.~[c~(z-') V Vy-'(/~(ff) A V~'o~(~) ~ 7(if))] ~ V~(5') V V~(,8(~) A V~(x(~) ---+ -),(if)), where ~ does not occur in fl(ff)A V~e(~) -+ 7(Y) and ff does not occur in ~( ~).