# Library PropiLindep

Require Export PropiLmodel.

# Independence of Instuitionistic Connectives

Disjunction property

Fixpoint HarropF u: Prop :=
match u with
| Var _True
| FalTrue
| Imp s tHarropF t
| And s tHarropF s HarropF t
| Or s tFalse
end.

Definition HarropC A: Prop := s, s el A HarropF s.

Lemma Harrop A p q: HarropC A gen A (Or p q) gen A p gen A q.

Lemma OrFree_Harrop s: OrFree s HarropF s.

Lemma genXM x:
¬ gen [] (Or (Var x) (Not (Var x))).

Lemma OrIndependence p q:
¬ (gen [p] q gen [q] p)
¬ s, OrFree s gen [] (Equi (Or p q) s).

# Undefinability due to McKinsey

(* The results are from
McKinsey, J. C. C. (1939). Proof of the independence of the primitive symbols
of Heyting's calculus of propositions. Journal of Symbolic Logic 4 (4):155-158
*)

# Independence of Falsehood

Section HeytingHMK1.
(* McKinsey's Matrix I to prove undefinability of Fal *)

(* Lattice:
top
|
|
a
|
|
bot
*)

Inductive HMK1: Type := HMK1bot | HMK1a | HMK1top.

Definition HMK1R (a b: HMK1) : Prop :=
match a,b with
| HMK1bot, _True
| _, HMK1botFalse
| _, HMK1topTrue
| HMK1top, _False
| HMK1a, HMK1aTrue
end.

Definition HMK1meet (a b: HMK1) : HMK1 :=
match a,b with
| HMK1bot, _HMK1bot
| _ , HMK1botHMK1bot
| HMK1top, bb
| a, HMK1topa
| HMK1a, HMK1aHMK1a
end.

Definition HMK1join (a b: HMK1) : HMK1 :=
match a,b with
| HMK1top, _HMK1top
| _, HMK1topHMK1top
| HMK1bot, bb
| a, HMK1bota
| HMK1a, HMK1aHMK1a
end.

Definition HMK1imp (a b : HMK1) : HMK1 :=
match a,b with
| HMK1bot, _HMK1top
| _, HMK1topHMK1top
| _, HMK1botHMK1bot
| HMK1top, bb
| HMK1a, HMK1aHMK1top
end.

Lemma HMK1Rref a: HMK1R a a.

Lemma HMK1Rtra a b c: HMK1R a b HMK1R b c HMK1R a c.

Definition HMK1HA : HeytingAlgebra.

(* Fal is undefinable by other connectives *)
Lemma FalIndependence_hey:
¬ s, FalFree s nd [] (Equi s Fal).

End HeytingHMK1.

# Independence of Disjunction

Section HeytingHMK2.
(* McKinsey's Matrix II to prove undefinability of Or *)

(* Lattice:
top
|
|
a \/ b
/      \
a        b
\      /
\    /
bot
*)

Inductive HMK2 : Type := HMK2bot | HMK2a | HMK2b | HMK2ab | HMK2top.

Definition HMK2R (a b: HMK2) : Prop :=
match a,b with
| HMK2bot, _True
| _, HMK2botFalse
| _, HMK2topTrue
| HMK2top, _False
| HMK2a, HMK2aTrue
| HMK2a, HMK2bFalse
| HMK2a, HMK2abTrue
| HMK2b, HMK2aFalse
| HMK2b, HMK2bTrue
| HMK2b, HMK2abTrue
| HMK2ab, HMK2aFalse
| HMK2ab, HMK2bFalse
| HMK2ab, HMK2abTrue
end.

Definition HMK2meet (a b: HMK2) : HMK2 :=
match a,b with
| HMK2bot, _HMK2bot
| _, HMK2botHMK2bot
| HMK2top, bb
| a, HMK2topa
| HMK2a, HMK2aHMK2a
| HMK2a, HMK2bHMK2bot
| HMK2a, HMK2abHMK2a
| HMK2b, HMK2aHMK2bot
| HMK2b, HMK2bHMK2b
| HMK2b, HMK2abHMK2b
| HMK2ab, bb
end.

Definition HMK2join (a b: HMK2) : HMK2 :=
match a,b with
| HMK2bot, bb
| a, HMK2bota
| HMK2top, _HMK2top
| _, HMK2topHMK2top
| _, HMK2abHMK2ab
| HMK2ab, _HMK2ab
| HMK2a, HMK2aHMK2a
| HMK2a, HMK2bHMK2ab
| HMK2b, HMK2aHMK2ab
| HMK2b, HMK2bHMK2b
end.

Definition HMK2imp (a b: HMK2) : HMK2 :=
match a,b with
| HMK2bot, _HMK2top
| _, HMK2topHMK2top
| HMK2a, HMK2botHMK2b
| HMK2a, HMK2aHMK2top
| HMK2a, HMK2bHMK2b
| HMK2a, HMK2abHMK2top
| HMK2b, HMK2botHMK2a
| HMK2b, HMK2aHMK2a
| HMK2b, HMK2bHMK2top
| HMK2b, HMK2abHMK2top
| HMK2ab, HMK2botHMK2bot
| HMK2ab, HMK2aHMK2a
| HMK2ab, HMK2bHMK2b
| HMK2ab, HMK2abHMK2top
| HMK2top, bb
end.

Lemma HMK2Rref a: HMK2R a a.

Lemma HMK2Rtra a b c: HMK2R a b HMK2R b c HMK2R a c.

Definition HMK2HA : HeytingAlgebra.

Lemma OrIndependence_hey:
¬ s, OrFree s nd [] (Equi (Or (Var 0) (Var 1)) s).

End HeytingHMK2.

# Independence of Implication and Conjunction

Section HeytingHMK3.
(* McKinsey's Matrix III to prove undefinability of Imp and And *)

(* Matrix III is actually the direct product of Matrix I with itself *)
(* Lattice: 1-top 2-a 3-bot
11
/  \
12  21
/  \/  \
13  22  31
\  /\  /
23  32
\  /
33
*)

Definition HMK3: Type := prod HMK1 HMK1.

Definition HMK3R (a b: HMK3) : Prop :=
match a, b with
| (a1,a2), (b1, b2)HMK1R a1 b1 HMK1R a2 b2
end.

Definition HMK3meet (a b: HMK3) : HMK3 :=
match a, b with
| (a1,a2), (b1, b2)(HMK1meet a1 b1, HMK1meet a2 b2)
end.

Definition HMK3join (a b: HMK3) : HMK3 :=
match a, b with
| (a1,a2), (b1, b2)(HMK1join a1 b1, HMK1join a2 b2)
end.

Definition HMK3imp (a b: HMK3) : HMK3 :=
match a, b with
| (a1,a2), (b1, b2)(HMK1imp a1 b1, HMK1imp a2 b2)
end.

Lemma HMK3Rref a: HMK3R a a.

Lemma HMK3Rtra a b c: HMK3R a b HMK3R b c HMK3R a c.

Definition HMK3HA : HeytingAlgebra.

(* Idea: Fal, Or, And are closed on {11, 12, 22, 33}, but 11->22 = 21
where 1-top 2-a 3-bot *)

Lemma ImpIndependence_hey:
¬ s, ImpFree s nd [] (Equi (Imp (Var 0) (Var 1)) s).

(* Idea: Fal, Or, Imp are closed on {11, 12, 13, 31, 33}, but 12/\31 = 32
where 1-top 2-a 3-bot *)

Lemma AndIndependence_hey:
¬ s, AndFree s nd [] (Equi (And (Var 0) (Var 1)) s).

End HeytingHMK3.

Some underivability results using Heyting

Lemma ndXM_hey x:
¬ nd [] (Or (Var x) (Not (Var x))).

Lemma ndDN_hey x:
¬ nd [] (Imp (Not (Not (Var x))) (Var x)).

Lemma ndDN'_hey x:
¬ nd [] (Or (Not (Var x)) (Not (Not (Var x)))).

Lemma ndDeMorgan_hey:
¬ nd [] (Imp (Not (And (Var 0) (Var 1))) (Or (Not (Var 0)) (Not (Var 1)))).