Theory Paraconsistency_Validity_Infinite

(* Anders Schlichtkrull, DTU Compute, Denmark *)

theory Paraconsistency_Validity_Infinite imports Paraconsistency
  abbrevs
    "Truth" = "❙⊤"
    and
    "Falsity" = "❙⊥"
    and
    "Neg'" = "❙¬"
    and
    "Con'" = "❙∧"
    and
    "Eql" = "❙⇔"
    and
    "Eql'" = "❙↔"
    and
    "Dis'" = "❙∨"
    and
    "Imp" = "❙⇒"
    and
    "Imp'" = "❙→"
    and
    "Box" = "❙□"
    and
    "Neg" = "❙⇁❙⇁"
    and
    "Con" = "❙∧❙∧"
    and
    "Dis" = "❙∨❙∨"
    and
    "Cla" = "❙Δ"
    and
    "Nab" = "❙∇"
    and
    "CON" = "[❙∧❙∧]"
    and
    "DIS" = "[❙∨❙∨]"
    and
    "NAB" = "[❙∇]"
    and
    "ExiEql" = "[❙∃❙=]"
begin

text
‹
The details about the definitions, lemmas and theorems are described in an article in the
Post-proceedings of the 24th International Conference on Types for Proofs and Programs (TYPES 2018).
›

section ‹Notation›

notation Pro ("⟨_⟩" [39] 39)
notation Truth ("❙⊤")
notation Neg' ("❙¬ _" [40] 40)
notation Con' (infixr "❙∧" 35)
notation Eql (infixr "❙⇔" 25)
notation Eql' (infixr "❙↔" 25)
notation Falsity ("❙⊥")
notation Dis' (infixr "❙∨" 30) 
notation Imp (infixr "❙⇒" 25) 
notation Imp' (infixr "❙→" 25)
notation Box ("❙□ _" [40] 40) 
notation Neg ("❙⇁❙⇁ _" [40] 40)
notation Con (infixr "❙∧❙∧" 35) 
notation Dis (infixr "❙∨❙∨" 30)
notation Cla ("❙Δ _" [40] 40) 
notation Nab ("❙∇ _" [40] 40)
abbreviation DetTrue :: tv ("∙") where "∙ ≡ Det True"
abbreviation DetFalse :: tv ("∘") where "∘ ≡ Det False"
notation Indet ("⌊_⌋" [39] 39)

text 
‹
Strategy: We define a formula that is valid in the sets {0..<1}, {0..<2}, ..., {0..<n-1} but is
not valid in the set {0..<n}
›

section ‹Injections From Sets to Sets›

text 
‹
We define the notion of an injection from a set X to a set Y 
›

definition inj_from_to :: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b set ⇒ bool" where
  "inj_from_to f X Y ≡ inj_on f X ∧ f ` X ⊆ Y"

lemma bij_betw_inj_from_to: "bij_betw f X Y ⟹ inj_from_to f X Y"
  unfolding bij_betw_def inj_from_to_def by simp

text 
‹
Special lemma for finite cardinality only
›

lemma inj_from_to_if_card:
  assumes "card X ≤ card Y"
  assumes "finite X"
  shows "∃f. inj_from_to f X Y"
  unfolding inj_from_to_def
  by (metis assms card_image card_le_inj card_subset_eq obtain_subset_with_card_n order_refl)

section ‹Extension of Paraconsistency Theory›

text 
‹
The Paraconsistency theory is extended with abbreviation ‹is_det› and a number of lemmas that are 
or generalizations of previous lemmas
›

abbreviation is_det :: "tv ⇒ bool" where "is_det tv ≡ ¬ is_indet tv"

theorem valid_iff_valid_in:
  assumes "card U ≥ card (props p)"
  shows "valid p ⟷ valid_in U p"
  using assms valid_in_valid valid_valid_in by blast

text 
‹
Generalization of ‹change_tv_injection›
›

lemma change_tv_injection_on:
  assumes "inj_on f U"
  shows "inj_on (change_tv f) (domain U)"
proof
  fix x y
  assume "x ∈ domain U" "y ∈ domain U" "change_tv f x = change_tv f y"
  then show "x = y"
    unfolding domain_def using assms inj_onD by (cases x; cases y) auto
qed

text 
‹
Similar to ‹change_tv_injection_on›
›

lemma change_tv_injection_from_to:
  assumes "inj_from_to f U W"
  shows "inj_from_to (change_tv f) (domain U) (domain W)"
  unfolding inj_from_to_def
proof
  show "inj_on (change_tv f) (domain U)"
    using assms change_tv_injection_on unfolding inj_from_to_def by blast
