Home Philosophy Advances in Proof-Theoretic Semantics

## Explicit Composition and Its Application in Proofs of Normalization
## IntroductionThe rules of inference of a logical system define an inductive class of formal derivations. The most natural way to prove properties for the class is by induction on the construction of derivations, i.e., by induction on the last rule applied. It is often a crucial component in such proofs to show that the property in question is maintained under the composition of two derivations, even if this aspect is regularly ignored and the composability of derivations taken for granted. Results that show composition to maintain properties of derivations were called A formal implementation of the (2) A proof of strong normalization by bar induction. ## Notation for Natural DerivationsThe rules of natural deduction are production rules by which the class of formal derivations is defined inductively. Whenever there is such a definition, the most natural way to prove properties of the corresponding class is by induction on the last rule applied. This is so also in proof theory; a proof of normalization for intuitionistic natural deduction is given as a first example. For a uniform treatment, we use natural deduction with general elimination rules and the related notion of normal derivability in which the condition is that the major premisses of elimination rules have to be assumptions. The modified rules are, with the multiplicity The normalizability result to be presented can be worked out also for the standard rules that can be seen as special cases of the general ones (Table 2). It will be convenient in this situation to leave out the degenerate derivations of the minor premisses, to have exactly the Gentzenian rules. In the standard tree notation for natural derivations, as above, the composition of two derivations can be indicated schematically, as in:
.
.
.
.
, ⊃, ∀ 1 1 1 1
.
&
.
.
1
A
B
xA A (t /x ) ⊃ Composition has the condition that the eigenvariables and discharge labels of the two derivations be distinct, if not, they can be changed. No trace is left of the composition in the rightmost derivation. As the calculus is defined by its logical rules, composition in natural deduction is usually left implicit. To represent the composition of two derivations formally and to reason about its properties in a convenient form, we write the logical rules and the additional rule of composition in More formally, we define a root-first translation into sequent calculus style. If the last rule is &
. .
∨ I
1
.
B ⊃ I,1 '"V A ,Γ → B I
The translation continues from the premisses until assumptions are reached. The logical rules of the calculus
Γ Γ , Δ Γ , Δ Γ → B I2Γ , Δ ,Θ Γ Γ , Δ ,Θ Γ Γ , Δ Γ Γ
Γ , Δ Natural deduction in sequent style The calculus is completed by adding initial sequents of the form an arbitrary formula, and the zero-premiss rule ⊥ derivation branch. We say that the closing of an assumption formula in
Vacuous and multiple closing of assumptions is seen in: 1 1
.
.
The former case corresponds to the situation in sequent calculus in which a formula active in a logical rule stems from a step of weakening, the latter to a situation in which it stems from a step of contraction, as shown in von Plato (2001) [5]. The composition of two derivations is an essential step in the normalization of derivations. It can now be written quite generally in the form:
Iterated compositions appear as so many successive instances of rule In a of the general rules is that such conversions work for all derived major premisses of elimination rules:
As a first step towards normalization, we need to show that derivations in natural deduction can be composed:
→ C, the instance of Comp can be eliminated.
that it can be eliminated. 1. Base case. The second premiss of
The conclusion of If the second premiss is of the form ⊥ not been derived by a right rule, so that 2. Inductive case with the second premiss of
Rule
3. Inductive case with the second premiss of
&
As in case 2, In the case of a multiple discharge, a detour conversion will lead to several compositions, with a multiplication of the contexts as in the example
I
, A , B ,Θ → &C E
The conversion is into
Such multiplication does not affect the normalization process. Note well that normalization depends on the admissibility of composition which latter has to be proved
In normalization, derived major premisses of
The idea of our proof of the normalization theorem is to show by induction on the last rule applied in a derivation that logical rules maintain normalizability. The cut elimination theorem is often called
1.
& By the inductive hypothesis, the derivations of the premisses of the last rule are normalizable. The second instance of &
&
The height of derivation of the major premiss of the last rule instance in the upper derivation has diminished by 1, so the subderivation down to that rule instance is normalizable. The height of the major premiss of the other rule instance has remained intact and therefore normalizability follows. All other cases of permutative convertibility go through in the same way. 2. 2.1. Detour convertibility on &:
I
&
Let us assume for the time being that
The result is not a derivation in
and it is taken in place of the original conclusion called a 'simplification convertibility' in Prawitz (1965) [3]. In all cases, the result of conversion is uniquely defined. 2.2. Detour convertibility on ∨. There are two cases, as in:
As in 2.1, assume for the time being that
The multiplicities are treated as in 2.1, except for the case of
There is a conversion, but it is not uniquely defined: Either one of the original minor premisses of ∨ with composition formula 2.3. Detour convertibility on ⊃
In the conversion, multiple discharge of assumptions is again resolved into iterated compositions, so we may assume
If
2.4. Detour convertibility on ∀:
As before, assume for the time being that of
The multiplicities are treated as before. 2.5. Detour convertibility on ∃:
As before, assume for the time being that
Multiplicities are treated as before. QED. It remains to give a proof of the
1.
Rule
In the end, the second premiss of
The conclusion of 2. in the proof of admissibility of composition. 3. as in 1. If
&
,Δ → C Comp
→ A & B Comp
&
The other cases of composition formulas are treated in a similar way. QED. Lemma 1, closure of derivations with respect to composition, merely shows that a derivation in natural deduction can be got from two composable derivations. The |

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

Related topics |

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