Home Philosophy Advances in ProofTheoretic Semantics


RemarksTheorem 8 still holds if atomic rules of S are allowed to have empty conclusions, and the closure S (Δ) of a set Δ of closed atoms under the rules in S is understood as follows (see [13, p. 152]): S (Δ) is the intersection of all sets Λ of closed atoms such that (i) Δ ⊆ Λ, and if and a 1 ... a n b ∈ S with {a1,..., an } ⊆ Λ, then b ∈ Λ, (ii) if a 1 ... a n ∈ S with {a1,..., an } ⊆ Λ, then b ∈ Λ for every closed atom b (whe∅re again ⊥ is not an atom). This generalization introduces a kind of negation at the level of atomic rules. In logic programming terms, this is a generalization of definite Horn clauses to Horn clauses. Theorem 8 fails, however, if secondlevel rules are allowed in S. For example, consider the atomic system S which contains only the secondlevel rule [a] b a Then FS (a → b) → a, but 'FS a, since J.S a. Thus 'F ((a → b) → a) → a, that is, Peirce's law is no longer valid, and soundness fails. We already remarked that absurdity ⊥ is not an atom here. Furthermore, it is essential that there are infinitely many atoms in the language; otherwise completeness would be lost, since for finite sets of n atoms the classically nonderivable formula a1 → (... → (an → ⊥).. .) becomes valid (see Makinson [13]). Soundness would fail if instead of clause (C4) the clause There is no S such that FS ⊥ were used (cf. [2, 13]). The use of a semantical clause for ⊥ could also be avoided. Instead of showing the validity of the law of double negation, which depends both on clause (C3) for → and on clause (C4) for ⊥, one can show the validity of Peirce's law, which does not depend on clause (C4) at all (cf. [2, 26]). Sandqvist's result is remarkable, since it shows that the intuitionistically acceptable semantics given by Definition 19 allows for a justification of classical logic, as long as disjunction is understood classically. The fact that the semantics is given for only a fragment of the language of firstorder logic might be seen as a critical point. This leads to the question of whether such a semantics fulfills the requirements of prooftheoretic semantics for a justification of a logic. Makinson [13] argues that one might require to treat every logical constant used in informal mathematical discourse as a primitive in the formal language of the semantics and to give adequate semantical clauses for each of them. But, as he points out, such a requirement would be difficult to fulfill since it is too vague. From the point of view of the formal systems used to represent logical reasoning in mathematical discourse one could argue that it is sufficient to have semantical clauses only for the standard logical constants present in the respective formal systems, such as the set {→, ∨, ∧, ⊥, ∀, ∃} of logical constants in natural deduction for intuitionistic or classical logic. In the case of classical logic the restriction to a semantics for a fragment like {→, ⊥, ∀}, which is sufficient to define all the standard logical constants, should then be acceptable for the purpose of giving a justification for the whole logic. 
CONTENTS 

Related topics 