%{ In the [[verifications and uses]] article we saw a typical presentation of a logic of verifications and uses, and in article on [[hereditary substitution with zippers]] we saw an attempt to clean up the "ugly part" of that proof by defining a zipper-like structure over terms. The reason that global soundness for this system did not hold is that Twelf could not verify (without the use of a [[structural metric]]) that a "zipped" use was the same size as an "unzipped" use, so [[termination checking]] failed when a recursive
call was made on a term that had been unzipped. 

In this article, we give a different solution. This system has something of the flavor of a [[spine form]] presentation; however, as we discussed in the 
[[hereditary substitution with zippers]], it is still much closer to a natural deduction system - the analogue of the natural deduction term <tt>atm (⊃E (⊃E (⊃E (var x) N<sub>1</sub>) N<sub>2</sub>)
N<sub>3</sub>)</tt> in the natural deduction system is 
<tt>atm x (⊃E (⊃E (⊃E end N<sub>1</sub>) N<sub>2</sub>) N<sub>3</sub>)</tt> in this version of "natural deduction" - the form of proofs stays the same
with the exception that the head variable <tt>x</tt> has been pulled out into the front. }%

%{ == Propositions and rules == }%

prop : type.
atom : type.
%block bl_atom : block {qp : atom}.

a : atom -> prop.
⊃ : prop -> prop -> prop. %infix right 9 ⊃.
∧ : prop -> prop -> prop. %infix right 8 ∧.

hyp   : prop -> type.
verif : prop -> type.
use   : prop -> prop -> type.
%block bl_hyp : some {A : prop} block {x : hyp A}.

end : use A A.
atm : hyp A -> use A (a Q) -> verif (a Q).
⊃I  : (hyp A -> verif B) -> verif (A ⊃ B).
⊃E  : use A (B₁ ⊃ B₂) -> verif B₁ -> use A B₂.
∧I  : verif A₁ -> verif A₂ -> verif (A₁ ∧ A₂).
∧E₁ : use A (B₁ ∧ B₂) -> use A B₁.
∧E₂ : use A (B₁ ∧ B₂) -> use A B₂.

%{ == Global completeness == }%