next
  show "change_tv f ` domain U ⊆ domain W"
  proof
    fix x
    assume "x ∈ change_tv f ` domain U"
    then show "x ∈ domain W"
      unfolding domain_def image_def
      using assms inj_from_to_def[of f U W]
      by (cases x) auto
  qed
qed

text 
‹
Similar to ‹eval_change_inj_on›
›

lemma change_tv_surj_on:
  assumes "f ` U = W"
  shows "(change_tv f) ` (domain U) = (domain W)"
proof
  show "change_tv f ` domain U ⊆ domain W"
  proof
    fix x
    assume "x ∈ change_tv f ` domain U"
    then show "x ∈ domain W"
    proof
      fix x'
      assume "x = change_tv f x'" "x' ∈ domain U"
      then show "x ∈ domain W"
        unfolding domain_def using assms by fastforce
    qed
  qed
next
  show "domain W ⊆ change_tv f ` domain U"
  proof
    fix x
    assume "x ∈ domain W"
    then show "x ∈ change_tv f ` domain U"
      unfolding domain_def using assms image_iff by fastforce
  qed
qed

text 
‹
Similar to ‹eval_change_inj_on›
›

lemma change_tv_bij_betw:
  assumes "bij_betw f U W"
  shows "bij_betw (change_tv f) (domain U) (domain W)"
  using assms change_tv_injection_on change_tv_surj_on unfolding bij_betw_def by simp

text 
‹
Generalization of ‹eval_change›
›

lemma eval_change_inj_on:
  assumes "inj_on f U"
  assumes "range i ⊆ domain U"
  shows "eval (change_int f i) p = change_tv f (eval i p)"
proof (induct p)
  fix p
  assume "eval (change_int f i) p = change_tv f (eval i p)"
  then have "eval_neg (eval (change_int f i) p) = eval_neg (change_tv f (eval i p))"
    by simp
  then have "eval_neg (eval (change_int f i) p) = change_tv f (eval_neg (eval i p))"
    by (cases "eval i p") (simp_all add: case_bool_if)
  then show "eval (change_int f i) (❙¬ p) = change_tv f (eval i (❙¬ p))"
    by simp
next
  fix p1 p2
  assume ih1: "eval (change_int f i) p1 = change_tv f (eval i p1)"
  assume ih2: "eval (change_int f i) p2 = change_tv f (eval i p2)"
  show "eval (change_int f i) (p1 ❙∧ p2) = change_tv f (eval i (p1 ❙∧ p2))"
    using assms ih1 ih2 change_tv.simps(1) change_tv_injection_on eval.simps(2) eval.simps(4)
      inj_onD ranges by metis
next
  fix p1 p2
  assume ih1: "eval (change_int f i) p1 = change_tv f (eval i p1)"
  assume ih2: "eval (change_int f i) p2 = change_tv f (eval i p2)"
  have "Det (eval (change_int f i) p1 = eval (change_int f i) p2) =
      Det (change_tv f (eval i p1) = change_tv f (eval i p2))"
    using ih1 ih2 by simp
  also have "... = Det ((eval i p1) = (eval i p2))"
  proof -
    have "inj_on (change_tv f) (domain U)"
      using assms(1) change_tv_injection_on by simp
    then show ?thesis
      using assms(2) ranges by (simp add: inj_on_eq_iff)
  qed
  also have "... = change_tv f (Det (eval i p1 = eval i p2))"
    by simp
  finally show "eval (change_int f i) (p1 ❙⇔ p2) = change_tv f (eval i (p1 ❙⇔ p2))"
    by simp
next
  fix p1 p2
  assume ih1: "eval (change_int f i) p1 = change_tv f (eval i p1)"
  assume ih2: "eval (change_int f i) p2 = change_tv f (eval i p2)"
  show "eval (change_int f i) (p1 ❙↔ p2) = change_tv f (eval i (p1 ❙↔ p2))"
    using assms ih1 ih2 inj_on_eq_iff change_tv.simps(1) change_tv_injection_on eval_equality
      eval_negation ranges by smt
qed (simp_all add: change_int_def)

section ‹Logics of Equal Cardinality Are Equal›

text 
‹
We prove that validity in a set depends only on the cardinality of the set
›

