Failure of Completeness

Theorem 6 Intuitionistic logic is not complete with respect to the semantics based on higher-level atomic systems.

This has been proved in [16] by showing that the intuitionistically non-derivable Harrop or Kreisel–Putnam formula (see Harrop [9], Kreisel and Putnam [11]) is intuitionistically valid under substitution, that is, that

f-i (¬ A(BC))((¬ AB)(¬ AC))

holds. We emphasize that the given proof of this theorem depends on the fact that the considered semantics is based on higher-level atomic systems.

Since higher-level rules can be reduced to second-level rules by an appropriate coding (see Sandqvist [27]), it follows that intuitionistic logic is incomplete for S-validity based on second-level atomic systems. Whether intuitionistic logic is complete (simpliciter) for validity based on first-level atomic systems is an open problem.

Similarly to Gabbay's completeness conjecture for substitution-Kreisel-validity, the following conjecture can be made for intuitionistic validity under substitution:

Conjecture 3 Intuitionistic propositional logic is complete (simpliciter) for intuitionistic validity based on first-level atomic systems. That is, Γ f-i A =⇒ Γ fA, for first-level atomic systems only.

Comparison with Kripke Semantics

Proof-theoretic validity shares some similarities with the notion of validity in Kripke semantics, which is sound and complete for intuitionistic logic (see Kripke [12]; cf. Moschovakis [14]). We mention that the semantical clauses for conjunction and disjunction have the same form in both cases, and that the clauses for implication are similar in that they depend on the idea of extensions. In Kripke semantics the clause for implication is

k forces AB :⇐⇒ ∀kt ≥ k : (kt forces A =⇒ kt forces B)

for nodes k, kt and partial orders ≥. The forcing relation for atoms a and nodes k is given by truth-value assignments v(k, a), which obey the monotonicity requirement

that if kt ≥ k and v(k, a) = true, then v(kt, a) = true. Thus kt is an extension of k in the sense that {a | kt forces a} ⊇ {a | k forces a}, just like St ⊇ S for atomic systems S, St of level 0 in the case of proof-theoretic validity.

Besides these similarities, there are the following main differences to Kripke semantics. In proof-theoretic validity, the S-validity of atoms is given by their derivability in S, whereas in Kripke semantics the validity (resp. the forcing relation) for nodes k and atoms a is given by truth-value assignments v(k, a).

In S-validity, atomic systems S are not only sets of atoms (which in Kripke semantics would be assigned to nodes k by v) but sets of atomic rules. This also means that St ⊃ S can be the case, although {a | f-St a} = {a | f-S a} (and consequently

{a | FSt a} = {a | FS a}), simply because St might contain inapplicable additional

rules besides the ones in S, which therefore do not enlarge the set of atoms derivable

in St. For example, let S contain only the axiom a and let St = S ∪ J b l then

St ⊃ S, while both in St and S only a is derivable. A notion like weak validity (see Sect. 3), where

St is an extension of S :⇐⇒ ∀a : (f-S a =⇒ f-St a),

is in this respect closer to the notion of validity in Kripke semantics than to S-validity.

In Kripke semantics, a formula has to be forced by every node in every Kripke structure in order to be Kripke valid. Besides different sets of nodes k and different truth-value assignments v(k, a), one therefore has to consider different partial orders ≥, whereas in proof-theoretic validity only one kind of structure is taken into account (cf. Goldfarb [8]; see also [16]), namely the one where the partial order is set inclusion ⊇ for atomic systems S.

Furthermore, inconsistent extensions are possible in the case of S-validity, since absurdity ⊥ could be added as an axiom to atomic systems S. This is not the case in Kripke semantics, where the forcing relation is consistent in the sense that a node k cannot force both A and ¬ A (cp., however, the modified Kripke models of Veldman [35]).

A Completeness Result for Intuitionistic Logic

A completeness result for intuitionistic propositional logic is available for the following notion of validity, which is given for second-level atomic systems S (see Sandqvist [27]; we adjust it to our notation):

Definition 18

(T1) FS a :⇐⇒ f-S a,

(T2) FS AB :⇐⇒ A FS B,

(T3) Γ FS A :⇐⇒ ∀St ⊇ S : (FSt Γ =⇒ FSt A), where Γ is a set of

formulas, and where FSt Γ stands for {FSt Ai | AiΓ },

(T4) FS AB :⇐⇒ ∀St ⊇ S and ∀c : ( A FSt c and B FSt c =⇒ FSt c), (T5) FS AB :⇐⇒ FS A and FS B,

(T6) FS ⊥ :⇐⇒ ∀a : FS a, (T7) Γ F A :⇐⇒ ∀S : Γ FS A.

Compared to S-validity (see Definition 13) there are two differences (besides the restriction to second-level atomic systems S):

(i) Clause (T4) for disjunction replaces (S4). It resembles the natural deduction elimination rule for disjunction. Note that the definiens is restricted to extensions St ⊇ S, and that propositional quantification is made use of in the universal quantification over all atoms c (not over all formulas; cf. Ferreira [4]).

(ii) Absurdity ⊥ is not an atom but a logical constant, whose meaning is given by clause (T6). This clause is based on Dummett's introduction rule for ⊥ (cf. Dummett [3, Chap. 13]).

Theorem 7 (Sandqvist [27]) Intuitionistic propositional logic is sound and complete for this semantics, that is, Γ F A ⇐⇒ Γ fA.

< Prev   CONTENTS   Next >