Classical.CutElim: completeness and cut elimination for CLL

Classical/Phase.v proved soundness: every provable two-sided sequent, with or without cuts, is valid in every classical phase space. This file proves the converse, and in a strong form: every valid sequent has a cut-free proof. Chaining the two gives cut elimination, exactly as in Intuitionistic/CutElim.v:

         Γ ⊢ Δ   ──soundness──▶   Γ ⊨ Δ   ──completeness──▶   Γ ⊢cf Δ

The syntactic phase space

The phases are two-sided contexts, and the pole is cut-free provability:

a phase is a pair (Γ, Δ) of lists of formulas, taken up to permutation on each side. Read it as the sequent fragment "Γ on the left, Δ on the right";
· concatenates both sides, and ε is ([], []);
the pole is { (Γ, Δ) | Γ ⊢cf Δ };
the reusable phases are the pairs (‼Σ, ⁇Π). They are exactly the contexts allowed around a promotion, and the structural rules for ! and ? let them be discarded and duplicated.

What changes compared with ILL

In the intuitionistic proof, the closure operator had to be chosen: a context lies in cl X when it passes every "test" (Δ, C) that the members of X pass. Here nothing is chosen besides the pole. The closure is X^⊥⊥, and unfolding it gives the same idea with two-sided tests:

        y ∈ X^⊥    iff  for every x ∈ X,  x.1 ++ y.1 ⊢cf x.2 ++ y.2
        z ∈ X^⊥⊥   iff  z passes every test y that all members of X pass

So the tests of the intuitionistic proof reappear as the counter-bags X^⊥. And because the right-hand side may hold any number of formulas, a test is just another context, with no distinguished conclusion C.

Okada's lemma

Write hyp A for the phase ([A], []) (one copy of A on the left) and concl A for ([], [A]) (one copy on the right). The heart of the proof is

        hyp A ∈ ⟦A⟧      and      concl A ∈ ⟦A⟧^⊥

In words: A used as a hypothesis is a bag of A, and A used as a conclusion is a counter-bag of A. Their product, ([A], [A]), is in the pole: that is the axiom. Given the lemma, a sequent Γ ⊢ Δ gives the phase (Γ, Δ), which lies in the big product ⨀ (sq Γ Δ). If the sequent is valid, that product lies in the pole, so Γ ⊢cf Δ.

This is simpler than the intuitionistic case in one respect. There, the right half of the lemma, ⟦A⟧ ⊆ { Γ | Γ ⊢cf A }, had to be applied at the end. Here the pole is cut-free provability, so the last step is free.

From LinearLogic.Classical Require Export Phase.[Loading ML file rocq-runtime.plugins.ring ... done]
[Loading ML file rocq-runtime.plugins.zify ... done]
[Loading ML file rocq-runtime.plugins.micromega_core ... done]
[Loading ML file rocq-runtime.plugins.micromega ... done]
[Loading ML file rocq-runtime.plugins.ssrmatching ... done]
[Loading ML file rocq-runtime.plugins.ssreflect ... done]
[Loading ML file rocq-runtime.plugins.btauto ... done]
[Loading ML file rocq-runtime.plugins.nsatz_core ... done]
[Loading ML file rocq-runtime.plugins.nsatz ... done]

The syntactic phase space

A two-sided context: hypotheses and conclusions.

Definition ctx : Type := list cformula * list cformula.

Two contexts are equivalent when both sides are permutations. We give this relation explicitly. stdpp also has generic Equiv instances for pairs and lists, but they are not the ones we want, so every lemma below types its phases as elements of syntactic.

Definition ctx_equiv : Equiv ctx := λ x y, x.1 ≡ₚ y.1 ∧ x.2 ≡ₚ y.2.

Concatenation on both sides.

Definition ctx_app (x y : ctx) : ctx := (x.1 ++ y.1, x.2 ++ y.2).

Lemma ctx_equivalence : Equivalence ctx_equiv.Equivalence ctx_equiv
Proof.Equivalence ctx_equiv
  unfold ctx_equiv.Equivalence (λ x y : ctx, x.1 ≡ₚ y.1 ∧ x.2 ≡ₚ y.2) split.Reflexive (λ x y : ctx, x.1 ≡ₚ y.1 ∧ x.2 ≡ₚ y.2)
Symmetric (λ x y : ctx, x.1 ≡ₚ y.1 ∧ x.2 ≡ₚ y.2)
Transitive (λ x y : ctx, x.1 ≡ₚ y.1 ∧ x.2 ≡ₚ y.2)
  -Reflexive (λ x y : ctx, x.1 ≡ₚ y.1 ∧ x.2 ≡ₚ y.2) done.
  -Symmetric (λ x y : ctx, x.1 ≡ₚ y.1 ∧ x.2 ≡ₚ y.2) intros x y [].x, y: ctx
H: x.1 ≡ₚ y.1
H0: x.2 ≡ₚ y.2
y.1 ≡ₚ x.1 ∧ y.2 ≡ₚ x.2 split; by symmetry.
  -Transitive (λ x y : ctx, x.1 ≡ₚ y.1 ∧ x.2 ≡ₚ y.2) intros x y z [] [].x, y, z: ctx
H: x.1 ≡ₚ y.1
H0: x.2 ≡ₚ y.2
H1: y.1 ≡ₚ z.1
H2: y.2 ≡ₚ z.2
x.1 ≡ₚ z.1 ∧ x.2 ≡ₚ z.2 split; by etrans.
Qed.

Lemma ctx_app_proper : Proper (ctx_equiv ==> ctx_equiv ==> ctx_equiv) ctx_app.Proper (ctx_equiv ==> ctx_equiv ==> ctx_equiv) ctx_app
Proof.Proper (ctx_equiv ==> ctx_equiv ==> ctx_equiv) ctx_app
  intros x x' [Hx1 Hx2] y y' [Hy1 Hy2].x, x': ctx
Hx1: x.1 ≡ₚ x'.1
Hx2: x.2 ≡ₚ x'.2
y, y': ctx
Hy1: y.1 ≡ₚ y'.1
Hy2: y.2 ≡ₚ y'.2
ctx_equiv (ctx_app x y) (ctx_app x' y') split; cbn [ctx_app fst snd]; by f_equiv.
Qed.

