Chuangjie Xu, January 2016

We explore the Dialectica interpretation of first order logic into
Martin-Löf type theory (in Agda notation).

The idea of the Dialectica interpretation is that each formula A is
transformed to a classically equivalent one of the form ∃x.∀y.|A|
where with ∣A∣ quantifier-free.

In this study, the language to interpret is a subset of Agda equipped
with a first order logic.  We adopt the inference rules of the system
IL from Oliva[1] to define the interpreted logic.  The Dialectica
interpretation is slightly adapted for dependent types as in Bauer[2].

References.

[1] Paulo Oliva, Unifying Functional Interpretation.  Notre Dame
    Journal of Formal Logic 47 (2):263-290, 2006.

[2] Andrej Bauer, The Dialectica interpretation in Coq.  Available at
    http://math.andrej.com/2011/01/03/the-dialectica-interpertation-in-coq/

\begin{code}

module Dialectica where

open import Preliminaries

\end{code}

The term language is the full hierarchy of finite types in which every
type is inhabited.

\begin{code}

infixr  _⊗_
infixr  _⇾_

data Ty : Set where
 Ⓝ : Ty
 _⊗_ : Ty → Ty → Ty
 _⇾_ : Ty → Ty → Ty

⟦_⟧ : Ty → Set
⟦ Ⓝ ⟧ = ℕ
⟦ σ ⊗ τ ⟧ = ⟦ σ ⟧ × ⟦ τ ⟧
⟦ σ ⇾ τ ⟧ = ⟦ σ ⟧ → ⟦ τ ⟧

⟦inhabitant⟧ : {σ : Ty} → ⟦ σ ⟧
⟦inhabitant⟧ {Ⓝ} = 
⟦inhabitant⟧ {σ ⊗ τ} = ⟦inhabitant⟧ , ⟦inhabitant⟧
⟦inhabitant⟧ {σ ⇾ τ} = λ _ → ⟦inhabitant⟧

\end{code}

We inductively define a first order logic on the full type hierarchy
consisting of types Prp of propositions and Prf of proofs.

Notice that predicates are represented as (Agda) functions into Prp.
This forces us to adapt the original Dialectica interpretation by
introducing certain type dependencies.

\begin{code}

infix  _==_
infix  _∧_
infix  _⇒_

data Prp : Set where
 _==_ : {σ : Ty} → ⟦ σ ⟧ → ⟦ σ ⟧ → Prp
 _∧_ : Prp → Prp → Prp
 _⇒_ : Prp → Prp → Prp
 ∀′ : {σ : Ty} → (⟦ σ ⟧ → Prp) → Prp
 ∃′ : {σ : Ty} → (⟦ σ ⟧ → Prp) → Prp

\end{code}

An element of Prf Γ A represents a proof of A under the assumption Γ
where an assumption is simply a list of propositions.

Each constructor represents an inference rule. For example,

      Γ ⊢ A         Δ ⊢ B
    ----------------------- ∧-intro
         Γ , Δ ⊢ A ∧ B

is represented by the constructor

 ∧-intro : {Γ Δ : Asmpt} {A B : Prp}
         → Prf Γ A → Prf Δ B → Prf (Γ ₊₊ Δ) (A ∧ B)

Notice that the constructors J and ind should have more general
assumptions.  We work with the ones in empty assumption for simplicity.

\begin{code}

Asmpt : Set
Asmpt = List Prp

data Prf : Asmpt → Prp → Set where
 refl : {σ : Ty} {a : ⟦ σ ⟧}
      → Prf ε (a == a)
 J    : {σ : Ty} (φ : ⟦ σ ⟧ → ⟦ σ ⟧ → Prp)
      → ((a : ⟦ σ ⟧) → Prf ε (φ a a))
      → {a b : ⟦ σ ⟧} → Prf ε (a == b) → Prf ε (φ a b)
 id   : {A : Prp}
      → Prf (ε ₊ A) A
 wkn  : {Γ : Asmpt} {A B : Prp}
      → Prf Γ B → Prf (Γ ₊ A) B
 cut  : {Γ Δ : Asmpt} {A B : Prp}
      → Prf (Γ ₊ A) B → Prf Δ A → Prf (Γ ₊₊ Δ) B
 swap : {Γ : Asmpt} (Δ : Asmpt) {A B C : Prp}
      → Prf (Γ ₊ A ₊ B ₊₊ Δ) C → Prf (Γ ₊ B ₊ A ₊₊ Δ) C
 ∧-intro : {Γ Δ : Asmpt} {A B : Prp}
         → Prf Γ A → Prf Δ B → Prf (Γ ₊₊ Δ) (A ∧ B)
 ∧-elim₀ : {Γ : Asmpt} {A B : Prp}
         → Prf Γ (A ∧ B) → Prf Γ A
 ∧-elim₁ : {Γ : Asmpt} {A B : Prp}
         → Prf Γ (A ∧ B) → Prf Γ B
 ⇒-intro : {Γ : Asmpt} {A B : Prp}
         → Prf (Γ ₊ A) B → Prf Γ (A ⇒ B)
 ⇒-elim  : {Γ : Asmpt} {A B : Prp}
         → Prf Γ (A ⇒ B) → Prf (Γ ₊ A) B
 ∀-intro : {Γ : Asmpt} {σ : Ty} {φ : ⟦ σ ⟧ → Prp}
         → ((x : ⟦ σ ⟧) → Prf Γ (φ x)) → Prf Γ (∀′ φ)
 ∀-elim  : {Γ : Asmpt} {σ : Ty} {φ : ⟦ σ ⟧ → Prp}
         → Prf Γ (∀′ φ) → (a : ⟦ σ ⟧) → Prf Γ (φ a)
 ∃-intro : {Γ : Asmpt} {σ : Ty} {φ : ⟦ σ ⟧ → Prp}
         → (a : ⟦ σ ⟧) → Prf Γ (φ a) → Prf Γ (∃′ φ)
 ∃-elim  : {Γ : Asmpt} {σ : Ty} {φ : ⟦ σ ⟧ → Prp} {A : Prp}
         → ((x : ⟦ σ ⟧) → Prf Γ (φ x ⇒ A)) → Prf Γ ((∃′ φ) ⇒ A)
 ind : (φ : ℕ → Prp)
     → Prf ε (φ ) → Prf ε (∀′ (λ n → φ n ⇒ φ (succ n))) → Prf ε (∀′ φ)

