Home Philosophy Advances in Proof-Theoretic Semantics

Introduction 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:

DlogT ( pq)T ( p), T (q)

T ( pq)T ( p)

T ( pq)T (q)

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:

T ( pq)(T ( p)T (q))

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 (fDlog) gives us the right-introduction rules for conjunction and

disjunction or, more precisely, those for T ( A), where A is a conjunction or disjunction. Definitional reflection (Dlog f-) gives us the left-introduction rules. The clause

for T ( pq) gives us the rules for implication, where the precise formulation of these rules depends on the exact formulation of the background logic governing ⇒.

Definitional reflection in general provides a much wider perspective on inversion principles than deductive logic alone. Using the definitional rule

t ∈ {x : a} ⇐ a[t /x ]

we obtain a principle of naive comprehension, which does not lead to a useless theory in which everything is derivable, even if we allow a to be the formula x/ x and t

the term {x : x/ x }. A definition of the form

p ⇐ ¬ p

yields a paraconsistent system in which both fp and f-¬ p are derivable, without every other formula being derivable. Formally, this means that the rule of cut

r f A A ,.6.f B

r, .6. fB

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'.

Found a mistake? Please highlight the word and press Shift + Enter
 Related topics