%{ Because we have changed the logic, the η-expansion theorem has changed somewhat. Recall that, in the pure system of [[verifications and uses]], the statement of global completeness/η-expansion was that, for all <tt>A</tt>, we can verify the truth of <tt>A</tt> in any context where we can use the fact that <tt>A</tt> is true. In this system, however, we don't ever use <tt>A</tt> in a vacuum - we always take a hypothesis of <tt>B</tt> and then prove that, given <tt>B</tt>, we can use <tt>A</tt>.
The eta expansion theorem reflects this: it says that, for any <tt>A</tt>, given an arbitrary <tt>B</tt> that we have hypothesized to be true and a proof
that we can use <tt>A</tt> given <tt>B</tt>, we can prove <tt>A</tt>.

The structure of the η-expansion theorem's proof is then mostly unchanged from the system of [[verifications and uses]]. }%

eta : {A} ({B} hyp B -> use B A -> verif A) -> type.
%mode eta +A -B.

- : eta (a Q) ([B][x][r] atm x r).
- : eta (A₁ ⊃ A₂) ([B][x][r] ⊃I [y] N₂ B x (⊃E r (N₁ A₁ y end)))
     <- eta A₁ ([B] N₁ B : hyp B -> use B A₁ -> verif A₁)
     <- eta A₂ ([B] N₂ B : hyp B -> use B A₂ -> verif A₂).
- : eta (A₁ ∧ A₂) ([B][x][r] ∧I (N₁ B x (∧E₁ r)) (N₂ B x (∧E₂ r)))
     <- eta A₁ ([B] N₁ B : hyp B -> use B A₁ -> verif A₁)
     <- eta A₂ ([B] N₂ B : hyp B -> use B A₂ -> verif A₂).

%worlds (bl_atom | bl_hyp) (eta _ _).
%total A (eta A _).

%{ Let's see some examples of η-expansions: | check = decl }%

%solve _ : {q1}{q2}{q3} eta (a q1 ⊃ a q2 ⊃ a q3) (X q1 q2 q3).

%{ | check = decl }%

%solve _ : {q1}{q2}{q3} eta ((a q1 ⊃ a q2) ⊃ a q3) (X q1 q2 q3).

%{ == Global soundness == }%

%{ The real benefit of this modified natural deduction system is that we no longer need to take any detours to prove the hereditary substitution theorem: when we reach
the <tt>atm</tt> case where we must verify an atomic proposition by using a proof of its truth, we know exactly what hypothesis we are using. If the
hypothesis is the one we're substituting for, then we call out to the <tt>hsubst_rn</tt> theorem where we do repeated reductions, and if the hypothesis
is not, we call out to the <tt>hsubst_rr</tt> theorem where the structure of the use stays essentially the same. }%

hsubst_n  : {A}    verif A -> (hyp A -> verif B) -> verif B -> type.
hsubst_rr : {A}    verif A -> (hyp A -> use C B) -> use C B -> type.
hsubst_rn : {A}{B} verif A -> (hyp A -> use A B) -> verif B -> type.
%mode hsubst_n  +A    +M₀ +M -N.
%mode hsubst_rr +A    +M₀ +R -R'.
%mode hsubst_rn +A +B +M₀ +R -N.

- : hsubst_n A M₀ ([x] ⊃I [y] M x y) (⊃I [y] N y)
     <- {y : hyp B₁} hsubst_n A M₀ ([x] M x y) (N y : verif B₂).
- : hsubst_n A M₀ ([x] ∧I (M₁ x) (M₂ x)) (∧I N₁ N₂)
     <- hsubst_n A M₀ ([x] M₁ x) (N₁ : verif B₁)
     <- hsubst_n A M₀ ([x] M₂ x) (N₂ : verif B₂).
- : hsubst_n A M₀ ([x] atm x (R x)) N
     <- hsubst_rn A (a Q) M₀ ([x] R x) N.
- : hsubst_n A M₀ ([x] atm Y (R x)) (atm Y R')
     <- hsubst_rr A M₀ ([x] R x) R'.

- : hsubst_rr A M₀ ([x] ⊃E (R x) (M x)) (⊃E R' N)
     <- hsubst_rr A M₀ ([x] R x) R' 
     <- hsubst_n A M₀ ([x] M x) N.
- : hsubst_rr A M₀ ([x] ∧E₁ (R x)) (∧E₁ R')
     <- hsubst_rr A M₀ ([x] R x) R'.
- : hsubst_rr A M₀ ([x] ∧E₂ (R x)) (∧E₂ R')
     <- hsubst_rr A M₀ ([x] R x) R'.
- : hsubst_rr A M₀ ([x] end) end.

- : hsubst_rn A B₂ M₀ ([x] ⊃E (R x) (M x)) N'
     <- hsubst_rn A (B₁ ⊃ B₂) M₀ ([x] R x) ((⊃I [y] N y) : verif (B₁ ⊃ B₂))
     <- hsubst_n A M₀ ([x] M x) (M' : verif B₁)
     <- hsubst_n B₁ M' ([y] N y) (N' : verif B₂).
- : hsubst_rn A B₁ M₀ ([x] ∧E₁ (R x)) N₁
     <- hsubst_rn A (B₁ ∧ B₂) M₀ ([x] R x) (∧I N₁ N₂ : verif (B₁ ∧ B₂)).
- : hsubst_rn A B₂ M₀ ([x] ∧E₂ (R x)) N₂
     <- hsubst_rn A _ M₀ ([x] R x) (∧I N₁ N₂ : verif (B₁ ∧ B₂)).
- : hsubst_rn A A M₀ ([x] end) M₀.

%worlds (bl_atom | bl_hyp)
(hsubst_n _ _ _ _)
(hsubst_rr _ _ _ _) 
(hsubst_rn _ _ _ _ _).

%reduces B <= A (hsubst_rn A B _ _ _).

%total {(A B C) (M R S)}
(hsubst_n A _ M _)
(hsubst_rr B _ R _) 
(hsubst_rn C _ _ S _).