\end{code}

Our goal is to transform each proposition A into a type Σx.Πy.∣A∣.  To
determine the types of x and y, we assign to each proposition A types
d⁺(A) and d⁻(A), where d⁺(A) is intended to be the type of a realizer
to be extracted from a proof of A and d⁻(A) is the type of a challenge
for the claim that this term realizes A.

The types of realizers and challenges are inhabited.  We make a
canonical choice of an inhabitant of each type.

\begin{code}

d⁺ d⁻ : Prp → Set
d⁺ (u == v) = 𝟙
d⁺ (A ∧ B) = (d⁺ A) × (d⁺ B)
d⁺ (A ⇒ B) = (d⁺ A → d⁺ B) × (d⁺ A → d⁻ B → d⁻ A)
d⁺ (∀′ {σ} φ) = (x : ⟦ σ ⟧) → d⁺ (φ x)
d⁺ (∃′ {σ} φ) = Σ \(x : ⟦ σ ⟧) → d⁺ (φ x)
d⁻ (u == v) = 𝟙
d⁻ (A ∧ B) = (d⁻ A) × (d⁻ B)
d⁻ (A ⇒ B) = (d⁺ A) × (d⁻ B)
d⁻ (∀′ {σ} φ) = Σ \(x : ⟦ σ ⟧) → d⁻ (φ x)
d⁻ (∃′ {σ} φ) = (x : ⟦ σ ⟧) → d⁺ (φ x) → d⁻ (φ x)

inhabitant⁺ : (A : Prp) → d⁺ A
inhabitant⁻ : (A : Prp) → d⁻ A
inhabitant⁺ (u == v) = ⋆
inhabitant⁺ (A ∧ B) = inhabitant⁺ A , inhabitant⁺ B
inhabitant⁺ (A ⇒ B) = (λ _ → inhabitant⁺ B) , (λ _ _ → inhabitant⁻ A)
inhabitant⁺ (∀′ φ) = λ x → inhabitant⁺ (φ x)
inhabitant⁺ (∃′ φ) = ⟦inhabitant⟧ , inhabitant⁺ (φ ⟦inhabitant⟧)
inhabitant⁻ (u == v) = ⋆
inhabitant⁻ (A ∧ B) = inhabitant⁻ A , inhabitant⁻ B
inhabitant⁻ (A ⇒ B) = inhabitant⁺ A , inhabitant⁻ B
inhabitant⁻ (∀′ φ) = ⟦inhabitant⟧ , inhabitant⁻ (φ ⟦inhabitant⟧)
inhabitant⁻ (∃′ φ) = λ x _ → inhabitant⁻ (φ x)

dd⁺ dd⁻ : Asmpt → Set
dd⁺ Γ = (i : Index Γ) → d⁺ (Γ ₍ i ₎)
dd⁻ Γ = (i : Index Γ) → d⁻ (Γ ₍ i ₎)

iA⁺ : (Γ : Asmpt) → dd⁺ Γ
iA⁺ Γ i = inhabitant⁺ (Γ ₍ i ₎)

iA⁻ : (Γ : Asmpt) → dd⁻ Γ
iA⁻ Γ i = inhabitant⁻ (Γ ₍ i ₎)

\end{code}

The dialectica interpretation (of propositions and assumptions)

\begin{code}

∣_∣ : (φ : Prp) → d⁺ φ → d⁻ φ → Set
∣ u == v ∣ _ _ = u ≡ v
∣ A ∧ B ∣ (t₀ , t₁) (y₀ , y₁)  = ∣ A ∣ t₀ y₀ × ∣ B ∣ t₁ y₁
∣ A ⇒ B ∣ (t₀ , t₁) (y₀ , y₁) = ∣ A ∣ y₀ (t₁ y₀ y₁) → ∣ B ∣ (t₀ y₀) y₁
∣ ∀′ φ ∣ t (a , y) =  ∣ φ a ∣ (t a) y
∣ ∃′ φ ∣ (a , t) y = ∣ φ a ∣ t (y a t)

∥_∥ : (Γ : Asmpt) → dd⁺ Γ → dd⁻ Γ → Set
∥ ε ∥ _ _ = 𝟙
∥ Γ ₊ X ∥ xs rs = ∥ Γ ∥ (xs ∘ succ) (rs ∘ succ) × ∣ X ∣ (xs zero) (rs zero)

\end{code}

The soundness theorem says that each proof of a proposition A in the
interpreted logic is transformed to an element of type Σt.Πy.∣A∣(t,y)
in Agda.  Since we work more generally with proofs in assumptions, the
theorem is generalized to the following.

\begin{code}

Prfᴬ : Set → Set → Set
Prfᴬ Γ A = Γ → A

Thm[soundness] : {Γ : Asmpt} {A : Prp} → Prf Γ A
               → (xs : dd⁺ Γ) → Σ \(t : d⁺ A) → (y : d⁻ A) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∣ t y)

\end{code}

The proof of Thm[soundness] is placed in the end of this file.  It's
done by induction on Prf.  We prove the cases (corresponding to the
constructors of Prf) one by one.

For this, we need the following auxiliary functions and lemmas of assumptions.

\begin{code}

