4.4 The consistency of Heyting arithmetic
4.4.2 Properties of derivations
4.4.3 Denition. A thread in a derivation is a sequence of sequents in a derivation, for which the following holds:
1. It begins with an initial sequent or the conclusion of an arith-metical rule without premises.
2. Every sequent but the last one is a premise of a rule and the sequent is followed by the conclusion of that rule.
4.4.4 Lemma. Assume thatS1is a sequent in a derivationP. LetP1
be the subderivation ending withS1 and letP10 be another derivation ending with S1. Now let P0 be the derivation that results from the process of substitutingP10 forP1 inP.
If o(S1;P0)< o(S1;P), theno(P0)< o(P).
Proof. For every thread in P passing through S1 we show that the following holds: If S is a sequent in a thread at or belowS1 and if S0 is the corresponding sequent toS in P0, then o(S0;P0)< o(S;P). According to the assumption the proposition holds if S =S1. The heights of the sequents belowS in P andS0 in P0 are the same and for every ordinalα, βandγthat satisfyα < β, we haveα#γ < β#γ. Thus, the inequality is retained for every rule applied. If we then let S be the end-sequent of the derivation we obtain the inequality for the derivations.
4.4. The consistency of Heyting arithmetic 49 4.4.5 Lemma. In a derivation we can permute the order of the rules and rst apply the arithmetical rules and thenIndand the logical and structural rules.
Proof. If we have a logical rule followed by an arithmetical rule, then the arithmetical rule is not applied on the principal formula of the logical rule, since this formula is compound. Hence, we can permute the order of the rules and apply the arithmetical rule rst.
Assume that we have an instance of contraction followed by an arithmetical rule. If the arithmetical rule is not applied on the con-traction formula, then we can permute the order of the rules. We now consider the case that the arithmetical rule is applied on the contrac-tion formula. If the arithmetical rule is a one-premise rule, then we can apply the arithmetical rule on each copy of the formula followed by an instance of contraction. If on the other hand the arithmetical rule has two premises, that is, if the rule is an instance of transitivity, then we can apply transitivity on each copy of the formula, multiply-ing the derivation of the other transitivity premise, and then apply contraction on the principal formula of the transitivity and also on possible formulas in the context of the multiplied premise.
If we have an instance of Cut followed by an arithmetical rule, then we can permute the order of the rules and the same holds for an instance ofInd followed by an arithmetical rule.
Note that this change in the order of the rules can increase the ordinal of the derivation.
4.4.6 Lemma. (i) For an arbitrary closed term t there exists a numeral n such that → t = n can be derived without Ind or Cut.
(ii) Let t and t0 be closed terms for which →t=t0 can be derived without Ind or Cut and let q be an arbitrary term. Now the sequent→q(t/x) =q(t0/x)is derivable withoutInd or Cut.
(iii) Let t and t0 be closed terms for which →t=t0 can be derived withoutInd or Cut and letqandrbe terms. Then the sequent q(t/x) =r(t/x)→q(t0/x) =r(t0/x)can be derived withoutInd or Cut.
50 4. A direct Gentzen-style consistency proof in HA (iv) Let t and t0 be closed terms for which → t = t0 can be de-rived without Indor Cut. Then for an arbitrary formulaAthe sequent A(t/x)→A(t0/x)can be derived without Indor Cut.
Proof. (i) For the constant 0the proposition holds. Assume that the proposition holds for the closed termstandt0, that is there are n and m, such that → t = n and → t0 = m can be de-rived withoutInd or Cut. Then the sequent →s(t) =s(n)is derivable withsRepwheres(n)≡n+ 1. on the conclusions of these derivations we get the result → t+t0 =n+m.
The sequent→t·t0=n·mis derivable in a similar manner.
(ii) If q is the constant 0 or a variable dierent fromx, then the sequent is derivable with Ref. If q is the variable x, then we already have the derivation according to the assumption. Now assume that q ≡ s(q0)and as induction hypothesis we have a derivation of→q0(t/x) =q0(t0/x)that fullls the requirements.
Then we get→s(q0(t/x)) =s(q0(t0/x))withsRep. Ifq≡q0+q00 we get the following derivation where we write q0(t)and q00(t) instead ofq0(t/x)andq00(t/x)and the sequent arrow is left out.
q0(t) =q0(t0)
q0(t) +q00(t) =q0(t0) +q00(t) +Rep1
q00(t) =q00(t0)
q0(t0) +q00(t) =q0(t0) +q00(t0) +Rep2 q0(t) +q00(t) =q0(t0) +q00(t0) T r
4.4. The consistency of Heyting arithmetic 51 Ifq≡q0·q00 the derivation is similar.
(iii) According to point (ii) we have derivations of → q(t) =q(t0) and →r(t) = r(t0)that fulll the requirements. We can now construct the derivation:
→q(t) =q(t0)
→q(t0) =q(t) Sym q(t) =r(t)→q(t) =r(t)
q(t) =r(t)→q(t0) =r(t) T r →r(t) =r(t0) q(t) =r(t)→q(t0) =r(t0) T r
(iv) The proof is carried out by induction on the complexity of the formula. If A is an atomic formula, then the proposition is proved in case (iii).
IfA≡B&Cand we as induction hypothesis have thatB(t/x)→ B(t0/x) and C(t/x) → C(t0/x) are derivable without Ind or Cut, then we get the derivation:
B(t/x)→B(t0/x) C(t/x)→C(t0/x) B(t/x), C(t/x)→B(t0/x)&C(t0/x) R&
B(t/x)&C(t/x)→B(t0/x)&C(t0/x) L&
Assume thatA ≡ ∀yB. Ifx ≡y then xis not free in A and A(t/x) → A(t0/x) is an initial sequent. On the other hand if x is not y, then we have by the induction hypothesis that (B(z/y))(t/x)→(B(z/y))(t0/x), where x6=z, can be derived withoutIndor Cut. Becausetandt0are closed terms, they do not containyand we may change the order of the substitutions, that is (B(z/y))(t/x) = (B(t/x))(z/y) and (B(z/y))(t0/x) = (B(t0/x))(z/y). We now get the derivation:
(B(t/x))(z/y)→(B(t0/x))(z/y)
∀yB(t/x)→(B(t0/x))(z/y) L∀
∀yB(t/x)→ ∀yB(t0/x) R∀
The other cases are similar.
52 4. A direct Gentzen-style consistency proof in HA In point (i) of the lemma, we only state the existence of a numeral that equals the closed term, not that this numeral is unique. The uniqueness of the numeral is equivalent to the consistency of simple derivations proved in lemma 4.4.20.