# Natural Deduction for IEL

Require Export forms.
Require Import List Permutation.
Require Import Coq.Program.Equality.
Require Import Coq.Arith.Max.
From Equations Require Import Equations.
Require Import PslBase.Base.

First, we add a type for contexts and proof some basic facts about subsets, define notation for element.
Definition theory := form -> Prop.
Notation context := (list form).
Implicit Type Γ Ω : context.
Implicit Type T U: theory.
Implicit Types ϕ ψ: form.
Definition subset T U := forall ϕ, T ϕ -> U ϕ.
Definition equalCtx T U := forall ϕ, T ϕ <-> U ϕ.
Definition unionCtx T U := fun z => T z \/ U z.
Definition elem T ϕ := T ϕ.
Definition consT ϕ T := fun z => z = ϕ \/ T z.
Define Notation for Contexts
Notation "A ∪ B" := (unionCtx A B) (at level 50).
Notation "A ≡ B" := (equalCtx A B) (at level 50).
Notation "a ∈ B" := (elem B a) (at level 20).
Notation "A ⊆ B" := (subset A B) (at level 10).
Notation "s # Γ" := (consT s Γ) (at level 30).
Inductive DerivationType := minus | normal.

Existing Class DerivationType.

## Natural Deduction

We define deduction for contexts first

Inductive nd : forall (D: DerivationType), list form -> form -> Prop :=
| ndA {D} (Γ: list form) s :List.In s Γ -> (nd D Γ s)
| ndE {D} (Γ: list form) s : (nd D Γ Bot) -> (nd D Γ s)

| ndII {D} (Γ: list form) s t : (nd D (s::Γ) t) -> (nd D Γ (s t))
| ndIE {D} (Γ: list form) s t : (nd D Γ (s t)) -> (nd D Γ s) -> (nd D Γ t)
| ndKImp {D} (Γ: list form) s t: (nd D Γ (K(s t))) -> (nd D Γ (K s K t))
| ndKpos {D} (Γ: list form) s: (nd D Γ s) -> (nd D Γ (K s))
| ndCEL {D} (Γ: list form) s t: nd D Γ (s t) -> nd D Γ s
| ndCER {D} (Γ: list form) s t: nd D Γ (s t) -> nd D Γ t
| ndCI {D} (Γ: list form) s t: nd D Γ s -> nd D Γ t -> nd D Γ (s t)
| ndDIL {D} (Γ: list form) s t: nd D Γ s -> (nd D Γ (s t))
| ndDIR {D} (Γ: list form) s t: nd D Γ t -> (nd D Γ (s t))
| ndDE {D} (Γ: list form) s t q: (nd D Γ (s t)) -> (nd D Γ (s q)) -> (nd D Γ (t q)) -> (nd D Γ q)
| ndIntRefl (Γ: list form) s: (nd normal Γ (K s)) -> (nd normal Γ (¬ ¬s))
.

Definition ndminus := @nd minus.
Global Hint Constructors nd : core export.

We reduce the theory case to existence of a contained sublist
Definition ndT (D: DerivationType) T ϕ :=
exists L, (forall ψ, ψ el L -> T ψ) /\ @nd D L ϕ.

Arguments nd {_} _ _.
Arguments ndT {_} _ _.
Define notations for the derivation
Global Notation "Γ ⊢ φ" := (nd Γ φ) (at level 40).
Global Notation "T ⊢T φ" := (ndT T φ) (at level 40).

Global Notation "Γ ⊢+ φ" := (@nd normal Γ φ) (at level 40).
Global Notation "T ⊢T+ φ" := (@ndT normal T φ) (at level 40).

Global Notation "Γ ⊢- φ" := (@nd minus Γ φ) (at level 40).
Global Notation "T ⊢T- φ" := (@ndT minus T φ) (at level 40).

## Weakening

We show weakening for contexts and theories.
Section Weakening.
Context {d : DerivationType}.

Fact ndtW φ T U:
T T φ -> T U -> U T φ.
Proof.
firstorder eauto.
Qed.

Fact ndW Γ φ Ω :
( Γ φ -> Γ <<= Ω -> Ω φ).
Proof.
intro H. revert Ω. induction H;eauto.
Qed.
(* For backwards compatability *)
Definition weak := ndW.