pr₀ᴸ⁺ : {Γ : Asmpt} (Δ : Asmpt) → dd⁺ (Γ ₊₊ Δ) → dd⁺ Γ
pr₀ᴸ⁺ ε xs = xs
pr₀ᴸ⁺ (Δ ₊ _) xs = pr₀ᴸ⁺ Δ (xs ∘ succ)

pr₁ᴸ⁺ : {Γ : Asmpt} (Δ : Asmpt) → dd⁺ (Γ ₊₊ Δ) → dd⁺ Δ
pr₁ᴸ⁺ ε xs ()
pr₁ᴸ⁺ (Δ ₊ X) xs zero = xs zero
pr₁ᴸ⁺ (Δ ₊ X) xs (succ i) = pr₁ᴸ⁺ Δ (xs ∘ succ) i

pairᴸ⁺ : {Γ : Asmpt} (Δ : Asmpt) → dd⁺ Γ → dd⁺ Δ → dd⁺ (Γ ₊₊ Δ)
pairᴸ⁺ ε rs₀ rs₁ = rs₀
pairᴸ⁺ (Δ ₊ _) rs₀ rs₁ zero = rs₁ zero
pairᴸ⁺ (Δ ₊ _) rs₀ rs₁ (succ i) = pairᴸ⁺ Δ rs₀ (rs₁ ∘ succ) i

pr₀ᴸ⁻ : {Γ : Asmpt} (Δ : Asmpt) → dd⁻ (Γ ₊₊ Δ) → dd⁻ Γ
pr₀ᴸ⁻ ε xs = xs
pr₀ᴸ⁻ (Δ ₊ _) xs = pr₀ᴸ⁻ Δ (xs ∘ succ)

pr₁ᴸ⁻ : {Γ : Asmpt} (Δ : Asmpt) → dd⁻ (Γ ₊₊ Δ) → dd⁻ Δ
pr₁ᴸ⁻ ε xs ()
pr₁ᴸ⁻ (Δ ₊ X) xs zero = xs zero
pr₁ᴸ⁻ (Δ ₊ X) xs (succ i) = pr₁ᴸ⁻ Δ (xs ∘ succ) i

pairᴸ⁻ : {Γ : Asmpt} (Δ : Asmpt) → dd⁻ Γ → dd⁻ Δ → dd⁻ (Γ ₊₊ Δ)
pairᴸ⁻ ε rs₀ rs₁ = rs₀
pairᴸ⁻ (Δ ₊ _) rs₀ rs₁ zero = rs₁ zero
pairᴸ⁻ (Δ ₊ _) rs₀ rs₁ (succ i) = pairᴸ⁻ Δ rs₀ (rs₁ ∘ succ) i

∥₊₊∥→× : {Γ : Asmpt} (Δ : Asmpt) (xs : dd⁺ (Γ ₊₊ Δ)) (rs₀ : dd⁻ Γ) (rs₁ : dd⁻ Δ)
      → ∥ Γ ₊₊ Δ ∥ xs (pairᴸ⁻ Δ rs₀ rs₁) → ∥ Γ ∥ (pr₀ᴸ⁺ Δ xs) rs₀ × ∥ Δ ∥ (pr₁ᴸ⁺ Δ xs) rs₁
∥₊₊∥→× ε xs rs₀ rs₁ ρ = ρ , ⋆
∥₊₊∥→× (Δ ₊ _) xs rs₀ rs₁ (ρ , x) = pr₀ IH , pr₁ IH , x
 where
  IH = ∥₊₊∥→× Δ (xs ∘ succ) rs₀ (rs₁ ∘ succ) ρ

×→∥₊₊∥ : {Γ : Asmpt} (Δ : Asmpt) (xs : dd⁺ (Γ ₊₊ Δ)) (rs : dd⁻ (Γ ₊₊ Δ))
      → ∥ Γ ∥ (pr₀ᴸ⁺ Δ xs) (pr₀ᴸ⁻ Δ rs) × ∥ Δ ∥ (pr₁ᴸ⁺ Δ xs) (pr₁ᴸ⁻ Δ rs) → ∥ Γ ₊₊ Δ ∥ xs rs
×→∥₊₊∥ ε xs rs (ρ , ⋆) = ρ
×→∥₊₊∥ (Δ ₊ _) xs rs (γ , δ , x) = ×→∥₊₊∥ Δ (xs ∘ succ) (rs ∘ succ) (γ , δ) , x

swap⁺ : {Γ : Asmpt} (Δ : Asmpt) {A B : Prp}
      → dd⁺ (Γ ₊ A ₊ B ₊₊ Δ) → dd⁺ (Γ ₊ B ₊ A ₊₊ Δ)
swap⁺ ε xs zero = xs (succ zero)
swap⁺ ε xs (succ zero) = xs zero
swap⁺ ε xs (succ (succ i)) = xs (succ (succ i))
swap⁺ (Δ ₊ _) xs zero = xs zero
swap⁺ (Δ ₊ _) xs (succ i) = swap⁺ Δ (xs ∘ succ) i

swap⁻ : {Γ : Asmpt} (Δ : Asmpt) {A B : Prp}
      → dd⁻ (Γ ₊ A ₊ B ₊₊ Δ) → dd⁻ (Γ ₊ B ₊ A ₊₊ Δ)
swap⁻ ε xs zero = xs (succ zero)
swap⁻ ε xs (succ zero) = xs zero
swap⁻ ε xs (succ (succ i)) = xs (succ (succ i))
swap⁻ (Δ ₊ _) xs zero = xs zero
swap⁻ (Δ ₊ _) xs (succ i) = swap⁻ Δ (xs ∘ succ) i

