Require Export PropL. Record HeytingAlgebra : Type := mkHeytingAlgebra { H:Type; R: H -> H -> Prop; bot: H; top: H; meet: H -> H -> H; join: H -> H -> H; imp: H -> H -> H; Rref : forall w, R w w; Rtra : forall u v w, R u v -> R v w -> R u w; bot1 : forall u, R bot u; top1 : forall u, R u top; meet1 : forall u v, R (meet u v) u; meet2 : forall u v, R (meet u v) v; meet3 : forall u v w, R w u -> R w v -> R w (meet u v); join1 : forall u v, R u (join u v); join2 : forall u v, R v (join u v); join3 : forall u v w, R u w -> R v w -> R (join u v) w; imp1 : forall u v, R (meet (imp u v) u) v; imp2 : forall u v w, R (meet w u) v -> R w (imp u v) }. Section HeytingAlgebra. Variable HA : HeytingAlgebra. Variable interp : var -> H HA. Fixpoint evalH (s : form) : H HA := match s with | Var x => interp x | Fal => bot HA | Imp s t => imp (evalH s) (evalH t) end. Fixpoint evalH' (A : list form) : H HA := match A with | nil => top HA | s::A => meet (evalH' A) (evalH s) end. Lemma nd_soundH A s : nd A s -> R (evalH' A) (evalH s). Proof. intros B. induction B as [A s B|A s t B IHB|A s t B1 IHB1 B2 IHB2|A s B IHB]. - induction A as [|t A]. + contradiction B. + destruct B as [B|B]. * subst t. simpl. apply meet2. * simpl. apply Rtra with (v := (evalH' A)); eauto using meet1. - simpl. apply imp2. simpl in IHB. exact IHB. - simpl in IHB1. apply Rtra with (v := (meet (imp (evalH s) (evalH t)) (evalH s))). + exact (meet3 IHB1 IHB2). + apply imp1. - apply Rtra with (v := evalH Fal); simpl; auto using bot1. Qed. End HeytingAlgebra. Section HeytingHa5. Inductive Ha5 : Type := Ha5bot | Ha5ab | Ha5a | Ha5b | Ha5top. Definition Ha5R (a b : Ha5) : Prop := match a,b with | Ha5bot,_ => True | _,Ha5bot => False | _,Ha5top => True | Ha5top,_ => False | Ha5a, Ha5a => True | Ha5a, Ha5b => False | Ha5a, Ha5ab => False | Ha5b, Ha5a => False | Ha5b, Ha5b => True | Ha5b, Ha5ab => False | Ha5ab, Ha5a => True | Ha5ab, Ha5b => True | Ha5ab, Ha5ab => True end. Definition Ha5meet (a b : Ha5) : Ha5 := match a,b with | Ha5bot,_ => Ha5bot | _,Ha5bot => Ha5bot | Ha5top,b => b | a,Ha5top => a | Ha5a, Ha5a => Ha5a | Ha5a, Ha5b => Ha5ab | Ha5a, Ha5ab => Ha5ab | Ha5b, Ha5a => Ha5ab | Ha5b, Ha5b => Ha5b | Ha5b, Ha5ab => Ha5ab | Ha5ab, Ha5a => Ha5ab | Ha5ab, Ha5b => Ha5ab | Ha5ab, Ha5ab => Ha5ab end. Definition Ha5join (a b : Ha5) : Ha5 := match a,b with | Ha5top,_ => Ha5top | _,Ha5top => Ha5top | Ha5bot,b => b | a,Ha5bot => a | Ha5a, Ha5a => Ha5a | Ha5a, Ha5b => Ha5top | Ha5a, Ha5ab => Ha5a | Ha5b, Ha5a => Ha5top | Ha5b, Ha5b => Ha5b | Ha5b, Ha5ab => Ha5b | Ha5ab, Ha5a => Ha5a | Ha5ab, Ha5b => Ha5b | Ha5ab, Ha5ab => Ha5ab end. Definition Ha5imp (a b : Ha5) : Ha5 := match a,b with | Ha5bot, _ => Ha5top | _, Ha5top => Ha5top | Ha5a, Ha5bot => Ha5bot | Ha5a, Ha5a => Ha5top | Ha5a, Ha5b => Ha5b | Ha5a, Ha5ab => Ha5b | Ha5b, Ha5bot => Ha5bot | Ha5b, Ha5a => Ha5a | Ha5b, Ha5b => Ha5top | Ha5b, Ha5ab => Ha5a | Ha5ab, Ha5bot => Ha5bot | Ha5ab, Ha5a => Ha5top | Ha5ab, Ha5b => Ha5top | Ha5ab, Ha5ab => Ha5top | Ha5top, Ha5bot => Ha5bot | Ha5top, Ha5a => Ha5a | Ha5top, Ha5b => Ha5b | Ha5top, Ha5ab => Ha5ab end. Lemma Ha5Rref a : Ha5R a a. Proof. destruct a; simpl; tauto. Qed. Lemma Ha5Rtra a b c : Ha5R a b -> Ha5R b c -> Ha5R a c. Proof. destruct a,b,c; simpl; tauto. Qed. Definition Ha5HA : HeytingAlgebra. apply (@mkHeytingAlgebra Ha5 Ha5R Ha5bot Ha5top Ha5meet Ha5join Ha5imp). - exact Ha5Rref. - exact Ha5Rtra. - intros u. destruct u; simpl; tauto. - intros u. destruct u; simpl; tauto. - intros u v. destruct u, v; simpl; tauto. - intros u v. destruct u, v; simpl; tauto. - intros u v w. destruct u, v, w; simpl; tauto. - intros u v. destruct u, v; simpl; tauto. - intros u v. destruct u, v; simpl; tauto. - intros u v w. destruct u, v, w; simpl; tauto. - intros u v. destruct u, v; simpl; tauto. - intros u v w. destruct u, v, w; simpl; tauto. Defined. Definition Ha5interp (x : var) : Ha5 := match x with | O => Ha5a | S _ => Ha5b end. Let Ha5eval := @evalH Ha5HA Ha5interp. (*** Lemma from which one can get undefinability of And, since Ha5ab is Ha5meet Ha5a Ha5b ***) Lemma undef_a_And_b u : Ha5eval u <> Ha5ab. Proof. induction u as [x|u IHu v IHv|]. - destruct x as [|x]; simpl; discriminate. - simpl. destruct (Ha5eval u); destruct (Ha5eval v); simpl; congruence. - simpl; discriminate. Qed. End HeytingHa5. Section HeytingHb5. (*** Idea: The poset with 5 elts: bottom, a, b, a \/ b, top bottom < a, bottom < b, a < (a \/ b), b < (a \/ b), a \/ b < top ***) Inductive Hb5 : Type := Hb5bot | Hb5a | Hb5b | Hb5ab | Hb5top. Definition Hb5R (a b : Hb5) : Prop := match a,b with | Hb5bot,_ => True | _,Hb5bot => False | _,Hb5top => True | Hb5top,_ => False | Hb5a, Hb5a => True | Hb5a, Hb5b => False | Hb5a, Hb5ab => True | Hb5b, Hb5a => False | Hb5b, Hb5b => True | Hb5b, Hb5ab => True | Hb5ab, Hb5a => False | Hb5ab, Hb5b => False | Hb5ab, Hb5ab => True end. Definition Hb5meet (a b : Hb5) : Hb5 := match a,b with | Hb5bot,_ => Hb5bot | _,Hb5bot => Hb5bot | Hb5top,b => b | a,Hb5top => a | Hb5a, Hb5a => Hb5a | Hb5a, Hb5b => Hb5bot | Hb5a, Hb5ab => Hb5a | Hb5b, Hb5a => Hb5bot | Hb5b, Hb5b => Hb5b | Hb5b, Hb5ab => Hb5b | Hb5ab, Hb5a => Hb5a | Hb5ab, Hb5b => Hb5b | Hb5ab, Hb5ab => Hb5ab end. Definition Hb5imp (a b : Hb5) : Hb5 := match a,b with | Hb5bot, _ => Hb5top | _, Hb5top => Hb5top | Hb5a, Hb5bot => Hb5b | Hb5a, Hb5a => Hb5top | Hb5a, Hb5b => Hb5b | Hb5a, Hb5ab => Hb5top | Hb5b, Hb5bot => Hb5a | Hb5b, Hb5a => Hb5a | Hb5b, Hb5b => Hb5top | Hb5b, Hb5ab => Hb5top | Hb5ab, Hb5bot => Hb5bot | Hb5ab, Hb5a => Hb5a | Hb5ab, Hb5b => Hb5b | Hb5ab, Hb5ab => Hb5top | Hb5top, Hb5bot => Hb5bot | Hb5top, Hb5a => Hb5a | Hb5top, Hb5b => Hb5b | Hb5top, Hb5ab => Hb5ab end. Definition Hb5join (a b : Hb5) : Hb5 := match a,b with | Hb5bot,b => b | a,Hb5bot => a | Hb5top,_ => Hb5top | _,Hb5top => Hb5top | _, Hb5ab => Hb5ab | Hb5ab, _ => Hb5ab | Hb5a, Hb5a => Hb5a | Hb5a, Hb5b => Hb5ab | Hb5b, Hb5a => Hb5ab | Hb5b, Hb5b => Hb5b end. Lemma Hb5Rref a : Hb5R a a. Proof. destruct a; simpl; tauto. Qed. Lemma Hb5Rtra a b c : Hb5R a b -> Hb5R b c -> Hb5R a c. Proof. destruct a,b,c; simpl; tauto. Qed. Definition Hb5HA : HeytingAlgebra. apply (@mkHeytingAlgebra Hb5 Hb5R Hb5bot Hb5top Hb5meet Hb5join Hb5imp). - exact Hb5Rref. - exact Hb5Rtra. - intros u. destruct u; simpl; tauto. - intros u. destruct u; simpl; tauto. - intros u v. destruct u, v; simpl; tauto. - intros u v. destruct u, v; simpl; tauto. - intros u v w. destruct u, v, w; simpl; tauto. - intros u v. destruct u, v; simpl; tauto. - intros u v. destruct u, v; simpl; tauto. - intros u v w. destruct u, v, w; simpl; tauto. - intros u v. destruct u, v; simpl; tauto. - intros u v w. destruct u, v, w; simpl; tauto. Defined. Definition Hb5interp (x : var) : Hb5 := match x with | O => Hb5a | S _ => Hb5b end. Let Hb5eval := @evalH Hb5HA Hb5interp. (*** Lemma from which one can get undefinability of Or, since Hb5ab is Hb5join Hb5a Hb5b ***) Lemma undef_a_Or_b u : Hb5eval u <> Hb5ab. Proof. induction u as [x|u IHu v IHv|]. - destruct x as [|x]; simpl; discriminate. - simpl. destruct (Hb5eval u); destruct (Hb5eval v); simpl; congruence. - simpl; discriminate. Qed. End HeytingHb5. Record KripkeModel : Type := mkKripkeModel { state : Type; step : state -> state -> Prop; pred := state -> Prop; label : nat -> pred; label_mon : forall a b n, step a b -> label n a -> label n b; step_refl : forall a, step a a; step_trans : forall a b c, step a b -> step b c -> step a c }. Section KripkeModel. Variable M:KripkeModel. Fixpoint evalK (s:form) : pred M := match s with | Var n => label n | Fal => fun _ => False | Imp s1 s2 => fun w => forall w', step w w' -> evalK s1 w' -> evalK s2 w' end. (*** Do not need induction because the logic only contains implication. ***) Lemma monotone (s:form) : forall w w', @step M w w' -> evalK s w -> evalK s w'. destruct s as [n| |s1 s2]; intros w w' H1 H2. - eapply (@label_mon M); eassumption. - simpl. simpl in H2. intros w''. intros H3 H4. apply H2. + apply (@step_trans M) with (b := w'); assumption. + assumption. - destruct H2. Qed. Definition evalK' (A:context) : pred M := fun w => forall s, s el A -> evalK s w. Lemma monotone_ctx (A:context) : forall w w', @step M w w' -> evalK' A w -> evalK' A w'. intros w w' H1 H2. intros u H3. eapply monotone. eassumption. apply H2. assumption. Qed. Lemma nd_soundK (A:context) (s:form) (D:nd A s) : forall w, evalK' A w -> evalK s w. induction D as [A s H'|A s1 s2 D1 IH1|A t s D1 IH1 D2 IH2|A s D1 IH1]. - auto. - simpl. intros w H1 w' H2 H3. apply IH1. intros s [H4|H4]. + congruence. + apply H1 in H4. revert H4. now apply monotone. - intros w H. simpl in IH1. apply (IH1 w H w). + apply (@step_refl M). + apply IH2. exact H. - intros w H. exfalso. exact (IH1 w H). Qed. End KripkeModel. Section KripkeModelToHeytingAlgebra. Variable M : KripkeModel. Let Cl : (state M -> Prop) -> Prop := fun p => forall u v : state M, step u v -> p u -> p v. Let H:Type := {p:state M -> Prop | Cl p}. Let R: H -> H -> Prop := fun a b => let (p,_) := a in let (q,_) := b in forall u, p u -> q u. Let bot: H. apply (exist Cl (fun _ => False)). unfold Cl. tauto. Defined. Let top: H. apply (exist Cl (fun _ => True)). unfold Cl. tauto. Defined. Let meet: H -> H -> H. intros [p pC] [q qC]. apply (exist Cl (fun u => p u /\ q u)). intros u v H1 [H2 H3]. split. - revert H2. now apply pC. - revert H3. now apply qC. Defined. Let imp: H -> H -> H. intros [p pC] [q qC]. apply (exist Cl (fun u => exists r, Cl r /\ (forall v, r v /\ p v -> q v) /\ r u)). intros u v H1 [r [H2 [H3 H4]]]. exists r. repeat split. - assumption. - assumption. - revert H4. now apply H2. Defined. Let join: H -> H -> H. intros [p pC] [q qC]. apply (exist Cl (fun u => p u \/ q u)). intros u v H1 [H2|H2]. - left. revert H2. now apply pC. - right. revert H2. now apply qC. Defined. Definition HeytingAlgebraOfKripkeModel : HeytingAlgebra. apply (@mkHeytingAlgebra H R bot top meet join imp). - intros [p pC]. unfold R. tauto. - intros [p pC] [q qC] [r rC]. simpl. auto. - intros [p pC]. unfold R. unfold bot. tauto. - intros [p pC]. unfold R. unfold top. tauto. - intros [p pC] [q qC]. unfold R. unfold meet. tauto. - intros [p pC] [q qC]. unfold R. unfold meet. tauto. - intros [p pC] [q qC] [r rC]. unfold R. unfold meet. auto. - intros [p pC] [q qC]. unfold R. unfold join. tauto. - intros [p pC] [q qC]. unfold R. unfold join. tauto. - intros [p pC] [q qC] [r rC]. unfold R. unfold join. intros H1 H2 u [H3|H3]; auto. - intros [p pC] [q qC]. unfold R. unfold meet, imp. intros u [[r [H1 [H2 H3]]] H4]. apply H2; tauto. - intros [p pC] [q qC] [r rC]. unfold R. unfold meet, imp. intros H1 u H2. exists r. repeat split; assumption. Defined. Definition HeytingInterpOfKripkeModel : var -> H. intros x. apply (exist Cl (@label M x)). unfold Cl. intros u v. apply label_mon. Defined. Theorem evalK_evalH_agree s : let (X,_) := @evalH HeytingAlgebraOfKripkeModel HeytingInterpOfKripkeModel s in forall w : state M, evalK s w <-> X w. Proof. induction s as [x|s IHs t IHt|]. - simpl. tauto. - simpl. assert (L1: exists Y Ys, evalH (HA:=HeytingAlgebraOfKripkeModel) HeytingInterpOfKripkeModel s = exist Cl Y Ys /\ forall w, evalK (M:=M) s w <-> Y w). { destruct (evalH (HA:=HeytingAlgebraOfKripkeModel) HeytingInterpOfKripkeModel s) as [Y Ys] eqn: E. exists Y. exists Ys. split. - reflexivity. - exact IHs. } assert (L2: exists Z Zs, evalH (HA:=HeytingAlgebraOfKripkeModel) HeytingInterpOfKripkeModel t = exist Cl Z Zs /\ forall w, evalK (M:=M) t w <-> Z w). { destruct (evalH (HA:=HeytingAlgebraOfKripkeModel) HeytingInterpOfKripkeModel t) as [Z Zs] eqn: E. exists Z. exists Zs. split. - reflexivity. - exact IHt. } destruct L1 as [Y [Ys [L1a L1b]]]. destruct L2 as [Z [Zs [L2a L2b]]]. rewrite L1a. rewrite L2a. unfold imp. split. + intros H1. exists (evalK (M:=M) (Imp s t)). repeat split. * exact (@monotone M (Imp s t)). * intros w' [H2 H3]. apply L2b. apply L1b in H3. revert H3. apply H2. apply step_refl. * exact H1. + intros [r [H1 [H2 H3]]] w' H4 H5. apply L2b. apply H2. split. * revert H3. now apply H1. * now apply L1b. - simpl. tauto. Qed. End KripkeModelToHeytingAlgebra. Section HeytingAlgebraToKripkeModel. Variable A : HeytingAlgebra. (*** If we had disjunction, I would need to take prime filters. ***) Definition ProperFilter (F:H A -> Prop) : Prop := ~ (F (bot A)) /\ F (top A) /\ (forall a b, F a -> F b -> F (meet a b)) /\ (forall a b, F a -> R a b -> F b). Variable interp : var -> H A. Definition KripkeModelOfHeytingAlgebra : KripkeModel. apply (@mkKripkeModel (sig ProperFilter) (fun F' G' => let (F,FF) := F' in let (G,GF) := G' in forall a, F a -> G a) (fun x F' => let (F,FF) := F' in forall a, R (interp x) a -> F a)). - intros [F FF] [G GF] x. auto. - intros [F FF]. auto. - intros [F FF] [G GF] [J JF]. auto. Defined. Hypothesis xm : forall X:Prop, X \/ ~ X. Lemma evalH_evalK_agree s : forall F: H A -> Prop, forall FF: ProperFilter F, @evalK KripkeModelOfHeytingAlgebra s (exist ProperFilter F FF) <-> F (@evalH A interp s). Proof. induction s as [x|s IHs t IHt|]; intros F [F1 [F2 [F3 F4]]]. - simpl. split. + intros H1. apply H1. apply Rref. + intros H1 a H2. revert H1 H2. apply F4. - simpl. split. + intros H1. set (G := fun a => exists b, F b /\ R (meet b (evalH (HA:=A) interp s)) a). destruct (xm (G (bot A))) as [G1|G1]. (*** a classical step ***) * { destruct G1 as [b [H2 H3]]. apply F4 with (a := imp (evalH (HA:=A) interp s) (bot A)). - apply imp2 in H3. exact (F4 _ _ H2 H3). - apply imp2. apply Rtra with (v := (bot A)). + apply imp1. + apply bot1. } * assert (G2: G (top A)). { exists (top A). split. - assumption. - apply top1. } assert (G3: forall a b, G a -> G b -> G (meet a b)). { intros a b [c [H2 H3]] [d [H4 H5]]. exists (meet c d). split. - now apply F3. - apply meet3. + apply Rtra with (v := meet c (evalH (HA:=A) interp s)). * { apply meet3. - apply Rtra with (v := meet c d). + apply meet1. + apply meet1. - apply meet2. } * assumption. + apply Rtra with (v := meet d (evalH (HA:=A) interp s)). * { apply meet3. - apply Rtra with (v := meet c d). + apply meet1. + apply meet2. - apply meet2. } * assumption. } assert (G4: forall a b, G a -> R a b -> G b). { intros a b [c [H2 H3]] H4. exists c. split. - assumption. - now apply Rtra with (v := a). } assert (L1: forall a, F a -> G a). { intros a H2. exists a. split. - assumption. - apply meet1. } assert (L2: evalK (M:=KripkeModelOfHeytingAlgebra) s (exist ProperFilter G (conj G1 (conj G2 (conj G3 G4))))). { apply IHs. unfold G. exists (top A). split; auto using meet2. } generalize (H1 (exist ProperFilter G (conj G1 (conj G2 (conj G3 G4)))) L1 L2). intros L3. apply IHt in L3 as [b [H2 H3]]. apply imp2 in H3. revert H2 H3. apply F4. + intros H1 [G [G1 [G2 [G3 G4]]]] H2 H3. apply IHt. apply IHs in H3. assert (L1: G (meet (imp (h:=A) (evalH (HA:=A) interp s) (evalH (HA:=A) interp t)) (evalH (HA:=A) interp s))). { apply G3. - now apply H2. - assumption. } generalize (imp1 (evalH (HA:=A) interp s) (evalH (HA:=A) interp t)). revert L1. apply G4. - simpl. split. + tauto. + exact F1. Qed. End HeytingAlgebraToKripkeModel.