The model. The obligations are the monoid laws, closure of the pole under ≡ (by ex), closure of J under ≡ (a permutation of ‼Σ is again of the form ‼Σ'), and the two structural laws for J (by weaken_bangs/weaken_whys and contract_bangs/contract_whys).

Definition syntactic : cphase_space.cphase_space
Proof.cphase_space
  refine (Build_cphase_space ctx ctx_equiv ctx_app ([], [])
            {[ x | x.1 ⊢cf x.2 ]} {[ x | ∃ Σ Π, x.1 = ‼Σ ∧ x.2 = ⁇Π ]}
            ctx_equivalence ctx_app_proper _ _ _ _ _ _ _ _ _);
    unfold equiv, ctx_equiv, ctx_app; cbn [fst snd]; set_unfold.∀ x x0 x1 : ctx,
  x.1 ++ x0.1 ++ x1.1 ≡ₚ (x.1 ++ x0.1) ++ x1.1
  ∧ x.2 ++ x0.2 ++ x1.2 ≡ₚ (x.2 ++ x0.2) ++ x1.2
∀ x x0 : ctx, x.1 ++ x0.1 ≡ₚ x0.1 ++ x.1 ∧ x.2 ++ x0.2 ≡ₚ x0.2 ++ x.2
∀ x : ctx, x.1 ≡ₚ x.1 ∧ x.2 ≡ₚ x.2
∀ x x0 : ctx, x.1 ≡ₚ x0.1 ∧ x.2 ≡ₚ x0.2 → x.1 ⊢cf x.2 → x0.1 ⊢cf x0.2
∀ x x0 : ctx,
  x.1 ≡ₚ x0.1 ∧ x.2 ≡ₚ x0.2
  → (∃ x1 x2 : list cformula, x.1 = ‼x1 ∧ x.2 = ⁇x2)
    → ∃ x1 x2 : list cformula, x0.1 = ‼x1 ∧ x0.2 = ⁇x2
∃ x x0 : list cformula, [] = ‼x ∧ [] = ⁇x0
∀ x x0 : ctx,
  (∃ x1 x2 : list cformula, x.1 = ‼x1 ∧ x.2 = ⁇x2)
  → (∃ x1 x2 : list cformula, x0.1 = ‼x1 ∧ x0.2 = ⁇x2)
    → ∃ x1 x2 : list cformula, x.1 ++ x0.1 = ‼x1 ∧ x.2 ++ x0.2 = ⁇x2
∀ x x0 : ctx,
  (∃ x1 x2 : list cformula, x.1 = ‼x1 ∧ x.2 = ⁇x2)
  → x0.1 ⊢cf x0.2 → x.1 ++ x0.1 ⊢cf x.2 ++ x0.2
∀ x x0 : ctx,
  (∃ x1 x2 : list cformula, x.1 = ‼x1 ∧ x.2 = ⁇x2)
  → (x.1 ++ x.1) ++ x0.1 ⊢cf (x.2 ++ x.2) ++ x0.2
    → x.1 ++ x0.1 ⊢cf x.2 ++ x0.2
  - (* assoc *)∀ x x0 x1 : ctx,
  x.1 ++ x0.1 ++ x1.1 ≡ₚ (x.1 ++ x0.1) ++ x1.1
  ∧ x.2 ++ x0.2 ++ x1.2 ≡ₚ (x.2 ++ x0.2) ++ x1.2 intros.x, x0, x1: ctx
x.1 ++ x0.1 ++ x1.1 ≡ₚ (x.1 ++ x0.1) ++ x1.1
∧ x.2 ++ x0.2 ++ x1.2 ≡ₚ (x.2 ++ x0.2) ++ x1.2 by rewrite !(assoc_L (++)).
  - (* comm *)∀ x x0 : ctx, x.1 ++ x0.1 ≡ₚ x0.1 ++ x.1 ∧ x.2 ++ x0.2 ≡ₚ x0.2 ++ x.2 intros.x, x0: ctx
x.1 ++ x0.1 ≡ₚ x0.1 ++ x.1 ∧ x.2 ++ x0.2 ≡ₚ x0.2 ++ x.2 split; apply Permutation_app_comm.
  - (* unit *)∀ x : ctx, x.1 ≡ₚ x.1 ∧ x.2 ≡ₚ x.2 done.
  - (* the pole respects ≡ *)∀ x x0 : ctx, x.1 ≡ₚ x0.1 ∧ x.2 ≡ₚ x0.2 → x.1 ⊢cf x.2 → x0.1 ⊢cf x0.2 intros x y [H1 H2].x, y: ctx
H1: x.1 ≡ₚ y.1
H2: x.2 ≡ₚ y.2
x.1 ⊢cf x.2 → y.1 ⊢cf y.2 by apply ex.
  - (* J respects ≡ *)∀ x x0 : ctx,
  x.1 ≡ₚ x0.1 ∧ x.2 ≡ₚ x0.2
  → (∃ x1 x2 : list cformula, x.1 = ‼x1 ∧ x.2 = ⁇x2)
    → ∃ x1 x2 : list cformula, x0.1 = ‼x1 ∧ x0.2 = ⁇x2
    intros x y [H1 H2] (Σ & Π & E1 & E2).x, y: ctx
H1: x.1 ≡ₚ y.1
H2: x.2 ≡ₚ y.2
Σ, Π: list cformula
E1: x.1 = ‼Σ
E2: x.2 = ⁇Π
∃ x0 x1 : list cformula, y.1 = ‼x0 ∧ y.2 = ⁇x1 rewrite E1 in H1.x, y: ctx
Σ: list cformula
H1: ‼Σ ≡ₚ y.1
H2: x.2 ≡ₚ y.2
Π: list cformula
E1: x.1 = ‼Σ
E2: x.2 = ⁇Π
∃ x0 x1 : list cformula, y.1 = ‼x0 ∧ y.2 = ⁇x1 rewrite E2 in H2.x, y: ctx
Σ: list cformula
H1: ‼Σ ≡ₚ y.1
Π: list cformula
H2: ⁇Π ≡ₚ y.2
E1: x.1 = ‼Σ
E2: x.2 = ⁇Π
∃ x0 x1 : list cformula, y.1 = ‼x0 ∧ y.2 = ⁇x1
    destruct (Permutation_map_inv _ _ (symmetry H1)) as (Σ' & ? & _).x, y: ctx
Σ: list cformula
H1: ‼Σ ≡ₚ y.1
Π: list cformula
H2: ⁇Π ≡ₚ y.2
E1: x.1 = ‼Σ
E2: x.2 = ⁇Π
Σ': list cformula
H: y.1 = ‼Σ'
∃ x0 x1 : list cformula, y.1 = ‼x0 ∧ y.2 = ⁇x1
    destruct (Permutation_map_inv _ _ (symmetry H2)) as (Π' & ? & _).x, y: ctx
Σ: list cformula
H1: ‼Σ ≡ₚ y.1
Π: list cformula
H2: ⁇Π ≡ₚ y.2
E1: x.1 = ‼Σ
E2: x.2 = ⁇Π
Σ': list cformula
H: y.1 = ‼Σ'
Π': list cformula
H0: y.2 = ⁇Π'
∃ x0 x1 : list cformula, y.1 = ‼x0 ∧ y.2 = ⁇x1
    by exists Σ', Π'.
  - (* ε ∈ J *)∃ x x0 : list cformula, [] = ‼x ∧ [] = ⁇x0 by exists [], [].
  - (* J is closed under · *)∀ x x0 : ctx,
  (∃ x1 x2 : list cformula, x.1 = ‼x1 ∧ x.2 = ⁇x2)
  → (∃ x1 x2 : list cformula, x0.1 = ‼x1 ∧ x0.2 = ⁇x2)
    → ∃ x1 x2 : list cformula, x.1 ++ x0.1 = ‼x1 ∧ x.2 ++ x0.2 = ⁇x2
    intros x y (Σ & Π & -> & ->) (Σ' & Π' & -> & ->).x, y: ctx
Σ, Π, Σ', Π': list cformula
∃ x0 x1 : list cformula, ‼Σ ++ ‼Σ' = ‼x0 ∧ ⁇Π ++ ⁇Π' = ⁇x1
    exists (Σ ++ Σ'), (Π ++ Π').x, y: ctx
Σ, Π, Σ', Π': list cformula
‼Σ ++ ‼Σ' = ‼(Σ ++ Σ') ∧ ⁇Π ++ ⁇Π' = ⁇(Π ++ Π') by rewrite !map_app.
  - (* reusable contexts can be discarded *)∀ x x0 : ctx,
  (∃ x1 x2 : list cformula, x.1 = ‼x1 ∧ x.2 = ⁇x2)
  → x0.1 ⊢cf x0.2 → x.1 ++ x0.1 ⊢cf x.2 ++ x0.2
    intros j y (Σ & Π & -> & ->) H.j, y: ctx
Σ, Π: list cformula
H: y.1 ⊢cf y.2
‼Σ ++ y.1 ⊢cf ⁇Π ++ y.2 by apply weaken_bangs, weaken_whys.
  - (* reusable contexts can be duplicated *)∀ x x0 : ctx,
  (∃ x1 x2 : list cformula, x.1 = ‼x1 ∧ x.2 = ⁇x2)
  → (x.1 ++ x.1) ++ x0.1 ⊢cf (x.2 ++ x.2) ++ x0.2
    → x.1 ++ x0.1 ⊢cf x.2 ++ x0.2
    intros j y (Σ & Π & -> & ->) H.j, y: ctx
Σ, Π: list cformula
H: (‼Σ ++ ‼Σ) ++ y.1 ⊢cf (⁇Π ++ ⁇Π) ++ y.2
‼Σ ++ y.1 ⊢cf ⁇Π ++ y.2
    apply contract_bangs, contract_whys.j, y: ctx
Σ, Π: list cformula
H: (‼Σ ++ ‼Σ) ++ y.1 ⊢cf (⁇Π ++ ⁇Π) ++ y.2
‼Σ ++ ‼Σ ++ y.1 ⊢cf ⁇Π ++ ⁇Π ++ y.2 by rewrite !(assoc_L (++)).
Defined.

Membership in the syntactic model

These lemmas restate the set formers of Phase.v in terms of sequents. They never unfold ∈ itself.

Lemma elem_of_pole_syn (x : syntactic) : x ∈ ⫫ ↔ x.1 ⊢cf x.2.x: syntactic
x ∈ ⫫ ↔ x.1 ⊢cf x.2
Proof.x: syntactic
x ∈ ⫫ ↔ x.1 ⊢cf x.2 exact (elem_of_PropSet (λ x : ctx, x.1 ⊢cf x.2) x). Qed.

Lemma elem_of_J_syn (x : syntactic) : x ∈ cph_J ↔ ∃ Σ Π, x = (‼Σ, ⁇Π).x: syntactic
x ∈ cph_J ↔ ∃ Σ Π : list cformula, x = (‼Σ, ⁇Π)
Proof.x: syntactic
x ∈ cph_J ↔ ∃ Σ Π : list cformula, x = (‼Σ, ⁇Π)
  rewrite (elem_of_PropSet (λ x : ctx, ∃ Σ Π, x.1 = ‼Σ ∧ x.2 = ⁇Π) x).x: syntactic
(∃ Σ Π : list cformula, x.1 = ‼Σ ∧ x.2 = ⁇Π)
↔ ∃ Σ Π : list cformula, x = (‼Σ, ⁇Π)
  destruct x as [Γ Δ].Γ, Δ: list cformula
(∃ Σ Π : list cformula, (Γ, Δ).1 = ‼Σ ∧ (Γ, Δ).2 = ⁇Π)
↔ ∃ Σ Π : list cformula, (Γ, Δ) = (‼Σ, ⁇Π) cbn [fst snd].Γ, Δ: list cformula
(∃ Σ Π : list cformula, Γ = ‼Σ ∧ Δ = ⁇Π)
↔ ∃ Σ Π : list cformula, (Γ, Δ) = (‼Σ, ⁇Π) naive_solver.
Qed.

Lemma elem_of_one_syn (x : syntactic) : x ∈ one_set ↔ x = ([], []).x: syntactic
x ∈ one_set ↔ x = ([], [])
Proof.x: syntactic
x ∈ one_set ↔ x = ([], [])
  rewrite elem_of_one.x: syntactic
x ≡ cph_e ↔ x = ([], []) destruct x as [Γ Δ].Γ, Δ: list cformula
(Γ, Δ) ≡ cph_e ↔ (Γ, Δ) = ([], []) split.Γ, Δ: list cformula
(Γ, Δ) ≡ cph_e → (Γ, Δ) = ([], [])
Γ, Δ: list cformula
(Γ, Δ) = ([], []) → (Γ, Δ) ≡ cph_e
  -Γ, Δ: list cformula
(Γ, Δ) ≡ cph_e → (Γ, Δ) = ([], []) intros [H1%Permutation_nil_r H2%Permutation_nil_r].Γ, Δ: list cformula
H1: (Γ, Δ).1 = []
H2: (Γ, Δ).2 = []
(Γ, Δ) = ([], []) by simplify_eq/=.
  -Γ, Δ: list cformula
(Γ, Δ) = ([], []) → (Γ, Δ) ≡ cph_e by intros [= -> ->].
Qed.

y is a counter-bag of X when it completes every member of X to a cut-free provable sequent.

Lemma elem_of_orth_syn (X : propset syntactic) (y : syntactic) :
  y ∈ X^⊥ ↔ ∀ x : syntactic, x ∈ X → x.1 ++ y.1 ⊢cf x.2 ++ y.2.X: propset syntactic
y: syntactic
y ∈ X^⊥ ↔ ∀ x : syntactic, x ∈ X → x.1 ++ y.1 ⊢cf x.2 ++ y.2
Proof.X: propset syntactic
y: syntactic
y ∈ X^⊥ ↔ ∀ x : syntactic, x ∈ X → x.1 ++ y.1 ⊢cf x.2 ++ y.2 rewrite elem_of_orth.X: propset syntactic
y: syntactic
(∀ x : syntactic, x ∈ X → x · y ∈ ⫫)
↔ ∀ x : syntactic, x ∈ X → x.1 ++ y.1 ⊢cf x.2 ++ y.2 by setoid_rewrite elem_of_pole_syn. Qed.

Lemma elem_of_prod_syn (X Y : propset syntactic) (x : syntactic) :
  x ∈ X ⊙ Y ↔
  ∃ a b : syntactic, a ∈ X ∧ b ∈ Y ∧ x.1 ≡ₚ a.1 ++ b.1 ∧ x.2 ≡ₚ a.2 ++ b.2.X, Y: propset syntactic
x: syntactic
x ∈ X ⊙ Y
↔ ∃ a b : syntactic, a ∈ X ∧ b ∈ Y ∧ x.1 ≡ₚ a.1 ++ b.1 ∧ x.2 ≡ₚ a.2 ++ b.2
Proof.X, Y: propset syntactic
x: syntactic
x ∈ X ⊙ Y
↔ ∃ a b : syntactic, a ∈ X ∧ b ∈ Y ∧ x.1 ≡ₚ a.1 ++ b.1 ∧ x.2 ≡ₚ a.2 ++ b.2 by rewrite elem_of_prod. Qed.

The counter-bags of {ε} are the provable contexts.

Lemma orth_one_syn (y : syntactic) : y ∈ one_set^⊥ → y.1 ⊢cf y.2.y: syntactic
y ∈ one_set^⊥ → y.1 ⊢cf y.2
Proof.y: syntactic
y ∈ one_set^⊥ → y.1 ⊢cf y.2
  rewrite elem_of_orth_syn.y: syntactic
(∀ x : syntactic, x ∈ one_set → x.1 ++ y.1 ⊢cf x.2 ++ y.2) → y.1 ⊢cf y.2 intros H.y: syntactic
H: ∀ x : syntactic, x ∈ one_set → x.1 ++ y.1 ⊢cf x.2 ++ y.2
y.1 ⊢cf y.2 apply (H ([], [])), elem_of_one_syn.y: syntactic
H: ∀ x : syntactic, x ∈ one_set → x.1 ++ y.1 ⊢cf x.2 ++ y.2
([], []) = ([], []) done.
Qed.

A formula on one side

hyp A holds one A as a hypothesis, concl A one A as a conclusion.

Definition hyp (A : cformula) : syntactic := ([A], []).
Definition concl (A : cformula) : syntactic := ([], [A]).

Four small lemmas do all the bookkeeping for Okada's lemma. The first two prove that hyp A or concl A is a counter-bag: check that it completes each member of X, adding A on the left or the right.

Lemma L_orth (X : propset syntactic) A :
  (∀ x : syntactic, x ∈ X → A :: x.1 ⊢cf x.2) → hyp A ∈ X^⊥.X: propset syntactic
A: cformula
(∀ x : syntactic, x ∈ X → A :: x.1 ⊢cf x.2) → hyp A ∈ X^⊥
Proof.X: propset syntactic
A: cformula
(∀ x : syntactic, x ∈ X → A :: x.1 ⊢cf x.2) → hyp A ∈ X^⊥
  intros H.X: propset syntactic
A: cformula
H: ∀ x : syntactic, x ∈ X → A :: x.1 ⊢cf x.2
hyp A ∈ X^⊥ apply elem_of_orth_syn.X: propset syntactic
A: cformula
H: ∀ x : syntactic, x ∈ X → A :: x.1 ⊢cf x.2
∀ x : syntactic, x ∈ X → x.1 ++ (hyp A).1 ⊢cf x.2 ++ (hyp A).2 intros x Hx.X: propset syntactic
A: cformula
H: ∀ x : syntactic, x ∈ X → A :: x.1 ⊢cf x.2
x: syntactic
Hx: x ∈ X
x.1 ++ (hyp A).1 ⊢cf x.2 ++ (hyp A).2 cbn [hyp fst snd].X: propset syntactic
A: cformula
H: ∀ x : syntactic, x ∈ X → A :: x.1 ⊢cf x.2
x: syntactic
Hx: x ∈ X
x.1 ++ [A] ⊢cf x.2 ++ []
  ex_to (A :: x.1) x.2.X: propset syntactic
A: cformula
H: ∀ x : syntactic, x ∈ X → A :: x.1 ⊢cf x.2
x: syntactic
Hx: x ∈ X
A :: x.1 ⊢cf x.2 auto.
Qed.

Lemma R_orth (X : propset syntactic) A :
  (∀ x : syntactic, x ∈ X → x.1 ⊢cf A :: x.2) → concl A ∈ X^⊥.X: propset syntactic
A: cformula
(∀ x : syntactic, x ∈ X → x.1 ⊢cf A :: x.2) → concl A ∈ X^⊥
Proof.X: propset syntactic
A: cformula
(∀ x : syntactic, x ∈ X → x.1 ⊢cf A :: x.2) → concl A ∈ X^⊥
  intros H.X: propset syntactic
A: cformula
H: ∀ x : syntactic, x ∈ X → x.1 ⊢cf A :: x.2
concl A ∈ X^⊥ apply elem_of_orth_syn.X: propset syntactic
A: cformula
H: ∀ x : syntactic, x ∈ X → x.1 ⊢cf A :: x.2
∀ x : syntactic, x ∈ X → x.1 ++ (concl A).1 ⊢cf x.2 ++ (concl A).2 intros x Hx.X: propset syntactic
A: cformula
H: ∀ x : syntactic, x ∈ X → x.1 ⊢cf A :: x.2
x: syntactic
Hx: x ∈ X
x.1 ++ (concl A).1 ⊢cf x.2 ++ (concl A).2 cbn [concl fst snd].X: propset syntactic
A: cformula
H: ∀ x : syntactic, x ∈ X → x.1 ⊢cf A :: x.2
x: syntactic
Hx: x ∈ X
x.1 ++ [] ⊢cf x.2 ++ [A]
  ex_to x.1 (A :: x.2).X: propset syntactic
A: cformula
H: ∀ x : syntactic, x ∈ X → x.1 ⊢cf A :: x.2
x: syntactic
Hx: x ∈ X
x.1 ⊢cf A :: x.2 auto.
Qed.

The other two use such facts: they turn membership into a cut-free proof with A on the left or on the right.

Lemma L_use (X : propset syntactic) A (y : syntactic) :
  hyp A ∈ X → y ∈ X^⊥ → A :: y.1 ⊢cf y.2.X: propset syntactic
A: cformula
y: syntactic
hyp A ∈ X → y ∈ X^⊥ → A :: y.1 ⊢cf y.2
Proof.X: propset syntactic
A: cformula
y: syntactic
hyp A ∈ X → y ∈ X^⊥ → A :: y.1 ⊢cf y.2 intros HA Hy.X: propset syntactic
A: cformula
y: syntactic
HA: hyp A ∈ X
Hy: y ∈ X^⊥
A :: y.1 ⊢cf y.2 rewrite elem_of_orth_syn in Hy.X: propset syntactic
A: cformula
y: syntactic
HA: hyp A ∈ X
Hy: ∀ x : syntactic, x ∈ X → x.1 ++ y.1 ⊢cf x.2 ++ y.2
A :: y.1 ⊢cf y.2 exact (Hy _ HA). Qed.

Lemma R_use (X : propset syntactic) A (x : syntactic) :
  concl A ∈ X^⊥ → x ∈ X → x.1 ⊢cf A :: x.2.X: propset syntactic
A: cformula
x: syntactic
concl A ∈ X^⊥ → x ∈ X → x.1 ⊢cf A :: x.2
Proof.X: propset syntactic
A: cformula
x: syntactic
concl A ∈ X^⊥ → x ∈ X → x.1 ⊢cf A :: x.2
  intros HA Hx.X: propset syntactic
A: cformula
x: syntactic
HA: concl A ∈ X^⊥
Hx: x ∈ X
x.1 ⊢cf A :: x.2 rewrite elem_of_orth_syn in HA.X: propset syntactic
A: cformula
x: syntactic
HA: ∀ x : syntactic, x ∈ X → x.1 ++ (concl A).1 ⊢cf x.2 ++ (concl A).2
Hx: x ∈ X
x.1 ⊢cf A :: x.2
  ex_to (x.1 ++ []) (x.2 ++ [A]).X: propset syntactic
A: cformula
x: syntactic
HA: ∀ x : syntactic, x ∈ X → x.1 ++ (concl A).1 ⊢cf x.2 ++ (concl A).2
Hx: x ∈ X
x.1 ++ [] ⊢cf x.2 ++ [A] auto.
Qed.

A counter-bag of X ⊙ Y completes every product a · b.

Lemma orth_prod_use (X Y : propset syntactic) (a b y : syntactic) :
  a ∈ X → b ∈ Y → y ∈ (X ⊙ Y)^⊥ → (a.1 ++ b.1) ++ y.1 ⊢cf (a.2 ++ b.2) ++ y.2.X, Y: propset syntactic
a, b, y: syntactic
a ∈ X → b ∈ Y → y ∈ (X ⊙ Y)^⊥ → (a.1 ++ b.1) ++ y.1 ⊢cf (a.2 ++ b.2) ++ y.2
Proof.X, Y: propset syntactic
a, b, y: syntactic
a ∈ X → b ∈ Y → y ∈ (X ⊙ Y)^⊥ → (a.1 ++ b.1) ++ y.1 ⊢cf (a.2 ++ b.2) ++ y.2
  intros Ha Hb Hy.X, Y: propset syntactic
a, b, y: syntactic
Ha: a ∈ X
Hb: b ∈ Y
Hy: y ∈ (X ⊙ Y)^⊥
(a.1 ++ b.1) ++ y.1 ⊢cf (a.2 ++ b.2) ++ y.2 rewrite elem_of_orth_syn in Hy.X, Y: propset syntactic
a, b, y: syntactic
Ha: a ∈ X
Hb: b ∈ Y
Hy: ∀ x : syntactic, x ∈ X ⊙ Y → x.1 ++ y.1 ⊢cf x.2 ++ y.2
(a.1 ++ b.1) ++ y.1 ⊢cf (a.2 ++ b.2) ++ y.2 apply (Hy (a · b)).X, Y: propset syntactic
a, b, y: syntactic
Ha: a ∈ X
Hb: b ∈ Y
Hy: ∀ x : syntactic, x ∈ X ⊙ Y → x.1 ++ y.1 ⊢cf x.2 ++ y.2
a · b ∈ X ⊙ Y
  apply elem_of_prod.X, Y: propset syntactic
a, b, y: syntactic
Ha: a ∈ X
Hb: b ∈ Y
Hy: ∀ x : syntactic, x ∈ X ⊙ Y → x.1 ++ y.1 ⊢cf x.2 ++ y.2
∃ a0 b0 : syntactic, a0 ∈ X ∧ b0 ∈ Y ∧ a · b ≡ a0 · b0 by exists a, b.
Qed.

Each variable $p denotes the single phase hyp ($p).

Definition syn_val : nat → propset syntactic := λ p, {[ x | x = hyp ($p) ]}.

Lemma elem_of_syn_val p (x : syntactic) : x ∈ syn_val p ↔ x = hyp ($p).p: nat
x: syntactic
x ∈ syn_val p ↔ x = hyp $p
Proof.p: nat
x: syntactic
x ∈ syn_val p ↔ x = hyp $p unfold syn_val.p: nat
x: syntactic
x ∈ {[ x0 | x0 = hyp $p ]} ↔ x = hyp $p by rewrite elem_of_PropSet. Qed.

Okada's lemma

Each case applies the left or right rule of the connective, and L_use/R_use supply its premises from the induction hypotheses. When the target set is a biorthogonal Y^⊥⊥, it is enough to land in Y (biorth). When the target is a fact ⟦A⟧, it is enough to land in ⟦A⟧^⊥⊥ (interp_fact), that is, to be a counter-bag of ⟦A⟧^⊥.

Lemma okada A : hyp A ∈ ⟦A⟧syn_val ∧ concl A ∈ (⟦A⟧syn_val)^⊥.A: cformula
hyp A ∈ ⟦A⟧syn_val ∧ concl A ∈ ⟦A⟧syn_val^⊥
Proof.A: cformula
hyp A ∈ ⟦A⟧syn_val ∧ concl A ∈ ⟦A⟧syn_val^⊥
  induction A as [p | A [HA1 HA2] | | | | | A [HA1 HA2] B [HB1 HB2]
                 | A [HA1 HA2] B [HB1 HB2] | A [HA1 HA2] B [HB1 HB2]
                 | A [HA1 HA2] B [HB1 HB2] | A [HA1 HA2] | A [HA1 HA2]];
    cbn [interp]; split.p: nat
hyp $p ∈ (syn_val p^⊥)^⊥
p: nat
concl $p ∈ ((syn_val p^⊥)^⊥)^⊥
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
hyp (A^⊥) ∈ ⟦A⟧syn_val^⊥
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
concl (A^⊥) ∈ (⟦A⟧syn_val^⊥)^⊥
hyp 𝟙 ∈ (one_set^⊥)^⊥
concl 𝟙 ∈ ((one_set^⊥)^⊥)^⊥
hyp ⊥ ∈ one_set^⊥
concl ⊥ ∈ (one_set^⊥)^⊥
hyp ⊤ ∈ full_set
concl ⊤ ∈ full_set^⊥
hyp 𝟘 ∈ (∅^⊥)^⊥
concl 𝟘 ∈ ((∅^⊥)^⊥)^⊥
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
hyp (A ⊗ B) ∈ ((⟦A⟧syn_val ⊙ ⟦B⟧syn_val)^⊥)^⊥
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
concl (A ⊗ B) ∈ (((⟦A⟧syn_val ⊙ ⟦B⟧syn_val)^⊥)^⊥)^⊥
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
hyp (A ⅋ B) ∈ (⟦A⟧syn_val^⊥ ⊙ ⟦B⟧syn_val^⊥)^⊥
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
concl (A ⅋ B) ∈ ((⟦A⟧syn_val^⊥ ⊙ ⟦B⟧syn_val^⊥)^⊥)^⊥
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
hyp (A & B) ∈ ⟦A⟧syn_val ∩ ⟦B⟧syn_val
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
concl (A & B) ∈ (⟦A⟧syn_val ∩ ⟦B⟧syn_val)^⊥
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
hyp (A ⊕ B) ∈ ((⟦A⟧syn_val ∪ ⟦B⟧syn_val)^⊥)^⊥
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
concl (A ⊕ B) ∈ (((⟦A⟧syn_val ∪ ⟦B⟧syn_val)^⊥)^⊥)^⊥
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
hyp (!A) ∈ ((⟦A⟧syn_val ∩ cph_J)^⊥)^⊥
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
concl (!A) ∈ (((⟦A⟧syn_val ∩ cph_J)^⊥)^⊥)^⊥
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
hyp (? A) ∈ (⟦A⟧syn_val^⊥ ∩ cph_J)^⊥
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
concl (? A) ∈ ((⟦A⟧syn_val^⊥ ∩ cph_J)^⊥)^⊥
  - (* $p, left: hyp $p ∈ v p *)p: nat
hyp $p ∈ (syn_val p^⊥)^⊥
    apply L_orth.p: nat
∀ x : syntactic, x ∈ syn_val p^⊥ → $p :: x.1 ⊢cf x.2 intros y Hy.p: nat
y: syntactic
Hy: y ∈ syn_val p^⊥
$p :: y.1 ⊢cf y.2
    apply (L_use (syn_val p)); [by apply elem_of_syn_val | done].
  - (* $p, right: the axiom *)p: nat
concl $p ∈ ((syn_val p^⊥)^⊥)^⊥
    apply biorth, R_orth.p: nat
∀ x : syntactic, x ∈ syn_val p → x.1 ⊢cf $p :: x.2 intros x ->%elem_of_syn_val.p: nat
(hyp $p).1 ⊢cf $p :: (hyp $p).2 apply ax.
  - (* A^⊥, left: ^⊥L *)A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
hyp (A^⊥) ∈ ⟦A⟧syn_val^⊥
    apply L_orth.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
∀ x : syntactic, x ∈ ⟦A⟧syn_val → (A^⊥)%cll :: x.1 ⊢cf x.2 intros x Hx.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
x: syntactic
Hx: x ∈ ⟦A⟧syn_val
(A^⊥)%cll :: x.1 ⊢cf x.2 apply negL.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
x: syntactic
Hx: x ∈ ⟦A⟧syn_val
x.1 ⊢cf A :: x.2 by apply (R_use (⟦A⟧syn_val)).
  - (* A^⊥, right: ^⊥R *)A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
concl (A^⊥) ∈ (⟦A⟧syn_val^⊥)^⊥
    apply R_orth.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
∀ x : syntactic, x ∈ ⟦A⟧syn_val^⊥ → x.1 ⊢cf (A^⊥)%cll :: x.2 intros y Hy.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
y: syntactic
Hy: y ∈ ⟦A⟧syn_val^⊥
y.1 ⊢cf (A^⊥)%cll :: y.2 apply negR.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
y: syntactic
Hy: y ∈ ⟦A⟧syn_val^⊥
A :: y.1 ⊢cf y.2 by apply (L_use (⟦A⟧syn_val)).
  - (* 𝟙, left: 𝟙L *)hyp 𝟙 ∈ (one_set^⊥)^⊥
    apply L_orth.∀ x : syntactic, x ∈ one_set^⊥ → 𝟙 :: x.1 ⊢cf x.2 intros y Hy.y: syntactic
Hy: y ∈ one_set^⊥
𝟙 :: y.1 ⊢cf y.2 by apply oneL, orth_one_syn.
  - (* 𝟙, right: 𝟙R *)concl 𝟙 ∈ ((one_set^⊥)^⊥)^⊥
    apply biorth, R_orth.∀ x : syntactic, x ∈ one_set → x.1 ⊢cf 𝟙 :: x.2 intros x ->%elem_of_one_syn.([], []).1 ⊢cf 𝟙 :: ([], []).2 apply oneR.
  - (* ⊥, left: ⊥L *)hyp ⊥ ∈ one_set^⊥
    apply L_orth.∀ x : syntactic, x ∈ one_set → ⊥ :: x.1 ⊢cf x.2 intros x ->%elem_of_one_syn.⊥ :: ([], []).1 ⊢cf ([], []).2 apply botL.
  - (* ⊥, right: ⊥R *)concl ⊥ ∈ (one_set^⊥)^⊥
    apply R_orth.∀ x : syntactic, x ∈ one_set^⊥ → x.1 ⊢cf ⊥ :: x.2 intros y Hy.y: syntactic
Hy: y ∈ one_set^⊥
y.1 ⊢cf ⊥ :: y.2 by apply botR, orth_one_syn.
  - (* ⊤, left: anything *)hyp ⊤ ∈ full_set
    apply elem_of_full.
  - (* ⊤, right: ⊤R *)concl ⊤ ∈ full_set^⊥
    apply R_orth.∀ x : syntactic, x ∈ full_set → x.1 ⊢cf ⊤ :: x.2 intros x _.x: syntactic
x.1 ⊢cf ⊤ :: x.2 apply topR.
  - (* 𝟘, left: 𝟘L *)hyp 𝟘 ∈ (∅^⊥)^⊥
    apply L_orth.∀ x : syntactic, x ∈ ∅^⊥ → 𝟘 :: x.1 ⊢cf x.2 intros y _.y: syntactic
𝟘 :: y.1 ⊢cf y.2 apply zeroL.
  - (* 𝟘, right: vacuous *)concl 𝟘 ∈ ((∅^⊥)^⊥)^⊥
    apply biorth, R_orth.∀ x : syntactic, x ∈ ∅ → x.1 ⊢cf 𝟘 :: x.2 set_solver.
  - (* A ⊗ B, left: ⊗L, using hyp A · hyp B ∈ ⟦A⟧ ⊙ ⟦B⟧ *)A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
hyp (A ⊗ B) ∈ ((⟦A⟧syn_val ⊙ ⟦B⟧syn_val)^⊥)^⊥
    apply L_orth.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
∀ x : syntactic, x ∈ (⟦A⟧syn_val ⊙ ⟦B⟧syn_val)^⊥ → A ⊗ B :: x.1 ⊢cf x.2 intros y Hy.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
y: syntactic
Hy: y ∈ (⟦A⟧syn_val ⊙ ⟦B⟧syn_val)^⊥
A ⊗ B :: y.1 ⊢cf y.2 apply tensorL.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
y: syntactic
Hy: y ∈ (⟦A⟧syn_val ⊙ ⟦B⟧syn_val)^⊥
A :: B :: y.1 ⊢cf y.2
    exact (orth_prod_use _ _ (hyp A) (hyp B) y HA1 HB1 Hy).
  - (* A ⊗ B, right: ⊗R *)A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
concl (A ⊗ B) ∈ (((⟦A⟧syn_val ⊙ ⟦B⟧syn_val)^⊥)^⊥)^⊥
    apply biorth, R_orth.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
∀ x : syntactic, x ∈ ⟦A⟧syn_val ⊙ ⟦B⟧syn_val → x.1 ⊢cf A ⊗ B :: x.2 intros x (a & b & Ha & Hb & H1 & H2)%elem_of_prod_syn.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
x, a, b: syntactic
Ha: a ∈ ⟦A⟧syn_val
Hb: b ∈ ⟦B⟧syn_val
H1: x.1 ≡ₚ a.1 ++ b.1
H2: x.2 ≡ₚ a.2 ++ b.2
x.1 ⊢cf A ⊗ B :: x.2
    apply (ex' (tensorR _ _ _ _ _ A B (R_use _ _ _ HA2 Ha) (R_use _ _ _ HB2 Hb)));
      by rewrite ?H1, ?H2.
  - (* A ⅋ B, left: ⅋L *)A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
hyp (A ⅋ B) ∈ (⟦A⟧syn_val^⊥ ⊙ ⟦B⟧syn_val^⊥)^⊥
    apply L_orth.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
∀ x : syntactic, x ∈ ⟦A⟧syn_val^⊥ ⊙ ⟦B⟧syn_val^⊥ → A ⅋ B :: x.1 ⊢cf x.2 intros x (a & b & Ha & Hb & H1 & H2)%elem_of_prod_syn.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
x, a, b: syntactic
Ha: a ∈ ⟦A⟧syn_val^⊥
Hb: b ∈ ⟦B⟧syn_val^⊥
H1: x.1 ≡ₚ a.1 ++ b.1
H2: x.2 ≡ₚ a.2 ++ b.2
A ⅋ B :: x.1 ⊢cf x.2
    apply (ex' (parL _ _ _ _ _ A B (L_use _ _ _ HA1 Ha) (L_use _ _ _ HB1 Hb)));
      by rewrite ?H1, ?H2.
  - (* A ⅋ B, right: ⅋R, using concl A · concl B ∈ ⟦A⟧^⊥ ⊙ ⟦B⟧^⊥ *)A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
concl (A ⅋ B) ∈ ((⟦A⟧syn_val^⊥ ⊙ ⟦B⟧syn_val^⊥)^⊥)^⊥
    apply R_orth.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
∀ x : syntactic, x ∈ (⟦A⟧syn_val^⊥ ⊙ ⟦B⟧syn_val^⊥)^⊥ → x.1 ⊢cf A ⅋ B :: x.2 intros y Hy.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
y: syntactic
Hy: y ∈ (⟦A⟧syn_val^⊥ ⊙ ⟦B⟧syn_val^⊥)^⊥
y.1 ⊢cf A ⅋ B :: y.2 apply parR.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
y: syntactic
Hy: y ∈ (⟦A⟧syn_val^⊥ ⊙ ⟦B⟧syn_val^⊥)^⊥
y.1 ⊢cf A :: B :: y.2
    exact (orth_prod_use _ _ (concl A) (concl B) y HA2 HB2 Hy).
  - (* A & B, left: &L₁ and &L₂ *)A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
hyp (A & B) ∈ ⟦A⟧syn_val ∩ ⟦B⟧syn_val
    apply elem_of_intersection.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
hyp (A & B) ∈ ⟦A⟧syn_val ∧ hyp (A & B) ∈ ⟦B⟧syn_val split; apply interp_fact, L_orth; intros y Hy.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
y: syntactic
Hy: y ∈ ⟦A⟧syn_val^⊥
A & B :: y.1 ⊢cf y.2
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
y: syntactic
Hy: y ∈ ⟦B⟧syn_val^⊥
A & B :: y.1 ⊢cf y.2
    +A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
y: syntactic
Hy: y ∈ ⟦A⟧syn_val^⊥
A & B :: y.1 ⊢cf y.2 apply withL1.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
y: syntactic
Hy: y ∈ ⟦A⟧syn_val^⊥
A :: y.1 ⊢cf y.2 by apply (L_use (⟦A⟧syn_val)).
    +A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
y: syntactic
Hy: y ∈ ⟦B⟧syn_val^⊥
A & B :: y.1 ⊢cf y.2 apply withL2.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
y: syntactic
Hy: y ∈ ⟦B⟧syn_val^⊥
B :: y.1 ⊢cf y.2 by apply (L_use (⟦B⟧syn_val)).
  - (* A & B, right: &R *)A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
concl (A & B) ∈ (⟦A⟧syn_val ∩ ⟦B⟧syn_val)^⊥
    apply R_orth.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
∀ x : syntactic, x ∈ ⟦A⟧syn_val ∩ ⟦B⟧syn_val → x.1 ⊢cf A & B :: x.2 intros x [Ha Hb]%elem_of_intersection.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
x: syntactic
Ha: x ∈ ⟦A⟧syn_val
Hb: x ∈ ⟦B⟧syn_val
x.1 ⊢cf A & B :: x.2
    apply withR; [by apply (R_use (⟦A⟧syn_val)) | by apply (R_use (⟦B⟧syn_val))].
  - (* A ⊕ B, left: ⊕L *)A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
hyp (A ⊕ B) ∈ ((⟦A⟧syn_val ∪ ⟦B⟧syn_val)^⊥)^⊥
    apply L_orth.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
∀ x : syntactic, x ∈ (⟦A⟧syn_val ∪ ⟦B⟧syn_val)^⊥ → A ⊕ B :: x.1 ⊢cf x.2 intros y Hy.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
y: syntactic
Hy: y ∈ (⟦A⟧syn_val ∪ ⟦B⟧syn_val)^⊥
A ⊕ B :: y.1 ⊢cf y.2
    apply plusL; apply (L_use (⟦A⟧syn_val ∪ ⟦B⟧syn_val)); set_solver.
  - (* A ⊕ B, right: ⊕R₁ and ⊕R₂ *)A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
concl (A ⊕ B) ∈ (((⟦A⟧syn_val ∪ ⟦B⟧syn_val)^⊥)^⊥)^⊥
    apply biorth, R_orth.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
∀ x : syntactic, x ∈ ⟦A⟧syn_val ∪ ⟦B⟧syn_val → x.1 ⊢cf A ⊕ B :: x.2 intros x [Hx | Hx]%elem_of_union.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
x: syntactic
Hx: x ∈ ⟦A⟧syn_val
x.1 ⊢cf A ⊕ B :: x.2
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
x: syntactic
Hx: x ∈ ⟦B⟧syn_val
x.1 ⊢cf A ⊕ B :: x.2
    +A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
x: syntactic
Hx: x ∈ ⟦A⟧syn_val
x.1 ⊢cf A ⊕ B :: x.2 apply plusR1.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
x: syntactic
Hx: x ∈ ⟦A⟧syn_val
x.1 ⊢cf A :: x.2 by apply (R_use (⟦A⟧syn_val)).
    +A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
x: syntactic
Hx: x ∈ ⟦B⟧syn_val
x.1 ⊢cf A ⊕ B :: x.2 apply plusR2.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
B: cformula
HA2: concl A ∈ ⟦A⟧syn_val^⊥
HB1: hyp B ∈ ⟦B⟧syn_val
HB2: concl B ∈ ⟦B⟧syn_val^⊥
x: syntactic
Hx: x ∈ ⟦B⟧syn_val
x.1 ⊢cf B :: x.2 by apply (R_use (⟦B⟧syn_val)).
  - (* !A, left: hyp (!A) ∈ ⟦A⟧ ∩ J, by !D *)A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
hyp (!A) ∈ ((⟦A⟧syn_val ∩ cph_J)^⊥)^⊥
    apply biorth, elem_of_intersection.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
hyp (!A) ∈ ⟦A⟧syn_val ∧ hyp (!A) ∈ cph_J split.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
hyp (!A) ∈ ⟦A⟧syn_val
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
hyp (!A) ∈ cph_J
    +A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
hyp (!A) ∈ ⟦A⟧syn_val apply interp_fact, L_orth.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
∀ x : syntactic, x ∈ ⟦A⟧syn_val^⊥ → !A :: x.1 ⊢cf x.2 intros y Hy.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
y: syntactic
Hy: y ∈ ⟦A⟧syn_val^⊥
!A :: y.1 ⊢cf y.2
      apply bangD.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
y: syntactic
Hy: y ∈ ⟦A⟧syn_val^⊥
A :: y.1 ⊢cf y.2 by apply (L_use (⟦A⟧syn_val)).
    +A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
hyp (!A) ∈ cph_J apply elem_of_J_syn.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
∃ Σ Π : list cformula, hyp (!A) = (‼Σ, ⁇Π) by exists [A], [].
  - (* !A, right: !R, on a reusable context (‼Σ, ⁇Π) *)A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
concl (!A) ∈ (((⟦A⟧syn_val ∩ cph_J)^⊥)^⊥)^⊥
    apply biorth, R_orth.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
∀ x : syntactic, x ∈ ⟦A⟧syn_val ∩ cph_J → x.1 ⊢cf !A :: x.2
    intros x [Hx (Σ & Π & ->)%elem_of_J_syn]%elem_of_intersection.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
Σ, Π: list cformula
Hx: (‼Σ, ⁇Π) ∈ ⟦A⟧syn_val
(‼Σ, ⁇Π).1 ⊢cf !A :: (‼Σ, ⁇Π).2
    apply bangR.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
Σ, Π: list cformula
Hx: (‼Σ, ⁇Π) ∈ ⟦A⟧syn_val
‼Σ ⊢cf A :: ⁇Π exact (R_use _ _ _ HA2 Hx).
  - (* ? A, left: ?L, on a reusable context (‼Σ, ⁇Π) *)A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
hyp (? A) ∈ (⟦A⟧syn_val^⊥ ∩ cph_J)^⊥
    apply L_orth.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
∀ x : syntactic, x ∈ ⟦A⟧syn_val^⊥ ∩ cph_J → ? A :: x.1 ⊢cf x.2 intros x [Hx (Σ & Π & ->)%elem_of_J_syn]%elem_of_intersection.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
Σ, Π: list cformula
Hx: (‼Σ, ⁇Π) ∈ ⟦A⟧syn_val^⊥
? A :: (‼Σ, ⁇Π).1 ⊢cf (‼Σ, ⁇Π).2
    apply whyL.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
Σ, Π: list cformula
Hx: (‼Σ, ⁇Π) ∈ ⟦A⟧syn_val^⊥
A :: ‼Σ ⊢cf ⁇Π exact (L_use _ _ _ HA1 Hx).
  - (* ? A, right: concl (? A) ∈ ⟦A⟧^⊥ ∩ J, by ?D *)A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
concl (? A) ∈ ((⟦A⟧syn_val^⊥ ∩ cph_J)^⊥)^⊥
    apply biorth, elem_of_intersection.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
concl (? A) ∈ ⟦A⟧syn_val^⊥ ∧ concl (? A) ∈ cph_J split.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
concl (? A) ∈ ⟦A⟧syn_val^⊥
A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
concl (? A) ∈ cph_J
    +A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
concl (? A) ∈ ⟦A⟧syn_val^⊥ apply fact_orth, R_orth.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
∀ x : syntactic, x ∈ (⟦A⟧syn_val^⊥)^⊥ → x.1 ⊢cf ? A :: x.2 intros y Hy.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
y: syntactic
Hy: y ∈ (⟦A⟧syn_val^⊥)^⊥
y.1 ⊢cf ? A :: y.2
      apply whyD.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
y: syntactic
Hy: y ∈ (⟦A⟧syn_val^⊥)^⊥
y.1 ⊢cf A :: y.2 apply (R_use (⟦A⟧syn_val)); [done | by apply interp_fact].
    +A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
concl (? A) ∈ cph_J apply elem_of_J_syn.A: cformula
HA1: hyp A ∈ ⟦A⟧syn_val
HA2: concl A ∈ ⟦A⟧syn_val^⊥
∃ Σ Π : list cformula, concl (? A) = (‼Σ, ⁇Π) by exists [], [A].
Qed.

Two direct consequences: in the syntactic model, every bag of A proves A, and every counter-bag of A refutes A.

Corollary okada_bag A (x : syntactic) : x ∈ ⟦A⟧syn_val → x.1 ⊢cf A :: x.2.A: cformula
x: syntactic
x ∈ ⟦A⟧syn_val → x.1 ⊢cf A :: x.2
Proof.A: cformula
x: syntactic
x ∈ ⟦A⟧syn_val → x.1 ⊢cf A :: x.2 apply R_use, okada. Qed.

Corollary okada_counter A (y : syntactic) :
  y ∈ (⟦A⟧syn_val)^⊥ → A :: y.1 ⊢cf y.2.A: cformula
y: syntactic
y ∈ ⟦A⟧syn_val^⊥ → A :: y.1 ⊢cf y.2
Proof.A: cformula
y: syntactic
y ∈ ⟦A⟧syn_val^⊥ → A :: y.1 ⊢cf y.2 apply L_use, okada. Qed.

Every two-sided context is a phase of its own sequent: (Γ, Δ) is the product of the hyp A for A ∈ Γ and the concl B for B ∈ Δ.

Lemma ctx_self Γ Δ : ((Γ, Δ) : syntactic) ∈ ⨀ (sq syn_val Γ Δ).Γ, Δ: list cformula
((Γ, Δ) : syntactic) ∈ ⨀ sq syn_val Γ Δ
Proof.Γ, Δ: list cformula
((Γ, Δ) : syntactic) ∈ ⨀ sq syn_val Γ Δ
  induction Γ as [| A Γ IH]; [induction Δ as [| B Δ IH] |];
    cbn [sq map app bigprod].([], []) ∈ one_set
B: cformula
Δ: list cformula
IH: ([], Δ) ∈ ⨀ sq syn_val [] Δ
([], B :: Δ) ∈ ⟦B⟧syn_val^⊥ ⊙ ⨀ map (λ B0 : cformula, ⟦B0⟧syn_val^⊥) Δ
A: cformula
Γ, Δ: list cformula
IH: (Γ, Δ) ∈ ⨀ sq syn_val Γ Δ
(A :: Γ, Δ)
∈ ⟦A⟧syn_val
  ⊙ ⨀ (map (interp syn_val) Γ ++ map (λ B : cformula, ⟦B⟧syn_val^⊥) Δ)
  -([], []) ∈ one_set by apply elem_of_one_syn.
  -B: cformula
Δ: list cformula
IH: ([], Δ) ∈ ⨀ sq syn_val [] Δ
([], B :: Δ) ∈ ⟦B⟧syn_val^⊥ ⊙ ⨀ map (λ B0 : cformula, ⟦B0⟧syn_val^⊥) Δ apply elem_of_prod.B: cformula
Δ: list cformula
IH: ([], Δ) ∈ ⨀ sq syn_val [] Δ
∃ a b : syntactic,
  a ∈ ⟦B⟧syn_val^⊥
  ∧ b ∈ ⨀ map (λ B0 : cformula, ⟦B0⟧syn_val^⊥) Δ ∧ ([], B :: Δ) ≡ a · b exists (concl B), ([], Δ).B: cformula
Δ: list cformula
IH: ([], Δ) ∈ ⨀ sq syn_val [] Δ
concl B ∈ ⟦B⟧syn_val^⊥
∧ ([], Δ) ∈ ⨀ map (λ B0 : cformula, ⟦B0⟧syn_val^⊥) Δ
  ∧ ([], B :: Δ) ≡ concl B · ([], Δ)
    split_and!; [apply okada | exact IH | done].
  -A: cformula
Γ, Δ: list cformula
IH: (Γ, Δ) ∈ ⨀ sq syn_val Γ Δ
(A :: Γ, Δ)
∈ ⟦A⟧syn_val
  ⊙ ⨀ (map (interp syn_val) Γ ++ map (λ B : cformula, ⟦B⟧syn_val^⊥) Δ) apply elem_of_prod.A: cformula
Γ, Δ: list cformula
IH: (Γ, Δ) ∈ ⨀ sq syn_val Γ Δ
∃ a b : syntactic,
  a ∈ ⟦A⟧syn_val
  ∧ b ∈ ⨀ (map (interp syn_val) Γ ++ map (λ B : cformula, ⟦B⟧syn_val^⊥) Δ)
    ∧ (A :: Γ, Δ) ≡ a · b exists (hyp A), (Γ, Δ).A: cformula
Γ, Δ: list cformula
IH: (Γ, Δ) ∈ ⨀ sq syn_val Γ Δ
hyp A ∈ ⟦A⟧syn_val
∧ (Γ, Δ) ∈ ⨀ (map (interp syn_val) Γ ++ map (λ B : cformula, ⟦B⟧syn_val^⊥) Δ)
  ∧ (A :: Γ, Δ) ≡ hyp A · (Γ, Δ)
    split_and!; [apply okada | exact IH | done].
Qed.

The main theorems

Completeness: a valid sequent has a cut-free proof. Validity in the syntactic model puts (Γ, Δ) in the pole, and the pole is cut-free provability.

Theorem completeness Γ Δ : Γ ⊨ Δ → Γ ⊢cf Δ.Γ, Δ: list cformula
Γ ⊨ Δ → Γ ⊢cf Δ
Proof.Γ, Δ: list cformula
Γ ⊨ Δ → Γ ⊢cf Δ
  intros H.Γ, Δ: list cformula
H: Γ ⊨ Δ
Γ ⊢cf Δ apply (elem_of_pole_syn (Γ, Δ)), (H syntactic syn_val (Γ, Δ)), ctx_self.
Qed.

Cut elimination: every proof can be replaced by a cut-free one.

Theorem cut_elimination Γ Δ : Γ ⊢ Δ → Γ ⊢cf Δ.Γ, Δ: list cformula
Γ ⊢ Δ → Γ ⊢cf Δ
Proof.Γ, Δ: list cformula
Γ ⊢ Δ → Γ ⊢cf Δ intros H.Γ, Δ: list cformula
H: Γ ⊢ Δ
Γ ⊢cf Δ by apply completeness, (soundness true). Qed.

As a consequence, cut is admissible in the cut-free calculus.

Corollary cut_admissible Γ₁ Γ₂ Δ₁ Δ₂ A :
  Γ₁ ⊢cf A :: Δ₁ → A :: Γ₂ ⊢cf Δ₂ → Γ₁ ++ Γ₂ ⊢cf Δ₁ ++ Δ₂.Γ₁, Γ₂, Δ₁, Δ₂: list cformula
A: cformula
Γ₁ ⊢cf A :: Δ₁ → A :: Γ₂ ⊢cf Δ₂ → Γ₁ ++ Γ₂ ⊢cf Δ₁ ++ Δ₂
Proof.Γ₁, Γ₂, Δ₁, Δ₂: list cformula
A: cformula
Γ₁ ⊢cf A :: Δ₁ → A :: Γ₂ ⊢cf Δ₂ → Γ₁ ++ Γ₂ ⊢cf Δ₁ ++ Δ₂
  intros H1 H2.Γ₁, Γ₂, Δ₁, Δ₂: list cformula
A: cformula
H1: Γ₁ ⊢cf A :: Δ₁
H2: A :: Γ₂ ⊢cf Δ₂
Γ₁ ++ Γ₂ ⊢cf Δ₁ ++ Δ₂ apply cut_elimination, (cut _ _ _ _ _ A); [done | |];
    by apply cf_to_full.
Qed.

All three notions coincide.

Theorem provable_valid_cutfree Γ Δ :
  (Γ ⊢ Δ ↔ Γ ⊨ Δ) ∧ (Γ ⊨ Δ ↔ Γ ⊢cf Δ).Γ, Δ: list cformula
(Γ ⊢ Δ ↔ Γ ⊨ Δ) ∧ (Γ ⊨ Δ ↔ Γ ⊢cf Δ)
Proof.Γ, Δ: list cformula
(Γ ⊢ Δ ↔ Γ ⊨ Δ) ∧ (Γ ⊨ Δ ↔ Γ ⊢cf Δ)
  split; split.Γ, Δ: list cformula
Γ ⊢ Δ → Γ ⊨ Δ
Γ, Δ: list cformula
Γ ⊨ Δ → Γ ⊢ Δ
Γ, Δ: list cformula
Γ ⊨ Δ → Γ ⊢cf Δ
Γ, Δ: list cformula
Γ ⊢cf Δ → Γ ⊨ Δ
  -Γ, Δ: list cformula
Γ ⊢ Δ → Γ ⊨ Δ apply soundness.
  -Γ, Δ: list cformula
Γ ⊨ Δ → Γ ⊢ Δ intros H.Γ, Δ: list cformula
H: Γ ⊨ Δ
Γ ⊢ Δ by apply cf_to_full, completeness.
  -Γ, Δ: list cformula
Γ ⊨ Δ → Γ ⊢cf Δ apply completeness.
  -Γ, Δ: list cformula
Γ ⊢cf Δ → Γ ⊨ Δ apply soundness.
Qed.