∥swap∥→× : {Γ : Asmpt} (Δ : Asmpt) {A B : Prp}
         → (xs : dd⁺ (Γ ₊ B ₊ A ₊₊ Δ)) (rs' : dd⁻ (Γ ₊ A ₊ B ₊₊ Δ))
         → ∥ Γ ₊ B ₊ A ₊₊ Δ ∥ xs (swap⁻ Δ rs')
         → ((∥ Γ ∥ (pr₀ᴸ⁺ Δ (swap⁺ Δ xs) ∘ succ ∘ succ) (pr₀ᴸ⁻ Δ rs' ∘ succ ∘ succ) ×
             ∣ B ∣ (pr₀ᴸ⁺ Δ (swap⁺ Δ xs) zero) (pr₀ᴸ⁻ Δ rs' zero)) ×
            ∣ A ∣ (pr₀ᴸ⁺ Δ (swap⁺ Δ xs) (succ zero)) (pr₀ᴸ⁻ Δ rs' (succ zero))) ×
           ∥ Δ ∥ (pr₁ᴸ⁺ Δ (swap⁺ Δ xs)) (pr₁ᴸ⁻ Δ rs')
∥swap∥→× ε xs rs' ρ = ρ , ⋆
∥swap∥→× (Δ ₊ _) xs rs' (ρ , x) = pr₀ IH , pr₁ IH , x
 where
  IH = ∥swap∥→× Δ (xs ∘ succ) (rs' ∘ succ) ρ

\end{code}

The cases of reflexivity and the J-eliminator

\begin{code}

case-refl : {σ : Ty} {a : ⟦ σ ⟧}
          → (_ : dd⁺ ε) → Σ \(t : d⁺ (a == a)) → (y : d⁻ (a == a)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ a == a ∣ t y)
case-refl _ = ⋆ , (λ _ → (λ()) , (λ _ → refl))

case-J : {σ : Ty} (φ : ⟦ σ ⟧ → ⟦ σ ⟧ → Prp)
       → ((a : ⟦ σ ⟧) → (_ : dd⁺ ε) → Σ \(t : d⁺ (φ a a)) → (y : d⁻ (φ a a)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ φ a a ∣ t y))
       → {a b : ⟦ σ ⟧} → ((_ : dd⁺ ε) → Σ \(t : d⁺ (a == b)) → (y : d⁻ (a == b)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ a == b ∣ t y))
       → (_ : dd⁺ ε) → Σ \(t : d⁺ (φ a b)) → (y : d⁻ (φ a b)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ φ a b ∣ t y)
case-J {σ} φ IH₀ {a} {b} IH₁ = goal
 where
  p : a ≡ b
  p = pr₁ (pr₁ (IH₁ (λ())) ⋆) ⋆
  Q : ⟦ σ ⟧ → Set
  Q x = (_ : dd⁺ ε) → Σ \(t : d⁺ (φ a x)) → (y : d⁻ (φ a x)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ φ a x ∣ t y)
  goal : (_ : dd⁺ ε) → Σ \(t : d⁺ (φ a b)) → (y : d⁻ (φ a b)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ φ a b ∣ t y)
  goal = transport Q p (IH₀ a)

\end{code}

The cases of basic rules in sequent calculi

\begin{code}

case-id : (A : Prp)
        → (xs : dd⁺ (ε ₊ A)) → Σ \(t : d⁺ A) → (y : d⁻ A) → Σ \(rs : dd⁻ (ε ₊ A)) → Prfᴬ (∥ ε ₊ A ∥ xs rs) (∣ A ∣ t y)
case-id A xs = t , goal
 where
  t :  d⁺ A
  t = xs zero
  frs : d⁻ A → dd⁻ (ε ₊ A)
  frs y zero = y
  frs y (succ ())
  goal : (y : d⁻ A) → Σ \(rs : dd⁻ (ε ₊ A)) → Prfᴬ (∥ ε ₊ A ∥ xs rs) (∣ A ∣ t y)
  goal y = frs y , pr₁


case-wkn : {Γ : Asmpt} (A B : Prp)
         → ((xs : dd⁺ Γ) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ B ∣ t y))
         → (xs : dd⁺ (Γ ₊ A)) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ (Γ ₊ A)) → Prfᴬ (∥ Γ ₊ A ∥ xs rs) (∣ B ∣ t y)
case-wkn {Γ} A B IH xs = t , goal
 where
  t : d⁺ B
  t = pr₀ (IH (xs ∘ succ))
  goal : (y : d⁻ B) → Σ \(rs : dd⁻ (Γ ₊ A)) → Prfᴬ (∥ Γ ₊ A ∥ xs rs) (∣ B ∣ t y)
  goal y = rs , claim
   where
    rs : dd⁻ (Γ ₊ A)
    rs zero = inhabitant⁻ A
    rs (succ i) = pr₀ (pr₁ (IH (xs ∘ succ)) y) i
    claim : Prfᴬ (∥ Γ ₊ A ∥ xs rs) (∣ B ∣ t y)
    claim (γ , _) = pr₁ (pr₁ (IH (xs ∘ succ)) y) γ


case-cut : {Γ Δ : Asmpt} (A B : Prp)
         → ((xs : dd⁺ (Γ ₊ A)) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ (Γ ₊ A)) → Prfᴬ (∥ Γ ₊ A ∥ xs rs) (∣ B ∣ t y))
         → ((xs : dd⁺ Δ) → Σ \(t : d⁺ A) → (y : d⁻ A) → Σ \(rs : dd⁻ Δ) → Prfᴬ (∥ Δ ∥ xs rs) (∣ A ∣ t y))
         → (xs : dd⁺ (Γ ₊₊ Δ)) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ (Γ ₊₊ Δ)) → Prfᴬ (∥ Γ ₊₊ Δ ∥ xs rs) (∣ B ∣ t y)
case-cut {Γ} {Δ} A B IH₀ IH₁ xs = tb , goal
 where
  xs₁ : dd⁺ Δ
  xs₁ = pr₁ᴸ⁺ Δ xs
  ta : d⁺ A
  ta = pr₀ (IH₁ xs₁)
  xs₀' : dd⁺ Γ
  xs₀' = pr₀ᴸ⁺ Δ xs
  xs₀ : dd⁺ (Γ ₊ A)
  xs₀ zero = ta
  xs₀ (succ i) = xs₀' i
  tb : d⁺ B
  tb = pr₀ (IH₀ xs₀)
  goal : (yb : d⁻ B) → Σ \(rs : dd⁻ (Γ ₊₊ Δ)) → Prfᴬ (∥ Γ ₊₊ Δ ∥ xs rs) (∣ B ∣ tb yb)
  goal yb = rs , claim₃
   where
    rs₀ : dd⁻ (Γ ₊ A)
    rs₀ = pr₀ (pr₁ (IH₀ xs₀) yb)
    rs₀' : dd⁻ Γ
    rs₀' = rs₀ ∘ succ
    ya : d⁻ A
    ya = rs₀ zero
    rs₁ : dd⁻ Δ
    rs₁ = pr₀ (pr₁ (IH₁ xs₁) ya)
    rs : dd⁻ (Γ ₊₊ Δ)
    rs = pairᴸ⁻ Δ rs₀' rs₁
    claim₀ : Prfᴬ (∥ Γ ₊ A ∥ xs₀ rs₀) (∣ B ∣ tb yb)
    claim₀ = pr₁ (pr₁ (IH₀ xs₀) yb)
    claim₁ : Prfᴬ (∥ Δ ∥ xs₁ rs₁) (∣ A ∣ ta ya)
    claim₁ = pr₁ (pr₁ (IH₁ xs₁) ya)
    claim₂ : Prfᴬ (∥ Γ ∥ xs₀' rs₀' × ∥ Δ ∥ xs₁ rs₁) (∣ B ∣ tb yb)
    claim₂ (γ , δ) = claim₀ (γ , claim₁ δ)
    claim₃ : Prfᴬ (∥ Γ ₊₊ Δ ∥ xs rs) (∣ B ∣ tb yb)
    claim₃ ρ = claim₂ (∥₊₊∥→× Δ xs rs₀' rs₁ ρ)


case-swap : (Γ Δ : Asmpt) (A B C : Prp)
          → ((xs : dd⁺ (Γ ₊ A ₊ B ₊₊ Δ)) → Σ \(t : d⁺ C) → (y : d⁻ C) → Σ \(rs : dd⁻ (Γ ₊ A ₊ B ₊₊ Δ)) → Prfᴬ (∥ Γ ₊ A ₊ B ₊₊ Δ ∥ xs rs) (∣ C ∣ t y))
          → (xs : dd⁺ (Γ ₊ B ₊ A ₊₊ Δ)) → Σ \(t : d⁺ C) → (y : d⁻ C) → Σ \(rs : dd⁻ (Γ ₊ B ₊ A ₊₊ Δ)) → Prfᴬ (∥ Γ ₊ B ₊ A ₊₊ Δ ∥ xs rs) (∣ C ∣ t y)
case-swap Γ Δ A B C IH xs = t , goal
 where
  xs' : dd⁺ (Γ ₊ A ₊ B ₊₊ Δ)
  xs' = swap⁺ Δ xs
  t : d⁺ C
  t = pr₀ (IH xs')
  goal : (y : d⁻ C) → Σ \(rs : dd⁻ (Γ ₊ B ₊ A ₊₊ Δ)) → Prfᴬ (∥ Γ ₊ B ₊ A ₊₊ Δ ∥ xs rs) (∣ C ∣ t y)
  goal y = rs , claim₃
   where
    rs' : dd⁻ (Γ ₊ A ₊ B ₊₊ Δ)
    rs' = pr₀ (pr₁ (IH xs') y)
    rs : dd⁻ (Γ ₊ B ₊ A ₊₊ Δ)
    rs = swap⁻ Δ rs'
    xs'₀ : dd⁺ (Γ ₊ A ₊ B) 
    xs'₀ = pr₀ᴸ⁺ Δ xs'
    tb : d⁺ B
    tb = xs'₀ zero
    ta : d⁺ A
    ta = xs'₀ (succ zero)
    xs₀ : dd⁺ Γ
    xs₀ = xs'₀ ∘ succ ∘ succ
    xs₁ : dd⁺ Δ
    xs₁ = pr₁ᴸ⁺ Δ xs'
    rs'₀ : dd⁻ (Γ ₊ A ₊ B)
    rs'₀ = pr₀ᴸ⁻ Δ rs'
    yb : d⁻ B
    yb = rs'₀ zero
    ya : d⁻ A
    ya = rs'₀ (succ zero)
    rs₀ : dd⁻ Γ
    rs₀ = rs'₀ ∘ succ ∘ succ
    rs₁ : dd⁻ Δ
    rs₁ = pr₁ᴸ⁻ Δ rs'
    claim₀ : Prfᴬ (∥ Γ ₊ A ₊ B ₊₊ Δ ∥ xs' rs') (∣ C ∣ t y)
    claim₀ = pr₁ (pr₁ (IH xs') y)
    claim₁ : Prfᴬ (((∥ Γ ∥ xs₀ rs₀ × ∣ A ∣ ta ya) × ∣ B ∣ tb yb) × ∥ Δ ∥ xs₁ rs₁) (∣ C ∣ t y)
    claim₁ ρ = claim₀ (×→∥₊₊∥ Δ xs' rs' ρ)
    claim₂ : Prfᴬ (((∥ Γ ∥ xs₀ rs₀ × ∣ B ∣ tb yb) × ∣ A ∣ ta ya) × ∥ Δ ∥ xs₁ rs₁) (∣ C ∣ t y)
    claim₂ (((γ , b) , a) , δ) = claim₁ (((γ , a) , b) , δ)
    claim₃ : Prfᴬ (∥ Γ ₊ B ₊ A ₊₊ Δ ∥ xs rs) (∣ C ∣ t y)
    claim₃ ρ = claim₂ (∥swap∥→× Δ xs rs' ρ)

\end{code}

The cases of inference rules of propositional logic

\begin{code}

case-∧-intro : {Γ Δ : Asmpt} (A B : Prp)
             → ((xs : dd⁺ Γ) → Σ \(t : d⁺ A) → (y : d⁻ A) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∣ t y))
             → ((xs : dd⁺ Δ) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ Δ) → Prfᴬ (∥ Δ ∥ xs rs) (∣ B ∣ t y))
             → (xs : dd⁺ (Γ ₊₊ Δ)) → Σ \(t : d⁺ (A ∧ B)) → (y : d⁻ (A ∧ B)) → Σ \(rs : dd⁻ (Γ ₊₊ Δ)) → Prfᴬ (∥ Γ ₊₊ Δ ∥ xs rs) (∣ A ∧ B ∣ t y)
case-∧-intro {Γ} {Δ} A B IH₀ IH₁ xs = t , goal
 where
  xs₀ : dd⁺ Γ
  xs₀ = pr₀ᴸ⁺ Δ xs
  t₀ : d⁺ A
  t₀ = pr₀ (IH₀ xs₀)
  xs₁ : dd⁺ Δ
  xs₁ = pr₁ᴸ⁺ Δ xs
  t₁ : d⁺ B
  t₁ = pr₀ (IH₁ xs₁)
  t : d⁺ (A ∧ B)
  t = t₀ , t₁
  goal : (y : d⁻ (A ∧ B)) → Σ \(rs : dd⁻ (Γ ₊₊ Δ)) → Prfᴬ (∥ Γ ₊₊ Δ ∥ xs rs) (∣ A ∧ B ∣ t y)
  goal (y₀ , y₁) = rs , claim₃
   where
    rs₀ : dd⁻ Γ
    rs₀ = pr₀ (pr₁ (IH₀ xs₀) y₀)
    rs₁ : dd⁻ Δ
    rs₁ = pr₀ (pr₁ (IH₁ xs₁) y₁)
    rs : dd⁻ (Γ ₊₊ Δ)
    rs = pairᴸ⁻ Δ rs₀ rs₁
    claim₀ : Prfᴬ (∥ Γ ∥ xs₀ rs₀) (∣ A ∣ t₀ y₀)
    claim₀ = pr₁ (pr₁ (IH₀ xs₀) y₀)
    claim₁ : Prfᴬ (∥ Δ ∥ xs₁ rs₁) (∣ B ∣ t₁ y₁)
    claim₁ = pr₁ (pr₁ (IH₁ xs₁) y₁)
    claim₂ : Prfᴬ (∥ Γ ∥ xs₀ rs₀ × ∥ Δ ∥ xs₁ rs₁) (∣ A ∣ t₀ y₀ × ∣ B ∣ t₁ y₁)
    claim₂ (γ , δ) = claim₀ γ , claim₁ δ
    claim₃ : Prfᴬ (∥ Γ ₊₊ Δ ∥ xs rs) (∣ A ∧ B ∣ (t₀ , t₁) (y₀ , y₁))
    claim₃ ρ = claim₂ (∥₊₊∥→× Δ xs rs₀ rs₁ ρ)


case-∧-elim₀ : {Γ : Asmpt} (A B : Prp)
             → ((xs : dd⁺ Γ) → Σ \(t : d⁺ (A ∧ B)) → (y : d⁻ (A ∧ B)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∧ B ∣ t y))
             → (xs : dd⁺ Γ) → Σ \(t : d⁺ A) → (y : d⁻ A) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∣ t y)
case-∧-elim₀ {Γ} A B IH xs = t , goal
 where
  t : d⁺ A
  t = pr₀ (pr₀ (IH xs))
  goal : (y : d⁻ A) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∣ t y)
  goal y = rs , claim
   where
    rs : dd⁻ Γ
    rs = pr₀ (pr₁ (IH xs) (y , inhabitant⁻ B))
    claim : Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∣ t y)
    claim γ = pr₀ (pr₁ (pr₁ (IH xs) (y , inhabitant⁻ B)) γ)


case-∧-elim₁ : {Γ : Asmpt} (A B : Prp)
             → ((xs : dd⁺ Γ) → Σ \(t : d⁺ (A ∧ B)) → (y : d⁻ (A ∧ B)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∧ B ∣ t y))
             → (xs : dd⁺ Γ) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ B ∣ t y)
case-∧-elim₁ {Γ} A B IH xs = t , goal
 where
  t : d⁺ B
  t = pr₁ (pr₀ (IH xs))
  goal : (y : d⁻ B) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ B ∣ t y)
  goal y = rs , claim
   where
    rs : dd⁻ Γ
    rs = pr₀ (pr₁ (IH xs) (inhabitant⁻ A , y))
    claim : Prfᴬ (∥ Γ ∥ xs rs) (∣ B ∣ t y)
    claim γ = pr₁ (pr₁ (pr₁ (IH xs) (inhabitant⁻ A , y)) γ)


case-⇒-intro : {Γ : Asmpt} (A B : Prp)
             → ((xs : dd⁺ (Γ ₊ A)) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ (Γ ₊ A)) → Prfᴬ (∥ Γ ₊ A ∥ xs rs) (∣ B ∣ t y))
             → (xs : dd⁺ Γ) → Σ \(t : d⁺ (A ⇒ B)) → (y : d⁻ (A ⇒ B)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ⇒ B ∣ t y)
