Require Import List.
Import ListNotations.
Require Import List PslBase.Lists.BaseLists.
Require Import PslBase.Base.
Require Import Coq.Program.Equality.

# Completeness for classical modal logics assuming dec

We sketch how, assuming decidability of Hilbert-systems for KT our method can be used to obtain completeness constructively
Define implicational fragment
Inductive form :=
| Imp : form -> form -> form
| Bot : form
| Var : nat -> form
| Box : form -> form.
(* Define Notation for negation *)
Notation "⊥" := Bot.
Notation "¬ ϕ" := (Imp ϕ Bot) (at level 100, right associativity).

Infix "⊃" := Imp (right associativity, at level 103).
Definition Or (A B: form) := (¬ A B).
Definition And (A B: form) := ¬ ((¬ B) A).
Definition Not s := Imp s Bot.
Definition Diamond A := Not(Box(Not(A))).
Inductive prf : list form -> form -> Prop :=
ax Γ p : List.In p Γ -> prf Γ p
| pl1 Γ {p q} : prf Γ (p (q p))
| pl2 Γ {p q r}: prf Γ ((p (q r)) ((p q) (p r)))
| pl3 {Γ} {p q} : prf Γ (((¬p) ¬q) (((¬p) q) p))
| k Γ {p q} : prf Γ ( Box(p q) (Box(p) Box(q)))
| t Γ {p}: prf Γ (Box(p) p)
(* | b Γ {p}:      prf Γ (p ⊃ Box(Diamond(p))) *)
| mp Γ p q : prf Γ (p q) -> prf Γ p -> prf Γ q
| nec Γ p : prf [] p -> prf Γ (Box(p))

.

Hypothesis prf_dec : forall Γ A, {prf Γ A}+{ ~ prf Γ A}.
Hint Constructors prf.

Lemma p_imp_p Γ p: prf Γ (p p).
Proof.
pose proof (@pl2 Γ p (p p) p).
pose proof (@pl1 Γ p (p p)).
assert (prf Γ ((p (p p)) (p p))). eapply mp. apply H. apply H0.
pose proof (@pl1 Γ p p).
eapply mp. apply H1. auto.
Qed.