lemma inj_from_to_valid_in:
  assumes "inj_from_to f W U"
  assumes "valid_in U p"
  shows "valid_in W p"
  unfolding valid_in_def proof (rule, rule)
  fix i :: "char list ⇒ tv"
  assume a: "range i ⊆ domain W"
  from assms have valid_p: "∀i. range i ⊆ domain U ⟶ eval i p = ∙"
    unfolding valid_in_def by simp
  have "range (change_int f i) ⊆ domain U"
  proof
    fix x
    assume "x ∈ range (change_int f i)"
    then obtain xa where xa: "change_int f i xa = x"
      by blast
    have "inj_from_to (change_tv f) (domain W) (domain U)"
      using change_tv_injection_from_to assms by simp
    then have "(change_tv f) (i xa) ∈ domain U"
      using a by (metis inj_from_to_def image_eqI range_eqI subsetCE)
    then show "x ∈ domain U"
      using xa change_int_def by simp
  qed
  then have "eval (change_int f i) p = ∙"
    using valid_p by simp
  then have "eval (change_int f i) p = ∙"
    by simp
  then have "change_tv f (eval i p) = ∙"
    using a assms(1) eval_change_inj_on unfolding inj_from_to_def by metis
  then show "eval i p = ∙"
    using change_tv.elims tv.distinct(1) by fast
qed

corollary
  assumes "inj_from_to f U W"
  assumes "inj_from_to g W U"
  shows "valid_in U p ⟷ valid_in W p"
  using assms inj_from_to_valid_in by fast

lemma bij_betw_valid_in:
  assumes "bij_betw f U W"
  shows "valid_in U p ⟷ valid_in W p"
  using assms inj_from_to_valid_in bij_betw_inv bij_betw_inj_from_to by metis

theorem eql_finite_eql_card_valid_in:
  assumes "finite U ⟷ finite W"
  assumes "card U = card W"
  shows "valid_in U p ⟷ valid_in W p"
proof (cases "finite U")
  case True
  then show ?thesis
    using assms bij_betw_iff_card bij_betw_valid_in by metis
next
  case False
  then have "(∃f :: nat ⇒ nat. bij_betw f U UNIV) ∧ (∃g :: nat ⇒ nat. bij_betw g W UNIV)"
    using assms Schroeder_Bernstein infinite_iff_countable_subset inj_Suc top_greatest by metis
  with bij_betw_valid_in show ?thesis
    by metis
qed

corollary
  assumes "U ≠ {}"
  assumes "W ≠ {}"
  assumes "card U = card W"
  shows "valid_in U p ⟷ valid_in W p"
  using assms eql_finite_eql_card_valid_in card_gt_0_iff by metis

theorem finite_eql_card_valid_in:
  assumes "finite U"
  assumes "finite W"
  assumes "card U = card W"
  shows "valid_in U p ⟷ valid_in W p"
  using eql_finite_eql_card_valid_in by (simp add: assms)

theorem infinite_valid_in:
  assumes "infinite U"
  assumes "infinite W"
  shows "valid_in U p ⟷ valid_in W p"
  using eql_finite_eql_card_valid_in by (simp add: assms)

section ‹Conversions Between Nats and Strings›

definition nat_of_digit :: "char ⇒ nat" where
  "nat_of_digit c =
   (if c = (CHR ''1'') then 1 else if c = (CHR ''2'') then 2 else if c = (CHR ''3'') then 3 else
    if c = (CHR ''4'') then 4 else if c = (CHR ''5'') then 5 else if c = (CHR ''6'') then 6 else
    if c = (CHR ''7'') then 7 else if c = (CHR ''8'') then 8 else if c = (CHR ''9'') then 9 else 0)"

proposition "range nat_of_digit = {0..<10}"
proof
  show "range nat_of_digit ⊆ {0..<10}"
    unfolding nat_of_digit_def by auto
next
  show "{0..<10} ⊆ range nat_of_digit"
  proof
    fix x :: nat
    assume a: "x ∈ {0..<10}"
    show "x ∈ range nat_of_digit"
    proof (cases "x = 0")
      case True
      then show ?thesis
        unfolding nat_of_digit_def by auto
    next
      case False
      with a show ?thesis
        unfolding nat_of_digit_def by auto
    qed
  qed
qed

lemma nat_of_digit_of_nat[simp]: "n < 10 ⟹ nat_of_digit (digit_of_nat n) = n"
  unfolding digit_of_nat_def nat_of_digit_def
  by simp presburger

function nat_of_string :: "string ⇒ nat"
  where
    "nat_of_string n = (if length n ≤ 1 then nat_of_digit (last n) else
      (nat_of_string (butlast n)) * 10 + (nat_of_digit (last n)))"
  by simp_all
termination
  by (relation "measure length") simp_all

lemma nat_of_string_step:
  "nat_of_string (string_of_nat (m div 10)) * 10 + m mod 10 = nat_of_string (string_of_nat m)"
  by simp