Lemma consWeak Γ ϕ ψ: Γ ϕ -> (ψ::Γ) ϕ.
Proof.
intro. apply ndW with (Γ := Γ); firstorder eauto.
Qed.

Fact derivationExtensional Γ Ω :
(Γ === Ω) -> (forall φ, Ω φ <-> Γ φ).
Proof.
intros. split; firstorder eauto using ndW.
Qed.
End Weakening.

We show the nd rules admissible for theories (ndT), we need weakening for nd to do this
Context {d : DerivationType}.
Variable (T: theory).
Fact ndtA s: T s -> T T s.
Proof.
intro. exists [s]; firstorder eauto. rewrite<- H0. auto.
Qed.

Fact ndtE s: ndT T -> T T s.
Proof.
intro. destruct H as [lB Hb]. exists lB. split; firstorder eauto.
Qed.

Fact ndtII s t: (s#T) T t -> T T (s t).
Proof.
intros.
destruct H as [lT lht].
exists (rem lT s). split. destruct lht. intros a Ha. specialize (H a). destruct H. apply in_rem_iff in Ha. firstorder.
subst a. apply in_rem_iff in Ha; tauto. auto. apply ndII. destruct lht. apply ndW with lT. auto.
intros a Ha. decide (s = a). subst a; firstorder. right. firstorder eauto.
Qed.

Fact ndtIE s t: (T) T (s t) -> T T s -> T T t.
Proof.
intros. destruct H as [lH H], H0 as [lH0 H0]. exists (lH++lH0). split.
- intros ψ Hp. apply in_app_iff in Hp. firstorder eauto.
- apply ndIE with s.
+ apply ndW with lH. tauto. auto.
+ apply ndW with lH0; firstorder eauto.
Qed.

Fact ndtKImp s t: T T (K(s t)) -> T T (K s K t).
Proof.
firstorder eauto.
Qed.

Fact ndtKpos s: T T s -> T T (K s).
Proof.
firstorder auto.
Qed.

Fact ndtCEL s t: ndT T (s t) -> ndT T s.
Proof.
firstorder eauto.
Qed.

Fact ndtCER s t: ndT T (s t) -> ndT T t.
Proof.
firstorder eauto.
Qed.

Fact ndtCI s t: ndT T s -> ndT T t -> ndT T (s t).
Proof.
intros Hs Ht. destruct Hs as [ls [Hs1 Hs2]], Ht as [lt [Ht1 Ht2]].
exists (ls++lt); firstorder eauto.
- apply in_app_iff in H. destruct H; auto.
- apply ndCI; firstorder eauto using ndW.
Qed.

Fact ndtDIL s t: ndT T s -> ndT T (s t).
Proof.
firstorder eauto.
Qed.

Fact ndtDIR s t: ndT T t -> ndT T (s t).
Proof.
firstorder eauto.
Qed.

Fact ndtDE s t q: ndT T (s t) -> ndT T (s q) -> ndT T (t q) -> ndT T q.
Proof.
intros Hs Ht Hq. destruct Hs as [ls [Hs1 Hs2]], Ht as [lt [Ht1 Ht2]], Hq as [lq [Hq1 Hq2]].
exists (ls++lt++lq); firstorder eauto.
- apply in_app_iff in H; destruct H; auto. apply in_app_iff in H. destruct H; eauto.
- apply ndDE with s t; firstorder eauto using ndW.
Qed.

Fact ndtIntRefl s: @ndT normal T (K s) -> @ndT normal T (¬ ¬ s).
Proof.
intro. firstorder eauto.
Qed.

We can show implication agreement:
Lemma ImpAgree (D: DerivationType) (Γ: theory) (a b: form) :
Γ T (a b) <-> (a#Γ T b).
Proof.
split.
- intro H. apply ndtIE with a; auto. apply ndtW with Γ; firstorder eauto.
apply ndtA. firstorder eauto.
- intros. apply ndtII. firstorder eauto.
Qed.

List and context derivation transaltion
Section Transl.
Definition ctx2thy (Γ: context) : theory := fun x => In x Γ.

Lemma ndTEq {D: DerivationType} Γ s: nd Γ s <-> ndT (ctx2thy Γ) s.
Proof.
split.
- intro. exists Γ. firstorder eauto.
- intro. destruct H as [lH H]. apply weak with lH; firstorder eauto.
Qed.
End Transl.

Fixpoint shift (l: list form) (s: form) :=
match l with
nil => s
| (x::xr) => (x (shift xr s)) end.

Definition kIfy (l: list form) := map K l.

## Modal shifting lemma

Section shifting.
Context {d : DerivationType}.

Lemma ImplDistr (Γ: context) (a b:form) :
(Γ (K(a b))) -> (Γ ((K a) (K b))).
Proof.
intros. apply ndKImp. exact H.
Qed.

Lemma ImpAss (Γ: context) (a b: form) :
(Γ (a b)) <-> (nd (a::Γ) b).
Proof.
split.
- intros.
apply ndIE with (s := a). apply consWeak. exact H.
apply ndA. left. auto.
- intros. apply ndII. exact H.
Qed.

Lemma kIfys2 (l: list form) (s: form):
forall Γ, (Γ (K (shift (l) (s)))) -> Γ (shift (map K l) (K s)).
Proof.
induction l.
+ intros. simpl map. simpl shift. simpl shift in H. exact H.
+ intros. simpl map. simpl shift. apply ndII. apply IHl. apply ImpAss.
apply ndKImp. exact H.
Qed.

Lemma partialShift (l1 l2: context) (s: form):
(l1++l2) s <-> l1 (shift l2 s).
Proof.
revert l1. revert s. induction l2; intros.
- simpl shift. rewrite app_nil_r. tauto.
- split.
+ intro. apply ndII. apply IHl2. apply ndW with (l1++a::l2); auto.
+ intro. apply ndW with (a::(l1++l2)).
simpl shift in H. apply ImpAss in H. apply IHl2 in H. auto.
intros x Hx. destruct Hx as [Hx | Hx]; try apply in_app_iff in Hx; try subst x;try destruct Hx; eauto.
Qed.
The next lemma shows that Krupski's rule from the sequent calculus is admissible in IEL
Fact ndKKrupski (l1 l2: context) (s: form):
(l1++l2++(List.map K l1)) s -> (l2++(List.map K l1)) (K s).
Proof.
intro.
apply ndW with ((l2 ++ map K l1) ++ (map K l1)); auto.
apply partialShift, kIfys2, ndKpos. apply-> partialShift.
apply ndW with (l1++l2++map K l1); auto.
Qed.

Now we can prove the modal shifting lemma.
Definition unbox (Γ: theory) : theory :=
fun x => Γ (K x).

Lemma unbox_rewrite (Γ: theory): forall φ,
(Γ (K φ)) <-> ((unbox Γ) φ).
Proof.
firstorder.
Qed.
Import ListNotations.

Lemma modalShiftingLemma (Γ: theory) (s: form):
ndT (unbox Γ ) s -> ndT Γ (K s).
Proof.
intros H0.
destruct H0 as [y [H0]].
exists (List.map K y). split.
- intros. eauto. apply in_map_iff in H1. destruct H1 as [z Hz]. destruct Hz. rewrite<- H1. apply H0. auto.
-
assert ((map K y) = ([]++(map K y))).
{ rewrite app_nil_l. auto. }
rewrite H1. apply partialShift, kIfys2, ndKpos.
apply-> partialShift. rewrite app_nil_l. auto.
Qed.

End shifting.

## Prime theories and contexts

Section Contexts.
Context {d : DerivationType}.

We begin by defining what a theory is
Definition dedClosed (T: theory) := forall φ, (T T φ) -> T φ.
Definition consistent (T: theory) : Prop := ~(T T ).

Definition is_prime (T: theory) := forall φ ψ, (T T (φ ψ) -> T T φ \/ T T ψ).
Definition is_primeDN (T: theory) := forall φ ψ, ~~(T T (φ ψ) -> (T T φ \/ T T ψ)).

### Lindenbaum Lemma

We will proof the Lindenbaum Lemma, which states that any set L of formulae which does not derive φ can be extended to a set of formula which
• is prime
• is a theory
• does not derive φ
Note, that such a set is consistent (otherwise it would derive φ )

Definition insert_form (Γ: theory) (φ ψ : form) : theory :=
fun z => (Γ z \/ (~(ndT (ψ#Γ) φ) /\ ψ = z)).

Definition insert_num (Γ: theory) (φ: form) (n: nat) :=
insert_form Γ φ (decode n).
Equations maxn (Gamma: theory) (φ: form) (n: nat) : theory :=
maxn Gamma φ 0 := Gamma;
maxn Gamma φ (S n) := insert_num (maxn Gamma φ n) φ n.

Definition max (Gamma: theory) (φ: form) : theory :=
fun z =>
exists n, (maxn Gamma φ n) z.

### Subset properties

Lemma insert_form_subset (Γ: theory) φ ψ: Γ (insert_form Γ φ ψ).
Proof.
intros x H. left. exact H.
Qed.

Lemma insert_phi_subset (Γ: theory) φ i : Γ (insert_num Γ φ i).
Proof.
unfold insert_num. apply insert_form_subset.
Qed.

Lemma maxn_subset (Γ: theory) φ i: Γ (maxn Γ φ i).
Proof.
induction i.
simpl. intros a B. assumption.
intros a H. simp maxn. unfold insert_num. unfold insert_form. left. auto.
Qed.

Fact max_subset (Γ: theory) φ: Γ (max Γ φ).
Proof.
intros x H. exists 0. auto.
Qed.
End Contexts.

Section Chaining.
(* We proof, that if Δ = ∪ Δ_i derives a formula φ there already is a level i, s.t. Δ_i derives φ. *)
Variable (D: DerivationType).
Lemma max_In_lemma (Γ: theory) φ ψ: (max Γ φ) ψ <-> exists i, (maxn Γ φ i) ψ.
Proof.
firstorder.
Qed.

Lemma maxn_subset_ij i j (Γ: theory) φ: i <= j -> (maxn Γ φ i) (maxn Γ φ j).
Proof.
intro. induction H; firstorder.
Qed.

Lemma maxnlist (l: list form) (Γ: theory) φ: (forall x, (List.In x l -> (max Γ φ) x)) -> exists i, forall x, (List.In x l -> (maxn Γ φ i) x ).
Proof.
induction l. (* TODO: Use length induction here *)
+ intros. exists 0. intro. specialize (H x). intro. exfalso. apply H0.
+ intros.
assert (exists i, forall x, List.In x l -> maxn Γ φ i x).
apply IHl. intros x H1. apply (H x). right. assumption.
(specialize (H a)).
assert (exists i, maxn Γ φ i a).
{
rewrite<- max_In_lemma.
apply H.
left. auto.
}
destruct H0 as [li lH]. destruct H1 as [ai aH].
exists (Nat.max li ai).
intros ψ L.
destruct L.
- apply maxn_subset_ij with (i := ai) (j := Nat.max li ai). apply le_max_r.
rewrite<- H0. apply aH.
- apply maxn_subset_ij with (i := li) (j := Nat.max li ai). apply le_max_l.
apply lH. assumption.
Qed.
Fact maxn_chain (Γ: theory) φ ψ:
(ndT (max Γ φ) ψ) <-> exists i, (ndT (maxn Γ φ i) ψ).
Proof.
split.
intro. destruct H as (l & linc & H).
assert (exists i, forall x', List.In x' l -> (maxn Γ φ i) x').
{
eauto using maxnlist.
}
destruct H0 as [ni nH].
exists ni.
exists l. auto.
+ intro. firstorder eauto.
Qed.
End Chaining.

Section Lindenbaum.
Variable (Dt: DerivationType).
Lemma does_not_derive_i (Γ: theory) φ i:
~(ndT Γ φ) -> ~(ndT (maxn Γ φ i) φ).
Proof.
induction i.
- intuition.
- intros nP. specialize (IHi nP).
intro.
apply IHi.
apply ndtW with (maxn Γ φ (S i)); auto.
intros a Ha. simp maxn in Ha. destruct Ha.
+ auto.
+ destruct H0. exfalso. apply H0. apply ndtW with (maxn Γ φ (S i)).
auto.
simp maxn. unfold insert_num. intros x Hx. destruct Hx; eauto.
firstorder eauto.
firstorder eauto.
Qed.

Fact does_not_derive (Γ: theory) φ:
~(ndT Γ φ) -> ~(ndT (max Γ φ) φ).
Proof.
intros. intro D.
apply maxn_chain in D. destruct D.
pose (does_not_derive_i H H0). auto.
Qed.

Lemma subset_derives (A B: theory) φ: A B -> ~(B T φ) -> ~(A T φ).
Proof.
intros H H0. intro H1. apply H0. apply ndtW with (T := A); auto.
Qed.
Theory property
Fact maxIsTheory (Γ: theory) φ ψ: ~(ndT Γ φ) -> (ndT (max Γ φ) ψ) -> (max Γ φ ψ).
Proof.
intros D M.
apply max_In_lemma.
destruct (decode_surj ψ).
exists (S x).
simp maxn.
unfold insert_num. rewrite H. unfold insert_form.
right. split. 2: reflexivity. intro.
assert (max Γ φ T φ).
apply ndtIE with (s := ψ). apply ndtII. apply ndtW with# maxn Γ φ x) . auto. intros a Ha; destruct Ha; firstorder auto. auto.
apply does_not_derive in D.
congruence.
Qed.

Lemma equalCtxCons A B a: A B -> a#A a#B.
Proof.
firstorder.
Qed.

Lemma max_nd_is_in (Γ: theory) φ γ: ~(ndT Γ φ) ->
((max Γ φ) T γ) <-> ((max Γ φ γ)).
Proof.
intros.
split. intro. apply maxIsTheory; auto.
intro. apply ndtA. auto.
Qed.

Lemma wm (P: Prop) : ~~(P \/ ~P).
tauto.
Qed.

Lemma max_does_not_derive_lemma (Γ: theory) φ ψ:
~( Γ T φ) -> ~((max Γ φ) ψ) -> ~~((max Γ φ) T (ψ φ)).
Proof.
intros D M.
intro.
(* ψ has a number in the enumeration *)
destruct (decode_surj ψ) as [npsi Hnpsi].
specialize wm with (@maxn Dt Γ φ (S npsi) ψ). intro. destruct H0.
intro. destruct H0.
- apply M. exists (S npsi). auto.
- apply H0. simp maxn. unfold insert_num. unfold insert_form. right. split.
2: auto.
intro. apply ImpAgree in H1. rewrite Hnpsi in H1.
apply H. apply ndtW with (maxn Γ φ npsi). exact H1.
intros a Ha. exists npsi. auto.
Qed.

### Primeness properties

Fact maxprime (Γ: theory) φ: ~(ndT Γ φ) -> is_primeDN (max Γ φ).
Proof.
intros H ϕ ψ.
intro.
specialize wm with ((@max Dt Γ φ) ψ).
intro. apply H1. clear H1. intro.
destruct H1.
apply H0. eauto using ndtA.

specialize wm with (((@max Dt Γ φ) ϕ)).
intro. apply H2. clear H2. intro.
destruct H2.

eauto using ndtA.
apply H0. intro.
apply max_does_not_derive_lemma in H1.
apply max_does_not_derive_lemma in H2.
assert (~~ (max Γ φ T φ)).
{
intro. apply H1. intro. apply H2. intro. apply H4. apply ndtDE with ϕ ψ; auto.
}
apply does_not_derive in H. exfalso. apply H4. auto. auto. auto.
Qed.

Lemma Lindenbaum (Γ: theory) (φ: form): ~(ndT Γ φ) ->
Γ (max Γ φ) /\ ~(ndT (max Γ φ) φ) /\ is_primeDN (max Γ φ) /\ dedClosed (max Γ φ).
Proof.
split.
+ apply max_subset.
+ split.
- apply does_not_derive. exact H.
- split.
-- apply maxprime. exact H.
-- intros x H1. apply maxIsTheory. exact H. exact H1.
Defined.

End Lindenbaum.

## Truth Conditions and Derivations

Section Derivations.
(* In this section derive for IEL *)
Definition empty :theory := fun x => False.
Notation "∅" := empty.
Lemma tripleNegIEL (Γ: theory) {d: DerivationType} ϕ:
(Γ T (¬ϕ)) <-> (Γ T ¬ ¬ ¬ ϕ).
Proof.
split.
- intro H. apply ndtII. apply ndtIE with (s := ¬ ϕ). apply ndtA. firstorder.
apply ndtII. apply ndtIE with (s := ϕ). apply ndtW with Γ. exact H.
firstorder eauto. apply ndtA. firstorder eauto.
- intro H. apply ndtII. apply ndtIE with (s := ¬ ¬ ϕ).
apply ndtW with Γ. exact H. firstorder eauto. apply ndtII. apply ndtIE with (s := ϕ).
apply ndtA. firstorder eauto.
apply ndtA. firstorder eauto.
Qed.

Lemma IELKBot: (@ndT normal empty (¬ (K ))).
Proof.
apply ndtII.
apply ndtIE with (s := ¬ ¬ ).
- apply ndtII. apply ndtIE with (s := (¬ )). apply ndtA; firstorder eauto. apply ndtII. apply ndtA; firstorder eauto.
- apply ndtIntRefl. apply ndtA. firstorder eauto.
Qed.

Lemma IELTruthB ϕ: (@ndT normal empty (¬(K ϕ ¬ ϕ))).
Proof.
apply ndtII.
apply ndtIE with (s := (¬ ¬ ϕ)).
+ apply ndtII. apply ndtIE with (s := ¬ ϕ). try apply ndtA; firstorder eauto.
apply ndtCER with (s := (K ϕ)); apply ndtA; firstorder eauto.
+ apply ndtIntRefl. apply ndtCEL with (t := ¬ ϕ). apply ndtA. firstorder eauto 7.
Qed.

Lemma IELContra {d': DerivationType} (ϕ ψ: form) (A: theory): ndT A (ϕ ψ) -> ndT A ((¬ ψ) (¬ ϕ)).
Proof.
intro H.
repeat apply ndtII. apply ndtIE with (s := ψ). apply ndtA; firstorder eauto.
apply ndtIE with (s := ϕ). apply ndtW with A. exact H. firstorder eauto. apply ndtA. firstorder eauto.
Qed.

Lemma IELTruthC ϕ: (@ndT normal empty ((¬ ϕ) (¬ K ϕ))).
Proof.
apply ndtII.
apply ndtIE with (s := ¬ ¬ ¬ ϕ).
+ apply IELContra.
apply ndtII. apply ndtIntRefl. apply ndtA. firstorder eauto.
+ rewrite <- tripleNegIEL. apply ndtA. firstorder eauto.
Qed.
Lemma linCoq (X Y: Prop): ((~ ~ X) -> (~~Y)) -> (~~ (X -> Y)).
Proof.
tauto.
Qed.

Lemma ndTautologyNotNotX (X Y: form) {D: DerivationType} :
(ndT empty ((((¬ ¬ X) (¬ ¬ Y)) (¬ ¬ (X Y))))) /\ (ndT empty ((¬ ¬ (X Y)) ((¬ ¬ X) (¬ ¬ Y)))).
Proof.
split.
- repeat apply ndtII.
apply ndtIE with (s := (X Y)). apply ndtA; firstorder eauto.
apply ndtII. apply ndtE. apply ndtIE with (s := ¬ Y).
apply ndtIE with (s := ((X ) )). apply ndtA; firstorder eauto.
apply ndtII. apply ndtIE with (s := X); apply ndtA; firstorder eauto.
apply ndtII. apply ndtIE with (s := (X Y)). apply ndtA; firstorder eauto. apply ndtII. apply ndtA; firstorder eauto.
- repeat apply ndtII. apply ndtIE with (s := ((X Y) )).
apply ndtA; firstorder eauto.
apply ndtII. apply ndtIE with (s := (X )).
apply ndtA; firstorder eauto.
apply ndtII.
apply ndtIE with (s := Y). apply ndtA; firstorder eauto.
apply ndtIE with (s := X); apply ndtA; firstorder eauto.
Qed.

Lemma IELTruthD ϕ: (@ndT normal empty (¬ ¬ (K ϕ ϕ))).
Proof.
pose (@ndTautologyNotNotX (K ϕ) ϕ normal) as H.
destruct H.
apply ndtIE with (s := (((K ϕ ) ) (ϕ ) )).
auto.
apply IELContra.
apply IELTruthC.
Qed.
Lemma t6 ϕ (Γ: theory): @ndT normal Γ ((K (¬ ϕ)) ¬ ϕ).
Proof.
apply ndtII.
apply tripleNegIEL. apply ndtIntRefl.
apply ndtA.
firstorder eauto.
Qed.
Lemma implToCoq (Γ: theory) {d: DerivationType} ϕ ψ: (Γ T (ϕ ψ) -> ((Γ T ϕ) -> (Γ T ψ))).
Proof.
- intros H H0.
apply ndtIE with (s := ϕ); firstorder eauto.
Qed.

Lemma t6C ϕ (Γ: theory): @ndT normal Γ (K (¬ ϕ)) -> @ndT normal Γ (¬ ϕ).
Proof.
apply implToCoq.
apply t6.
Qed.

Lemma t7 ϕ : T+ ((¬ (K ϕ)) (K (¬ ϕ))) /\ T+ ((K (¬ ϕ)) ¬ (K ϕ)).
Proof.
split.
- apply ndtII.
apply ndtIE with (s := ¬ ϕ).
apply ndtII. apply ndtKpos. apply ndtA; firstorder eauto.
rewrite<- ImpAgree.
apply IELContra.
apply ndtII.
apply ndtKpos.
apply ndtA; firstorder eauto.
- apply ndtII.
apply ndtIE with (s := ¬ ϕ).
apply ndtW with .
apply IELTruthC.
firstorder eauto.
rewrite<- ImpAgree.
apply t6.
Qed.

Lemma t8 ϕ: T+ ((¬ K ϕ) <--> (¬ ϕ)).
Proof.
apply ndtCI.
apply IELContra.
apply ndtII.
apply ndtKpos.
apply ndtA; firstorder eauto.
apply ndtII.
apply ndtIE with (s := (K (¬ϕ))).
apply ndtW with empty.
destruct (t7 ϕ). auto. firstorder eauto.
apply ndtKpos. apply ndtA; firstorder eauto.
Qed.

Lemma t9 ϕ: T+ ¬ ((¬ K ϕ) ¬ (K (¬ ϕ))).
Proof.
apply ndtII.
apply ndtIE with (s := ((¬ ϕ) (¬ ¬ ϕ))).
apply ndtII. apply ndtIE with (s := (¬ ϕ)).
apply ndtCER with (s := ¬ ϕ). apply ndtA; firstorder eauto.
apply ndtCEL with (t := ¬ ¬ ϕ). apply ndtA; firstorder eauto.
apply ndtCI.
- apply t6C. apply ndtIE with (s := ¬ (K ϕ)).
+ apply ndtW with .
apply t7.
firstorder eauto.
+
apply ndtCEL with (t := (K (ϕ ) )). apply ndtA; firstorder eauto.
- apply t6C. apply ndtIE with (s := ¬ (K (¬ ϕ))). apply ndtW with .
apply t7.
firstorder eauto.
apply ndtCER with (s := (K ϕ )).
apply ndtA; firstorder eauto.
Qed.
End Derivations.

## Equivalence between IEL and IELm

Section IELMtoIEL.

Lemma ielToIELM Γ s: (@nd normal Γ s) -> (@nd minus ((¬ (K ))::Γ) s).
Proof.
intros.
induction H; firstorder eauto.
apply ndII. apply weak with ((K ) :: (s :: Γ)). auto. auto.
apply ndII. apply ndIE with (K ). apply ndA; auto. apply ndIE with (K s). apply ndKImp. apply ndKpos. apply ndA. auto.
apply ndW with ((K ) :: Γ); firstorder eauto.
Qed.

Lemma ielmToIEL Γ s: (@nd minus Γ s) -> (@nd normal Γ s).
Proof.
intros.
induction H; firstorder eauto.
Qed.
Lemma ielmToIELKb Γ s: (@nd minus ((¬ (K ))::Γ) s) -> forall Γ', Γ <<= Γ' -> (@nd normal Γ' s).
Proof.
intros. apply ndIE with (¬ K ). apply ndII. apply ielmToIEL. apply ndW with ( (K )::Γ). auto. intro; firstorder eauto. apply ndTEq.
apply ndtW with empty. apply IELKBot. firstorder eauto.
Qed.

Lemma ielmReducesIEL Γ s: (@nd minus ((¬ (K ))::Γ) s) <-> (@nd normal Γ s).
Proof.
split; eauto using ielmToIELKb, ielToIELM.
Qed.

Lemma ielmReducesIEL_theories (T: theory) s: ((¬ (K ))#T) T- s <-> T T+ s.
Proof.
split.
- intro. destruct H. destruct H. exists (rem x ((K ))). split.
+ intros. destruct (H ψ); apply in_rem_iff in H1. tauto. destruct H1. congruence. auto.
+ apply ielmReducesIEL. apply ndW with x. auto. intros a Ha. specialize (H a Ha).
decide (a = (¬ K )).
* subst a; auto.
* right. apply in_rem_iff; tauto.
- intro. repeat destruct H. apply ielmReducesIEL in H0. exists ((K ) :: x). split.
+ firstorder eauto.
+ auto.
Qed.
End IELMtoIEL.