Home Philosophy Advances in Proof-Theoretic Semantics

## RemarksTheorem 8 still holds if atomic rules of Δ of closed atoms under the rules in S is understood as follows (see [13, p. 152]): is the intersection of all sets S (Δ)Λ of closed atoms such that(i)
(ii) if S with {a1,..., an } ⊆ Λ, then b ∈ Λ for every closedatom 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 second-level rules are allowed in [ Then F 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 There is no 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 proof-theoretic 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. |

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

Related topics |

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