lemma nat_of_string_of_nat: "nat_of_string (string_of_nat n) = n"
proof (induct rule: string_of_nat.induct)
  case (1 m)
  then show ?case
  proof (cases "m < 10")
    case True
    then show ?thesis
      by simp
  next
    case False
    then have "nat_of_string (string_of_nat (m div 10)) = m div 10"
      using 1 by simp
    then have "nat_of_string (string_of_nat (m div 10)) * 10 = (m div 10) * 10"
      by simp
    then have "nat_of_string (string_of_nat (m div 10)) * 10 + (m mod 10) =
        (m div 10) * 10 + (m mod 10)"
      by simp
    also have "... = m"
      by simp
    finally show ?thesis
      using nat_of_string_step by simp
  qed
qed

lemma "inj string_of_nat"
  using inj_on_inverseI nat_of_string_of_nat by metis

section ‹Derived Formula Constructors›

definition PRO :: "id list ⇒ fm list" where
  "PRO ids ≡ map Pro ids"

definition Pro_nat :: "nat ⇒ fm" ("⟨_⟩⇩1" [40] 40) where
  "⟨n⟩⇩1 ≡ ⟨string_of_nat n⟩"

definition PRO_nat :: "nat list ⇒ fm list" ("⟨_⟩⇩1⇩2⇩3" [40] 40) where
  "⟨ns⟩⇩1⇩2⇩3 ≡ map Pro_nat ns"

definition CON :: "fm list ⇒ fm" ("[❙∧❙∧] _" [40] 40) where
  "[❙∧❙∧] ps ≡ foldr Con ps ❙⊤"

definition DIS :: "fm list ⇒ fm" ("[❙∨❙∨] _" [40] 40) where
  "[❙∨❙∨] ps ≡ foldr Dis ps ❙⊥"

definition NAB :: "fm list ⇒ fm" ("[❙∇] _" [40] 40) where
  "[❙∇] ps ≡ [❙∧❙∧] (map Nab ps)"

definition off_diagonal_product :: "'a set ⇒ 'a set ⇒ ('a × 'a) set" where
  "off_diagonal_product xs ys ≡ {(x,y). (x,y) ∈ (xs × ys) ∧ x ≠ y }"

definition List_off_diagonal_product :: "'a list ⇒ 'a list ⇒ ('a × 'a) list" where
  "List_off_diagonal_product xs ys ≡ filter (λ(x,y). not_equal x y) (List.product xs ys)"

definition ExiEql :: "fm list ⇒ fm" ("[❙∃❙=] _" [40] 40) where
  "[❙∃❙=] ps ≡ [❙∨❙∨] (map (λ(x,y). x ❙⇔ y) (List_off_diagonal_product ps ps))"

lemma cla_false_Imp:
  assumes "eval i a = ∙"
  assumes "eval i b = ∘"
  shows "eval i (a ❙⇒ b) = ∘"
  using assms by simp

lemma eval_CON:
  "eval i ([❙∧❙∧] ps) = Det (∀p ∈ set ps. eval i p = ∙)"
  unfolding CON_def
  by (induct ps) simp_all

lemma eval_DIS:
  "eval i ([❙∨❙∨] ps) = Det (∃p ∈ set ps. eval i p = ∙)"
  unfolding DIS_def
proof (induct ps)
  case Nil
  then show ?case
    by simp
next
  case Cons
  with eval.simps eval_negation foldr.simps list.set_intros o_apply set_ConsD show ?case by smt
qed

lemma eval_Nab: "eval i (❙∇ p) = Det (is_indet (eval i p))"
proof (induct p)
  case (Pro x)
  then show ?case
    using string_tv.cases tv.simps(5) tv.simps(6) eval_negation
      eval.simps(2) eval.simps(4) eval.simps(5) by smt
