Home Philosophy Advances in Proof-Theoretic Semantics

## Completeness Results for Classical LogicSo 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 between finite sets 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 (C2) For non-empty for every (C3) F (C4) F (C5) F (C6) (C7) Note that the definiens in clause (C1) could be expressed equivalently as f- Δ of closed atoms under the rules in S. That is, is the intersection of all sets S (Δ)Λ of closed atoms such that Δ ⊆ Λ, and if
can then be written as follows: (C1t) For closed atoms ). (C4t) FS ⊥ :⇐⇒ a ∈ ∅S () for every closed atom a.We point out that ⊥ is 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: elimination amounts to classical logic, the following soundness and completeness result for classical first-order logic holds:
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 (
Sandqvist's semantics contains clauses only for the logical constants of the fragment {→, ⊥, ∀}. A clause for conjunction ∧ like (S5) F 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) F were added, then Theorem 8 would no longer hold. For example, the law of double negation elimination F and F 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 |

< Prev | CONTENTS | Next > |
---|

Related topics |

Academic library - free online college e textbooks - info{at}ebrary.net - © 2014 - 2020