case-⇒-intro {Γ} A B IH xs = t , goal
 where
  fxs' : d⁺ A → dd⁺ (Γ ₊ A)
  fxs' ta zero = ta
  fxs' _ (succ i) = xs i
  t₀ : d⁺ A → d⁺ B
  t₀ ta = pr₀ (IH (fxs' ta))
  frs' : d⁺ A → d⁻ B → dd⁻ (Γ ₊ A)
  frs' ta yb = pr₀ (pr₁ (IH (fxs' ta)) yb)
  t₁ : d⁺ A → d⁻ B → d⁻ A
  t₁ ta yb = (frs' ta yb) zero
  t : d⁺ (A ⇒ B)
  t = t₀ , t₁
  goal : (y : d⁻ (A ⇒ B)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ⇒ B ∣ t y)
  goal (ta , yb) = rs , claim₁
   where
    rs : dd⁻ Γ
    rs = (frs' ta yb) ∘ succ
    tb : d⁺ B
    tb = pr₀ (IH (fxs' ta))
    ya : d⁻ A
    ya = (frs' ta yb) zero
    claim₀ : Prfᴬ (∥ Γ ∥ xs rs × ∣ A ∣ ta ya) (∣ B ∣ tb yb)
    claim₀ = pr₁ (pr₁ (IH (fxs' ta)) yb)
    claim₁ : Prfᴬ (∥ Γ ∥ xs rs) (∣ A ⇒ B ∣ t (ta , yb))
    claim₁ γ a = claim₀ (γ , a)


case-⇒-elim : {Γ : Asmpt} (A B : Prp)
            → ((xs : dd⁺ Γ) → Σ \(t : d⁺ (A ⇒ B)) → (y : d⁻ (A ⇒ B)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ⇒ B ∣ t y))
            → (xs : dd⁺ (Γ ₊ A)) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ (Γ ₊ A)) → Prfᴬ (∥ Γ ₊ A ∥ xs rs) (∣ B ∣ t y)
case-⇒-elim {Γ} A B IH xs' = tb , goal
 where
  xs : dd⁺ Γ
  xs = xs' ∘ succ
  t : d⁺ (A ⇒ B)
  t = pr₀ (IH xs)
  ta : d⁺ A
  ta = xs' zero
  tb : d⁺ B
  tb = pr₀ t ta
  goal : (yb : d⁻ B) → Σ \(rs' : dd⁻ (Γ ₊ A)) → Prfᴬ (∥ Γ ₊ A ∥ xs' rs') (∣ B ∣ tb yb)
  goal yb = rs' , claim₁
   where
    ya : d⁻ A
    ya = pr₁ t ta yb
    y  : d⁻ (A ⇒ B)
    y  = ta , yb
    rs : dd⁻ Γ
    rs = pr₀ (pr₁ (IH xs) y)
    rs' : dd⁻ (Γ ₊ A)
    rs' zero = ya
    rs' (succ i) = rs i
    claim₀ : Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∣ ta ya → ∣ B ∣ tb yb)
    claim₀ = pr₁ (pr₁ (IH xs) y)
    claim₁ : Prfᴬ (∥ Γ ₊ A ∥ xs' rs') (∣ B ∣ tb yb)
    claim₁ (γ , a) = claim₀ γ a

\end{code}

The cases of inference rules of quantifiers

\begin{code}

case-∀-intro : {Γ : Asmpt} {σ : Ty} (φ : ⟦ σ ⟧ → Prp)
             → ((x : ⟦ σ ⟧) → (xs : dd⁺ Γ) → Σ \(t : d⁺ (φ x)) → (y : d⁻ (φ x)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ φ x ∣ t y))
             → (xs : dd⁺ Γ) → Σ \(t : d⁺ (∀′ φ)) → (y : d⁻ (∀′ φ)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ ∀′ φ ∣ t y)
case-∀-intro {Γ} {σ} φ IH xs = t , goal
 where
  t : d⁺ (∀′ φ)
  t x = pr₀ (IH x xs)
  goal : (y : d⁻ (∀′ φ)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ ∀′ φ ∣ t y)
  goal (a , y') = pr₁ (IH a xs) y'


case-∀-elim : {Γ : Asmpt} {σ : Ty} (φ : ⟦ σ ⟧ → Prp)
            → ((xs : dd⁺ Γ) → Σ \(t : d⁺ (∀′ φ)) → (y : d⁻ (∀′ φ)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ ∀′ φ ∣ t y))
            → (a : ⟦ σ ⟧) → (xs : dd⁺ Γ) → Σ \(t : d⁺ (φ a)) → (y : d⁻ (φ a)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ φ a ∣ t y)
case-∀-elim {Γ} {σ} φ IH a xs = t , goal
 where
  t : d⁺ (φ a)
  t = pr₀ (IH xs) a
  goal : (y : d⁻ (φ a)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ φ a ∣ t y)
  goal y = pr₁ (IH xs) (a , y)


case-∃-intro : {Γ : Asmpt} {σ : Ty} (φ : ⟦ σ ⟧ → Prp)
             → (a : ⟦ σ ⟧) → ((xs : dd⁺ Γ) → Σ \(t : d⁺ (φ a)) → (y : d⁻ (φ a)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ φ a ∣ t y))
             → (xs : dd⁺ Γ) → Σ \(t : d⁺ (∃′ φ)) → (y : d⁻ (∃′ φ)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ ∃′ φ ∣ t y)
case-∃-intro {Γ} {σ} φ a IH xs = t , goal
 where
  t : d⁺ (∃′ φ)
  t = a , pr₀ (IH xs)
  goal : (y : d⁻ (∃′ φ)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ ∃′ φ ∣ t y)
  goal y = pr₁ (IH xs) (y a (pr₀ (IH xs)))


case-∃-elim : {Γ : Asmpt} {σ : Ty} (φ : ⟦ σ ⟧ → Prp) (A : Prp)
            → ((x : ⟦ σ ⟧) → (xs : dd⁺ Γ) → Σ \(t : d⁺ (φ x ⇒ A)) → (y : d⁻ (φ x ⇒ A)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ φ x ⇒ A ∣ t y))
            → (xs : dd⁺ Γ) → Σ \(t : d⁺ ((∃′ φ) ⇒ A)) → (y : d⁻ ((∃′ φ) ⇒ A)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ (∃′ φ) ⇒ A ∣ t y)
case-∃-elim {Γ} {σ} φ A IH xs = t , goal
 where
  t₀ : (Σ \(x : ⟦ σ ⟧) → d⁺ (φ x)) → d⁺ A
  t₀ (x , w) = pr₀ (pr₀ (IH x xs)) w
  t₁ : (Σ \(x : ⟦ σ ⟧) → d⁺ (φ x)) → d⁻ A → (x : ⟦ σ ⟧) → d⁺ (φ x) → d⁻ (φ x)
  t₁ _ y x w = pr₁ (pr₀ (IH x xs)) w y
  t : d⁺ ((∃′ φ) ⇒ A)
  t = t₀ , t₁
  goal : (y : (Σ \(x : ⟦ σ ⟧) → d⁺ (φ x)) × d⁻ A)
       → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ (∃′ φ) ⇒ A ∣ t y)
  goal ((x , w) , y) = pr₁ (IH x xs) (w , y)

\end{code}

The case of the induction principle (in empty assumption)

\begin{code}

ICond : (ℕ → Prp) → Prp
ICond φ = ∀′ (λ n → φ n ⇒ φ (succ n))

case-ind : (φ : ℕ → Prp)
         → ((_ : dd⁺ ε) → Σ \(t : d⁺ (φ )) → (y : d⁻ (φ )) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ φ  ∣ t y))
         → ((_ : dd⁺ ε) → Σ \(t : d⁺ (ICond φ)) → (y : d⁻ (ICond φ)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ ICond φ ∣ t y))
         → (_ : dd⁺ ε) → Σ \(t : d⁺ (∀′ φ)) → (y : d⁻ (∀′ φ)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ ∀′ φ ∣ t y)
case-ind φ IH₀ IH₁ _ = t , uncurry goal -- I have to do this, otherwise Agda doesn't believe its termination.
 where
  t0 : d⁺ (φ )
  t0 = pr₀ (IH₀ (λ())) 
  ts : (n : ℕ) → d⁺ (φ n) → d⁺ (φ (succ n))
  ts n tn = pr₀ (pr₀ (IH₁ (λ())) n) tn
  t : d⁺ (∀′ φ)
  t  = t0
  t (succ n) = ts n (t n)
  goal : (n : ℕ) → (yn : d⁻ (φ n)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ ∀′ φ ∣ t (n , yn))
  goal  y0 = (λ()) , pr₁ (pr₁ (IH₀ (λ())) y0)
  goal (succ n) ysn = (λ()) , claim₂
   where
    tn : d⁺ (φ n)
    tn = t n
    fy : (n : ℕ) → d⁺ (φ n) → d⁻ (φ (succ n)) → d⁻ (φ n)
    fy n = pr₁ (pr₀ (IH₁ (λ())) n)
    yn : d⁻ (φ n)
    yn = fy n tn ysn
    tsn : d⁺ (φ (succ n))
    tsn = t (succ n)
    claim₀ : Prfᴬ 𝟙 (∣ φ n ∣ tn yn)
    claim₀ = pr₁ (goal n yn)
    claim₁ : Prfᴬ 𝟙 (∣ φ n ∣ tn yn → ∣ φ (succ n) ∣ tsn ysn)
    claim₁ = pr₁ (pr₁ (IH₁ (λ())) (n , tn , ysn))
    claim₂ : Prfᴬ 𝟙 (∣ φ (succ n) ∣ tsn ysn)
    claim₂ ⋆ = claim₁ ⋆ (claim₀ ⋆)

\end{code}

Finally we use the above to prove Thm[soundness].

\begin{code}

Thm[soundness] refl = case-refl
Thm[soundness] (J {σ} φ base {a} {b} p) = case-J φ (λ x → Thm[soundness] (base x)) (Thm[soundness] p)
Thm[soundness] (id {A}) = case-id A
Thm[soundness] (wkn {A = A} {B = B} p) = case-wkn A B (Thm[soundness] p)
Thm[soundness] (cut {A = A} {B = B} p q) = case-cut A B (Thm[soundness] p) (Thm[soundness] q)
Thm[soundness] (swap {Γ} Δ {A} {B} {C} p) = case-swap Γ Δ A B C (Thm[soundness] p)
Thm[soundness] (∧-intro {A = A} {B = B} p q) = case-∧-intro A B (Thm[soundness] p) (Thm[soundness] q)
Thm[soundness] (∧-elim₀ {A = A} {B = B} p) = case-∧-elim₀ A B (Thm[soundness] p)
Thm[soundness] (∧-elim₁ {A = A} {B = B} p) = case-∧-elim₁ A B (Thm[soundness] p)
Thm[soundness] (⇒-intro {A = A} {B = B} p) = case-⇒-intro A B (Thm[soundness] p)
Thm[soundness] (⇒-elim {A = A} {B = B} p) = case-⇒-elim A B (Thm[soundness] p)
Thm[soundness] (∀-intro {φ = φ} f) = case-∀-intro φ (λ x → Thm[soundness] (f x))
Thm[soundness] (∀-elim {φ = φ} p a) = case-∀-elim φ (Thm[soundness] p) a
Thm[soundness] (∃-intro {φ = φ} a p) = case-∃-intro φ a (Thm[soundness] p)
Thm[soundness] (∃-elim {φ = φ} {A = A} f) = case-∃-elim φ A (λ x → Thm[soundness] (f x))
Thm[soundness] (ind φ base ih) = case-ind φ (Thm[soundness] base) (Thm[soundness] ih)

\end{code}

Work in progress include

(0) to add examples,

(1) to interpret J and ind with arbitrary assumptions,

(2) to interpret Markov Principle, Axiom of Choice and Independence of Premise,

(3) to generalize the method for modified realizability.

(4) to generalize the interpretation for non-standard systems.