next
  case (Neg' p)
  then show ?case
    using eval_negation by fastforce
next
  case (Eql' p1 p2)
  then show ?case
    using string_tv.cases tv.simps(5) tv.simps(6) eval_negation
      eval.simps(2) eval.simps(4) eval.simps(5) by smt
qed auto

lemma eval_NAB:
  "eval i ([❙∇] ps) = Det (∀p ∈ set ps. is_indet (eval i p))"
proof (cases "∀p∈set ps. is_indet (eval i p)")
  case True
  then have "eval i ([❙∇] ps) = ∙"
    unfolding NAB_def using eval_CON by fastforce
  then show ?thesis
    using True by simp
next
  case False
  then have "¬ (∀p∈set ps. eval i (❙∇ p) = ∙)"
    using eval_Nab by simp
  then have "¬ (∀p∈set (map Nab ps). eval i p = ∙)"
    by simp
  then have "eval i ([❙∇] ps) = ∘"
    unfolding NAB_def using eval_CON[of i "(map Nab ps)"] by simp
  then show ?thesis
    using False by simp
qed

lemma eval_ExiEql:
  "eval i ([❙∃❙=] ps) =
    Det (∃(p1, p2)∈(off_diagonal_product (set ps) (set ps)). eval i p1 = eval i p2)"
  using eval_DIS[of i "(map (λ(x, y). x ❙⇔ y) (List_off_diagonal_product ps ps))"]
  unfolding off_diagonal_product_def ExiEql_def List_off_diagonal_product_def
  by auto

section ‹Pigeon Hole Formula›

definition pigeonhole_fm :: "nat ⇒ fm" where
  "pigeonhole_fm n ≡ [❙∇] ⟨[0..<n]⟩⇩1⇩2⇩3 ❙⇒ [❙∃❙=] ⟨[0..<n]⟩⇩1⇩2⇩3"

definition interp_of_id :: "nat ⇒ id ⇒ tv" where
  "interp_of_id maxi i ≡ if (nat_of_string i) < maxi then ⌊nat_of_string i⌋  else ∙"

lemma interp_of_id_pigeonhole_fm_False: "eval (interp_of_id n) (pigeonhole_fm n) = ∘"
proof -
  have all_indet: "∀p ∈ set (⟨[0..<n]⟩⇩1⇩2⇩3). is_indet (eval (interp_of_id n) p)"
  proof
    fix p
    assume a: "p ∈ set (⟨[0..<n]⟩⇩1⇩2⇩3)"
    show "is_indet (eval (interp_of_id n) p)"
    proof -
      from a have "p ∈ Pro_nat ` {..<n}"
        unfolding PRO_nat_def using atLeast_upt set_map by metis
      then have "∃m<n. p = (⟨m⟩⇩1)"
        unfolding Pro_nat_def by fast
      then show ?thesis                
        unfolding interp_of_id_def Pro_nat_def using nat_of_string_of_nat by fastforce
    qed
  qed
  then have "eval (interp_of_id n) ([❙∇] (⟨[0..<n]⟩⇩1⇩2⇩3)) = ∙"
    using eval_NAB by simp
  moreover
  have "∀a b. a ∈ set (map (λn. ⟨n⟩⇩1) [0..<n]) ⟶
         b ∈ set (map (λn. ⟨n⟩⇩1) [0..<n]) ⟶ a ≠ b ⟶
         eval (interp_of_id n) a = eval (interp_of_id n) b ⟶ False"
    using all_indet in_set_conv_nth length_map nat_of_string_of_nat nth_map tv.inject tv.simps(5)
      eval.simps(1)
    unfolding interp_of_id_def PRO_def PRO_nat_def Pro_nat_def
    by smt
  then have "∀(p1, p2)∈off_diagonal_product (set (⟨[0..<n]⟩⇩1⇩2⇩3)) (set (⟨[0..<n]⟩⇩1⇩2⇩3)).
               eval (interp_of_id n) p1 ≠ eval (interp_of_id n) p2"
    unfolding off_diagonal_product_def PRO_nat_def Pro_nat_def by blast
  then have "¬ (∃(p1, p2)∈off_diagonal_product (set (⟨[0..<n]⟩⇩1⇩2⇩3)) (set (⟨[0..<n]⟩⇩1⇩2⇩3)).
              eval (interp_of_id n) p1 = eval (interp_of_id n) p2)"
    by blast
  then have "eval (interp_of_id n) ([❙∃❙=] (⟨[0..<n]⟩⇩1⇩2⇩3)) = ∘"
    using eval_ExiEql[of "interp_of_id n" "⟨[0..<n]⟩⇩1⇩2⇩3"] by simp
  ultimately
  show ?thesis
    unfolding pigeonhole_fm_def using cla_false_Imp[of "interp_of_id n"] by blast
qed

lemma range_interp_of_id: "range (interp_of_id n) ⊆ domain {0..<n}"
  unfolding interp_of_id_def domain_def by (simp add: image_subset_iff)

theorem not_valid_in_n_pigeonhole_fm: "¬ (valid_in {0..<n} (pigeonhole_fm n))"
  unfolding valid_in_def using interp_of_id_pigeonhole_fm_False[of n] range_interp_of_id[of n]
  by fastforce

theorem not_valid_pigeonhole_fm: "¬ (valid (pigeonhole_fm n))"
  unfolding valid_def using interp_of_id_pigeonhole_fm_False[of n]
  by fastforce

lemma cla_imp_I:
  assumes "is_det (eval i a)"
  assumes "is_det (eval i b)"
  assumes "eval i a = ∙ ⟹ eval i b = ∙"
  shows "eval i (a ❙⇒ b) = ∙"
proof -
  have "is_det tv = (case tv of Det _ ⇒ True | ⌊_⌋ ⇒ False)" for tv
    by (metis (full_types) tv.exhaust tv.simps(5) tv.simps(6))
  then show ?thesis
    using assms
    by (metis (full_types) eval.simps(4) eval.simps(5) tv.exhaust tv.simps(6))
qed

lemma is_det_NAB: "is_det (eval i ([❙∇] ps))"
  unfolding eval_NAB by auto

lemma is_det_ExiEql: "is_det (eval i ([❙∃❙=] ps))"
  using eval_ExiEql by auto

lemma pigeonhole_nat:
  assumes "finite n"
  assumes "finite m"
  assumes "card n > card m"
  assumes "f ` n ⊆ m"
  shows "∃x∈n. ∃y∈n. x ≠ y ∧ f x = f y"
  using assms not_le inj_on_iff_card_le unfolding inj_on_def
  by metis

lemma pigeonhole_nat_set:
  assumes "f ` {0..<n} ⊆ {0..<m}"
  assumes "m < (n :: nat)"
  shows "∃j1∈{0..<n}. ∃j2∈{0..<n}. j1 ≠ j2 ∧ f j1 = f j2"
  using assms pigeonhole_nat[of "({0..<n})" "{0..<m}" f]
  by simp

lemma inj_Pro_nat: "(⟨p1⟩⇩1) = (⟨p2⟩⇩1) ⟹ p1 = p2"
  unfolding Pro_nat_def using fm.inject(1) nat_of_string_of_nat
  by metis

lemma eval_true_in_lt_n_pigeonhole_fm:
  assumes "m < n"
  assumes "range i ⊆ domain {0..<m}"
  shows "eval i (pigeonhole_fm n) = ∙"
proof -
  {
    assume "eval i ([❙∇] (⟨[0..<n]⟩⇩1⇩2⇩3)) = ∙"
    then have "∀p ∈ set (⟨[0..<n]⟩⇩1⇩2⇩3). is_indet (eval i p)"
      using eval_NAB by auto
    then have *: "∀j<n. is_indet (eval i (⟨j⟩⇩1))"
      unfolding PRO_nat_def by auto
    have **: "∀j<n. ∃k<m. eval i (⟨j⟩⇩1) = (⌊k⌋)"
    proof -
      have "∀j<n. is_indet (eval i (⟨j⟩⇩1)) ⟹ j < n ⟹ ∃k<m. eval i (⟨j⟩⇩1) = (⌊k⌋)" for j
      proof (rule_tac x="get_indet (i (string_of_nat j))" in exI)
        show "∀j<n. is_indet (eval i (⟨j⟩⇩1)) ⟹ j < n ⟹ get_indet (i (string_of_nat j)) < m ∧
               eval i (⟨j⟩⇩1) = (⌊get_indet (i (string_of_nat j))⌋)"
        proof (induct "i (string_of_nat j)")
          case (Det x)
          then show ?case
            unfolding Pro_nat_def using eval.simps(1) tv.simps(5) by metis
        next
          case (Indet x)
          then show ?case
          proof (subgoal_tac "x<m")
            show "(⌊x⌋) = i (string_of_nat j) ⟹ ∀j<n. is_indet (eval i (⟨j⟩⇩1)) ⟹ j < n ⟹
                   x < m ⟹ get_indet (i (string_of_nat j)) < m ∧
                   eval i (⟨j⟩⇩1) = (⌊get_indet (i (string_of_nat j))⌋)"
              unfolding Pro_nat_def using eval.simps(1) tv.simps(6) by metis
          next
            show "(⌊x⌋) = i (string_of_nat j) ⟹ ∀j<n. is_indet (eval i (⟨j⟩⇩1)) ⟹ j < n ⟹ x < m"
              using assms(2) atLeast0LessThan unfolding domain_def by fast
          qed
        qed
      qed
      then show ?thesis
        using * by simp
    qed
    then have "∀j<n. ∃k<m. get_indet (eval i (⟨j⟩⇩1)) = k"
      by fastforce
    then have "(λj. get_indet (eval i (⟨j⟩⇩1))) ` {0..<n} ⊆ {0..<m}"
      by fastforce
    then have "∃j1 ∈ {0..<n}. ∃j2 ∈ {0..<n}. j1 ≠ j2 ∧ get_indet (eval i (⟨j1⟩⇩1)) =
                get_indet (eval i (⟨j2⟩⇩1))"
      using assms(1) pigeonhole_nat_set by simp
    then have "∃j1 < n. ∃j2 < n. j1 ≠ j2 ∧ get_indet (eval i (⟨j1⟩⇩1)) =
                get_indet (eval i (⟨j2⟩⇩1))"
      using atLeastLessThan_iff by blast
    then have "∃j1 < n. ∃j2 < n. j1 ≠ j2 ∧ eval i (⟨j1⟩⇩1) = eval i (⟨j2⟩⇩1)"
      using ** tv.simps(6) by metis
    then have "∃(p1, p2)∈off_diagonal_product (set (⟨[0..<n]⟩⇩1⇩2⇩3)) (set (⟨[0..<n]⟩⇩1⇩2⇩3)).
                 eval i p1 = eval i p2"
    proof (rule_tac P="λj1. j1<n ∧ (∃j2<n. j1 ≠ j2 ∧ eval i (⟨j1⟩⇩1) =
                        eval i (⟨j2⟩⇩1))" in exE)
      show "∃j1<n. ∃j2<n. j1 ≠ j2 ∧ eval i (⟨j1⟩⇩1) = eval i (⟨j2⟩⇩1) ⟹
              ∃x<n. ∃j2<n. x ≠ j2 ∧ eval i (⟨x⟩⇩1) = eval i (⟨j2⟩⇩1)"
        by simp
    next
      show "∃j1<n. ∃j2<n. j1 ≠ j2 ∧ eval i (⟨j1⟩⇩1) = eval i (⟨j2⟩⇩1) ⟹
              j1 < n ∧ (∃j2<n. j1 ≠ j2 ∧ eval i (⟨j1⟩⇩1) = eval i (⟨j2⟩⇩1)) ⟹
              ∃(p1, p2)∈off_diagonal_product (set (⟨[0..<n]⟩⇩1⇩2⇩3)) (set (⟨[0..<n]⟩⇩1⇩2⇩3)).
              eval i p1 = eval i p2" for j1
      proof (rule_tac P="λj2. j2<n ∧ j1 ≠ j2 ∧ eval i (⟨j1⟩⇩1) = eval i (⟨j2⟩⇩1)" in exE)
        show "∃j1<n. ∃j2<n. j1 ≠ j2 ∧ eval i (⟨j1⟩⇩1) = eval i (⟨j2⟩⇩1) ⟹
                j1 < n ∧ (∃j2<n. j1 ≠ j2 ∧ eval i (⟨j1⟩⇩1) = eval i (⟨j2⟩⇩1)) ⟹
                ∃x<n. j1 ≠ x ∧ eval i (⟨j1⟩⇩1) = eval i (⟨x⟩⇩1)"
          by simp
      next
        show "∃j1<n. ∃j2<n. j1 ≠ j2 ∧ eval i (⟨j1⟩⇩1) = eval i (⟨j2⟩⇩1) ⟹
                j1 < n ∧ (∃j2<n. j1 ≠ j2 ∧ eval i (⟨j1⟩⇩1) = eval i (⟨j2⟩⇩1)) ⟹
                j2 < n ∧ j1 ≠ j2 ∧ eval i (⟨j1⟩⇩1) = eval i (⟨j2⟩⇩1) ⟹
                ∃(p1, p2)∈off_diagonal_product (set (⟨[0..<n]⟩⇩1⇩2⇩3)) (set (⟨[0..<n]⟩⇩1⇩2⇩3)).
                eval i p1 = eval i p2" for j2
          unfolding off_diagonal_product_def PRO_nat_def using inj_Pro_nat
          by (rule_tac x="(⟨j1⟩⇩1, ⟨j2⟩⇩1)" in bexI) auto
      qed
    qed
    then have "eval i ([❙∃❙=] (⟨[0..<n]⟩⇩1⇩2⇩3)) = ∙"
      using eval_ExiEql by simp
  }
  then show ?thesis
    unfolding pigeonhole_fm_def using cla_imp_I is_det_ExiEql is_det_NAB by simp
qed

theorem valid_in_lt_n_pigeonhole_fm:
  assumes "m<n"
  shows "valid_in {0..<m} (pigeonhole_fm n)"
  using assms
  unfolding valid_in_def
  using interp_of_id_pigeonhole_fm_False[of n]
  using range_interp_of_id[of n]
  using eval_true_in_lt_n_pigeonhole_fm
  by simp

theorem not_valid_in_pigeonhole_fm_card:
  assumes "finite U"
  shows "¬ valid_in U (pigeonhole_fm (card U))"
  using assms ex_bij_betw_nat_finite not_valid_in_n_pigeonhole_fm bij_betw_valid_in by metis

theorem not_valid_in_pigeonhole_fm_lt_card:
  assumes "finite (U::nat set)"
  assumes "inj_from_to f U W"
  shows "¬ valid_in W (pigeonhole_fm (card U))"
proof -
  have "¬ valid_in U (pigeonhole_fm (card U))"
    using not_valid_in_pigeonhole_fm_card assms by simp
  then show ?thesis
    using assms inj_from_to_valid_in by metis
qed

theorem valid_in_pigeonhole_fm_n_gt_card:
  assumes "finite U"
  assumes "card U < n"
  shows "valid_in U (pigeonhole_fm n)"
  using assms ex_bij_betw_finite_nat bij_betw_valid_in valid_in_lt_n_pigeonhole_fm by metis

section ‹Validity Is the Intersection of the Finite Logics›

lemma "valid p ⟷ (∀U. finite U ⟶ valid_in U p)"
proof
  assume "valid p"
  then show "∀U. finite U ⟶ valid_in U p"
    using transfer by blast
next
  assume "∀U. finite U ⟶ valid_in U p"
  then have "valid_in {1..card (props p)} p"
    by simp
  then show "valid p"
    using reduce by simp
qed

section ‹Logics of Different Cardinalities Are Different›

lemma finite_card_lt_valid_in_not_valid_in:
  assumes "finite U"
  assumes "card U < card W"
  shows "valid_in U ≠ valid_in W"
proof -
  have finite_W: "finite W"
    using assms(2) card.infinite by fastforce
  have "valid_in U (pigeonhole_fm (card W))"
    using valid_in_pigeonhole_fm_n_gt_card assms by simp
  moreover
  have "¬ valid_in W (pigeonhole_fm (card W))"
    using not_valid_in_pigeonhole_fm_card assms finite_W by simp
  ultimately show ?thesis
    by fastforce
qed

lemma valid_in_UNIV_p_valid: "valid_in UNIV p = valid p"
  using universal_domain valid_def valid_in_def by simp

theorem infinite_valid_in_valid:
  assumes "infinite U"
  shows "valid_in U p ⟷ valid p"
  using assms infinite_valid_in[of U UNIV p] valid_in_UNIV_p_valid by simp

lemma finite_not_finite_valid_in_not_valid_in:
  assumes "finite U ≠ finite W"
  shows "valid_in U ≠ valid_in W"
proof -
  {
    fix U W :: "nat set"
    assume inf: "infinite U"
    assume fin: "finite W"
    then have valid_in_W_pigeonhole_fm: "valid_in W (pigeonhole_fm (Suc (card W)))"
      using valid_in_pigeonhole_fm_n_gt_card[of W] by simp
    have "¬ valid (pigeonhole_fm (Suc (card W)))"
      using not_valid_pigeonhole_fm by simp
    then have "¬ valid_in U (pigeonhole_fm (Suc (card W)))"
      using inf fin infinite_valid_in_valid by simp
    then have "valid_in U ≠ valid_in W"
      using valid_in_W_pigeonhole_fm by fastforce
  }
  then show ?thesis
    using assms by metis
qed

lemma card_not_card_valid_in_not_valid_in:
  assumes "card U ≠ card W"
  shows "valid_in U ≠ valid_in W"
  using assms
proof -
  {
    fix U W :: "nat set"
    assume a: "card U < card W"
    then have "finite W"
      using card.infinite gr_implies_not0 by blast
    then have valid_in_W_pigeonhole_fm: "valid_in W (pigeonhole_fm (Suc (card W)))"
      using valid_in_pigeonhole_fm_n_gt_card[of W] by simp
    have "valid_in U ≠ valid_in W"
    proof (cases "finite U")
      case True
      then show ?thesis
        using a finite_card_lt_valid_in_not_valid_in by simp
    next
      case False
      have "¬ valid (pigeonhole_fm (Suc (card W)))"
        using not_valid_pigeonhole_fm by simp
      then have "¬ valid_in U (pigeonhole_fm (Suc (card W)))"
        using False infinite_valid_in_valid by simp
      then show ?thesis
        using valid_in_W_pigeonhole_fm by fastforce
    qed
  }
  then show ?thesis
    using assms neqE by metis
qed

section ‹Finite Logics Are Different from Infinite Logics›

theorem extend: "valid ≠ valid_in U" if "finite U"
  using that not_valid_pigeonhole_fm valid_in_pigeonhole_fm_n_gt_card by fastforce

corollary "¬ (∃n. ∀p. valid p ⟷ valid_in {0..n} p)"
  using extend by fast

corollary "∀n. ∃p. ¬ (valid p ⟷ valid_in {0..n} p)"
  using extend by fast

corollary "¬ (∀p. valid p ⟷ valid_in {0..n} p)"
  using extend by fast

corollary "valid ≠ valid_in {0..n}"
  using extend by simp

proposition "valid = valid_in {0..}"
  unfolding valid_def valid_in_def
  using universal_domain
  by simp

corollary "valid = valid_in {n..}"
  using infinite_valid_in[of UNIV "{n..}"] universal_domain
  unfolding valid_def valid_in_def
  by (simp add: infinite_Ici)

corollary "¬ (∃n m. ∀p. valid p ⟷ valid_in {m..n} p)"
  using extend by fast

end ― ‹‹Paraconsistency_Validity_Infinite› file›