Verifications and uses with zippers

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 STELF 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 atm (⊃E (⊃E (⊃E (var x) $N_{1}$) $N_{2}$) $N_{3}$) in the natural deduction system is atm x (⊃E (⊃E (⊃E end $N_{1}$) $N_{2}$) $N_{3}$) in this version of “natural deduction” - the form of proofs stays the same with the exception that the head variable x has been pulled out into the front.

Propositions and rules

%sort prop %.
%sort atom %.
%block bl_atom {qp atom}%.
%term a %pi atom %-> prop %.
%term ⊃ %pi prop %-> prop %-> prop %.
%prec %right 9 ⊃ %.
%term ∧ %pi prop %-> prop %-> prop %.
%prec %right 8 ∧ %.
%sort hyp {_ prop} %.
%sort verif {_ prop} %.
%sort use {_ prop} {_ prop} %.
%block bl_hyp [A prop] {x hyp A}%.
%term end use A A %.
%term atm %pi (hyp A) %-> (use A (a Q)) %-> (verif (a Q)) %.
%term ⊃I %pi (%pi (hyp A) %-> (verif B)) %-> (verif (A ⊃ B)) %.
%term ⊃E %pi (use A (B₁ ⊃ B₂)) %-> (verif B₁) %-> (use A B₂) %.
%term ∧I %pi (verif A₁) %-> (verif A₂) %-> (verif (A₁ ∧ A₂)) %.
%term ∧E₁ %pi (use A (B₁ ∧ B₂)) %-> (use A B₁) %.
%term ∧E₂ %pi (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 A, we can verify the truth of A in any context where we can use the fact that A is true. In this system, however, we don’t ever use A in a vacuum - we always take a hypothesis of B and then prove that, given B, we can use A. The eta expansion theorem reflects this: it says that, for any A, given an arbitrary B that we have hypothesized to be true and a proof that we can use A given B, we can prove A.

The structure of the η-expansion theorem’s proof is then mostly unchanged from the system of verifications and uses.

%sort eta {A} {_ {B} %pi (hyp B) %-> (use B A) %-> (verif A)} %.
%mode eta %in %out %.
%term _ eta (a Q) ([B] [x] [r] atm x r) %.
%term _
  %pi (eta (A₁ ⊃ A₂) ([B] [x] [r] ⊃I ([y] N₂ B x (⊃E r (N₁ A₁ y end)))))
  %<- (eta A₁ ([B] %the (%pi (hyp B) %-> (use B A₁) %-> (verif A₁)) (N₁ B)))
  %<- (eta A₂ ([B] %the (%pi (hyp B) %-> (use B A₂) %-> (verif A₂)) (N₂ B))) %.
%term _
  %pi (eta (A₁ ∧ A₂) ([B] [x] [r] ∧I (N₁ B x (∧E₁ r)) (N₂ B x (∧E₂ r))))
  %<- (eta A₁ ([B] %the (%pi (hyp B) %-> (use B A₁) %-> (verif A₁)) (N₁ B)))
  %<- (eta A₂ ([B] %the (%pi (hyp B) %-> (use B A₂) %-> (verif A₂)) (N₂ B))) %.
%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 atm 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 hsubst_rn theorem where we do repeated reductions, and if the hypothesis is not, we call out to the hsubst_rr theorem where the structure of the use stays essentially the same.

%sort hsubst_n {A} {_ verif A} {_ %pi (hyp A) %-> (verif B)} {_ verif B} %.
%sort hsubst_rr {A} {_ verif A} {_ %pi (hyp A) %-> (use C B)} {_ use C B} %.
%sort hsubst_rn {A} {B} {_ verif A} {_ %pi (hyp A) %-> (use A B)} {_ verif B} %.
%mode hsubst_n %in %in %in %out %.
%mode hsubst_rr %in %in %in %out %.
%mode hsubst_rn %in %in %in %in %out %.
%term _
  %pi (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) (%the (verif B₂) (N y))) %.
%term _
  %pi (hsubst_n A M₀ ([x] ∧I (M₁ x) (M₂ x)) (∧I N₁ N₂))
  %<- (hsubst_n A M₀ ([x] M₁ x) (%the (verif B₁) N₁))
  %<- (hsubst_n A M₀ ([x] M₂ x) (%the (verif B₂) N₂)) %.
%term _ %pi (hsubst_n A M₀ ([x] atm x (R x)) N) %<- (hsubst_rn A (a Q) M₀ ([x] R x) N) %.
%term _
  %pi (hsubst_n A M₀ ([x] atm Y (R x)) (atm Y R'))
  %<- (hsubst_rr A M₀ ([x] R x) R') %.
%term _
  %pi (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) %.
%term _ %pi (hsubst_rr A M₀ ([x] ∧E₁ (R x)) (∧E₁ R')) %<- (hsubst_rr A M₀ ([x] R x) R') %.
%term _ %pi (hsubst_rr A M₀ ([x] ∧E₂ (R x)) (∧E₂ R')) %<- (hsubst_rr A M₀ ([x] R x) R') %.
%term _ hsubst_rr A M₀ ([x] end) end %.
%term _
  %pi (hsubst_rn A B₂ M₀ ([x] ⊃E (R x) (M x)) N')
  %<- (hsubst_rn A (B₁ ⊃ B₂) M₀ ([x] R x) (%the (verif (B₁ ⊃ B₂)) (⊃I ([y] N y))))
  %<- (hsubst_n A M₀ ([x] M x) (%the (verif B₁) M'))
  %<- (hsubst_n B₁ M' ([y] N y) (%the (verif B₂) N')) %.
%term _
  %pi (hsubst_rn A B₁ M₀ ([x] ∧E₁ (R x)) N₁)
  %<- (hsubst_rn A (B₁ ∧ B₂) M₀ ([x] R x) (%the (verif (B₁ ∧ B₂)) (∧I N₁ N₂))) %.
%term _
  %pi (hsubst_rn A B₂ M₀ ([x] ∧E₂ (R x)) N₂)
  %<- (hsubst_rn A _ M₀ ([x] R x) (%the (verif (B₁ ∧ B₂)) (∧I N₁ N₂))) %.
%term _ 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 _) %.