Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics


Failure of Completeness for Intuitionistic Logic

Our first example of a notion of validity for formulas is due to Kreisel [10]. We follow the expositions given by Gabbay in [5] and [6, Chap. 13], adjust the notation and speak of 'Kreisel validity'.

Let A be a fixed alphabet and S a Post system on A . If a word w over A is derivable in S, we write f-S w. Let h be any function which assigns words over A to all variables x , y, x1, x2,... and relation symbols R of a first-order language, and let h1 =x h2 := h1(y) = h2(y) for all y /= x .

Definition 6 Kreisel S-validity (Fh ) and Kreisel validity (F) are defined as follows:

(K1) Fh R(x1,..., xn ) :⇐⇒ f-S h(R)h(x1)... h(xn ) (where R(x1,..., xn )

is an atom),

(K2) Fh AB :⇐⇒ ∀St ⊇ S : (Fh A =⇒ Fh B),

S St St

(K3) Fh AB :⇐⇒ Fh A or Fh B,


(K4) Fh AB :⇐⇒ Fh A and Fh B,


(K5) Fh ¬ A :⇐⇒ for all consistent St ⊇ S : 'Fh A (where St is consistent

S St

iff J.St w for some word w),

(K6) Fhx A(x ) :⇐⇒ for some h1 =x h : Fh1 A(x ),


(K7) Fhx A(x ) :⇐⇒ for all h1 =x h : Fh1 A(x ),


(K8) F A :⇐⇒ ∀A, S, h : Fh A.

(K9) A is substitution-Kreisel-valid :⇐⇒ all substitution instances of A are

Kreisel valid (where substitutions are uniform substitutions of formulas for atoms in A).

Note that clause (K5) for negation is restricted to consistent extensions, and that extensions St ⊇ S are understood in the normal set-theoretic sense, that is, the Post system St contains at least all the rules of the Post system S. Alternatively, extensions

St of S can be understood to mean that the implication f-S w =⇒ f-St w holds for all words w over A . In this latter case, Gabbay speaks of weak validity.

Intuitionistic first-order logic is neither complete for weak validity nor for Kreisel validity. Completeness already fails in the propositional case for both notions (we now consider weak validity and Kreisel validity restricted to the propositional fragment):

Theorem 1 (Gabbay [6, p. 224]) Intuitionistic propositional logic is not complete for weak validity. The formula ((¬¬ AA)(¬ A ∨ ¬¬ A))(¬ A ∨ ¬¬ A) is a counterexample.

Theorem 2 (Gabbay [6, p. 225]) Intuitionistic propositional logic is not complete for Kreisel validity. The set of Kreisel valid sentences is not closed under substitution. The formula (a(bc))((ab)(ac)), for propositional atoms a, b, c, is a counterexample.

Considering only the propositional fragment, completeness has been conjectured for substitution-Kreisel-validity:

Conjecture 2 (Gabbay [6, p. 226]) Intuitionistic propositional logic is complete for substitution-Kreisel-validity (restricted to the propositional fragment).

Found a mistake? Please highlight the word and press Shift + Enter  

Related topics