Home Philosophy



ProofTheoretic ValidityWe now consider a notion of validity for intuitionistic propositional logic (see [16]), which will be based on the following clauses for the fragment {→, ∨, ∧}. Absurdity ⊥ is taken as a distinguished atom. Extensions St of atomic systems S are again understood in the settheoretic sense: An atomic system St is an extension of an atomic system S (written St ⊇ S), if St results from adding a (possibly empty) set of atomic rules to S. Definition 13 Svalidity (FS ) and validity (F) are defined as follows: (S1) FS a :⇐⇒ fS a, (S2) FS A → B :⇐⇒ A FS B, (S3) Γ FS A :⇐⇒ ∀St ⊇ S : (FSt Γ =⇒ FSt A), where Γ is a set of formulas, and where FSt Γ stands for {FSt Ai  Ai ∈ Γ }, (S4) FS A ∨ B :⇐⇒ FS A or FS B, (S5) FS A ∧ B :⇐⇒ FS A and FS B, (S6) Γ F A :⇐⇒ ∀S : Γ FS A. Since only the logical constants of the fragment {→, ∨, ∧} are considered, and ⊥ is just an atom, one could also speak of minimal validity or validity for minimal logic here. This notion is very similar to the 'minimal part' of Kreisel validity, given by clauses (K1)–(K4) and (K8) of Definition 6, when restricted to a propositional language and for words w identified with atoms a. In analogy to substitutionKreiselvalidity, we define in addition validity under substitution as validity for all substitution instances (resulting from uniform substitutions of formulas for atoms). Thus validity under substitution is by definition closed under substitution. Definition 14 Svalidity under substitution (fS ) and validity under substitution (f) are defined as follows: (i) Γ fS A :⇐⇒ for each substitution instance Γ t, At of Γ, A: Γ t FS At. (ii) Γ fA :⇐⇒ for each substitution instance Γ t, At of Γ, A: Γ t F At. These notions of validity are now extended for intuitionistic propositional logic: Definition 15 Intuitionistic Svalidity (Fi ) is defined as follows. Let (⊥) stand for the set of rules J ⊥ I a atomicl Then Γ Fi A :⇐⇒ Γ FS ( ) A. a I . S ∪ ⊥ Correspondingly, Γ Fi A, Γ fi A and Γ fi A are defined as Γ F( ⊥) A, Γ fS∪(⊥) A and Γ f(⊥) A, respectively. The treatment of absurdity ⊥, and therefore of negation if understood as ¬ A := A → ⊥, differs from the one given by clause (K5) of Kreisel validity and from the one given by clauses (G5) or (G5t). If ⊥ were defined as a nonatomic constant by a semantical clause which says that there is no atomic system S such that FS ⊥, then FS ¬¬a would hold for any atom a; this is the case, since 'FSt ¬a for any St ⊇ S, as FStt a for some Stt ⊇ St. We note the following properties of Svalidity: Lemma 3(i) FS is a consequence relation, that is, (1) A FS A, (2) Γ FS A =⇒ Γ, Δ FS A, (3) (Γ FS A and Δ, A FS B) =⇒ Γ, Δ FS B. (ii) FS is monotone with respect to S, that is, Γ FS A =⇒ ∀St ⊇ S : Γ FSt A. (iii) Γ FS A → B ⇐⇒ Γ, A FS B. For intuitionistic Svalidity (i.e., for FS replaced with Fi ) these properties hold as well. Atomic rules can be represented by formulas and vice versa (for details see [16]). Let Σ ∗ stand for the set of formulas representing a finite set Σ of atomic rules. The following completeness and soundness result holds: Lemma 4 Σ ∗ FS a ⇐⇒ Σ ∗ fS a. 
<<  CONTENTS  >> 

Related topics 