Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics


Proof-Theoretic Validity

We 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 set-theoretic 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 S-validity (FS ) and validity (F) are defined as follows: (S1) FS a :⇐⇒ f-S a,

(S2) FS AB :⇐⇒ 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 AB :⇐⇒ FS A or FS B,

(S5) FS AB :⇐⇒ 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 substitution-Kreisel-validity, 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 S-validity under substitution (f-S ) and validity under substitution (f-) are defined as follows:

(i) Γ f-S 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 S-validity (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, Γ f-i A and Γ f-i A are defined as Γ F() A,

Γ f-S() 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 non-atomic 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 S-validity:

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 AB ⇐⇒ Γ, A FS B.

For intuitionistic S-validity (i.e., for FS replaced with Fi ) these properties hold as


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 ⇐⇒ Σ ∗ f-S a.

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

Related topics