Home Philosophy Advances in ProofTheoretic Semantics


Failure of CompletenessTheorem 6 Intuitionistic logic is not complete with respect to the semantics based on higherlevel atomic systems. This has been proved in [16] by showing that the intuitionistically nonderivable Harrop or Kreisel–Putnam formula (see Harrop [9], Kreisel and Putnam [11]) is intuitionistically valid under substitution, that is, that fi (¬ A → (B ∨ C)) → ((¬ A → B) ∨ (¬ A → C)) holds. We emphasize that the given proof of this theorem depends on the fact that the considered semantics is based on higherlevel atomic systems. Since higherlevel rules can be reduced to secondlevel rules by an appropriate coding (see Sandqvist [27]), it follows that intuitionistic logic is incomplete for Svalidity based on secondlevel atomic systems. Whether intuitionistic logic is complete (simpliciter) for validity based on firstlevel atomic systems is an open problem. Similarly to Gabbay's completeness conjecture for substitutionKreiselvalidity, the following conjecture can be made for intuitionistic validity under substitution: Conjecture 3 Intuitionistic propositional logic is complete (simpliciter) for intuitionistic validity based on firstlevel atomic systems. That is, Γ fi A =⇒ Γ fA, for firstlevel atomic systems only. Comparison with Kripke SemanticsProoftheoretic 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 A → B :⇐⇒ ∀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 truthvalue 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 prooftheoretic validity. Besides these similarities, there are the following main differences to Kripke semantics. In prooftheoretic validity, the Svalidity 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 truthvalue assignments v(k, a). In Svalidity, 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  fSt a} = {a  fS 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 : (fS a =⇒ fSt a), is in this respect closer to the notion of validity in Kripke semantics than to Svalidity. 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 truthvalue assignments v(k, a), one therefore has to consider different partial orders ≥, whereas in prooftheoretic 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 Svalidity, 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 LogicA completeness result for intuitionistic propositional logic is available for the following notion of validity, which is given for secondlevel atomic systems S (see Sandqvist [27]; we adjust it to our notation): Definition 18(T1) FS a :⇐⇒ fS a, (T2) FS A → B :⇐⇒ 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 A ∨ B :⇐⇒ ∀St ⊇ S and ∀c : ( A FSt c and B FSt c =⇒ FSt c), (T5) FS A ∧ B :⇐⇒ FS A and FS B, (T6) FS ⊥ :⇐⇒ ∀a : FS a, (T7) Γ F A :⇐⇒ ∀S : Γ FS A. Compared to Svalidity (see Definition 13) there are two differences (besides the restriction to secondlevel 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 > 

Related topics 