Home Philosophy Advances in Proof-Theoretic Semantics

## Logic, Paradoxes, Partial DefinitionsIntroduction rules (clauses) for logically compound formulas are not distinguished in principle from introduction rules (clauses) for atoms. The introduction rules for conjunction and disjunction would, for example, be handled by means of clauses for a truth predicate with conjunction and disjunction as term-forming operators: D
⎩ In order to define implication, we need a rule arrow in the body, which, for the whole clause, corresponds to using a higher-level rule:
This definition requires some sort of 'background logic'. By that we mean the structural logic governing the comma and the rule arrow ⇒, which determine how the bodies of clauses are handled. In standard logic we have just the comma, which is handled implicitly. In extended versions of logic programming we would have the (iterated) rule arrow, that is, structural implication and associated principles governing it, and perhaps even structural disjunction (this is present in disjunctive logic programming, but not needed for the applications considered here). It is obvious that disjunction or, more precisely, those for for Definitional reflection in general provides a much wider perspective on inversion principles than deductive logic alone. Using the definitional rule
we obtain a principle of naive comprehension, which does not lead to a useless theory in which everything is derivable, even if we allow the term {
yields a paraconsistent system in which both f
is not always admissible. For special cases cut can be obtained, for example, if the definition is stratified, which essentially means that it is well-founded. So the wellbehaviour of a definition in the case of logic, where we do have cut elimination, is due to the fact that it obeys certain principles, which in the general case cannot be expected to hold. This connects the proof theory of clausal definitions with theories of paradoxes, which conceive paradoxes as based on locally correct reasoning (Prawitz [44] (Appendix B), Tennant [68], Schroeder-Heister [62], Tranchini [71]). For the situation that obtains here, Hallnäs [28] proposed the terms 'total' vs. 'partial' in analogy with the terminology used in recursive function theory. That a computable (i.e., partial recursive) function is total is not something required by definition, but is a matter of (mathematical) fact, actually an undecidable matter. Similarly, that a clausal definition yields a system that admits the elimination of cuts is a result that may or may not hold true, but nothing that should enter the requirements for something to be admitted as a definition. If it holds, the definition is called 'total', otherwise it is properly 'partial'. |

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

Related topics |

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