Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics

Completeness Results for Classical Logic

So far, we have only discussed notions of proof-theoretic validity intended for intuitionistic logic or for certain fragments thereof. Now we will discuss a notion of proof-theoretic validity for classical logic.

Sandqvist [26] gives a semantics for the fragment {→, ⊥, ∀} of the language of

first-order logic. He considers basic sequents of the form : a), which are relations

between finite sets Γ of basic sentences and basic sentences a. Basic sentences are closed atomic formulas, that is, formulas containing neither logical constants nor free variables. Sets of basic sequents are called 'bases'. In our terminology, basic sequents are first-level rules, and bases are first-level atomic systems S. Sandqvist shows that minimal logic can be justified and that the law of double negation elimination is

valid for the fragment {→, ⊥, ∀}. The other logical constants can then be defined,

and a justification of classical logic is achieved without making use of the principle of bivalence. That classical logic is sound and complete for the given semantics is surprising, since this semantics is very similar to semantics proposed for intuitionistic logic. Discussions of these results can be found in Makinson [13] and in [2].

Sandqvist's semantics is the following (again, we use our notation):

Definition 19

(C1) For closed atoms a: FS a :⇐⇒ every set of closed atoms which is closed under S contains a.

(C2) For non-empty Γ : Γ FS A :⇐⇒ FS A for every St ⊇ S such that FSt B

for every BΓ .

(C3) FS AB :⇐⇒ A FS B.

(C4) FS ⊥ :⇐⇒ FS a for every closed atom a.

(C5) FSx A(x ) :⇐⇒ FS A(x )[x /t ] for every closed term t .

(C6) Γ F A :⇐⇒ ∀S : Γ FS A.

(C7) Γ F∗ A :⇐⇒ Γσ F for all ground substitutions σ .

Note that the definiens in clause (C1) could be expressed equivalently as f-S a. Another (equivalent) formulation has been given by Makinson [13], where S (Δ) is written for the closure of a set Δ of closed atoms under the rules in S. That is, S (Δ) is the intersection of all sets Λ of closed atoms such that ΔΛ, and if

a 1 ... a n

bS with {a1,..., an } ⊆ Λ, then bΛ. Clauses (C1) and (C4)

can then be written as follows:

(C1t) For closed atoms a: FS a :⇐⇒ aS (). (C4t) FS ⊥ :⇐⇒ aS () for every closed atom a.

We point out that ⊥ is not an atom here. In clause (C5), the notation A(x )[x /t ] means that each occurrence of x in A is replaced by the term t . The relation Γ F∗ A defined in clause (C7) deals with open formulas; a ground substitution is a substitution of variable-free terms for variables. The sets Γ of formulas are finite, but in Definition 19 infinite sets Γ could be allowed as well. The relation FS is called 'valid inferability' by Sandqvist; by 'validity' we refer to the relation F defined in clause (C6).

The given semantics validates minimal logic (see Sandqvist [26, Lemma 3]). Furthermore, Sandqvist [26, Lemma 4] shows that the law of double negation elimination holds: ( A → ⊥) → ⊥ F∗ A. Since minimal logic plus double negation

elimination amounts to classical logic, the following soundness and completeness result for classical first-order logic holds:

Theorem 8 (Sandqvist [25, 26]) Γ F A ⇐⇒ Γ fA in classical first-order logic.

The theorem is proved constructively by Sandqvist. An alternative proof is given by Makinson [13], who uses classical meta-reasoning.

Sandqvist [26] refers to the implication from right to left as soundness, whereas Makinson [13] takes the opposite perspective, in which the implication from right to left expresses that Sandqvist's semantics is complete with respect to the usual model-theoretic semantics of classical logic. The implication from left to right, that is, completeness in the sense that Sandqvist validity (Γ F A) implies classical derivability, or equivalently classical validity, holds as well.

6.1 Other Logical Constants

Sandqvist's semantics contains clauses only for the logical constants of the fragment

{→, ⊥, ∀}. A clause for conjunction ∧ like (S5)

FS AB :⇐⇒ FS A and FS B

could be added without causing any problems with respect to completeness (cf. Makinson [13]). However, as noted by Sandqvist [26], if a clause for disjunction ∨ like (S4)

FS AB :⇐⇒ FS A or FS B

were added, then Theorem 8 would no longer hold. For example, the law of double negation elimination ( A → ⊥) →⊥ F A does then not hold for each substitution instance anymore; a counterexample is A := B(B → ⊥) (cf. [2]). In other words, validity fails to be closed under substitution, if disjunction is taken as primitive and understood according to the given semantical clause. This is also the case for the following stricter disjunction clauses (see Makinson [13]):

FS AB :⇐⇒ ∀St ⊇ S : (FSt A or FSt B),

and FS AB :⇐⇒ ∀St ⊇ S : FSt A or ∀St ⊇ S : FSt B.

Similar observations can be made for the existential quantifier.

Makinson also gives an alternative clause for disjunction (see [13, p. 149]), which does not affect completeness. However, this clause is modeled on the definition AB := ( A → ⊥)B, which represents a classical understanding of disjunction, whereas by clause (S4) disjunction is given its intuitionistic meaning.

Found a mistake? Please highlight the word and press Shift + Enter  
< Prev   CONTENTS   Next >

Related topics