Lemma weakening Γ p: prf Γ p -> forall Δ, Γ <<= Δ -> prf Δ p.
Proof.
intro H. induction H; eauto.
Qed.
Theorem deduction_thm Γ p q: prf Γ (p q) <-> prf (p::Γ) q.
Proof.
split.
- intro. remember (p::Γ) as Γ'. dependent induction H.
+ apply mp with p. apply ax. rewrite HeqΓ'. auto. apply ax. rewrite HeqΓ'. auto.
+ pose proof (@pl1 Γ' p q0). apply mp with p. apply H. apply ax. rewrite HeqΓ'. auto.
+ pose proof (@pl2 Γ' p0 q0 r). eapply mp. apply H. apply ax. rewrite HeqΓ'. auto.
+ pose proof (@pl3 Γ' p0 q0). eapply mp. apply H. apply ax. rewrite HeqΓ'. auto.
+ apply mp with (Box (p0 q0)). apply k. rewrite HeqΓ'. apply ax. auto.
+ apply mp with (Box q). apply t. apply ax. subst Γ'. eauto.
+ assert (prf Γ (p q)). apply mp with p0. auto. auto.
apply mp with (p). apply weakening with Γ. apply H1. rewrite HeqΓ'. eauto. apply ax. rewrite HeqΓ'. auto.
- intro H1. dependent induction H1; eauto. destruct H.
+ subst p0. apply p_imp_p.
+ eauto.
Qed.

Lemma exfalso_qoudlibet Γ A B: prf Γ ((¬ A) (A B)).
Proof.
apply deduction_thm.
apply deduction_thm.
pose proof (@pl1 Γ (¬ A) (¬ B)).
pose proof (@pl1 Γ A (¬ B)).
pose proof (@pl3 Γ B A).
assert (prf (A :: (A ) :: Γ) ((B ) A )). {
eapply mp. apply weakening with Γ; eauto. apply ax; eauto.
}
assert (prf (A :: (A ) :: Γ) ((B ) A)). {
eapply mp. apply weakening with Γ; eauto. apply ax; eauto.
}
apply mp with ((B ) A); auto. apply mp with (((B ) A )); eauto.
Qed.

Lemma prf_bot_to_arb Γ A: prf Γ ( A).
Proof.
firstorder eauto.
pose proof (exfalso_qoudlibet Γ A).
apply mp with ( ); auto.
apply p_imp_p.
Qed.

Lemma prf_imp_char Γ s t: (prf Γ (¬ s) \/ prf Γ t) -> prf Γ (s t).
Proof.
intro H. destruct H.
- apply deduction_thm. apply mp with . apply prf_bot_to_arb. apply deduction_thm. auto.
- apply mp with t. apply pl1. auto.
Qed.

Lemma hilbert_dne Γ s: prf Γ (¬ ¬ s) -> prf Γ s.
Proof.
intro.

Section Models.
Class KripkeModel := mkKripkeModel {
world : Type;
valuation := nat -> Prop;
acc: world -> world -> Prop;
val: world -> valuation;

acc_refl: forall w, acc w w;
}.
Fixpoint evalK {M: KripkeModel} (s: form) : (world) -> Prop :=
match s with
| (Box x) => (fun y => forall r, ((acc y r) -> evalK x r))
| Bot => (fun x => False)
| Var y => (fun x => val x y)
| x y => (fun z => (evalK y z) \/ ~(evalK x z))
end.

Definition evalK' {M: KripkeModel} (Γ: list form) :=
fun w => forall s, (In s Γ) -> @evalK M s w.

Definition entails Γ φ :=
forall (M : KripkeModel), ((forall w,evalK' Γ w -> @evalK M φ w)).

End Models.
Notation context := (list form).

Definition sf_closed (A : context) : Prop :=
forall u, u el A -> match u with
| (Imp s1 s2) => s1 el A /\ s2 el A
| Box s => s el A
| _ => True
end.
Lemma sf_closed_app A B:
sf_closed A -> sf_closed B -> sf_closed (A ++ B).
Proof.
intros.
intros u Hu.
apply in_app_iff in Hu. destruct Hu.
specialize (H u). destruct u; firstorder eauto.
specialize (H0 u). destruct u; firstorder eauto.
Qed.

Lemma sf_closed_cons u s t A :
(u = Imp s t \/ u = Box s ) ->
s el A -> t el A -> sf_closed A -> sf_closed (u :: A).
Proof.
intros H H0 H1 H2.
destruct H.
- subst u. intros a Ha. destruct Ha. subst a. firstorder. destruct a; firstorder.
- subst u. intros a Ha. destruct Ha; try subst a; firstorder eauto. destruct a ; firstorder.
Qed.

Fixpoint scl' (s : form) : context :=
s :: match s with
| Imp u v => scl' u ++ scl' v
| Box s => scl' s
| _ => nil
end.

Lemma scl'_in s: s el scl' s.
Proof. destruct s; simpl; auto. Qed.

Lemma scl'_closed s: sf_closed (scl' s).
Proof.
induction s; simpl; auto.
- apply sf_closed_cons with (s:=s1) (t:=s2);
auto using scl'_in, sf_closed_app.
- intros u [A | A].
+ inversion A. auto using scl'_in, sf_closed_app.
+ destruct u; firstorder eauto.
- intros u [A|A]. inv A. auto using scl'_in, sf_closed_app. destruct u; firstorder eauto.

- intros u [A|A]. inv A. auto using scl'_in, sf_closed_app. destruct u; firstorder eauto.

Qed.

Fixpoint scl (A : context) : context :=
match A with
| nil => nil
| s :: A' => scl' s ++ scl A'
end.

Lemma scl_incl' A: A <<= scl A.
Proof. induction A as [|s A]; simpl; auto using scl'_in. Qed.

Lemma scl_incl A B: A <<= B -> A <<= scl B.
Proof. intros E. setoid_rewrite E. apply scl_incl'. Qed.

Lemma scl_closed A: sf_closed (scl A).
Proof.
induction A as [|s A]; simpl. now auto.
auto using scl'_closed, sf_closed_app.
Qed.

Lemma feqd: eq_dec form.
intros a b. unfold dec. repeat decide equality.
Defined.
Instance form_eq_dec' :
eq_dec form.
Proof.
apply feqd.
Defined.

Section Canonical.
We define the *canonical models*, whose worlds are the maximally consistent theories. We first define the relations.

Variable A0 : context.
Variable s0 : form.
Fixpoint negateAll (l: list form) :=
match l with nil => [] | A::xr => A::(¬ A)::negateAll xr end.

Lemma negateAll_in_iff Γ A: A el (negateAll Γ) <-> (A el Γ \/ (exists F, (A = ¬F) /\ (F el Γ))).
Proof.
induction Γ; firstorder eauto. simpl negateAll. subst x. subst A. firstorder.
Qed.

Definition U' := (scl (s0::::A0)).
Definition U'_sfc : sf_closed U' := @scl_closed _.

Record mcTheory := mkmcTheory {
T: list form;
Tsubs: (T el (power (negateAll U'))) ;
Tcons: ~(prf T );
Tmax: forall A, A el (U') -> A el T \/ (¬ A) el T;
}.

Lemma Tdedclos {m: mcTheory}: forall A, A el (negateAll U') -> prf (T m) A -> A el (T m).
Proof.
intros.
apply negateAll_in_iff in H. destruct H.
+ destruct (Tmax m H); auto.
exfalso. eapply Tcons. eauto.
+ destruct H as (A' & HA'). destruct HA'.
destruct (Tmax m H1); auto.
* subst A. decide ((A' ) el (T m)); eauto.
exfalso. eapply Tcons. eauto.
* subst A. decide ((A') el (T m)); eauto.
Qed.

Definition valuationMKT (A: mcTheory) (a: nat) := (Var a) el (T A).
Fixpoint unK (l: list form) : list form := match l with
nil => nil |
(Box A::xr) => (A)::(unK xr)
| x::xr => unK xr
end .

## Option 1: Define unK with A \/ Box A

Definition subsetVerif (A B:mcTheory) := forall x, In (Box x) (T A) -> In x (T B).
Lemma unK_in_iff Γ A: A el (unK Γ) <-> (Box A) el Γ .
Ltac todo := exfalso; exact todoF.

Require Import Coq.Relations.Relation_Operators.
Print clos_refl_trans.
Lemma U'_scl_closed_Box x: (Box x) el U' -> x el U' .
Proof.
intros H % U'_sfc. tauto.
(* Follows immidieatly by using subformula-closure of U' *)
Qed.

Lemma negAllKClosed x: Box x el negateAll U' -> x el negateAll U'.
Proof.
intros Ha.
apply negateAll_in_iff in Ha. destruct Ha.
- apply U'_scl_closed_Box in H. apply negateAll_in_iff. tauto.
- destruct H. destruct H. congruence.
Qed.

Instance canonical: (KripkeModel).
Proof.
eapply mkKripkeModel with (acc := subsetVerif).
apply valuationMKT.
- intros ta. intros a Ha. apply Tdedclos. apply negAllKClosed. destruct ta. pose proof (Hx := Tsubs0). apply power_incl in Hx. apply Hx. exact Ha. apply mp with (Box a). apply t. apply ax. auto.
Defined.

Definition single_extend (Ω: context) (A: form) (a: form) :=
if (@prf_dec (a::Ω) A) then ((¬ a)::Ω) else (a::Ω).

Lemma single_extend_subcontext A Ω B: Ω <<= (single_extend Ω A B).
Proof.
intros a Ha. unfold single_extend. destruct (prf_dec (B :: Ω) A); eauto.
Qed.

Lemma extend_two_possibilites Γ A B:
((single_extend Γ A B) === ((¬ B)::Γ) /\ prf (B::Γ) A) \/ (single_extend Γ A B) === (B::Γ) /\ ~(prf (B::Γ) A).
Proof.
destruct (prf_dec (B::Γ) A) eqn:id.
- left. split; try tauto.
split.
+ intros a Ha. unfold single_extend in Ha. rewrite id in Ha. auto.
+ unfold single_extend. rewrite id; auto.
- right. split; auto. split.
+ intros a Ha. unfold single_extend in Ha. rewrite id in Ha. auto.
+ unfold single_extend. rewrite id; auto.
Qed.
Lemma hil_exfalso Γ: prf Γ Bot -> (forall A, prf Γ A).
Proof.
intros H A.

Fixpoint extend (Ω: context) (A: form) (Γ: context) : context :=
match Γ with
nil => Ω
| (a::Γ') =>
single_extend (extend Ω A Γ') A a end.

Lemma a_does_not_matter Γ a b: prf (a::Γ) b -> prf ((¬ a)::Γ) b -> prf Γ b.
Proof.

Lemma extend_does_not_derive Ω A Γ: ~(prf Ω A) -> ~(prf (extend Ω A Γ) A).
Proof.
revert Ω.
induction Γ; eauto.
- intros. destruct (prf_dec (a :: extend Ω A Γ) A) eqn:di.
+ simpl extend. unfold single_extend. rewrite di. intro. apply (IHΓ Ω). apply H. apply a_does_not_matter with a; auto. (* Use that a \/ ~a is derived *)
+ simpl extend. unfold single_extend. rewrite di. apply n.
Qed.

Lemma extend_subset Ω Γ A: Ω <<= (extend Ω A Γ).
Proof.
revert Ω.
induction Γ; eauto.
- intro. simpl extend. unfold single_extend. destruct (prf_dec (a :: extend Ω A Γ) A); eauto.
Qed.

Lemma extend_adds_all Ω Γ A B: B el Γ -> B el (extend Ω A Γ) \/ (¬ B) el (extend Ω A Γ).
Proof.
intros H.
dependent induction Γ; auto.
destruct H.
+ destruct (prf_dec (a :: extend Ω A Γ) A) eqn:di; simpl extend; unfold single_extend; rewrite di; subst a ; auto.
+ specialize (IHΓ A B H). destruct IHΓ.
* left. unfold extend. apply single_extend_subcontext. apply H0.
* right. unfold extend. apply single_extend_subcontext. apply H0.
Qed.

Lemma extend_locally_dclosed Γ Ω A B: ~(prf Ω A) -> (prf (extend Ω A Γ) (B)) -> B el Γ -> B el (extend Ω A Γ).
Proof.
revert Ω B. intros.
destruct (@extend_adds_all Ω Γ A B H1).
- auto.
- apply extend_does_not_derive with (Γ := Γ) in H. exfalso. apply H. apply hil_exfalso. apply mp with B. apply ax. auto. auto.
Qed.
Lemma extend_does_not_derive_imp Ω Γ A B:
~(prf Ω A) -> B el Γ -> ~(prf (extend Ω A Γ) B) -> (prf (extend Ω A Γ) (B A)).
Proof.
intros H H1. revert H. revert Ω.
induction Γ.
- intros. eauto.
- intros. destruct H1.
+ subst a. simpl.
destruct (extend_two_possibilites (extend Ω A Γ) A B) as [(E1 & E2) | (E1 & E2)].
* apply weakening with (extend Ω A Γ). eauto. destruct E1; auto. apply deduction_thm. auto. apply single_extend_subcontext.
* exfalso. apply H0. simpl extend; fold extend. apply weakening with ( B :: extend Ω A Γ). apply ax. auto. destruct E1; auto.
+ assert (~(prf (extend Ω A Γ) B)). intro. apply H0. apply weakening with (extend Ω A Γ). auto. apply single_extend_subcontext.
specialize (IHΓ H1 (Ω) H H2).
simpl extend. apply weakening with (extend Ω A Γ). auto. apply single_extend_subcontext.
Qed.

(* Lemma extend_locally_easy_subset Ω A Γ: (extend Ω A Γ) <<= (Ω ++ Γ).
Proof.

Lemma extend_locally_subset Γ A Ω: Ω <<= Γ -> (extend Ω A Γ) <<= Γ.
Proof.
intros. enough (extend Ω A Γ <<= Γ ++ Γ).  intros a Ha. specialize (H0 a Ha). apply in_app_iff in H0; destruct H0; assumption.
enough (extend Ω A Γ <<= Ω ++ Γ). intros a Ha. specialize (H0 a Ha).  apply in_app_iff in H0. destruct H0; eauto.  apply extend_locally_easy_subset.
Qed.  *)

Lemma lindenbaum_subset_helper Γ A: extend Γ A U' <<= (Γ ++ negateAll U').
Proof.
revert Γ. induction U'.
- eauto.
- intros Γ f Hf.
unfold extend in Hf. fold extend in Hf. unfold single_extend at 1 in Hf.
destruct (prf_dec (a :: (extend Γ A l)) A) eqn:di.
+ destruct Hf.
* apply in_app_iff. right. simpl negateAll. firstorder.
* specialize (IHl Γ f H). apply in_app_iff in IHl; destruct IHl; firstorder. apply in_app_iff; right; simpl negateAll. firstorder.
+ destruct Hf.
* apply in_app_iff. right. simpl negateAll. firstorder.
* specialize (IHl Γ f H). apply in_app_iff in IHl; destruct IHl; firstorder. apply in_app_iff; right; simpl negateAll. firstorder.
Qed.

Lemma lindenbaum_subset Γ A: Γ <<= U' -> extend Γ A U' <<= (negateAll U').
Proof.
intros H. specialize (lindenbaum_subset_helper). intros H1.
intros a Ha. specialize (H1 Γ A). specialize (H1 a). specialize (H1 Ha). apply in_app_iff in H1. destruct H1.
- apply negateAll_in_iff. left. apply H. auto.
- auto.
Qed.

Lemma lindenbaum_subset2 Γ A: Γ <<= (negateAll U') -> extend Γ A U' <<= (negateAll U').
Proof.
intros H. specialize (lindenbaum_subset_helper). intros H1.
intros a Ha. specialize (H1 Γ A). specialize (H1 a). specialize (H1 Ha). apply in_app_iff in H1. destruct H1.
- apply H. auto.
- auto.
Qed.

Definition Lindenbaum (Γ : list form) (A: form) (H: Γ <<= (negateAll U')) (H': ~(prf Γ A)) : mcTheory.
Proof.

eapply mkmcTheory with (rep (extend Γ A U') (negateAll U')).
- apply rep_power.
- enough (~ prf (extend Γ A U') ).
intro. apply H0. eapply weakening. eapply H1. apply rep_incl.
intro. apply extend_does_not_derive with Γ A U' in H'. apply H'. apply hil_exfalso. auto.

- intros. rewrite rep_equi. apply extend_adds_all. auto. apply lindenbaum_subset2. auto.

Defined.

Lemma U'_scl_closed_imp x y: (x y) el U' -> x el U' /\ y el U'.
Proof.
intro. apply U'_sfc in H. tauto.
Qed.

Lemma admissibility_K A s: prf (unK A) s -> prf A (Box s).
Proof.
revert s. induction A. simpl; auto.
intros s H1.
destruct a; auto.
- apply weakening with A. apply IHA; auto. eauto.
- apply weakening with A. apply IHA; auto. eauto.
- apply weakening with A. apply IHA; auto. eauto.

- apply deduction_thm. apply mp with (Box (a s)). apply k. apply IHA. simpl unK in H1. apply deduction_thm. auto.
Qed.

Lemma negAllImoClosed x1 x2 : (x1 x2) el negateAll U' -> x1 el (negateAll U') /\ x2 el (negateAll U').
Proof.
intros H.
apply negateAll_in_iff in H. destruct H.
- apply U'_scl_closed_imp in H. repeat rewrite negateAll_in_iff. tauto.
- destruct H as (x1' & Hx1 & Hx1').
inversion Hx1; subst x1' x2.
split; eauto.
+ apply negateAll_in_iff. auto.
+ apply negateAll_in_iff. left. unfold U'. apply scl_incl'. auto.
Qed.
Lemma truth_lemma : forall (x: form), In x (negateAll U') -> forall (t: (@world canonical)), (evalK x t) <-> x el (T t).
Proof.
intros x Hx.
induction x.
- intros w. split.
+ intro.
destruct H.
* apply Tdedclos. auto. rewrite IHx2 in H. apply deduction_thm. apply ax. auto. apply negAllImoClosed in Hx. tauto.
* apply Tdedclos. auto. assert (x1 el (U')). {
apply negateAll_in_iff in Hx; destruct Hx.
* apply U'_scl_closed_imp in H0. tauto.
* destruct H0 as (F & Hf). destruct Hf. inversion H0. auto.
} destruct (Tmax w H0).
-- assert (x1 el (negateAll U')). {
apply negateAll_in_iff. tauto.
} exfalso; firstorder eauto.

-- apply deduction_thm. apply hil_exfalso. apply mp with x1. auto. auto.
+ intro H. simpl evalK.
decide (x1 el (T w)).
decide (x2 el (T w)).
all: eauto using IHx1, IHx2.
* left. apply IHx2; try apply negAllImoClosed in Hx. tauto. auto.
* exfalso. apply n. apply Tdedclos. apply negAllImoClosed in Hx. tauto. apply mp with x1; apply ax; auto.
* right. rewrite IHx1. auto. apply negAllImoClosed in Hx. tauto.
- intros. split.
+ intro H. simpl in H. tauto.
+ intro. destruct t0. simpl. apply Tcons0. apply ax. apply H.
- firstorder eauto.
- intros w. split.
decide (Box x el (T w)); auto.
intro H. exfalso.
assert (~ prf (unK (T w)) x). {
intro. apply admissibility_K in H0 . apply n. apply Tdedclos. auto.
auto.
}
assert (exists Δ: mcTheory, (unK (T w) <<= (T Δ)) /\ ~(x el (T Δ))).
assert ( (unK (T w) <<= negateAll U')) as HS. intros a Ha. apply unK_in_iff in Ha. enough (Box a el (negateAll U')).
apply negAllKClosed. auto. specialize (Tsubs w). intro. apply power_incl in H1. apply H1. auto.
eexists (@Lindenbaum (unK (T w)) x HS H0 ).
split.
+ simpl. rewrite rep_equi. apply extend_subset. apply lindenbaum_subset2. auto. (* extend_subset *)
+ intro. eapply extend_does_not_derive. apply H0. apply ax. simpl T in H1. apply rep_equi in H1. eapply H1. apply lindenbaum_subset2. auto.
+
destruct H1 as (Δ & Hd1 & Hd2).
apply Hd2. apply IHx. apply negAllKClosed. auto. apply H. intros a Ha. apply Hd1. apply unK_in_iff. auto.
+ intro. intros w' Hw'.
apply IHx. apply negAllKClosed. auto.
apply Hw'. auto.

Qed.

Show completeness next
Lemma prf_stable Γ A: ~~(prf Γ A) -> prf Γ A.
Proof.
intros. destruct (@prf_dec Γ A). auto. exfalso. tauto.
Qed.

Show completeness for subformulas
Lemma completeness' Ω A: A el U' -> Ω <<= (negateAll U') -> entails Ω A -> prf Ω A.
Proof.
intros Au U H. apply prf_stable. intro.
unfold entails in H.
specialize (H (@canonical)).
assert (exists Δ: mcTheory, ~(prf (T Δ) A) /\ (Ω <<= (T Δ))).
{
eexists (Lindenbaum U H0). split.
- simpl. enough (~ prf (extend Ω A U') A). intro. apply H1. eapply weakening. apply H2.
apply rep_equi. apply lindenbaum_subset2. auto.
apply extend_does_not_derive. auto.
- simpl. intros a Ha. apply rep_in. apply lindenbaum_subset2. auto. apply extend_subset. auto.
}
destruct H1 as [Δ H2].
specialize (H Δ). destruct H2.
assert ( {In A (T Δ)} + {~In A (T Δ)}). eauto.
destruct H3; eauto.
rewrite<- truth_lemma in n; auto. apply n. apply H. unfold evalK'. intros. apply truth_lemma. eauto. eauto.
apply negateAll_in_iff. tauto.
Qed.

End Canonical.

Lemma completeness Ω A: entails Ω A -> prf Ω A.
Proof.
intro. apply completeness' with Ω A. unfold U'. apply scl_incl'. auto. intros a Ha. apply negateAll_in_iff. left. apply scl_incl'. auto. auto.
Qed.

Print Assumptions completeness.