AOT_define MapsToOneToOne :: ‹τ → τ → τ → φ› (‹_ |: _ 1-1⟶ _›) "fFG:2": ‹R |: F 1-1⟶ G ≡df
R |: F ⟶ G & ∀x∀y∀z (([F]x & [F]y & [G]z) → ([R]xz & [R]yz ='font-size: 18px;'>→ x = y))›
AOT_define MapsOnto :: ‹τ → τ → τ → φ› (‹_ |: _ ⟶onto _›) "fFG:3": ‹R |: F ⟶onto G ≡df R |: F ⟶ G & ∀y ([G]y →∃x([F]x & [R]xy))›
AOT_define MapsOneToOneOnto :: ‹τ → τ → τ → φ› (‹_ |: _ 1-1⟶onto _›) "fFG:4": ‹R |: F 1-1⟶onto G ≡df R |: F 1-1⟶ G & R |: F ⟶onto G›
AOT_theorem "eq-1-1": ‹R |: F 1-1⟷ G ≡ R |: F 1-1⟶onto G› proof(rule "≡I"; rule "→I")
AOT_assume ‹R |: F 1-1⟷ G›
AOT_hence A: ‹∀x ([F]x →∃!y([G]y & [R]xy))› and B: ‹∀y ([G]y →∃!x([F]x & [R]xy))› using"≡dfE"[OF "1-1-cor"] "&E"by blast+
AOT_have C: ‹R |: F ⟶ G› proof (rule "≡dfI"[OF "fFG:1"]; rule "&I")
AOT_show ‹R↓ & F↓ & G↓› using"cqt:2[const_var]"[axiom_inst] "&I"by metis next
AOT_show ‹∀x ([F]x →∃!y([G]y & [R]xy))›by (rule A) qed
AOT_show ‹R |: F 1-1⟶onto G› proof (rule "≡dfI"[OF "fFG:4"]; rule "&I")
AOT_show ‹R |: F 1-1⟶ G› proof (rule "≡dfI"[OF "fFG:2"]; rule "&I")
AOT_show ‹R |: F ⟶ G›using C. next
AOT_show ‹∀x∀y∀z ([F]x & [F]y & [G]z → ([R]xz & [R]yz → x = y))› proof(rule GEN; rule GEN; rule GEN; rule "→I"; rule "→I") fix x y z
AOT_assume 1: ‹[F]x & [F]y & [G]z› moreover AOT_assume 2: ‹[R]xz & [R]yz› ultimately AOT_have 3: ‹∃!x ([F]x & [R]xz)› using B "&E""∀E""→E"by fast
AOT_show ‹x = y› by (rule "uni-most"[THEN"→E", OF 3, THEN"∀E"(2)[where β=x], THEN"∀E"(2)[where β=y], THEN"→E"])
(metis "&I""&E"12) qed qed next
AOT_show ‹R |: F ⟶onto G› proof (rule "≡dfI"[OF "fFG:3"]; rule "&I")
AOT_show ‹R |: F ⟶ G›using C. next
AOT_show ‹∀y ([G]y →∃x ([F]x & [R]xy))› proof(rule GEN; rule "→I") fix y
AOT_assume ‹[G]y›
AOT_hence ‹∃!x ([F]x & [R]xy)› using B[THEN"∀E"(2), THEN"→E"] by blast
AOT_hence ‹∃x ([F]x & [R]xy & ∀β (([F]β & [R]βy) → β = x))› using"uniqueness:1"[THEN"≡dfE"] by blast then AOT_obtain x where ‹[F]x & [R]xy› using"∃E"[rotated] "&E"by blast
AOT_thus ‹∃x ([F]x & [R]xy)›by (rule "∃I") qed qed qed next
AOT_assume ‹R |: F 1-1⟶onto G›
AOT_hence ‹R |: F 1-1⟶ G›and‹R |: F ⟶onto G› using"≡dfE"[OF "fFG:4"] "&E"by blast+
AOT_hence C: ‹R |: F ⟶ G› and D: ‹∀x∀y∀z ([F]x & [F]y & [G]z → ([R]xz & [R]yz → x = y))› and E: ‹∀y ([G]y →∃x ([F]x & [R]xy))› using"≡dfE"[OF "fFG:2"] "≡dfE"[OF "fFG:3"] "&E"by blast+
AOT_show ‹R |: F 1-1⟷ G› proof(rule "1-1-cor"[THEN"≡dfI"]; safe intro!: "&I""cqt:2[const_var]"[axiom_inst])
AOT_show ‹∀x ([F]x →∃!y ([G]y & [R]xy))› using"≡dfE"[OF "fFG:1", OF C] "&E"by blast next
AOT_show ‹∀y ([G]y →∃!x ([F]x & [R]xy))› proof (rule "GEN"; rule "→I") fix y
AOT_assume 0: ‹[G]y›
AOT_hence ‹∃x ([F]x & [R]xy)› using E "∀E""→E"by fast then AOT_obtain a where a_prop: ‹[F]a & [R]ay› using"∃E"[rotated] by blast moreover AOT_have ‹∀z ([F]z & [R]zy → z = a)› proof (rule GEN; rule "→I") fix z
AOT_assume ‹[F]z & [R]zy›
AOT_thus ‹z = a› using D[THEN"∀E"(2)[where β=z], THEN"∀E"(2)[where β=a], THEN"∀E"(2)[where β=y], THEN"→E", THEN"→E"]
a_prop 0"&E""&I"by metis qed ultimately AOT_have ‹∃x ([F]x & [R]xy & ∀z ([F]z & [R]zy → z = x))› using"&I""∃I"(2) by fast
AOT_thus ‹∃!x ([F]x & [R]xy)› using"uniqueness:1"[THEN"≡dfI"] by fast qed qed qed
text‹We have already introduced the restricted type of Ordinary objects in the
Extended Relation Comprehension theory. However, make sure all variable names
are defined as expected (avoiding conflicts with situations
of possible world theory).›
AOT_register_variable_names
Ordinary: u v r t s
AOT_theorem "equi:1": ‹∃!u φ{u} ≡∃u (φ{u} & ∀v (φ{v} → v =E u))› proof(rule "≡I"; rule "→I")
AOT_assume ‹∃!u φ{u}›
AOT_hence ‹∃!x (O!x & φ{x})›.
AOT_hence ‹∃x (O!x & φ{x} & ∀β (O!β & φ{β} → β = x))› using"uniqueness:1"[THEN"≡dfE"] by blast then AOT_obtain x where x_prop: ‹O!x & φ{x} & ∀β (O!β & φ{β} → β = x)› using"∃E"[rotated] by blast
{ fix β
AOT_assume beta_ord: ‹O!β› moreover AOT_assume ‹φ{β}› ultimately AOT_have ‹β = x› using x_prop[THEN"&E"(2), THEN"∀E"(2)[where β=β]] "&I""→E"by blast
AOT_hence ‹β =E x› using"ord-=E=:1"[THEN"→E", OF "∨I"(1)[OF beta_ord], THEN"qml:2"[axiom_inst, THEN"→E"], THEN"≡E"(1)] by blast
}
AOT_hence ‹(O!β → (φ{β} → β =E x))›for β using"→I"by blast
AOT_hence ‹∀β(O!β → (φ{β} → β =E x))› by (rule GEN)
AOT_hence ‹O!x & φ{x} & ∀y (O!y → (φ{y} → y =E x))› using x_prop[THEN"&E"(1)] "&I"by blast
AOT_hence ‹O!x & (φ{x} & ∀y (O!y → (φ{y} → y =E x)))› using"&E""&I"by meson
AOT_thus ‹∃u (φ{u} & ∀v (φ{v} → v =E u))› using"∃I"by fast next
AOT_assume ‹∃u (φ{u} & ∀v (φ{v} → v =E u))›
AOT_hence ‹∃x (O!x & (φ{x} & ∀y (O!y → (φ{y} → y =E x))))› by blast then AOT_obtain x where x_prop: ‹O!x & (φ{x} & ∀y (O!y → (φ{y} → y =E x)))› using"∃E"[rotated] by blast
AOT_have ‹∀y ([O!]y & φ{y} → y = x)› proof(rule GEN; rule "→I") fix y
AOT_assume ‹O!y & φ{y}›
AOT_hence ‹y =E x› using x_prop[THEN"&E"(2), THEN"&E"(2), THEN"∀E"(2)[where β=y]] "→E""&E"by blast
AOT_thus ‹y = x› using"ord-=E=:1"[THEN"→E", OF "∨I"(2)[OF x_prop[THEN"&E"(1)]], THEN"qml:2"[axiom_inst, THEN"→E"], THEN"≡E"(2)] by blast qed
AOT_hence ‹[O!]x & φ{x} & ∀y ([O!]y & φ{y} → y = x)› using x_prop "&E""&I"by meson
AOT_hence ‹∃x ([O!]x & φ{x} & ∀y ([O!]y & φ{y} → y = x))› by (rule "∃I")
AOT_hence ‹∃!x (O!x & φ{x})› by (rule "uniqueness:1"[THEN"≡dfI"])
AOT_thus ‹∃!u φ{u}›. qed
AOT_define EquinumerousE :: ‹τ → τ → φ› (infixl‹≈E›50) "equi:3": ‹F ≈E G ≡df∃R (R |: F 1-1⟷E G)›
text‹Note: not explicitly in PLM.›
AOT_theorem eq_den_1: ‹Π↓›if‹Π ≈E Π'› proof -
AOT_have ‹∃R (R |: Π 1-1⟷E Π')› using"equi:3"[THEN"≡dfE"] that by blast then AOT_obtain R where ‹R |: Π 1-1⟷E Π'› using"∃E"[rotated] by blast
AOT_thus ‹Π↓› using"equi:2"[THEN"≡dfE"] "&E"by blast qed
text‹Note: not explicitly in PLM.›
AOT_theorem eq_den_2: ‹Π'↓›if‹Π ≈E Π'› proof -
AOT_have ‹∃R (R |: Π 1-1⟷E Π')› using"equi:3"[THEN"≡dfE"] that by blast then AOT_obtain R where ‹R |: Π 1-1⟷E Π'› using"∃E"[rotated] by blast
AOT_thus ‹Π'↓› using"equi:2"[THEN"≡dfE"] "&E"by blast+ qed
AOT_theorem "eq-part:1": ‹F ≈E F› proof (safe intro!: "&I" GEN "→I""cqt:2[const_var]"[axiom_inst] "≡dfI"[OF "equi:3"] "≡dfI"[OF "equi:2"] "∃I"(1)) fix x
AOT_assume 1: ‹O!x›
AOT_assume 2: ‹[F]x›
AOT_show ‹∃!v ([F]v & x =E v)› proof(rule "equi:1"[THEN"≡E"(2)];
rule "∃I"(2)[where β=x];
safe dest!: "&E"(2)
intro!: "&I""→I"12 Ordinary.GEN "ord=Eequiv:1"[THEN"→E", OF 1])
AOT_show ‹v =E x›if‹x =E v›for v by (metis that "ord=Eequiv:2"[THEN"→E"]) qed next fix y
AOT_assume 1: ‹O!y›
AOT_assume 2: ‹[F]y›
AOT_show ‹∃!u ([F]u & u =E y)› by(safe dest!: "&E"(2)
intro!: "equi:1"[THEN"≡E"(2)] "∃I"(2)[where β=y] "&I""→I"12 GEN "ord=Eequiv:1"[THEN"→E", OF 1]) qed(auto simp: "=E[denotes]")
AOT_theorem "eq-part:2": ‹F ≈E G → G ≈E F› proof (rule "→I")
AOT_assume ‹F ≈E G›
AOT_hence ‹∃R R |: F 1-1⟷E G› using"equi:3"[THEN"≡dfE"] by blast then AOT_obtain R where ‹R |: F 1-1⟷E G› using"∃E"[rotated] by blast
AOT_hence 0: ‹R↓ & F↓ & G↓ & style='font-size: 18px;'>∀u ([F]u →∃!v([G]v & [R]uv)) & ∀v ([G]v →∃!u([F]u & [R]uv))› using"equi:2"[THEN"≡dfE"] by blast
AOT_have ‹[λxy [R]yx]↓ & G↓ & F>↓ & ∀u ([G]u →∃!v([F]v & [λxy [R]yx]uv)) & ∀v ([F]v →∃!u([G]u & [λxy [R]yx]uv))› proof (AOT_subst ‹[λxy [R]yx]yx›‹[R]xy›for: x y;
(safe intro!: "&I""cqt:2[const_var]"[axiom_inst] 0[THEN"&E"(2)] 0[THEN"&E"(1), THEN"&E"(2)]; "cqt:2[lambda]")?)
AOT_modally_strict {
AOT_have ‹[λxy [R]yx]xy›if‹[R]yx›for y x by (auto intro!: "β←C"(1) "cqt:2"
simp: "&I""ex:1:a" prod_denotesI "rule-ui:3" that) moreover AOT_have ‹[R]yx›if‹[λxy [R]yx]xy›for y x using"β→C"(1)[where φ="λ(x,y). _ (x,y)"and κ1κn="(_,_)",
simplified, OF that, simplified]. ultimately AOT_show ‹[λxy [R]yx]αβ ≡ [R]βα›for α β by (metis "deduction-theorem""≡I")
} qed
AOT_hence ‹[λxy [R]yx] |: G 1-1⟷E F› using"equi:2"[THEN"≡dfI"] by blast
AOT_hence ‹∃R R |: G 1-1⟷E F› by (rule "∃I"(1)) "cqt:2[lambda]"
AOT_thus ‹G ≈E F› using"equi:3"[THEN"≡dfI"] by blast qed
text‹Note: not explicitly in PLM.›
AOT_theorem "eq-part:2[terms]": ‹Π ≈E Π' → Π' ≈E Π› using"eq-part:2"[unvarify F G] eq_den_1 eq_den_2 "→I"by meson declare"eq-part:2[terms]"[THEN"→E", sym]
AOT_theorem "eq-part:3": ‹(F ≈E G & G ≈E H) → F ≈E H› proof (rule "→I")
AOT_assume ‹F ≈E G & G ≈E H› then AOT_obtain R1and R2 where ‹R1 |: F 1-1⟷E G› and‹R2 |: G 1-1⟷E H› using"equi:3"[THEN"≡dfE"] "&E""∃E"[rotated] by metis
AOT_hence θ: ‹∀u ([F]u →∃!v([G]v & [R1]uv)) & ∀v ([G]v →∃!u([F]u & [R1]uv))› and ξ: ‹∀u ([G]u →∃!v([H]v & [R2]uv)) & ∀v ([H]v →∃!u([G]u & [R2]uv))› using"equi:2"[THEN"≡dfE", THEN"&E"(2)] "equi:2"[THEN"≡dfE", THEN"&E"(1), THEN"&E"(2)] "&I"by blast+
AOT_have ‹∃R R = [λxy O!x & O!y & ∃v ([G]v & [R1]xv & [R2]vy)]› by (rule "free-thms:3[lambda]") cqt_2_lambda_inst_prover then AOT_obtain R where R_def: ‹R = [λxy O!x & O!y & ∃v ([G]v & [R1]xv & [R2]vy)]› using"∃E"[rotated] by blast
AOT_have 1: ‹∃!v (([H]v & [R]uv))›if a: ‹[O!]u›and b: ‹[F]u›for u proof (rule "≡E"(2)[OF "equi:1"])
AOT_obtain b where
b_prop: ‹[O!]b & ([G]b & [R1]ub & ∀v ([G]v & [R1]uv → v =E b))› using θ[THEN"&E"(1), THEN"∀E"(2), THEN"→E", THEN"→E",
OF a b, THEN"≡E"(1)[OF "equi:1"]] "∃E"[rotated] by blast
AOT_obtain c where
c_prop: "[O!]c & ([H]c & [R2]bc & ∀v ([H]v & [R2]bv → v =E c))" using ξ[THEN"&E"(1), THEN"∀E"(2)[where β=b], THEN"→E",
OF b_prop[THEN"&E"(1)], THEN"→E",
OF b_prop[THEN"&E"(2), THEN"&E"(1), THEN"&E"(1)], THEN"≡E"(1)[OF "equi:1"]] "∃E"[rotated] by blast
AOT_show ‹∃v ([H]v & [R]uv & ∀v' ([H]v' & [R]uv' → v' =E v))› proof (safe intro!: "&I" GEN "→I""∃I"(2)[where β=c])
AOT_show ‹O!c›using c_prop "&E"by blast next
AOT_show ‹[H]c›using c_prop "&E"by blast next
AOT_have 0: ‹[O!]u & [O!]c & ∃v ([G]v & [R1]uv & [R2]vc)› by (safe intro!: "&I" a c_prop[THEN"&E"(1)] "∃I"(2)[where β=b]
b_prop[THEN"&E"(1)] b_prop[THEN"&E"(2), THEN"&E"(1)]
c_prop[THEN"&E"(2), THEN"&E"(1), THEN"&E"(2)])
AOT_show ‹[R]uc› by (auto intro: "rule=E"[rotated, OF R_def[symmetric]]
intro!: "β←C"(1) "cqt:2"
simp: "&I""ex:1:a" prod_denotesI "rule-ui:3"0) next fix x
AOT_assume ordx: ‹O!x›
AOT_assume ‹[H]x & [R]ux›
AOT_hence hx: ‹[H]x›and‹[R]ux›using"&E"by blast+
AOT_hence ‹[λxy O!x & O!y & ∃v ([G]v & [R1]xv & [R2]vy)]ux› using"rule=E"[rotated, OF R_def] by fast
AOT_hence ‹O!u & O!x & ∃v ([G]v & [R1]uv & [R2]vx)› by (rule "β→C"(1)[where φ="λ(κ,κ'). _ κ κ'"and κ1κn="(_,_)", simplified]) then AOT_obtain z where z_prop: ‹O!z & ([G]z & [R1]uz & [R2]zx)› using"&E""∃E"[rotated] by blast
AOT_hence ‹z =E b› using b_prop[THEN"&E"(2), THEN"&E"(2), THEN"∀E"(2)[where β=z]] using"&E""→E"by metis
AOT_hence ‹z = b› by (metis "=E-simple:2"[THEN"→E"])
AOT_hence ‹[R2]bx› using z_prop[THEN"&E"(2), THEN"&E"(2)] "rule=E"by fast
AOT_thus ‹x =E c› using c_prop[THEN"&E"(2), THEN"&E"(2), THEN"∀E"(2)[where β=x], THEN"→E", THEN"→E", OF ordx]
hx "&I"by blast qed qed
AOT_have 2: ‹∃!u (([F]u & [R]uv))›if a: ‹[O!]v›and b: ‹[H]v›for v proof (rule "≡E"(2)[OF "equi:1"])
AOT_obtain b where
b_prop: ‹[O!]b & ([G]b & [R2]bv & ∀u ([G]u & [R2]uv → u =E b))› using ξ[THEN"&E"(2), THEN"∀E"(2), THEN"→E", THEN"→E",
OF a b, THEN"≡E"(1)[OF "equi:1"]] "∃E"[rotated] by blast
AOT_obtain c where
c_prop: "[O!]c & ([F]c & [R1]cb & ∀v ([F]v & [R1]vb → v =E c))" using θ[THEN"&E"(2), THEN"∀E"(2)[where β=b], THEN"→E",
OF b_prop[THEN"&E"(1)], THEN"→E",
OF b_prop[THEN"&E"(2), THEN"&E"(1), THEN"&E"(1)], THEN"≡E"(1)[OF "equi:1"]] "∃E"[rotated] by blast
AOT_show ‹∃u ([F]u & [R]uv & ∀v' ([F]v' & [R]v'v → v' =E u))› proof (safe intro!: "&I" GEN "→I""∃I"(2)[where β=c])
AOT_show ‹O!c›using c_prop "&E"by blast next
AOT_show ‹[F]c›using c_prop "&E"by blast next
AOT_have ‹[O!]c & [O!]v & ∃u ([G]u & [R1]cu & [R2]uv)› by (safe intro!: "&I" a "∃I"(2)[where β=b]
c_prop[THEN"&E"(1)] b_prop[THEN"&E"(1)]
b_prop[THEN"&E"(2), THEN"&E"(1), THEN"&E"(1)]
b_prop[THEN"&E"(2), THEN"&E"(1), THEN"&E"(2)]
c_prop[THEN"&E"(2), THEN"&E"(1), THEN"&E"(2)])
AOT_thus ‹[R]cv› by (auto intro: "rule=E"[rotated, OF R_def[symmetric]]
intro!: "β←C"(1) "cqt:2"
simp: "&I""ex:1:a" prod_denotesI "rule-ui:3") next fix x
AOT_assume ordx: ‹O!x›
AOT_assume ‹[F]x & [R]xv›
AOT_hence hx: ‹[F]x›and‹[R]xv›using"&E"by blast+
AOT_hence ‹[λxy O!x & O!y & ∃v ([G]v & [R1]xv & [R2]vy)]xv› using"rule=E"[rotated, OF R_def] by fast
AOT_hence ‹O!x & O!v & ∃u ([G]u & [R1]xu & [R2]uv)› by (rule "β→C"(1)[where φ="λ(κ,κ'). _ κ κ'"and κ1κn="(_,_)", simplified]) then AOT_obtain z where z_prop: ‹O!z & ([G]z & [R1]xz & [R2]zv)› using"&E""∃E"[rotated] by blast
AOT_hence ‹z =E b› using b_prop[THEN"&E"(2), THEN"&E"(2), THEN"∀E"(2)[where β=z]] using"&E""→E""&I"by metis
AOT_hence ‹z = b› by (metis "=E-simple:2"[THEN"→E"])
AOT_hence ‹[R1]xb› using z_prop[THEN"&E"(2), THEN"&E"(1), THEN"&E"(2)] "rule=E"by fast
AOT_thus ‹x =E c› using c_prop[THEN"&E"(2), THEN"&E"(2), THEN"∀E"(2)[where β=x], THEN"→E", THEN"→E", OF ordx]
hx "&I"by blast qed qed
AOT_show ‹F ≈E H› apply (rule "equi:3"[THEN"≡dfI"]) apply (rule "∃I"(2)[where β=R]) by (auto intro!: 12"equi:2"[THEN"≡dfI"] "&I""cqt:2[const_var]"[axiom_inst]
Ordinary.GEN "→I" Ordinary.ψ) qed
text‹Note: not explicitly in PLM.›
AOT_theorem "eq-part:3[terms]": ‹Π ≈E Π''›if‹Π ≈E Π'›and‹Π' ≈E Π''› using"eq-part:3"[unvarify F G H, THEN"→E"] eq_den_1 eq_den_2 "→I""&I" by (metis that(1) that(2)) declare"eq-part:3[terms]"[trans]
AOT_theorem "eq-part:4": ‹F ≈E G ≡∀H (H ≈E F ≡ H ≈E G)› proof(rule "≡I"; rule "→I")
AOT_assume 0: ‹F ≈E G›
AOT_hence 1: ‹G ≈E F›using"eq-part:2"[THEN"→E"] by blast
AOT_show ‹∀H (H ≈E F ≡ H ≈E G)› proof (rule GEN; rule "≡I"; rule "→I")
AOT_show ‹H ≈E G›if‹H ≈E F›for H using0 by (meson "&I""eq-part:3" that "vdash-properties:6") next
AOT_show ‹H ≈E F›if‹H ≈E G›for H using1 by (metis "&I""eq-part:3" that "vdash-properties:6") qed next
AOT_assume ‹∀H (H ≈E F ≡ H ≈E G)›
AOT_hence ‹F ≈E F ≡ F ≈E G›using"∀E"by blast
AOT_thus ‹F ≈E G›using"eq-part:1""≡E"by blast qed
text‹Note: not explicitly in PLM.›
AOT_theorem "F-u[den]": ‹[F]-x↓› by (rule "=dfI"(1)[OF "F-u", where τ1τn="(_,_)", simplified]; "cqt:2[lambda]")
AOT_theorem "F-u[equiv]": ‹[[F]-x]y ≡ ([F]y & y ≠E x)› by (auto intro: "F-u"[THEN"=dfI"(1), where τ1τn="(_,_)", simplified]
intro!: "cqt:2""beta-C-cor:2"[THEN"→E", THEN"∀E"(2)])
AOT_theorem eqP': ‹F ≈E G & [F]u & [G]v → [F]-u≈E [G]-v› proof (rule "→I"; frule "&E"(2); drule "&E"(1); frule "&E"(2); drule "&E"(1))
AOT_assume ‹F ≈E G›
AOT_hence ‹∃R R |: F 1-1⟷E G› using"equi:3"[THEN"≡dfE"] by blast then AOT_obtain R where R_prop: ‹R |: F 1-1⟷E G› using"∃E"[rotated] by blast
AOT_hence A: ‹∀u ([F]u →∃!v ([G]v & [R]uv))› and B: ‹∀v ([G]v →∃!u ([F]u & [R]uv))› using"equi:2"[THEN"≡dfE"] "&E"by blast+
AOT_have ‹R |: F 1-1⟶ontoE G› using"equi-rem-thm"[THEN"≡E"(1), OF R_prop].
AOT_hence ‹R |: F 1-1⟶E G & R |: F ⟶ontoE G› using"equi-rem:4"[THEN"≡dfE"] by blast
AOT_hence C: ‹∀t∀u∀v (([F]t & [F]u & [G]v) → ([R]tv & [R]uv → t =E u))› using"equi-rem:2"[THEN"≡dfE"] "&E"by blast
AOT_assume fu: ‹[F]u›
AOT_assume gv: ‹[G]v›
AOT_have ‹[λz [Π]z & z ≠E κ]↓›for Π κ by"cqt:2[lambda]" note Π_minus_κI = "rule-id-df:2:b[2]"[
where τ=‹(λ(Π, κ). «[Π]-\κ¬)›, simplified, OF "F-u", simplified, OF this] and Π_minus_κE = "rule-id-df:2:a[2]"[
where τ=‹(λ(Π, κ). «[Π]-\κ¬)›, simplified, OF "F-u", simplified, OF this]
AOT_have Π_minus_κ_den: ‹[Π]-\κ↓›for Π κ by (rule Π_minus_κI) "cqt:2[lambda]"+
{ fix R
AOT_assume R_prop: ‹R |: F 1-1⟷E G›
AOT_hence A: ‹∀u ([F]u →∃!v ([G]v & [R]uv))› and B: ‹∀v ([G]v →∃!u ([F]u & [R]uv))› using"equi:2"[THEN"≡dfE"] "&E"by blast+
AOT_have ‹R |: F 1-1⟶ontoE G› using"equi-rem-thm"[THEN"≡E"(1), OF R_prop].
AOT_hence ‹R |: F 1-1⟶E G & R |: F ⟶ontoE G› using"equi-rem:4"[THEN"≡dfE"] by blast
AOT_hence C: ‹∀t∀u∀v (([F]t & [F]u & [G]v) → ([R]tv & [R]uv → t =E u))› using"equi-rem:2"[THEN"≡dfE"] "&E"by blast
AOT_assume Ruv: ‹[R]uv›
AOT_have ‹R |: [F]-u1-1⟷E [G]-v› proof(safe intro!: "equi:2"[THEN"≡dfI"] "&I""cqt:2[const_var]"[axiom_inst]
Π_minus_κ_den Ordinary.GEN "→I") fix u'
AOT_assume ‹[[F]-u]u'›
AOT_hence 0: ‹[λz [F]z & z ≠E u]u'› using Π_minus_κE by fast
AOT_have 0: ‹[F]u' & u' ≠E u› by (rule "β→C"(1)[where κ1κn="AOT_term_of_var (Ordinary.Rep u')"]) (fact 0)
AOT_have ‹∃!v ([G]v & [R]u'v)› using A[THEN"Ordinary.∀E"[where α=u'], THEN"→E", OF 0[THEN"&E"(1)]]. then AOT_obtain v' where
v'_prop: ‹[G]v' & [R]u'v' & ∀ t ([G]t & [R]u't → t =E v')› using"equi:1"[THEN"≡E"(1)] "Ordinary.∃E"[rotated] by fastforce
AOT_show ‹∃!v' ([[G]-v]v' & [R]u'v')› proof (safe intro!: "equi:1"[THEN"≡E"(2)] "Ordinary.∃I"[where β=v'] "&I" Ordinary.GEN "→I")
AOT_show ‹[[G]-v]v'› proof (rule Π_minus_κI;
safe intro!: "β←C"(1) "cqt:2""&I""thm-neg=E"[THEN"≡E"(2)])
AOT_show ‹[G]v'›using v'_prop"&E"by blast next
AOT_show ‹¬v' =E v› proof (rule "raa-cor:2")
AOT_assume ‹v' =E v›
AOT_hence ‹v' = v›by (metis "=E-simple:2""→E")
AOT_hence Ruv': ‹[R]uv'›using"rule=E" Ruv id_sym by fast
AOT_have ‹u' =E u› by (rule C[THEN"Ordinary.∀E", THEN"Ordinary.∀E", THEN"Ordinary.∀E"[where α=v'], THEN"→E", THEN"→E"])
(safe intro!: "&I"0[THEN"&E"(1)] fu
v'_prop[THEN"&E"(1), THEN"&E"(1)]
Ruv' v'_prop[THEN"&E"(1), THEN"&E"(2)]) moreover AOT_have ‹¬(u' =E u)› using"0""&E"(2) "≡E"(1) "thm-neg=E"by blast ultimately AOT_show ‹u' =E u & ¬u' =E u›using"&I"by blast qed qed next
AOT_show ‹[R]u'v'›using v'_prop"&E"by blast next fix t
AOT_assume t_prop: ‹[[G]-v]t & [R]u't›
AOT_have gt_t_noteq_v: ‹[G]t & t ≠E v› apply (rule "β→C"(1)[where κ1κn="AOT_term_of_var (Ordinary.Rep t)"]) apply (rule Π_minus_κE) by (fact t_prop[THEN"&E"(1)])
AOT_show ‹t =E v'› using v'_prop[THEN"&E"(2), THEN"Ordinary.∀E", THEN"→E",
OF "&I", OF gt_t_noteq_v[THEN"&E"(1)],
OF t_prop[THEN"&E"(2)]]. qed next fix v'
AOT_assume G_minus_v_v': ‹[[G]-v]v'›
AOT_have gt_t_noteq_v: ‹[G]v' & v' ≠E v› apply (rule "β→C"(1)[where κ1κn="AOT_term_of_var (Ordinary.Rep v')"]) apply (rule Π_minus_κE) by (fact G_minus_v_v')
AOT_have ‹∃!u([F]u & [R]uv')› using B[THEN"Ordinary.∀E", THEN"→E", OF gt_t_noteq_v[THEN"&E"(1)]]. then AOT_obtain u' where
u'_prop: ‹[F]u' & [R]u'v' & ∀t ([F]t & [R]tv' → t =E u')› using"equi:1"[THEN"≡E"(1)] "Ordinary.∃E"[rotated] by fastforce
AOT_show ‹∃!u' ([[F]-u]u' & [R]u'v')› proof (safe intro!: "equi:1"[THEN"≡E"(2)] "Ordinary.∃I"[where β=u'] "&I"
u'_prop[THEN"&E"(1), THEN"&E"(2)] Ordinary.GEN "→I")
AOT_show ‹[[F]-u]u'› proof (rule Π_minus_κI;
safe intro!: "β←C"(1) "cqt:2""&I""thm-neg=E"[THEN"≡E"(2)]
u'_prop[THEN"&E"(1), THEN"&E"(1)]; rule "raa-cor:2")
AOT_assume u'_eq_u: ‹u' =E u›
AOT_hence ‹u' = u› using"=E-simple:2""vdash-properties:10"by blast
AOT_hence Ru'v: ‹[R]u'v›using"rule=E" Ruv id_sym by fast
AOT_have ‹v' ≠E v› using"&E"(2) gt_t_noteq_v by blast
AOT_hence v'_noteq_v: ‹¬(v' =E v)›by (metis "≡E"(1) "thm-neg=E")
AOT_have ‹∃u ([G]u & [R]u'u & ∀v ([G]v & [R]u'v → v =E u))› using A[THEN"Ordinary.∀E", THEN"→E",
OF u'_prop[THEN"&E"(1), THEN"&E"(1)], THEN"equi:1"[THEN"≡E"(1)]]. then AOT_obtain t where
t_prop: ‹[G]t & [R]u't & ∀v ([G]v & [R]u'v → v =E t)› using"Ordinary.∃E"[rotated] by meson
AOT_have ‹v =E t›if‹[G]v›and‹[R]u'v›for v using t_prop[THEN"&E"(2), THEN"Ordinary.∀E", THEN"→E",
OF "&I", OF that].
AOT_hence ‹v' =E t›and‹v =E t› by (auto simp: gt_t_noteq_v[THEN"&E"(1)] Ru'v gv
u'_prop[THEN"&E"(1), THEN"&E"(2)])
AOT_hence ‹v' =E v› using"rule=E""=E-simple:2" id_sym "→E"by fast
AOT_thus ‹v' =E v & ¬v' =E v› using v'_noteq_v "&I"by blast qed next fix t
AOT_assume 0: ‹[[F]-u]t & [R]tv'› moreover AOT_have ‹[F]t & t ≠E u› apply (rule "β→C"(1)[where κ1κn="AOT_term_of_var (Ordinary.Rep t)"]) apply (rule Π_minus_κE) by (fact 0[THEN"&E"(1)]) ultimately AOT_show ‹t =E u'› using u'_prop[THEN"&E"(2), THEN"Ordinary.∀E", THEN"→E", OF "&I"] "&E"by blast qed qed
AOT_hence ‹∃R R |: [F]-u1-1⟷E [G]-v› by (rule "∃I")
} note1 = this moreover {
AOT_assume not_Ruv: ‹¬[R]uv›
AOT_have ‹∃!v ([G]v & [R]uv)› using A[THEN"Ordinary.∀E", THEN"→E", OF fu]. then AOT_obtain b where
b_prop: ‹O!b & ([G]b & [R]ub & ∀t([G]t & [R]ut → t =E b))› using"equi:1"[THEN"≡E"(1)] "∃E"[rotated] by fastforce
AOT_hence ob: ‹O!b›and gb: ‹[G]b›and Rub: ‹[R]ub› using"&E"by blast+
AOT_have ‹O!t → ([G]t & [R]ut → t =E b)›for t using b_prop "&E"(2) "∀E"(2) by blast
AOT_hence b_unique: ‹t =E b›if‹O!t›and‹[G]t›and‹[R]ut›for t by (metis Adjunction "modus-tollens:1""reductio-aa:1" that)
AOT_have not_v_eq_b: ‹¬(v =E b)› proof(rule "raa-cor:2")
AOT_assume ‹v =E b›
AOT_hence 0: ‹v = b› by (metis "=E-simple:2""→E")
AOT_have ‹[R]uv› using b_prop[THEN"&E"(2), THEN"&E"(1), THEN"&E"(2)] "rule=E"[rotated, OF 0[symmetric]] by fast
AOT_thus ‹[R]uv & ¬[R]uv› using not_Ruv "&I"by blast qed
AOT_have not_b_eq_v: ‹¬(b =E v)› using"modus-tollens:1" not_v_eq_b "ord=Eequiv:2"by blast
AOT_have ‹∃!u ([F]u & [R]uv)› using B[THEN"Ordinary.∀E", THEN"→E", OF gv]. then AOT_obtain a where
a_prop: ‹O!a & ([F]a & [R]av & ∀t([F]t & [R]tv → t =E a))› using"equi:1"[THEN"≡E"(1)] "∃E"[rotated] by fastforce
AOT_hence Oa: ‹O!a›and fa: ‹[F]a›and Rav: ‹[R]av› using"&E"by blast+
AOT_have ‹O!t → ([F]t & [R]tv → t =E a)›for t using a_prop "&E""∀E"(2) by blast
AOT_hence a_unique: ‹t =E a›if‹O!t›and‹[F]t›and‹[R]tv›for t by (metis Adjunction "modus-tollens:1""reductio-aa:1" that)
AOT_have not_u_eq_a: ‹¬(u =E a)› proof(rule "raa-cor:2")
AOT_assume ‹u =E a›
AOT_hence 0: ‹u = a› by (metis "=E-simple:2""→E")
AOT_have ‹[R]uv› using a_prop[THEN"&E"(2), THEN"&E"(1), THEN"&E"(2)] "rule=E"[rotated, OF 0[symmetric]] by fast
AOT_thus ‹[R]uv & ¬[R]uv› using not_Ruv "&I"by blast qed
AOT_have not_a_eq_u: ‹¬(a =E u)› using"modus-tollens:1" not_u_eq_a "ord=Eequiv:2"by blast let ?R = ‹«[λu'v' (u' ≠E u & v' ≠E v & [R]u'v') ∨
(u' =E a & v' =E b) ∨
(u' =E u & v' =E v)]¬›
AOT_have ‹[«?R¬]↓›by"cqt:2[lambda]"
AOT_hence ‹∃ β β = [«?R¬]› using"free-thms:1""≡E"(1) by fast then AOT_obtain R1 where R1_def: ‹R1 = [«?R¬]› using"∃E"[rotated] by blast
AOT_have Rxy1: ‹[R]xy›if‹[R1]xy›and‹x ≠E u›and‹x ≠E a›for x y proof -
AOT_have 0: ‹[«?R¬]xy› by (rule "rule=E"[rotated, OF R1_def]) (fact that(1))
AOT_have ‹(x ≠E u & y ≠E v & [R]xy) ∨ (x =E a & y =E b) ∨ (x =E u & y =E v)› using"β→C"(1)[OF 0] by simp
AOT_hence ‹x ≠E u & y ≠E v & [R]xy›using that(2,3) by (metis "∨E"(3) "Conjunction Simplification"(1) "≡E"(1) "modus-tollens:1""thm-neg=E")
AOT_thus ‹[R]xy›using"&E"by blast+ qed
AOT_have Rxy2: ‹[R]xy›if‹[R1]xy›and‹y ≠E v›and‹y ≠E b›for x y proof -
AOT_have 0: ‹[«?R¬]xy› by (rule "rule=E"[rotated, OF R1_def]) (fact that(1))
AOT_have ‹(x ≠E u & y ≠E v & [R]xy) ∨ (x =E a & y =E b) ∨ (x =E u & y =E v)› using"β→C"(1)[OF 0] by simp
AOT_hence ‹x ≠E u & y ≠E v & [R]xy› using that(2,3) by (metis "∨E"(3) "Conjunction Simplification"(2) "≡E"(1) "modus-tollens:1""thm-neg=E")
AOT_thus ‹[R]xy›using"&E"by blast+ qed
AOT_have R1xy: ‹[R1]xy›if‹[R]xy›and‹x ≠E u›and‹y ≠E v›for x y by (rule "rule=E"[rotated, OF R1_def[symmetric]])
(auto intro!: "β←C"(1) "cqt:2"
simp: "&I""ex:1:a" prod_denotesI "rule-ui:3" that "∨I"(1))
AOT_have R1ab: ‹[R1]ab› apply (rule "rule=E"[rotated, OF R1_def[symmetric]]) apply (safe intro!: "β←C"(1) "cqt:2" prod_denotesI "&I") by (meson a_prop b_prop "&I""&E"(1) "∨I"(1) "∨I"(2) "ord=Eequiv:1""→E")
AOT_have R1uv: ‹[R1]uv› apply (rule "rule=E"[rotated, OF R1_def[symmetric]]) apply (safe intro!: "β←C"(1) "cqt:2" prod_denotesI "&I") by (meson "&I""∨I"(2) "ord=Eequiv:1" Ordinary.ψ "→E") moreover AOT_have ‹R1 |: F 1-1⟷E G› proof (safe intro!: "equi:2"[THEN"≡dfI"] "&I""cqt:2" Ordinary.GEN "→I") fix u'
AOT_assume fu': ‹[F]u'›
{
AOT_assume not_u'_eq_u: ‹¬(u' =E u)›and not_u'_eq_a: ‹¬(u' =E a)›
AOT_hence u'_noteq_u: ‹u' ≠E u›and u'_noteq_a: ‹u' ≠E a› by (metis "≡E"(2) "thm-neg=E")+
AOT_have ‹∃!v ([G]v & [R]u'v)› using A[THEN"Ordinary.∀E", THEN"→E", OF fu'].
AOT_hence ‹∃v ([G]v & [R]u'v & ∀t ([G]t & [R]u't → t =E v))› using"equi:1"[THEN"≡E"(1)] by simp then AOT_obtain v' where
v'_prop: ‹[G]v' & [R]u'v' & ∀t ([G]t & [R]u't → t =E v')› using"Ordinary.∃E"[rotated] by meson
AOT_hence gv': ‹[G]v'›and Ru'v': ‹[R]u'v'› using"&E"by blast+
AOT_have not_v'_eq_v: ‹¬v' =E v› proof (rule "raa-cor:2")
AOT_assume ‹v' =E v›
AOT_hence ‹v' = v› by (metis "=E-simple:2""→E")
AOT_hence Ru'v: ‹[R]u'v› using"rule=E" Ru'v' by fast
AOT_have ‹u' =E a› using a_unique[OF Ordinary.ψ, OF fu', OF Ru'v].
AOT_thus ‹u' =E a & ¬u' =E a› using not_u'_eq_a "&I"by blast qed
AOT_hence v'_noteq_v: ‹v' ≠E v› using"≡E"(2) "thm-neg=E"by blast
AOT_have ‹∀t ([G]t & [R]u't → t =E v')› using v'_prop"&E"by blast
AOT_hence ‹[G]t & [R]u't → t =E v'›for t using"Ordinary.∀E"by meson
AOT_hence v'_unique: ‹t =E v'›if‹[G]t›and‹[R]u't›for t by (metis "&I" that "→E")
AOT_have ‹[G]v' & [R1]u'v' & ∀t ([G]t & [R1]u't → t =E v')› proof (safe intro!: "&I" gv' R1xy Ru'v' u'_noteq_u u'_noteq_a "→I"
Ordinary.GEN "thm-neg=E"[THEN"≡E"(2)] not_v'_eq_v) fix t
AOT_assume 1: ‹[G]t & [R1]u't›
AOT_have ‹[R]u't› using Rxy1[OF 1[THEN"&E"(2)], OF u'_noteq_u, OF u'_noteq_a].
AOT_thus ‹t =E v'› using v'_unique 1[THEN"&E"(1)] by blast qed
AOT_hence ‹∃v ([G]v & [R1]u'v & ∀t ([G]t & [R1]u't → t =E v))› by (rule "Ordinary.∃I")
AOT_hence ‹∃!v ([G]v & [R1]u'v)› by (rule "equi:1"[THEN"≡E"(2)])
} moreover {
AOT_assume 0: ‹u' =E u›
AOT_hence u'_eq_u: ‹u' = u› using"=E-simple:2""→E"by blast
AOT_have ‹∃!v ([G]v & [R1]u'v)› proof (safe intro!: "equi:1"[THEN"≡E"(2)] "Ordinary.∃I"[where β=v] "&I" Ordinary.GEN "→I" gv)
AOT_show ‹[R1]u'v› apply (rule "rule=E"[rotated, OF R1_def[symmetric]]) apply (safe intro!: "β←C"(1) "cqt:2""&I" prod_denotesI) by (safe intro!: "∨I"(2) "&I"0"ord=Eequiv:1"[THEN"→E", OF Ordinary.ψ]) next fix v'
AOT_assume ‹[G]v' & [R1]u'v'›
AOT_hence 0: ‹[R1]uv'› using"rule=E"[rotated, OF u'_eq_u] "&E"(2) by fast
AOT_have 1: ‹[«?R¬]uv'› by (rule "rule=E"[rotated, OF R1_def]) (fact 0)
AOT_have 2: ‹(u ≠E u & v' ≠E v & [R]uv') ∨
(u =E a & v' =E b) ∨
(u =E u & v' =E v)› using"β→C"(1)[OF 1] by simp
AOT_have ‹¬u ≠E u› using"≡E"(4) "modus-tollens:1""ord=Eequiv:1" Ordinary.ψ "reductio-aa:2""thm-neg=E"by blast
AOT_hence ‹¬((u ≠E u & v' ≠E v & [R]uv') ∨ (u =E a & v' =E b))› using not_u_eq_a by (metis "∨E"(2) "Conjunction Simplification"(1) "modus-tollens:1""reductio-aa:1")
AOT_hence ‹(u =E u & v' =E v)› using2by (metis "∨E"(2))
AOT_thus ‹v' =E v› using"&E"by blast qed
} moreover {
AOT_assume 0: ‹u' =E a›
AOT_hence u'_eq_a: ‹u' = a› using"=E-simple:2""→E"by blast
AOT_have ‹∃!v ([G]v & [R1]u'v)› proof (safe intro!: "equi:1"[THEN"≡E"(2)] "∃I"(2)[where β=b] "&I"
Ordinary.GEN "→I" b_prop[THEN"&E"(1)]
b_prop[THEN"&E"(2), THEN"&E"(1), THEN"&E"(1)])
AOT_show ‹[R1]u'b› apply (rule "rule=E"[rotated, OF R1_def[symmetric]]) apply (safe intro!: "β←C"(1) "cqt:2""&I" prod_denotesI) apply (rule "∨I"(1); rule "∨I"(2); rule "&I") apply (fact 0) using b_prop "&E"(1) "ord=Eequiv:1""→E"by blast next fix v'
AOT_assume gv'_R1u'v': ‹[G]v' & [R1]u'v'›
AOT_hence 0: ‹[R1]av'› using u'_eq_a by (meson "rule=E""&E"(2))
AOT_have 1: ‹[«?R¬]av'› by (rule "rule=E"[rotated, OF R1_def]) (fact 0)
AOT_have ‹(a ≠E u & v' ≠E v & [R]av') ∨
(a =E a & v' =E b) ∨
(a =E u & v' =E v)› using"β→C"(1)[OF 1] by simp moreover {
AOT_assume 0: ‹a ≠E u & v' ≠E v & [R]av'›
AOT_have ‹∃!v ([G]v & [R]u'v)› using A[THEN"Ordinary.∀E", THEN"→E", OF fu'].
AOT_hence ‹∃!v ([G]v & [R]av)› using u'_eq_a "rule=E"by fast
AOT_hence ‹∃v ([G]v & [R]av & ∀t ([G]t & [R]at → t =E v))› using"equi:1"[THEN"≡E"(1)] by fast then AOT_obtain s where
s_prop: ‹[G]s & [R]as & ∀t ([G]t & [R]at → t =E s)› using"Ordinary.∃E"[rotated] by meson
AOT_have ‹v' =E s› using s_prop[THEN"&E"(2), THEN"Ordinary.∀E"]
gv'_R1u'v'[THEN"&E"(1)] 0[THEN"&E"(2)] by (metis "&I""vdash-properties:10") moreover AOT_have ‹v =E s› using s_prop[THEN"&E"(2), THEN"Ordinary.∀E"] gv Rav by (metis "&I""→E") ultimately AOT_have ‹v' =E v› by (metis "&I""ord=Eequiv:2""ord=Eequiv:3""→E") moreover AOT_have ‹¬(v' =E v)› using0[THEN"&E"(1), THEN"&E"(2)] by (metis "≡E"(1) "thm-neg=E") ultimately AOT_have ‹v' =E b› by (metis "raa-cor:3")
} moreover {
AOT_assume ‹a =E u & v' =E v›
AOT_hence ‹v' =E b› by (metis "&E"(1) not_a_eq_u "reductio-aa:1")
} ultimately AOT_show ‹v' =E b› by (metis "&E"(2) "∨E"(3) "reductio-aa:1") qed
} ultimately AOT_show ‹∃!v ([G]v & [R1]u'v)› by (metis "raa-cor:1") next fix v'
AOT_assume gv': ‹[G]v'›
{
AOT_assume not_v'_eq_v: ‹¬(v' =E v)› and not_v'_eq_b: ‹¬(v' =E b)›
AOT_hence v'_noteq_v: ‹v' ≠E v› and v'_noteq_b: ‹v' ≠E b› by (metis "≡E"(2) "thm-neg=E")+
AOT_have ‹∃!u ([F]u & [R]uv')› using B[THEN"Ordinary.∀E", THEN"→E", OF gv'].
AOT_hence ‹∃u ([F]u & [R]uv' & ∀t ([F]t & [R]tv' → t =E u))› using"equi:1"[THEN"≡E"(1)] by simp then AOT_obtain u' where
u'_prop: ‹[F]u' & [R]u'v' & ∀t ([F]t & [R]tv' → t =E u')› using"Ordinary.∃E"[rotated] by meson
AOT_hence fu': ‹[F]u'›and Ru'v': ‹[R]u'v'› using"&E"by blast+
AOT_have not_u'_eq_u: ‹¬u' =E u› proof (rule "raa-cor:2")
AOT_assume ‹u' =E u›
AOT_hence ‹u' = u› by (metis "=E-simple:2""→E")
AOT_hence Ruv': ‹[R]uv'› using"rule=E" Ru'v' by fast
AOT_have ‹v' =E b› using b_unique[OF Ordinary.ψ, OF gv', OF Ruv'].
AOT_thus ‹v' =E b & ¬v' =E b› using not_v'_eq_b "&I"by blast qed
AOT_hence u'_noteq_u: ‹u' ≠E u› using"≡E"(2) "thm-neg=E"by blast
AOT_have ‹∀t ([F]t & [R]tv' → t =E u')› using u'_prop"&E"by blast
AOT_hence ‹[F]t & [R]tv' → t =E u'›for t using"Ordinary.∀E"by meson
AOT_hence u'_unique: ‹t =E u'›if‹[F]t›and‹[R]tv'›for t by (metis "&I" that "→E")
AOT_have ‹[F]u' & [R1]u'v' & ∀t ([F]t & [R1]tv' → t =E u')› proof (safe intro!: "&I" gv' R1xy Ru'v' u'_noteq_u Ordinary.GEN "→I" "thm-neg=E"[THEN"≡E"(2)] not_v'_eq_v fu') fix t
AOT_assume 1: ‹[F]t & [R1]tv'›
AOT_have ‹[R]tv'› using Rxy2[OF 1[THEN"&E"(2)], OF v'_noteq_v, OF v'_noteq_b].
AOT_thus ‹t =E u'› using u'_unique 1[THEN"&E"(1)] by blast qed
AOT_hence ‹∃u ([F]u & [R1]uv' & ∀t ([F]t & [R1]tv' → t =E u))› by (rule "Ordinary.∃I")
AOT_hence ‹∃!u ([F]u & [R1]uv')› by (rule "equi:1"[THEN"≡E"(2)])
} moreover {
AOT_assume 0: ‹v' =E v›
AOT_hence u'_eq_u: ‹v' = v› using"=E-simple:2""→E"by blast
AOT_have ‹∃!u ([F]u & [R1]uv')› proof (safe intro!: "equi:1"[THEN"≡E"(2)] "Ordinary.∃I"[where β=u] "&I" Ordinary.GEN "→I" fu)
AOT_show ‹[R1]uv'› by (rule "rule=E"[rotated, OF R1_def[symmetric]])
(safe intro!: "β←C"(1) "cqt:2""&I" prod_denotesI Ordinary.ψ "∨I"(2) 0"ord=Eequiv:1"[THEN"→E"]) next fix u'
AOT_assume ‹[F]u' & [R1]u'v'›
AOT_hence 0: ‹[R1]u'v› using"rule=E"[rotated, OF u'_eq_u] "&E"(2) by fast
AOT_have 1: ‹[«?R¬]u'v› by (rule "rule=E"[rotated, OF R1_def]) (fact 0)
AOT_have 2: ‹(u' ≠E u & v ≠E v & [R]u'v) ∨
(u' =E a & v =E b) ∨
(u' =E u & v =E v)› using"β→C"(1)[OF 1, simplified] by simp
AOT_have ‹¬v ≠E v› using"≡E"(4) "modus-tollens:1""ord=Eequiv:1" Ordinary.ψ "reductio-aa:2""thm-neg=E"by blast
AOT_hence ‹¬((u' ≠E u & v ≠E v & [R]u'v) ∨ (u' =E a & v =E b))› by (metis "&E"(1) "&E"(2) "∨E"(3) not_v_eq_b "raa-cor:3")
AOT_hence ‹(u' =E u & v =E v)› using2by (metis "∨E"(2))
AOT_thus ‹u' =E u› using"&E"by blast qed
} moreover {
AOT_assume 0: ‹v' =E b›
AOT_hence v'_eq_b: ‹v' = b› using"=E-simple:2""→E"by blast
AOT_have ‹∃!u ([F]u & [R1]uv')› proof (safe intro!: "equi:1"[THEN"≡E"(2)] "∃I"(2)[where β=a] "&I"
Ordinary.GEN "→I" b_prop[THEN"&E"(1)] Oa fa
b_prop[THEN"&E"(2), THEN"&E"(1), THEN"&E"(1)])
AOT_show ‹[R1]av'› apply (rule "rule=E"[rotated, OF R1_def[symmetric]]) apply (safe intro!: "β←C"(1) "cqt:2""&I" prod_denotesI) apply (rule "∨I"(1); rule "∨I"(2); rule "&I") using Oa "ord=Eequiv:1""→E"apply blast using"0"by blast next fix u'
AOT_assume fu'_R1u'v': ‹[F]u' & [R1]u'v'›
AOT_hence 0: ‹[R1]u'b› using v'_eq_b by (meson "rule=E""&E"(2))
AOT_have 1: ‹[«?R¬]u'b› by (rule "rule=E"[rotated, OF R1_def]) (fact 0)
AOT_have ‹(u' ≠E u & b ≠E v & [R]u'b) ∨
(u' =E a & b =E b) ∨
(u' =E u & b =E v)› using"β→C"(1)[OF 1, simplified] by simp moreover {
AOT_assume 0: ‹u' ≠E u & b ≠E v & [R]u'b›
AOT_have ‹∃!u ([F]u & [R]uv')› using B[THEN"Ordinary.∀E", THEN"→E", OF gv'].
AOT_hence ‹∃!u ([F]u & [R]ub)› using v'_eq_b "rule=E"by fast
AOT_hence ‹∃u ([F]u & [R]ub & ∀t ([F]t & [R]tb → t =E u))› using"equi:1"[THEN"≡E"(1)] by fast then AOT_obtain s where
s_prop: ‹[F]s & [R]sb & ∀t ([F]t & [R]tb → t =E s)› using"Ordinary.∃E"[rotated] by meson
AOT_have ‹u' =E s› using s_prop[THEN"&E"(2), THEN"Ordinary.∀E"]
fu'_R1u'v'[THEN"&E"(1)] 0[THEN"&E"(2)] by (metis "&I""→E") moreover AOT_have ‹u =E s› using s_prop[THEN"&E"(2), THEN"Ordinary.∀E"] fu Rub by (metis "&I""→E") ultimately AOT_have ‹u' =E u› by (metis "&I""ord=Eequiv:2""ord=Eequiv:3""→E") moreover AOT_have ‹¬(u' =E u)› using0[THEN"&E"(1), THEN"&E"(1)] by (metis "≡E"(1) "thm-neg=E") ultimately AOT_have ‹u' =E a› by (metis "raa-cor:3")
} moreover {
AOT_assume ‹u' =E u & b =E v›
AOT_hence ‹u' =E a› by (metis "&E"(2) not_b_eq_v "reductio-aa:1")
} ultimately AOT_show ‹u' =E a› by (metis "&E"(1) "∨E"(3) "reductio-aa:1") qed
} ultimately AOT_show ‹∃!u ([F]u & [R1]uv')› by (metis "raa-cor:1") qed ultimately AOT_have ‹∃R R |: [F]-u1-1⟷E [G]-v› using1by blast
} ultimately AOT_have ‹∃R R |: [F]-u1-1⟷E [G]-v› using R_prop by (metis "reductio-aa:2")
AOT_thus ‹[F]-u≈E [G]-v› by (rule "equi:3"[THEN"≡dfI"]) qed
AOT_theorem "P'-eq": ‹[F]-u≈E [G]-v & [F]u & [G]v → F ≈E G› proof(safe intro!: "→I"; frule "&E"(1); drule "&E"(2);
frule "&E"(1); drule "&E"(2))
AOT_have ‹[λz [Π]z & z ≠E κ]↓›for Π κ by"cqt:2[lambda]" note Π_minus_κI = "rule-id-df:2:b[2]"[
where τ=‹(λ(Π, κ). «[Π]-\κ¬)›, simplified, OF "F-u", simplified, OF this] and Π_minus_κE = "rule-id-df:2:a[2]"[
where τ=‹(λ(Π, κ). «[Π]-\κ¬)›, simplified, OF "F-u", simplified, OF this]
AOT_have Π_minus_κ_den: ‹[Π]-\κ↓›for Π κ by (rule Π_minus_κI) "cqt:2[lambda]"+
AOT_have Π_minus_κE1: ‹[Π]κ'› and Π_minus_κE2: ‹κ' ≠E κ›if‹[[Π]-\κ]κ'›for Π κ κ' proof -
AOT_have ‹[λz [Π]z & z ≠E κ]κ'› using Π_minus_κE that by fast
AOT_hence ‹[Π]κ' & κ' ≠E κ› by (rule "β→C"(1))
AOT_thus ‹[Π]κ'›and‹κ' ≠E κ› using"&E"by blast+ qed
AOT_have Π_minus_κI': ‹[[Π]-\κ]κ'›if‹[Π]κ'›and‹κ' ≠E κ›for Π κ κ' proof -
AOT_have κ'_den: ‹κ'↓› by (metis "russell-axiom[exe,1].ψ_denotes_asm" that(1))
AOT_have ‹[λz [Π]z & z ≠E κ]κ'› by (safe intro!: "β←C"(1) "cqt:2" κ'_den "&I" that)
AOT_thus ‹[[Π]-\κ]κ'› using Π_minus_κI by fast qed
AOT_assume Gv: ‹[G]v›
AOT_assume Fu: ‹[F]u›
AOT_assume ‹[F]-u≈E [G]-v›
AOT_hence ‹∃R R |: [F]-u1-1⟷E [G]-v› using"equi:3"[THEN"≡dfE"] by blast then AOT_obtain R where R_prop: ‹R |: [F]-u1-1⟷E [G]-v› using"∃E"[rotated] by blast
AOT_hence Fact1: ‹∀r([[F]-u]r →∃!s ([[G]-v]s & [R]rs))› and Fact1': ‹∀s([[G]-v]s →∃!r ([[F]-u]r & [R]rs))› using"equi:2"[THEN"≡dfE"] "&E"by blast+
AOT_have ‹R |: [F]-u1-1⟶ontoE [G]-v› using"equi-rem-thm"[unvarify F G, OF Π_minus_κ_den, OF Π_minus_κ_den, THEN"≡E"(1), OF R_prop].
AOT_hence ‹R |: [F]-u1-1⟶E [G]-v & R |: [F]-u⟶ontoE [G]-v› using"equi-rem:4"[THEN"≡dfE"] by blast
AOT_hence Fact2: ‹∀r∀s∀t(([[F]-u]r & [[F]-u]s & [[G]-v]t) → ([R]rt & [R]st → r =E s))› using"equi-rem:2"[THEN"≡dfE"] "&E"by blast
let ?R = ‹«[λxy ([[F]-u]x & [[G]-v]y & [R]xy) ∨ (x =E u & y =E v)]¬›
AOT_have R_den: ‹«?R¬↓›by"cqt:2[lambda]"
AOT_show ‹F ≈E G› proof(safe intro!: "equi:3"[THEN"≡dfI"] "∃I"(1)[where τ="?R"] R_den "equi:2"[THEN"≡dfI"] "&I""cqt:2" Ordinary.GEN "→I") fix r
AOT_assume Fr: ‹[F]r›
{
AOT_assume not_r_eq_u: ‹¬(r =E u)›
AOT_hence r_noteq_u: ‹r ≠E u› using"≡E"(2) "thm-neg=E"by blast
AOT_have ‹[[F]-u]r› by(rule Π_minus_κI; safe intro!: "β←C"(1) "cqt:2""&I" Fr r_noteq_u)
AOT_hence ‹∃!s ([[G]-v]s & [R]rs)› using Fact1[THEN"∀E"(2)] "→E" Ordinary.ψ by blast
AOT_hence ‹∃s ([[G]-v]s & [R]rs & ∀t ([[G]-v]t & [R]rt → t =E s))› using"equi:1"[THEN"≡E"(1)] by simp then AOT_obtain s where s_prop: ‹[[G]-v]s & [R]rs & ∀t ([[G]-v]t & [R]rt >→ t =E s)› using"Ordinary.∃E"[rotated] by meson
AOT_hence G_minus_v_s: ‹[[G]-v]s›and Rrs: ‹[R]rs› using"&E"by blast+
AOT_have s_unique: ‹t =E s›if‹[[G]-v]t›and‹[R]rt›for t using s_prop[THEN"&E"(2), THEN"Ordinary.∀E", THEN"→E", OF "&I", OF that].
AOT_have Gs: ‹[G]s› using Π_minus_κE1[OF G_minus_v_s].
AOT_have s_noteq_v: ‹s ≠E v› using Π_minus_κE2[OF G_minus_v_s].
AOT_have ‹∃s ([G]s & [«?R¬]rs & (∀t ([G]t & [«?R¬]rt → t =E s)))› proof(safe intro!: "Ordinary.∃I"[where β=s] "&I" Gs Ordinary.GEN "→I")
AOT_show ‹[«?R¬]rs› by (auto intro!: "β←C"(1) "cqt:2""&I""∨I"(1) Π_minus_κI' Fr Gs
s_noteq_v Rrs r_noteq_u
simp: "&I""ex:1:a" prod_denotesI "rule-ui:3") next fix t
AOT_assume 0: ‹[G]t & [«?R¬]rt›
AOT_hence ‹([[F]-u]r & [[G]-v]t & [R]rt) ∨ (r =E u & t =E v)› using"β→C"(1)[OF 0[THEN"&E"(2)], simplified] by blast
AOT_hence 1: ‹[[F]-u]r & [[G]-v]t & [R]rt› using not_r_eq_u by (metis "&E"(1) "∨E"(3) "reductio-aa:1")
AOT_show ‹t =E s›using s_unique 1"&E"by blast qed
} moreover {
AOT_assume r_eq_u: ‹r =E u›
AOT_have ‹∃s ([G]s & [«?R¬]rs & (∀t ([G]t & [«?R¬]rt → t =E s)))› proof(safe intro!: "Ordinary.∃I"[where β=v] "&I" Gv Ordinary.GEN "→I")
AOT_show ‹[«?R¬]rv› by (auto intro!: "β←C"(1) "cqt:2""&I""∨I"(2) Π_minus_κI' Fr r_eq_u "ord=Eequiv:1"[THEN"→E"] Ordinary.ψ
simp: "&I""ex:1:a" prod_denotesI "rule-ui:3") next fix t
AOT_assume 0: ‹[G]t & [«?R¬]rt›
AOT_hence ‹([[F]-u]r & [[G]-v]t & [R]rt) ∨ (r =E u & t =E v)› using"β→C"(1)[OF 0[THEN"&E"(2)], simplified] by blast
AOT_hence ‹r =E u & t =E v› using r_eq_u Π_minus_κE2 by (metis "&E"(1) "∨E"(2) "≡E"(1) "reductio-aa:1""thm-neg=E")
AOT_thus ‹t =E v›using"&E"by blast qed
} ultimately AOT_show ‹∃!s ([G]s & [«?R¬]rs)› using"reductio-aa:2""equi:1"[THEN"≡E"(2)] by fast next fix s
AOT_assume Gs: ‹[G]s›
{
AOT_assume not_s_eq_v: ‹¬(s =E v)›
AOT_hence s_noteq_v: ‹s ≠E v› using"≡E"(2) "thm-neg=E"by blast
AOT_have ‹[[G]-v]s› by (rule Π_minus_κI; auto intro!: "β←C"(1) "cqt:2""&I" Gs s_noteq_v)
AOT_hence ‹∃!r ([[F]-u]r & [R]rs)› using Fact1'[THEN"Ordinary.∀E"] "→E"by blast
AOT_hence ‹∃r ([[F]-u]r & [R]rs & ∀t ([[F]-u]t & [R]ts → t =E r))› using"equi:1"[THEN"≡E"(1)] by simp then AOT_obtain r where
r_prop: ‹[[F]-u]r & [R]rs & ∀t ([[F]-u]t & [R]ts → t =E r)› using"Ordinary.∃E"[rotated] by meson
AOT_hence F_minus_u_r: ‹[[F]-u]r›and Rrs: ‹[R]rs› using"&E"by blast+
AOT_have r_unique: ‹t =E r›if‹[[F]-u]t›and‹[R]ts›for t using r_prop[THEN"&E"(2), THEN"Ordinary.∀E", THEN"→E", OF "&I", OF that].
AOT_have Fr: ‹[F]r› using Π_minus_κE1[OF F_minus_u_r].
AOT_have r_noteq_u: ‹r ≠E u› using Π_minus_κE2[OF F_minus_u_r].
AOT_have ‹∃r ([F]r & [«?R¬]rs & (∀t ([F]t & [«?R¬]ts → t =E r)))› proof(safe intro!: "Ordinary.∃I"[where β=r] "&I" Fr Ordinary.GEN "→I")
AOT_show ‹[«?R¬]rs› by (auto intro!: "β←C"(1) "cqt:2""&I""∨I"(1) Π_minus_κI' Fr
Gs s_noteq_v Rrs r_noteq_u
simp: "&I""ex:1:a" prod_denotesI "rule-ui:3") next fix t
AOT_assume 0: ‹[F]t & [«?R¬]ts›
AOT_hence ‹([[F]-u]t & [[G]-v]s & [R]ts) ∨ (t =E u & s =E v)› using"β→C"(1)[OF 0[THEN"&E"(2)], simplified] by blast
AOT_hence 1: ‹[[F]-u]t & [[G]-v]s & [R]ts› using not_s_eq_v by (metis "&E"(2) "∨E"(3) "reductio-aa:1")
AOT_show ‹t =E r›using r_unique 1"&E"by blast qed
} moreover {
AOT_assume s_eq_v: ‹s =E v›
AOT_have ‹∃r ([F]r & [«?R¬]rs & (∀t ([F]t & [«?R¬]ts → t =E r)))› proof(safe intro!: "Ordinary.∃I"[where β=u] "&I" Fu Ordinary.GEN "→I")
AOT_show ‹[«?R¬]us› by (auto intro!: "β←C"(1) "cqt:2""&I" prod_denotesI "∨I"(2)
Π_minus_κI' Gs s_eq_v Ordinary.ψ "ord=Eequiv:1"[THEN"→E"]) next fix t
AOT_assume 0: ‹[F]t & [«?R¬]ts›
AOT_hence 1: ‹([[F]-u]t & [[G]-v]s & [R]ts) ∨ (t =E u & s =E v)› using"β→C"(1)[OF 0[THEN"&E"(2)], simplified] by blast moreover AOT_have ‹¬([[F]-u]t & [[G]-v]s & [R]ts)› proof (rule "raa-cor:2")
AOT_assume ‹([[F]-u]t & [[G]-v]s & [R]ts)›
AOT_hence ‹[[G]-v]s›using"&E"by blast
AOT_thus ‹s =E v & ¬(s =E v)› by (metis Π_minus_κE2 "≡E"(4) "reductio-aa:1" s_eq_v "thm-neg=E") qed ultimately AOT_have ‹t =E u & s =E v› by (metis "∨E"(2))
AOT_thus ‹t =E u›using"&E"by blast qed
} ultimately AOT_show ‹∃!r ([F]r & [«?R¬]rs)› using"≡E"(2) "equi:1""reductio-aa:2"by fast qed qed
AOT_theorem "approx-cont:1": ‹∃F∃G ♢(F ≈E G & ♢¬F ≈E G)› proof - let ?P = ‹«[λx E!x & ¬\AE!x]¬›
AOT_have ‹♢q0 & ♢¬q0›by (metis q0_prop)
AOT_hence 1: ‹♢∃x(E!x & ¬\AE!x) & ♢¬∃x(E!x & ¬\AE!x)› by (rule q0_def[THEN"=dfE"(2), rotated])
(simp add: "log-prop-prop:2")
AOT_have θ: ‹♢∃x [«?P¬]x & ♢¬∃x [«?P¬]x› apply (AOT_subst ‹[«?P¬]x›‹E!x & ¬\AE!x›for: x) apply (rule "beta-C-meta"[THEN"→E"]; "cqt:2[lambda]") by (fact 1) show ?thesis proof (rule "∃I"(1))+
AOT_have ‹♢[L]-≈E [«?P¬] & ♢¬[L]-≈E [«?P¬]› proof (rule "&I"; rule "RM♢"[THEN"→E"]; (rule "→I")?)
AOT_modally_strict {
AOT_assume A: ‹¬∃x [«?P¬]x›
AOT_show ‹[L]-≈E [«?P¬]› proof (safe intro!: "empty-approx:1"[unvarify F H, THEN"→E"] "rel-neg-T:3""&I")
AOT_show ‹[«?P¬]↓›by"cqt:2[lambda]" next
AOT_show ‹¬∃u [L-]u› proof (rule "raa-cor:2")
AOT_assume ‹∃u [L-]u› then AOT_obtain u where ‹[L-]u› using"Ordinary.∃E"[rotated] by blast moreover AOT_have ‹¬[L-]u› using"thm-noncont-e-e:2"[THEN"contingent-properties:2"[THEN"≡dfE"], THEN"&E"(2)] by (metis "qml:2"[axiom_inst] "rule-ui:3""→E") ultimately AOT_show ‹p & ¬p›for p by (metis "raa-cor:3") qed next
AOT_show ‹¬∃v [«?P¬]v› proof (rule "raa-cor:2")
AOT_assume ‹∃v [«?P¬]v› then AOT_obtain u where ‹[«?P¬]u› using"Ordinary.∃E"[rotated] by blast
AOT_hence ‹[«?P¬]u› using"&E"by blast
AOT_hence ‹∃x [«?P¬]x› by (rule "∃I")
AOT_thus ‹∃x [«?P¬]x & ¬∃x [«?P¬]x› using A "&I"by blast qed qed
} next
AOT_show ‹♢¬∃x [«?P¬]x› using θ "&E"by blast next
AOT_modally_strict {
AOT_assume A: ‹∃x [«?P¬]x›
AOT_have B: ‹¬[«?P¬] ≈E [L]-› proof (safe intro!: "empty-approx:2"[unvarify F H, THEN"→E"] "rel-neg-T:3""&I")
AOT_show ‹[«?P¬]↓› by"cqt:2[lambda]" next
AOT_obtain x where Px: ‹[«?P¬]x› using A "∃E"by blast
AOT_hence ‹E!x & ¬\AE!x› by (rule "β→C"(1))
AOT_hence 1: ‹♢E!x› by (metis "T♢""&E"(1) "vdash-properties:10")
AOT_have ‹[λx ♢E!x]x› by (auto intro!: "β←C"(1) "cqt:2"1)
AOT_hence ‹O!x› by (rule AOT_ordinary[THEN"=dfI"(2), rotated]) "cqt:2[lambda]"
AOT_hence ‹O!x & [«?P¬]x› using Px "&I"by blast
AOT_thus ‹∃u [«?P¬]u› by (rule "∃I") next
AOT_show ‹¬∃u [L-]u› proof (rule "raa-cor:2")
AOT_assume ‹∃u [L-]u› then AOT_obtain u where ‹[L-]u› using"Ordinary.∃E"[rotated] by blast moreover AOT_have ‹¬[L-]u› using"thm-noncont-e-e:2"[THEN"contingent-properties:2"[THEN"≡dfE"]] by (metis "qml:2"[axiom_inst] "rule-ui:3""→E""&E"(2)) ultimately AOT_show ‹p & ¬p›for p by (metis "raa-cor:3") qed qed
AOT_show ‹¬[L]-≈E [«?P¬]› proof (rule "raa-cor:2")
AOT_assume ‹[L]-≈E [«?P¬]›
AOT_hence ‹[«?P¬] ≈E [L]-› apply (rule "eq-part:2"[unvarify F G, THEN"→E", rotated 2]) apply"cqt:2[lambda]" by (simp add: "rel-neg-T:3")
AOT_thus ‹[«?P¬] ≈E [L]- & ¬[«?P¬] ≈E [L]-› using B "&I"by blast qed
} next
AOT_show ‹♢∃x [«?P¬]x› using θ "&E"by blast qed
AOT_thus ‹♢([L]-≈E [«?P¬] & ♢¬[L]-≈E [«?P¬])› using"S5Basic:11""≡E"(2) by blast next
AOT_show ‹[λx [E!]x & ¬\A[E!]x]↓› by"cqt:2" next
AOT_show ‹[L]-↓› by (simp add: "rel-neg-T:3") qed qed
AOT_theorem "approx-cont:2": ‹∃F∃G ♢([λz \A[F]z] ≈E G & ♢¬[λz \A[F]z] ≈E G)› proof - let ?P = ‹«[λx E!x & ¬\AE!x]¬›
AOT_have ‹♢q0 & ♢¬q0›by (metis q0_prop)
AOT_hence 1: ‹♢∃x(E!x & ¬\AE!x) & ♢¬∃x(E!x & ¬\AE!x)› by (rule q0_def[THEN"=dfE"(2), rotated])
(simp add: "log-prop-prop:2")
AOT_have θ: ‹♢∃x [«?P¬]x & ♢¬∃x [«?P¬]x› apply (AOT_subst ‹[«?P¬]x›‹E!x & ¬\AE!x›for: x) apply (rule "beta-C-meta"[THEN"→E"]; "cqt:2") by (fact 1) show ?thesis proof (rule "∃I"(1))+
AOT_have ‹♢[λz \A[L-]z] ≈E [«?P¬] & ♢¬[λz \A[L-]z] ≈E [«?P¬]› proof (rule "&I"; rule "RM♢"[THEN"→E"]; (rule "→I")?)
AOT_modally_strict {
AOT_assume A: ‹¬∃x [«?P¬]x›
AOT_show ‹[λz \A[L-]z] ≈E [«?P¬]› proof (safe intro!: "empty-approx:1"[unvarify F H, THEN"→E"] "rel-neg-T:3""&I")
AOT_show ‹[«?P¬]↓›by"cqt:2" next
AOT_show ‹¬∃u [λz \A[L-]z]u› proof (rule "raa-cor:2")
AOT_assume ‹∃u [λz \A[L-]z]u› then AOT_obtain u where ‹[λz \A[L-]z]u› using"Ordinary.∃E"[rotated] by blast
AOT_hence ‹\A[L-]u› using"β→C"(1) "&E"by blast moreover AOT_have ‹◻¬[L-]u› using"thm-noncont-e-e:2"[THEN"contingent-properties:2"[THEN"≡dfE"]] by (metis RN "qml:2"[axiom_inst] "rule-ui:3""→E""&E"(2)) ultimately AOT_show ‹p & ¬p›for p by (metis "Act-Sub:3""KBasic2:1""≡E"(1) "raa-cor:3""→E") qed next
AOT_show ‹¬∃v [«?P¬]v› proof (rule "raa-cor:2")
AOT_assume ‹∃v [«?P¬]v› then AOT_obtain u where ‹[«?P¬]u› using"Ordinary.∃E"[rotated] by blast
AOT_hence ‹[«?P¬]u› using"&E"by blast
AOT_hence ‹∃x [«?P¬]x› by (rule "∃I")
AOT_thus ‹∃x [«?P¬]x & ¬∃x [«?P¬]x› using A "&I"by blast qed next
AOT_show ‹[λz \A[L-]z]↓›by"cqt:2" qed
} next
AOT_show ‹♢¬∃x [«?P¬]x›using θ "&E"by blast next
AOT_modally_strict {
AOT_assume A: ‹∃x [«?P¬]x›
AOT_have B: ‹¬[«?P¬] ≈E [λz \A[L-]z]› proof (safe intro!: "empty-approx:2"[unvarify F H, THEN"→E"] "rel-neg-T:3""&I")
AOT_show ‹[«?P¬]↓›by"cqt:2" next
AOT_obtain x where Px: ‹[«?P¬]x› using A "∃E"by blast
AOT_hence ‹E!x & ¬\AE!x› by (rule "β→C"(1))
AOT_hence ‹♢E!x› by (metis "T♢""&E"(1) "→E")
AOT_hence ‹[λx ♢E!x]x› by (auto intro!: "β←C"(1) "cqt:2")
AOT_hence ‹O!x› by (rule AOT_ordinary[THEN"=dfI"(2), rotated]) "cqt:2"
AOT_hence ‹O!x & [«?P¬]x› using Px "&I"by blast
AOT_thus ‹∃u [«?P¬]u› by (rule "∃I") next
AOT_show ‹¬∃u [λz \A[L-]z]u› proof (rule "raa-cor:2")
AOT_assume ‹∃u [λz \A[L-]z]u› then AOT_obtain u where ‹[λz \A[L-]z]u› using"Ordinary.∃E"[rotated] by blast
AOT_hence ‹\A[L-]u› using"β→C"(1) "&E"by blast moreover AOT_have ‹◻¬[L-]u› using"thm-noncont-e-e:2"[THEN"contingent-properties:2"[THEN"≡dfE"]] by (metis RN "qml:2"[axiom_inst] "rule-ui:3""→E""&E"(2)) ultimately AOT_show ‹p & ¬p›for p by (metis "Act-Sub:3""KBasic2:1""≡E"(1) "raa-cor:3""→E") qed next
AOT_show ‹[λz \A[L-]z]↓›by"cqt:2" qed
AOT_show ‹¬[λz \A[L-]z] ≈E [«?P¬]› proof (rule "raa-cor:2")
AOT_assume ‹[λz \A[L-]z] ≈E [«?P¬]›
AOT_hence ‹[«?P¬] ≈E [λz \A[L-]z]› by (rule "eq-part:2"[unvarify F G, THEN"→E", rotated 2]) "cqt:2"+
AOT_thus ‹[«?P¬] ≈E [λz \A[L-]z] & ¬[«?P¬] ≈E [λz \A[L-]z]› using B "&I"by blast qed
} next
AOT_show ‹♢∃x [«?P¬]x› using θ "&E"by blast qed
AOT_thus ‹♢([λz \A[L-]z] ≈E [«?P¬] & ♢¬[λz \A[L-]z] ≈E [«?P¬])› using"S5Basic:11""≡E"(2) by blast next
AOT_show ‹[λx [E!]x & ¬\A[E!]x]↓›by"cqt:2" next
AOT_show ‹[L]-↓› by (simp add: "rel-neg-T:3") qed qed
notepad begin text‹We already have defined being equivalent on the ordinary objects in the
Extended Relation Comprehension theory.›
AOT_have ‹F ≡E G ≡df F↓ & G↓ & ∀u ([F]u ≡ [G]u)›for F G using eqE by blast end
AOT_theorem "apE-eqE:1": ‹F ≡E G → F ≈E G› proof(rule "→I")
AOT_assume 0: ‹F ≡E G›
AOT_have ‹∃R R |: F 1-1⟷E G› proof (safe intro!: "∃I"(1)[where τ="«(=E)¬"] "equi:2"[THEN"≡dfI"] "&I" "=E[denotes]""cqt:2[const_var]"[axiom_inst] Ordinary.GEN "→I""equi:1"[THEN"≡E"(2)]) fix u
AOT_assume Fu: ‹[F]u›
AOT_hence Gu: ‹[G]u› using"≡dfE"[OF eqE, OF 0, THEN"&E"(2), THEN"Ordinary.∀E"[where α=u], THEN"≡E"(1)]
Ordinary.ψ Fu by blast
AOT_show ‹∃v ([G]v & u =E v & ∀v' ([G]v' & u =E v' → v' =E v))› by (safe intro!: "Ordinary.∃I"[where β=u] "&I" GEN "→I" Ordinary.ψ Gu "ord=Eequiv:1"[THEN"→E", OF Ordinary.ψ] "ord=Eequiv:2"[THEN"→E"] dest!: "&E"(2)) next fix v
AOT_assume Gv: ‹[G]v›
AOT_hence Fv: ‹[F]v› using"≡dfE"[OF eqE, OF 0, THEN"&E"(2), THEN"Ordinary.∀E"[where α=v], THEN"≡E"(2)]
Ordinary.ψ Gv by blast
AOT_show ‹∃u ([F]u & u =E v & ∀v' ([F]v' & v' =E v → v' =E u))› by (safe intro!: "Ordinary.∃I"[where β=v] "&I" GEN "→I" Ordinary.ψ Fv "ord=Eequiv:1"[THEN"→E", OF Ordinary.ψ] "ord=Eequiv:2"[THEN"→E"] dest!: "&E"(2)) qed
AOT_thus ‹F ≈E G› by (rule "equi:3"[THEN"≡dfI"]) qed
AOT_theorem "apE-eqE:2": ‹(F ≈E G & G ≡E H) → F ≈E H› proof(rule "→I")
AOT_assume ‹F ≈E G & G ≡E H›
AOT_hence ‹F ≈E G›and‹G ≈E H› using"apE-eqE:1"[THEN"→E"] "&E"by blast+
AOT_thus ‹F ≈E H› by (metis Adjunction "eq-part:3""vdash-properties:10") qed
AOT_act_theorem "eq-part-act:1": ‹[λz \A[F]z] ≡E F› proof (safe intro!: eqE[THEN"≡dfI"] "&I""cqt:2" Ordinary.GEN "→I") fix u
AOT_have ‹[λz \A[F]z]u ≡\A[F]u› by (rule "beta-C-meta"[THEN"→E"]) "cqt:2[lambda]" also AOT_have ‹…≡ [F]u› using"act-conj-act:4""logic-actual"[act_axiom_inst, THEN"→E"] by blast finally AOT_show ‹[λz \A[F]z]u ≡ [F]u›. qed
AOT_theorem "num-can:1": ‹#G = \ιx(A!x & ∀F (x[F] ≡ [λz \A[F]z] ≈E G))› proof -
AOT_have ‹◻∀x(Numbers(x,G) ≡ [A!]x & ∀F (x[F] ≡ [λz \A[F]z] ≈E G))› by (safe intro!: RN GEN "numbers[den]"[THEN"→E"] "cqt:2")
AOT_hence ‹\ιx Numbers(x, G) = \ιx([A!]x & ∀F (x[F] ≡ [λz \A[F]z] ≈E G))› using"num-uniq""equiv-desc-eq:3"[THEN"→E", OF "&I"] by auto thus ?thesis by (rule "=dfI"(1)[OF "num-def:1", OF "num-uniq"]) qed
AOT_theorem "num-can:2": ‹#G = \ιx(A!x & ∀F (x[F] ≡ F ≈E G))› proof (rule id_trans[OF "num-can:1"]; rule "equiv-desc-eq:2"[THEN"→E"];
safe intro!: "&I""A-descriptions" GEN "Act-Basic:5"[THEN"≡E"(2)] "logic-actual-nec:3"[axiom_inst, THEN"≡E"(2)])
AOT_have act_den: ‹\⊨\◻ [λz \A[F]z]↓›for F by"cqt:2"
AOT_have "eq-part:3[terms]": ‹\⊨\◻ F ≈E G & F ≈E H → G ≈E H›for F G H by (metis "&I""eq-part:2""eq-part:3""→I""&E""→E") fix x
{ fix F
AOT_have ‹\A(F ≈E [λz \A[F]z])› by (simp add: "actuallyF:1") moreover AOT_have ‹\A((F ≈E [λz \A[F]z]) → ([λz \A[F]z] ≈E G ≡ F ≈E G))› by (auto intro!: "RA[2]""→I""≡I"
simp: "eq-part:3"[unvarify G, OF act_den, THEN"→E", OF "&I"] "eq-part:3[terms]"[unvarify G, OF act_den, THEN"→E", OF "&I"]) ultimately AOT_have ‹\A([λz \A[F]z] ≈E G ≡ F ≈E G)› using"logic-actual-nec:2"[axiom_inst, THEN"≡E"(1), THEN"→E"] by blast
AOT_hence ‹\A[λz \A[F]z] ≈E G ≡\AF ≈E G› by (metis "Act-Basic:5""≡E"(1))
AOT_hence 0: ‹(\Ax[F] ≡\A[λz \A[F]z] ≈E G) ≡ (\Ax[F] ≡\AF ≈E G)› by (auto intro!: "≡I""→I" elim: "≡E")
AOT_have ‹\A(x[F] ≡ [λz \A[F]z] ≈E G) ≡ (\Ax[F] ≡\A[λz \A[F]z] ≈E G)› by (simp add: "Act-Basic:5") also AOT_have ‹…≡ (\Ax[F] ≡\AF ≈E G)›using0. also AOT_have ‹…≡\A((x[F] ≡ F ≈E G))› by (meson "Act-Basic:5""≡E"(6) "oth-class-taut:3:a") finally AOT_have 0: ‹\A(x[F] ≡ [λz \A[F]z] ≈E G) ≡\A((x[F] ≡ F ≈E G))›.
} note0 = this
AOT_have ‹\A∀F (x[F] ≡ [λz \A[F]z] ≈E G) ≡∀F \A(x[F] ≡ [λz \A[F]z] ≈E G)› using"logic-actual-nec:3""vdash-properties:1[2]"by blast also AOT_have ‹…≡∀F \A((x[F] ≡ F ≈E G))› apply (safe intro!: "≡I""→I" GEN) using0"≡E"(1) "≡E"(2) "rule-ui:3"by blast+ also AOT_have ‹…≡\A(∀F (x[F] ≡ F ≈E G))› using"≡E"(6) "logic-actual-nec:3"[axiom_inst] "oth-class-taut:3:a"by fast finally AOT_have 0: ‹\A∀F (x[F] ≡ [λz \A[F]z] ≈E G) ≡\A(∀F (x[F] ≡ F ≈E G))›.
AOT_have ‹\A([A!]x & ∀F (x[F] ≡ [λz \A[F]z] ≈E G)) ≡
(\AA!x & \A∀F (x[F] ≡ [λz \A[F]z] ≈E G))› by (simp add: "Act-Basic:2") also AOT_have ‹…≡\A[A!]x & \A(∀F (x[F] ≡ F ≈E G))› using0"oth-class-taut:4:f""→E"by blast also AOT_have ‹…≡\A(A!x & ∀F (x[F] ≡ F ≈E G))› using"Act-Basic:2""≡E"(6) "oth-class-taut:3:a"by blast finally AOT_show ‹\A([A!]x & ∀F (x[F] ≡ [λz \A[F]z] ≈EG)) ≡ \A([A!]x & ∀F (x[F] ≡ F ≈E G))›. qed
AOT_theorem "eq-num:1": ‹\ANumbers(x, G) ≡ Numbers(x,[λz \A[G]z])› proof -
AOT_have act_den: ‹\⊨\◻ [λz \A[F]z]↓›for F by"cqt:2"
AOT_have ‹◻(∃x(Numbers(x, G) & Numbers(x,[λz \A[G]z])) ≡ G ≈E [λz \A[G]z])› using"hume-strict:1"[unvarify G, OF act_den, THEN RN].
AOT_hence ‹\A(∃x(Numbers(x, G) & Numbers(x,[λz \A[G]z])) ≡ G ≈E [λz \A[G]z])› using"nec-imp-act"[THEN"→E"] by fast
AOT_hence ‹\A(∃x(Numbers(x, G) & Numbers(x,[λz \A[G]z])))› using"actuallyF:1""Act-Basic:5""≡E"(1) "≡E"(2) by fast
AOT_hence ‹∃x \A((Numbers(x, G) & Numbers(x,[λz \A[G]z])))› by (metis "Act-Basic:10""intro-elim:3:a") then AOT_obtain a where ‹\A(Numbers(a, G) & Numbers(a,[λz \A[G]z]))› using"∃E"[rotated] by blast
AOT_hence act_a_num_G: ‹\ANumbers(a, G)› and act_a_num_actG: ‹\ANumbers(a,[λz \A[G]z])› using"Act-Basic:2""&E""≡E"(1) by blast+
AOT_hence num_a_act_g: ‹Numbers(a, [λz \A[G]z])› using"num-cont:2"[unvarify G, OF act_den, THEN"→E", OF "actuallyF:2", THEN CBF[THEN"→E"], THEN"∀E"(2)] by (metis "≡E"(1) "sc-eq-fur:2""vdash-properties:6")
AOT_have 0: ‹\⊨\◻ Numbers(x, G) & Numbers(y, G) → x = y›for y using"pre-Hume"[THEN"→E", THEN"≡E"(2), rotated, OF "eq-part:1"] "→I"by blast show ?thesis proof(safe intro!: "≡I""→I")
AOT_assume ‹\ANumbers(x, G)›
AOT_hence ‹\Ax = a› using0[THEN"RA[2]", THEN"act-cond"[THEN"→E"], THEN"→E",
OF "Act-Basic:2"[THEN"≡E"(2)], OF "&I"]
act_a_num_G by blast
AOT_hence ‹x = a›by (metis "id-act:1""≡E"(2))
AOT_hence ‹a = x›using id_sym by auto
AOT_thus ‹Numbers(x, [λz \A[G]z])› using"rule=E" num_a_act_g by fast next
AOT_assume ‹Numbers(x, [λz \A[G]z])›
AOT_hence ‹a = x› using"pre-Hume"[unvarify G H, THEN"→E", OF act_den, OF act_den, OF "&I",
OF num_a_act_g, THEN"≡E"(2)] "eq-part:1"[unvarify F, OF act_den] by blast
AOT_thus ‹\ANumbers(x, G)› using act_a_num_G "rule=E"by fast qed qed
AOT_theorem "eq-num:2": ‹Numbers(x,[λz \A[G]z]) ≡ x = #G› proof -
AOT_have 0: ‹\⊨\◻ x = \ιx Numbers(x, G) ≡∀y (Numbers(y, [λz \A[G]z]) ≡ y = x)›for x by (AOT_subst (reverse) ‹Numbers(x, [λz \A[G]z])›‹\ANumbers(x, G)›for: x)
(auto simp: "eq-num:1" descriptions[axiom_inst])
AOT_have ‹#G = \ιx Numbers(x, G) ≡∀y (Numbers(y, [λz \A[G]z]) ≡ y = #G)› using0[unvarify x, OF "num-def:2"]. moreover AOT_have ‹#G = \ιx Numbers(x, G)› using"num-def:1""num-uniq""rule-id-df:1"by blast ultimately AOT_have ‹∀y (Numbers(y, [λz \A[G]z]) ≡ y = #G)› using"≡E"by blast thus ?thesis using"∀E"(2) by blast qed
AOT_theorem "eq-num:3": ‹Numbers(#G, [λy \A[G]y])› proof -
AOT_have ‹#G = #G› by (simp add: "rule=I:1""num-def:2") thus ?thesis using"eq-num:2"[unvarify x, OF "num-def:2", THEN"≡E"(2)] by blast qed
AOT_theorem "eq-num:6": ‹Numbers(x, G) → NaturalCardinal(x)› proof(rule "→I")
AOT_have act_den: ‹\⊨\◻ [λz \A[F]z]↓›for F by"cqt:2"
AOT_obtain F where ‹Rigidifies(F, G)› by (metis "instantiation""rigid-der:3")
AOT_hence θ: ‹Rigid(F)›and‹∀x([F]x ≡ [G]x)› using"df-rigid-rel:2"[THEN"≡dfE", THEN"&E"(2)] "df-rigid-rel:2"[THEN"≡dfE", THEN"&E"(1)] by blast+
AOT_hence ‹F ≡E G› by (auto intro!: eqE[THEN"≡dfI"] "&I""cqt:2" GEN "→I" elim: "∀E"(2)) moreover AOT_assume ‹Numbers(x, G)› ultimately AOT_have ‹Numbers(x, F)› using"num-tran:3"[THEN"→E", THEN"≡E"(2)] by blast moreover AOT_have ‹F ≈E [λz \A[F]z]› using θ "approx-nec:1""→E"by blast ultimately AOT_have ‹Numbers(x, [λz \A[F]z])› using"num-tran:1"[unvarify H, OF act_den, THEN"→E", THEN"≡E"(1)] by blast
AOT_hence ‹x = #F› using"eq-num:2"[THEN"≡E"(1)] by blast
AOT_hence ‹∃F x = #F› by (rule "∃I")
AOT_thus ‹NaturalCardinal(x)› using card[THEN"≡dfI"] by blast qed
AOT_theorem "eq-df-num": ‹∃G (x = #G) ≡∃G (Numbers(x,G))› proof(safe intro!: "≡I""→I")
AOT_assume ‹∃G (x = #G)› then AOT_obtain P where ‹x = #P› using"∃E"[rotated] by blast
AOT_hence ‹Numbers(x,[λz \A[P]z])› using"eq-num:2"[THEN"≡E"(2)] by blast moreover AOT_have ‹[λz \A[P]z]↓›by"cqt:2" ultimately AOT_show ‹∃G(Numbers(x,G))›by (rule "∃I") next
AOT_assume ‹∃G (Numbers(x,G))› then AOT_obtain Q where ‹Numbers(x,Q)› using"∃E"[rotated] by blast
AOT_hence ‹NaturalCardinal(x)› using"eq-num:6"[THEN"→E"] by blast
AOT_thus ‹∃G (x = #G)› using card[THEN"≡dfE"] by blast qed
AOT_theorem "card-en": ‹NaturalCardinal(x) →∀F(x[F] ≡ x = #F)› proof(rule "→I"; rule GEN)
AOT_have act_den: ‹\⊨\◻ [λz \A[F]z]↓›for F by"cqt:2" fix F
AOT_assume ‹NaturalCardinal(x)›
AOT_hence ‹∃F x = #F› using card[THEN"≡dfE"] by blast then AOT_obtain P where x_def: ‹x = #P› using"∃E"[rotated] by blast
AOT_hence num_x_act_P: ‹Numbers(x,[λz \A[P]z])› using"eq-num:2"[THEN"≡E"(2)] by blast
AOT_have ‹#P[F] ≡ [λz \A[F]z] ≈E [λz \A[P]z]› using"eq-num:4"[THEN"&E"(2), THEN"∀E"(2)] by blast
AOT_hence ‹x[F] ≡ [λz \A[F]z] ≈E [λz \A[P]z]› using x_def[symmetric] "rule=E"by fast also AOT_have ‹…≡ Numbers(x, [λz \A[F]z])› using"num-tran:1"[unvarify G H, OF act_den, OF act_den] using"num-tran:2"[unvarify G H, OF act_den, OF act_den] by (metis "&I""deduction-theorem""≡I""≡E"(2) num_x_act_P) also AOT_have ‹…≡ x = #F› using"eq-num:2"by blast finally AOT_show ‹x[F] ≡ x = #F›. qed
AOT_theorem "0F:1": ‹¬∃u [F]u ≡ Numbers(0, F)› proof -
AOT_have unotEu_act_ord: ‹¬∃v[λx O!x & \Ax ≠E x]v› proof(rule "raa-cor:2")
AOT_assume ‹∃v[λx O!x & \Ax ≠E x]v› then AOT_obtain y where ‹[λx O!x & \Ax ≠E x]y› using"∃E"[rotated] "&E"by blast
AOT_hence 0: ‹O!y & \Ay ≠E y› by (rule "β→C"(1))
AOT_have ‹\A¬(y =E y)› apply (AOT_subst ‹¬(y =E y)›‹y ≠E y›) apply (meson "≡E"(2) "Commutativity of ≡""thm-neg=E") by (fact 0[THEN"&E"(2)])
AOT_hence ‹¬(y =E y)› by (metis "¬¬I""Act-Sub:1""id-act2:1""≡E"(4)) moreover AOT_have ‹y =E y› by (metis 0[THEN"&E"(1)] "ord=Eequiv:1""→E") ultimately AOT_show ‹p & ¬p›for p by (metis "raa-cor:3") qed
AOT_have ‹Numbers(0, [λy \A[λx O!x & x ≠E x]y])› apply (rule "=dfI"(2)[OF "zero:1"]) apply (rule "num-def:2"[unvarify G]; "cqt:2") apply (rule "eq-num:3"[unvarify G]) by"cqt:2[lambda]"
AOT_hence numbers0: ‹Numbers(0, [λx [O!]x & \Ax ≠E x])› proof (rule "num-tran:3"[unvarify x G H, THEN"→E", THEN"≡E"(1), rotated 4])
AOT_show ‹[λy \A[λx O!x & x ≠E x]y] ≡E [λx [O!]x & \Ax ≠Ex]› proof (safe intro!: eqE[THEN"≡dfI"] "&I" Ordinary.GEN "→I""cqt:2") fix u
AOT_have ‹[λy \A[λx O!x & x ≠E x]y]u ≡\A[λx O!x & x e='font-size: 18px;'>≠E x]u› by (rule "beta-C-meta"[THEN"→E"]; "cqt:2[lambda]") also AOT_have ‹…≡\A(O!u & u ≠E u)› apply (AOT_subst ‹[λx O!x & x ≠E x]u›‹O!u & u ≠E u›) apply (rule "beta-C-meta"[THEN"→E"]; "cqt:2[lambda]") by (simp add: "oth-class-taut:3:a") also AOT_have ‹…≡ (\AO!u & \Au ≠E u)› by (simp add: "Act-Basic:2") also AOT_have ‹…≡ (O!u & \Au ≠E u)› by (metis Ordinary.ψ "&I""&E"(2) "→I""≡I""≡E"(1) "oa-facts:7") also AOT_have ‹…≡ [λx [O!]x & \Ax ≠E x]u› by (rule "beta-C-meta"[THEN"→E", symmetric]; "cqt:2[lambda]") finally AOT_show ‹[λy \A[λx O!x & x ≠E x]y]u ≡ [λx [O!]x & \Ax ≠E x]u›. qed qed(fact "zero:2" | "cqt:2")+ show ?thesis proof(safe intro!: "≡I""→I")
AOT_assume ‹¬∃u [F]u› moreover AOT_have ‹¬∃v [λx [O!]x & \Ax ≠E x]v› using unotEu_act_ord. ultimately AOT_have 0: ‹F ≈E [λx [O!]x & \Ax ≠E x]› by (rule "empty-approx:1"[unvarify H, THEN"→E", rotated, OF "&I"]) "cqt:2"
AOT_thus ‹Numbers(0, F)› by (rule "num-tran:1"[unvarify x H, THEN"→E", THEN"≡E"(2), rotated, rotated])
(fact "zero:2" numbers0 | "cqt:2[lambda]")+ next
AOT_assume ‹Numbers(0, F)›
AOT_hence 1: ‹F ≈E [λx [O!]x & \Ax ≠E x]› by (rule "num-tran:2"[unvarify x H, THEN"→E", rotated 2, OF "&I"])
(fact numbers0 "zero:2" | "cqt:2[lambda]")+
AOT_show ‹¬∃u [F]u› proof(rule "raa-cor:2")
AOT_have 0: ‹[λx [O!]x & \Ax ≠E x]↓›by"cqt:2[lambda]"
AOT_assume ‹∃u [F]u›
AOT_hence ‹¬(F ≈E [λx [O!]x & \Ax ≠E x])› by (rule "empty-approx:2"[unvarify H, OF 0, THEN"→E", OF "&I"])
(rule unotEu_act_ord)
AOT_thus ‹F ≈E [λx [O!]x & \Ax ≠E x] & ¬(F ≈E [λx [O!]x & \Ax ≠E x])› using1"&I"by blast qed qed qed
AOT_theorem "0F:2": ‹¬∃u \A[F]u ≡ #F = 0› proof(rule "≡I"; rule "→I")
AOT_assume 0: ‹¬∃u \A[F]u›
AOT_have ‹¬∃u [λz \A[F]z]u› proof(rule "raa-cor:2")
AOT_assume ‹∃u [λz \A[F]z]u› then AOT_obtain u where ‹[λz \A[F]z]u› using"Ordinary.∃E"[rotated] by blast
AOT_hence ‹\A[F]u› by (metis "betaC:1:a")
AOT_hence ‹∃u \A[F]u› by (rule "Ordinary.∃I")
AOT_thus ‹∃u \A[F]u & ¬∃u \A[F]u› using0"&I"by blast qed
AOT_hence ‹Numbers(0,[λz \A[F]z])› by (safe intro!: "0F:1"[unvarify F, THEN"≡E"(1)]) "cqt:2"
AOT_hence ‹0 = #F› by (rule "eq-num:2"[unvarify x, OF "zero:2", THEN"≡E"(1)])
AOT_thus ‹#F = 0›using id_sym by blast next
AOT_assume ‹#F = 0›
AOT_hence ‹0 = #F›using id_sym by blast
AOT_hence ‹Numbers(0,[λz \A[F]z])› by (rule "eq-num:2"[unvarify x, OF "zero:2", THEN"≡E"(2)])
AOT_hence 0: ‹¬∃u [λz \A[F]z]u› by (safe intro!: "0F:1"[unvarify F, THEN"≡E"(2)]) "cqt:2"
AOT_show ‹¬∃u \A[F]u› proof(rule "raa-cor:2")
AOT_assume ‹∃u \A[F]u› then AOT_obtain u where ‹\A[F]u› using"Ordinary.∃E"[rotated] by meson
AOT_hence ‹[λz \A[F]z]u› by (auto intro!: "β←C""cqt:2")
AOT_hence ‹∃u [λz \A[F]z]u› using"Ordinary.∃I"by blast
AOT_thus ‹∃u [λz \A[F]z]u & ¬∃u [λz \A[F]z]u› using"&I"0by blast qed qed
AOT_theorem "0F:3": ‹◻¬∃u [F]u → #F = 0› proof(rule "→I")
AOT_assume ‹◻¬∃u [F]u›
AOT_hence 0: ‹¬♢∃u [F]u› using"KBasic2:1""≡E"(1) by blast
AOT_have ‹¬∃u [λz \A[F]z]u› proof(rule "raa-cor:2")
AOT_assume ‹∃u [λz \A[F]z]u› then AOT_obtain u where ‹[λz \A[F]z]u› using"Ordinary.∃E"[rotated] by blast
AOT_hence ‹\A[F]u› by (metis "betaC:1:a")
AOT_hence ‹♢[F]u› by (metis "Act-Sub:3""→E")
AOT_hence ‹∃u ♢[F]u› by (rule "Ordinary.∃I")
AOT_hence ‹♢∃u [F]u› using"Ordinary.res-var-bound-reas[CBF♢]"[THEN"→E"] by blast
AOT_thus ‹♢∃u [F]u & ¬♢∃u [F]u› using0"&I"by blast qed
AOT_hence ‹Numbers(0,[λz \A[F]z])› by (safe intro!: "0F:1"[unvarify F, THEN"≡E"(1)]) "cqt:2"
AOT_hence ‹0 = #F› by (rule "eq-num:2"[unvarify x, OF "zero:2", THEN"≡E"(1)])
AOT_thus ‹#F = 0›using id_sym by blast qed
AOT_theorem "0F:4": ‹w ⊨¬∃u [F]u ≡ #[F]w = 0› proof (rule "rule-id-df:2:b"[OF "w-index", where τ1τn="(_,_)", simplified])
AOT_show ‹[λx1...xn w ⊨ [F]x1...xn]↓› by (simp add: "w-rel:3") next
AOT_show ‹w ⊨¬∃u [F]u ≡ #[λx w ⊨ [F]x] = 0› proof (rule "≡I"; rule "→I")
AOT_assume ‹w ⊨¬∃u [F]u›
AOT_hence 0: ‹¬w ⊨∃u [F]u› using"coherent:1"[unvarify p, OF "log-prop-prop:2", THEN"≡E"(1)] by blast
AOT_have ‹¬∃u \A[λx w ⊨ [F]x]u› proof(rule "raa-cor:2")
AOT_assume ‹∃u \A[λx w ⊨ [F]x]u› then AOT_obtain u where ‹\A[λx w ⊨ [F]x]u› using"Ordinary.∃E"[rotated] by meson
AOT_hence ‹\Aw ⊨ [F]u› by (AOT_subst (reverse) ‹w ⊨ [F]u›‹[λx w ⊨ [F]x]u›;
safe intro!: "beta-C-meta"[THEN"→E"] "w-rel:1"[THEN"→E"]) "cqt:2"
AOT_hence 1: ‹w ⊨ [F]u› using"rigid-truth-at:4"[unvarify p, OF "log-prop-prop:2", THEN"≡E"(1)] by blast
AOT_have ‹◻([F]u →∃u [F]u)› using"Ordinary.∃I""→I" RN by simp
AOT_hence ‹w ⊨ ([F]u →∃u [F]u)› using"fund:2"[unvarify p, OF "log-prop-prop:2", THEN"≡E"(1)] "PossibleWorld.∀E"by fast
AOT_hence ‹w ⊨∃u [F]u› using1"conj-dist-w:2"[unvarify p q, OF "log-prop-prop:2",
OF "log-prop-prop:2", THEN"≡E"(1), THEN"→E"] by blast
AOT_thus ‹w ⊨∃u [F]u & ¬w ⊨∃u [F]u› using0"&I"by blast qed
AOT_thus ‹#[λx w ⊨ [F]x] = 0› by (safe intro!: "0F:2"[unvarify F, THEN"≡E"(1)] "w-rel:1"[THEN"→E"]) "cqt:2" next
AOT_assume ‹#[λx w ⊨ [F]x] = 0›
AOT_hence 0: ‹¬∃u \A[λx w ⊨ [F]x]u› by (safe intro!: "0F:2"[unvarify F, THEN"≡E"(2)] "w-rel:1"[THEN"→E"]) "cqt:2"
AOT_have ‹¬w ⊨∃u [F]u› proof (rule "raa-cor:2")
AOT_assume ‹w ⊨∃u [F]u›
AOT_hence ‹∃x w ⊨ (O!x & [F]x)› using"conj-dist-w:6"[THEN"≡E"(1)] by fast then AOT_obtain x where ‹w ⊨ (O!x & [F]x)› using"∃E"[rotated] by blast
AOT_hence ‹w ⊨ O!x›and Fx_in_w: ‹w ⊨ [F]x› using"conj-dist-w:1"[unvarify p q] "≡E"(1) "log-prop-prop:2" "&E"by blast+
AOT_hence ‹♢O!x› using"fund:1"[unvarify p, OF "log-prop-prop:2", THEN"≡E"(2)] "PossibleWorld.∃I"by simp
AOT_hence ord_x: ‹O!x› using"oa-facts:3"[THEN"→E"] by blast
AOT_have ‹\Aw ⊨ [F]x› using"rigid-truth-at:4"[unvarify p, OF "log-prop-prop:2", THEN"≡E"(2)]
Fx_in_w by blast
AOT_hence ‹\A[λx w ⊨ [F]x]x› by (AOT_subst ‹[λx w ⊨ [F]x]x›‹w ⊨ [F]x›;
safe intro!: "beta-C-meta"[THEN"→E"] "w-rel:1"[THEN"→E"]) "cqt:2"
AOT_hence ‹O!x & \A[λx w ⊨ [F]x]x› using ord_x "&I"by blast
AOT_hence ‹∃x (O!x & \A[λx w ⊨ [F]x]x)› using"∃I"by fast
AOT_thus ‹∃u (\A[λx w ⊨ [F]x]u) & ¬∃u \A[λx w ⊨ [F]x]u› using0"&I"by blast qed
AOT_thus ‹w ⊨¬∃u[F]u› using"coherent:1"[unvarify p, OF "log-prop-prop:2", THEN"≡E"(2)] by blast qed qed
AOT_act_theorem "zero=:1": ‹NaturalCardinal(x) →∀F (x[F] ≡ Numbers(x, F))› proof(safe intro!: "→I" GEN) fix F
AOT_assume ‹NaturalCardinal(x)›
AOT_hence ‹∀F (x[F] ≡ x = #F)› by (metis "card-en""→E")
AOT_hence 1: ‹x[F] ≡ x = #F› using"∀E"(2) by blast
AOT_have 2: ‹x[F] ≡ x = \ιy(Numbers(y, F))› by (rule "num-def:1"[THEN"=dfE"(1)])
(auto simp: 1"num-uniq")
AOT_have ‹x = \ιy(Numbers(y, F)) → Numbers(x, F)› using"y-in:1"by blast moreover AOT_have ‹Numbers(x, F) → x = \ιy(Numbers(y, F))› proof(rule "→I")
AOT_assume 1: ‹Numbers(x, F)› moreover AOT_obtain z where z_prop: ‹∀y (Numbers(y, F) → y = z)› using"num:2"[THEN"uniqueness:1"[THEN"≡dfE"]] "∃E"[rotated] "&E"by blast ultimately AOT_have ‹x = z› using"∀E"(2) "→E"by blast
AOT_hence ‹∀y (Numbers(y, F) → y = x)› using z_prop "rule=E" id_sym by fast
AOT_thus ‹x = \ιy(Numbers(y,F))› by (rule hintikka[THEN"≡E"(2), OF "&I", rotated])
(fact 1) qed ultimately AOT_have ‹x = \ιy(Numbers(y, F)) ≡ Numbers(x, F)› by (metis "≡I")
AOT_thus ‹x[F] ≡ Numbers(x, F)› using2by (metis "≡E"(5)) qed
AOT_act_theorem "zero=:2": ‹0[F] ≡¬∃u[F]u› proof -
AOT_have ‹0[F] ≡ Numbers(0, F)› using"zero=:1"[unvarify x, OF "zero:2", THEN"→E",
OF "zero-card", THEN"∀E"(2)]. also AOT_have ‹…≡¬∃u[F]u› using"0F:1"[symmetric]. finallyshow ?thesis. qed
AOT_act_theorem "zero=:3": ‹¬∃u[F]u ≡ #F = 0› proof -
AOT_have ‹¬∃u[F]u ≡ 0[F]›using"zero=:2"[symmetric]. also AOT_have ‹…≡ 0 = #F› using"card-en"[unvarify x, OF "zero:2", THEN"→E",
OF "zero-card", THEN"∀E"(2)]. also AOT_have ‹…≡ #F = 0› by (simp add: "deduction-theorem" id_sym "≡I") finallyshow ?thesis. qed
AOT_theorem "df-1-1:3": ‹Rigid1-1(R) →◻1-1(R)› proof(rule "→I")
AOT_assume ‹Rigid1-1(R)›
AOT_hence ‹1-1(R)›and RigidR: ‹Rigid(R)› using"df-1-1:2"[THEN"≡dfE"] "&E"by blast+
AOT_hence 1: ‹[R]xz & [R]yz → x = y›for x y z using"df-1-1:1"[THEN"≡dfE"] "&E"(2) "∀E"(2) by blast
AOT_have 1: ‹[R]xz & [R]yz →◻x = y›for x y z by (AOT_subst (reverse) ‹◻x = y›‹x = y›)
(auto simp: 1"id-nec:2""≡I""qml:2"[axiom_inst])
AOT_have ‹◻∀x1...∀xn ([R]x1...xn→◻[R]x1...xn)› using"df-rigid-rel:1"[THEN"≡dfE", OF RigidR] "&E"by blast
AOT_hence ‹∀x1...∀xn◻([R]x1...xn→◻[R]x1...xn)› using"CBF"[THEN"→E"] by fast
AOT_hence ‹∀x1∀x2◻([R]x1x2→◻[R]x1x2)› using tuple_forall[THEN"≡dfE"] by blast
AOT_hence ‹◻([R]xy →◻[R]xy)›for x y using"∀E"(2) by blast
AOT_hence ‹◻(([R]xz →◻[R]xz) & ([R]yz →◻[R]yz))›for x y z by (metis "KBasic:3""&I""≡E"(3) "raa-cor:3") moreover AOT_have ‹◻(([R]xz →◻[R]xz) & ([R]yz →◻[R]yz)) → ◻(([R]xz & [R]yz) →◻([R]xz & [R]yz))›for x y z by (rule RM) (metis "→I""KBasic:3""&I""&E"(1) "&E"(2) "≡E"(2) "→E") ultimately AOT_have 2: ‹◻(([R]xz & [R]yz) →◻([R]xz & [R]yz))›forx y z using"→E"by blast
AOT_hence 3: ‹◻([R]xz & [R]yz → x = y)›for x y z using"sc-eq-box-box:6"[THEN"→E", THEN"→E", OF 2, OF 1] by blast
AOT_hence 4: ‹◻∀x∀y∀z([R]xz & [R]yz → x = y)› by (safe intro!: GEN BF[THEN"→E"] 3)
AOT_thus ‹◻1-1(R)› by (AOT_subst_thm "df-1-1:1"[THEN"≡Df", THEN"≡S"(1),
OF "cqt:2[const_var]"[axiom_inst]]) qed
AOT_theorem "df-1-1:4": ‹∀R(Rigid1-1(R) →◻Rigid1-1(R))› proof(rule GEN;rule "→I")
AOT_modally_strict { fix R
AOT_assume 0: ‹Rigid1-1(R)›
AOT_hence 1: ‹R↓› by (meson "≡dfE""&E"(1) "df-1-1:1""df-1-1:2")
AOT_hence 2: ‹◻R↓› using"exist-nec""→E"by blast
AOT_have 4: ‹◻1-1(R)› using"df-1-1:3"[unvarify R, OF 1, THEN"→E", OF 0].
AOT_have ‹Rigid(R)› using0"≡dfE"[OF "df-1-1:2"] "&E"by blast
AOT_hence ‹◻∀x1...∀xn ([R]x1...xn→◻[R]x1...xn)› using"df-rigid-rel:1"[THEN"≡dfE"] "&E"by blast
AOT_hence ‹◻◻∀x1...∀xn ([R]x1...xn→◻[R]x1...xn)› by (metis "S5Basic:6""≡E"(1))
AOT_hence ‹◻Rigid(R)› apply (AOT_subst_def "df-rigid-rel:1") using2"KBasic:3""≡S"(2) "≡E"(2) by blast
AOT_thus ‹◻Rigid1-1(R)› apply (AOT_subst_def "df-1-1:2") using4"KBasic:3""≡S"(2) "≡E"(2) by blast
} qed
AOT_theorem "id-R-thm:1": ‹x =\R y ≡∃z ([R]xz & [R]yz)› proof -
AOT_have 0: ‹[λxy ∃z ([R]xz & [R]yz)]↓›by"cqt:2" show ?thesis apply (rule "=dfI"(1)[OF "id-d-R"]) apply (fact 0) apply (rule "beta-C-meta"[THEN"→E", OF 0, unvarify ν1νn,
where τ=‹(_,_)›, simplified]) by (simp add: "&I""ex:1:a" prod_denotesI "rule-ui:3") qed
AOT_theorem "id-R-thm:2": ‹x =\R y → (InDomainOf(x, R) & InDomainOf(y, R))› proof(rule "→I")
AOT_assume ‹x =\R y›
AOT_hence ‹∃z ([R]xz & [R]yz)› using"id-R-thm:1"[THEN"≡E"(1)] by simp then AOT_obtain z where z_prop: ‹[R]xz & [R]yz› using"∃E"[rotated] by blast
AOT_show ‹InDomainOf(x, R) & InDomainOf(y, R)› proof (safe intro!: "&I""df-1-1:5"[THEN"≡dfI"])
AOT_show ‹∃y [R]xy› using z_prop[THEN"&E"(1)] "∃I"by fast next
AOT_show ‹∃z [R]yz› using z_prop[THEN"&E"(2)] "∃I"by fast qed qed
AOT_theorem "id-R-thm:3": ‹x =\R y → x = y› proof(rule "→I")
AOT_assume ‹x =\R y›
AOT_hence ‹∃z ([R]xz & [R]yz)› using"id-R-thm:1"[THEN"≡E"(1)] by simp then AOT_obtain z where z_prop: ‹[R]xz & [R]yz› using"∃E"[rotated] by blast
AOT_thus ‹x = y› using"df-1-1:3"[THEN"→E", OF RigidOneToOneRelation.ψ, THEN"qml:2"[axiom_inst, THEN"→E"], THEN"≡dfE"[OF "df-1-1:1"], THEN"&E"(2), THEN"∀E"(2), THEN"∀E"(2), THEN"∀E"(2), THEN"→E"] by blast qed
AOT_theorem "id-R-thm:4": ‹(InDomainOf(x, R) ∨ InDomainOf(y, R)) → (x =\R y ≡ x = y)› proof (rule "→I")
AOT_assume ‹InDomainOf(x, R) ∨ InDomainOf(y, R)› moreover {
AOT_assume ‹InDomainOf(x, R)›
AOT_hence ‹∃z [R]xz› by (metis "≡dfE""df-1-1:5") then AOT_obtain z where z_prop: ‹[R]xz› using"∃E"[rotated] by blast
AOT_have ‹x =\R y ≡ x = y› proof(safe intro!: "≡I""→I""id-R-thm:3"[THEN"→E"])
AOT_assume ‹x = y›
AOT_hence ‹[R]yz› using z_prop "rule=E"by fast
AOT_hence ‹[R]xz & [R]yz› using z_prop "&I"by blast
AOT_hence ‹∃z ([R]xz & [R]yz)› by (rule "∃I")
AOT_thus ‹x =\R y› using"id-R-thm:1""≡E"(2) by blast qed
} moreover {
AOT_assume ‹InDomainOf(y, R)›
AOT_hence ‹∃z [R]yz› by (metis "≡dfE""df-1-1:5") then AOT_obtain z where z_prop: ‹[R]yz› using"∃E"[rotated] by blast
AOT_have ‹x =\R y ≡ x = y› proof(safe intro!: "≡I""→I""id-R-thm:3"[THEN"→E"])
AOT_assume ‹x = y›
AOT_hence ‹[R]xz› using z_prop "rule=E" id_sym by fast
AOT_hence ‹[R]xz & [R]yz› using z_prop "&I"by blast
AOT_hence ‹∃z ([R]xz & [R]yz)› by (rule "∃I")
AOT_thus ‹x =\R y› using"id-R-thm:1""≡E"(2) by blast qed
} ultimately AOT_show ‹x =\R y ≡ x = y› by (metis "∨E"(2) "raa-cor:1") qed
AOT_theorem "id-R-thm:5": ‹InDomainOf(x, R) → x =\R x› proof (rule "→I")
AOT_assume ‹InDomainOf(x, R)›
AOT_hence ‹∃z [R]xz› by (metis "≡dfE""df-1-1:5") then AOT_obtain z where z_prop: ‹[R]xz› using"∃E"[rotated] by blast
AOT_hence ‹[R]xz & [R]xz› using"&I"by blast
AOT_hence ‹∃z ([R]xz & [R]xz)› using"∃I"by fast
AOT_thus ‹x =\R x› using"id-R-thm:1""≡E"(2) by blast qed
AOT_theorem "id-R-thm:6": ‹x =\R y → y =\R x› proof(rule "→I")
AOT_assume 0: ‹x =\R y›
AOT_hence 1: ‹InDomainOf(x,R) & InDomainOf(y,R)› using"id-R-thm:2"[THEN"→E"] by blast
AOT_hence ‹x =\R y ≡ x = y› using"id-R-thm:4"[THEN"→E", OF "∨I"(1)] "&E"by blast
AOT_hence ‹x = y› using0by (metis "≡E"(1))
AOT_hence ‹y = x› using id_sym by blast moreover AOT_have ‹y =\R x ≡ y = x› using"id-R-thm:4"[THEN"→E", OF "∨I"(2)] 1"&E"by blast ultimately AOT_show ‹y =\R x› by (metis "≡E"(2)) qed
AOT_theorem "id-R-thm:7": ‹x =\R y & y =\R z → x =\R z› proof (rule "→I"; frule "&E"(1); drule "&E"(2))
AOT_assume 0: ‹x =\R y›
AOT_hence 1: ‹InDomainOf(x,R) & InDomainOf(y,R)› using"id-R-thm:2"[THEN"→E"] by blast
AOT_hence ‹x =\R y ≡ x = y› using"id-R-thm:4"[THEN"→E", OF "∨I"(1)] "&E"by blast
AOT_hence x_eq_y: ‹x = y› using0by (metis "≡E"(1))
AOT_assume 2: ‹y =\R z›
AOT_hence 3: ‹InDomainOf(y,R) & InDomainOf(z,R)› using"id-R-thm:2"[THEN"→E"] by blast
AOT_hence ‹y =\R z ≡ y = z› using"id-R-thm:4"[THEN"→E", OF "∨I"(1)] "&E"by blast
AOT_hence ‹y = z› using2by (metis "≡E"(1))
AOT_hence x_eq_z: ‹x = z› using x_eq_y id_trans by blast
AOT_have ‹InDomainOf(x,R) & InDomainOf(z,R)› using13"&I""&E"by meson
AOT_hence ‹x =\R z ≡ x = z› using"id-R-thm:4"[THEN"→E", OF "∨I"(1)] "&E"by blast
AOT_thus ‹x =\R z› using x_eq_z "≡E"(2) by blast qed
AOT_have ‹[λy [F]y & [R]+zy]x› proof (rule "w-ances-her:2"[unvarify F, OF den, THEN"→E"]; safe intro!: "&I")
AOT_show ‹[λy [F]y & [R]+zy]z› proof (safe intro!: "β←C"(1) "cqt:2""&I")
AOT_show ‹[F]z›using θ "&E"by blast next
AOT_show ‹[R]+zz› by (rule "w-ances"[THEN"≡E"(2), OF "∨I"(2)])
(meson "0""id-R-thm:5""1-1-R:5""→E") qed next
AOT_show ‹[R]+zx›by (fact 0) next
AOT_show ‹Hereditary([λy [F]y & [R]+zy],R)› proof (safe intro!: "hered:1"[THEN"≡dfI"] "&I""cqt:2" GEN "→I") fix x' y
AOT_assume 1: ‹[R]x'y›
AOT_assume ‹[λy [F]y & [R]+zy]x'›
AOT_hence 2: ‹[F]x' & [R]+zx'›by (rule "β→C"(1))
AOT_have ‹[R]*zy›using12[THEN"&E"(2)] by (metis Adjunction "modus-tollens:1""reductio-aa:1""w-ances-her:3")
AOT_hence 3: ‹[R]+zy›by (metis "∨I"(1) "≡E"(2) "w-ances")
AOT_show ‹[λy [F]y & [R]+zy]y› proof (safe intro!: "β←C"(1) "cqt:2""&I"3)
AOT_show ‹[F]y› proof (rule θ[THEN"&E"(2), THEN"∀E"(2), THEN"∀E"(2), THEN"→E", THEN"→E", THEN"→E"])
AOT_show ‹[R]+zx' & [R]+zy› using23"&E""&I"by blast next
AOT_show ‹[R]x'y›by (fact 1) next
AOT_show ‹[F]x'›using2"&E"by blast qed qed qed qed
AOT_thus ‹[F]x›using"β→C"(1) "&E"(1) by fast qed
text‹The following is not part of PLM, but a theorem of AOT.
It states that the predecessor relation coexists with numbering a property.
We will use this fact to derive the predecessor axiom, which asserts that the
predecessor relation denotes, from the fact that our models validate that
numbering a property denotes.›
AOT_theorem pred_coex: ‹[λxy ∃F∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))]↓≡∀F ([λx Numbers(x,F)]↓)› proof(safe intro!: "≡I""→I" GEN) fix F let ?P = ‹«[λxy ∃F∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))]¬›
AOT_assume ‹[«?P¬]↓›
AOT_hence ‹◻[«?P¬]↓› using"exist-nec""→E"by blast moreover AOT_have ‹◻[«?P¬]↓→◻(∀x∀y(∀F([F]x ≡ [F]y) → (Numbers(x,F) ≡ Numbers(y,F))))› proof(rule RM; safe intro!: "→I" GEN)
AOT_modally_strict { fix x y
AOT_assume pred_den: ‹[«?P¬]↓›
AOT_hence pred_equiv: ‹[«?P¬]xy ≡∃F∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))›for x y by (safe intro!: "beta-C-meta"[unvarify ν1νn, where τ=‹(_,_)›, THEN"→E",
rotated, OF pred_den, simplified]
tuple_denotes[THEN"≡dfI"] "&I""cqt:2") text‹We show as a subproof that any natural cardinal that is not zero
has a predecessor.›
AOT_have CardinalPredecessor: ‹∃y [«?P¬]yx›if card_x: ‹NaturalCardinal(x)›and x_nonzero: ‹x ≠ 0›for x proof -
AOT_have ‹∃G x = #G› using card[THEN"≡dfE", OF card_x].
AOT_hence ‹∃G Numbers(x,G)› using"eq-df-num"[THEN"≡E"(1)] by blast then AOT_obtain G' where numxG': ‹Numbers(x,G')› using"∃E"[rotated] by blast
AOT_obtain G where ‹Rigidifies(G,G')› using"rigid-der:3""∃E"[rotated] by blast
AOT_hence H: ‹Rigid(G) & ∀x ([G]x ≡ [G']x)› using"df-rigid-rel:2"[THEN"≡dfE"] by blast
AOT_have H_rigid: ‹◻∀x ([G]x →◻[G]x)› using H[THEN"&E"(1), THEN"df-rigid-rel:1"[THEN"≡dfE"], THEN"&E"(2)].
AOT_hence ‹∀x ◻([G]x →◻[G]x)› using"CBF""→E"by blast
AOT_hence R: ‹◻([G]x →◻[G]x)›for x using"∀E"(2) by blast
AOT_hence rigid: ‹[G]x ≡\A[G]x›for x by (metis "≡E"(6) "oth-class-taut:3:a""sc-eq-fur:2""→E")
AOT_have ‹G ≡E G'› proof (safe intro!: eqE[THEN"≡dfI"] "&I""cqt:2" GEN "→I")
AOT_show ‹[G]x ≡ [G']x›for x using H[THEN"&E"(2)] "∀E"(2) by fast qed
AOT_hence ‹G ≈E G'› by (rule "apE-eqE:2"[THEN"→E", OF "&I", rotated])
(simp add: "eq-part:1")
AOT_hence numxG: ‹Numbers(x,G)› using"num-tran:1"[THEN"→E", THEN"≡E"(2)] numxG' by blast
{
AOT_assume ‹¬∃y(y ≠ x & [«?P¬]yx)›
AOT_hence ‹∀y ¬(y ≠ x & [«?P¬]yx)› using"cqt-further:4""→E"by blast
AOT_hence ‹¬(y ≠ x & [«?P¬]yx)›for y using"∀E"(2) by blast
AOT_hence 0: ‹¬y ≠ x ∨¬[«?P¬]yx›for y using"¬¬E""intro-elim:3:c""oth-class-taut:5:a"by blast
{ fix y
AOT_assume ‹[«?P¬]yx›
AOT_hence ‹¬y ≠ x› using0"¬¬I""con-dis-i-e:4:c"by blast
AOT_hence ‹y = x› using"=-infix""≡dfI""raa-cor:4"by blast
} note Pxy_imp_eq = this
AOT_have ‹[«?P¬]xx› proof(rule "raa-cor:1")
AOT_assume notPxx: ‹¬[«?P¬]xx›
AOT_hence ‹¬∃F∃u([F]u & Numbers(x,F) & Numbers(x,[F]-u))› using pred_equiv "intro-elim:3:c"by blast
AOT_hence ‹∀F ¬∃u([F]u & Numbers(x,F) & Numbers(x,[F]-u))› using"cqt-further:4"[THEN"→E"] by blast
AOT_hence ‹¬∃u([F]u & Numbers(x,F) & Numbers(x,[F]-u))›for F using"∀E"(2) by blast
AOT_hence ‹∀y ¬(O!y & ([F]y & Numbers(x,F) & Numbers(x,[F]-y)))›for F using"cqt-further:4"[THEN"→E"] by blast
AOT_hence 0: ‹¬(O!u & ([F]u & Numbers(x,F) & Numbers(x,[F]-u)))›for F u using"∀E"(2) by blast
AOT_have ‹◻¬∃u [G]u› proof(rule "raa-cor:1")
AOT_assume ‹¬◻¬∃u [G]u›
AOT_hence ‹♢∃u [G]u› using"≡dfI""conventions:5"by blast
AOT_hence ‹∃u ♢[G]u› by (metis "Ordinary.res-var-bound-reas[BF♢]"[THEN"→E"]) then AOT_obtain u where posGu: ‹♢[G]u› using"Ordinary.∃E"[rotated] by meson
AOT_hence Gu: ‹[G]u› by (meson "B♢""K♢""→E" R)
AOT_have ‹¬([G]u & Numbers(x,G) & Numbers(x,[G]-u))› using0 Ordinary.ψ by (metis "con-dis-i-e:1""raa-cor:1")
AOT_hence notnumx: ‹¬Numbers(x,[G]-u)› using Gu numxG "con-dis-i-e:1""raa-cor:5"by metis
AOT_obtain y where numy: ‹Numbers(y,[G]-u)› using"num:1"[unvarify G, OF "F-u[den]"] "∃E"[rotated] by blast
AOT_hence ‹[G]u & Numbers(x,G) & Numbers(y,[G]-u)› using Gu numxG "&I"by blast
AOT_hence ‹∃u ([G]u & Numbers(x,G) & Numbers(y,[G]-u))› by (rule "Ordinary.∃I")
AOT_hence ‹∃G∃u ([G]u & Numbers(x,G) & Numbers(y,[G]-u))› by (rule "∃I")
AOT_hence ‹[«?P¬]yx› using pred_equiv[THEN"≡E"(2)] by blast
AOT_hence ‹y = x›using Pxy_imp_eq by blast
AOT_hence ‹Numbers(x,[G]-u)› using numy "rule=E"by fast
AOT_thus ‹p & ¬p›for p using notnumx "reductio-aa:1"by blast qed
AOT_hence ‹¬∃u [G]u› using"qml:2"[axiom_inst, THEN"→E"] by blast
AOT_hence num0G: ‹Numbers(0, G)› using"0F:1"[THEN"≡E"(1)] by blast
AOT_hence ‹x = 0› using"pre-Hume"[unvarify x, THEN"→E", OF "zero:2", OF "&I", THEN"≡E"(2), OF num0G, OF numxG, OF "eq-part:1"]
id_sym by blast moreover AOT_have ‹¬x = 0› using x_nonzero using"=-infix""≡dfE"by blast ultimately AOT_show ‹p & ¬p›for p using"reductio-aa:1"by blast qed
}
AOT_hence ‹[«?P¬]xx ∨∃y (y ≠ x & [«?P¬]yx)› using"con-dis-i-e:3:a""con-dis-i-e:3:b""raa-cor:1"by blast moreover {
AOT_assume ‹[«?P¬]xx›
AOT_hence ‹∃y [«?P¬]yx› by (rule "∃I")
} moreover {
AOT_assume ‹∃y (y ≠ x & [«?P¬]yx)› then AOT_obtain y where ‹y ≠ x & [«?P¬]yx› using"∃E"[rotated] by blast
AOT_hence ‹[«?P¬]yx› using"&E"by blast
AOT_hence ‹∃y [«?P¬]yx› by (rule "∃I")
} ultimately AOT_show ‹∃y [«?P¬]yx› using"∨E"(1) "→I"by blast qed
text‹Given above lemma, we can show that if one of two indistinguishable objects
numbers a property, the other one numbers this property as well.›
AOT_assume indist: ‹∀F([F]x ≡ [F]y)›
AOT_assume numxF: ‹Numbers(x,F)›
AOT_hence 0: ‹NaturalCardinal(x)› by (metis "eq-num:6""vdash-properties:10") text‹We show by case distinction that x equals y.
As first case we consider x to be non-zero.›
{
AOT_assume ‹¬(x = 0)›
AOT_hence ‹x ≠ 0› by (metis "=-infix""≡dfI")
AOT_hence ‹∃y [«?P¬]yx› using CardinalPredecessor 0by blast then AOT_obtain z where Pxz: ‹[«?P¬]zx› using"∃E"[rotated] by blast
AOT_hence ‹[λy [«?P¬]zy]x› by (safe intro!: "β←C""cqt:2")
AOT_hence ‹[λy [«?P¬]zy]y› by (safe intro!: indist[THEN"∀E"(1), THEN"≡E"(1)] "cqt:2")
AOT_hence Pyz: ‹[«?P¬]zy› using"β→C"(1) by blast
AOT_hence ‹∃F∃u ([F]u & Numbers(y,F) & Numbers(z,[F]-u))› using Pyz pred_equiv[THEN"≡E"(1)] by blast then AOT_obtain F1 where ‹∃u ([F1]u & Numbers(y,F1) & Numbers(z,[F1]-u))› using"∃E"[rotated] by blast then AOT_obtain u where u_prop: ‹[F1]u & Numbers(y,F1) & Numbers(z,[F1]-u)› using"Ordinary.∃E"[rotated] by meson
AOT_have ‹∃F∃u ([F]u & Numbers(x,F) & Numbers(z,[F]-u))› using Pxz pred_equiv[THEN"≡E"(1)] by blast then AOT_obtain F2 where ‹∃u ([F2]u & Numbers(x,F2) & Numbers(z,[F2]-u))› using"∃E"[rotated] by blast then AOT_obtain v where v_prop: ‹[F2]v & Numbers(x,F2) & Numbers(z,[F2]-v)› using"Ordinary.∃E"[rotated] by meson
AOT_have ‹[F2]-v≈E [F1]-u› using"hume-strict:1"[unvarify F G, THEN"≡E"(1), OF "F-u[den]",
OF "F-u[den]", OF "∃I"(2)[where β=z], OF "&I"]
v_prop u_prop "&E"by blast
AOT_hence ‹F2≈E F1› using"P'-eq"[THEN"→E", OF "&I", OF "&I"]
u_prop v_prop "&E"by meson
AOT_hence ‹x = y› using"pre-Hume"[THEN"→E", THEN"≡E"(2), OF "&I"]
v_prop u_prop "&E"by blast
} text‹The second case handles x being equal to zero.› moreover { fix u
AOT_assume x_is_zero: ‹x = 0› moreover AOT_have ‹Numbers(0,[λz z =E u]-u)› proof (safe intro!: "0F:1"[unvarify F, THEN"≡E"(1)] "cqt:2""raa-cor:2" "F-u[den]"[unvarify F])
AOT_assume ‹∃v [[λz z =E u]-u]v› then AOT_obtain v where ‹[[λz z =E u]-u]v› using"Ordinary.∃E"[rotated] by meson
AOT_hence ‹[λz z =E u]v & v ≠E u› by (auto intro: "F-u"[THEN"=dfE"(1), where τ1τn="(_,_)", simplified]
intro!: "cqt:2""F-u[equiv]"[unvarify F, THEN"≡E"(1)] "F-u[den]"[unvarify F])
AOT_thus ‹p & ¬p›for p using"β→C""thm-neg=E"[THEN"≡E"(1)] "&E""&I" "raa-cor:3"by fast qed ultimately AOT_have 0: ‹Numbers(x,[λz z =E u]-u)› using"rule=E" id_sym by fast
AOT_have ‹∃y Numbers(y,[λz z =E u])› by (safe intro!: "num:1"[unvarify G] "cqt:2") then AOT_obtain z where ‹Numbers(z,[λz z =E u])› using"∃E"by metis moreover AOT_have ‹[λz z=E u]u› by (safe intro!: "β←C""cqt:2""ord=Eequiv:1"[THEN"→E"] Ordinary.ψ) ultimately AOT_have 1: ‹[λz z=E u]u & Numbers(z,[λz z=E u]) & Numbers(x,[λz z=E u]-u)› using0"&I"by auto
AOT_hence ‹∃v([λz z=E u]v & Numbers(z,[λz z =E u]) & Numbers(x,[λz z=E u]-v))› by (rule "Ordinary.∃I")
AOT_hence ‹∃F∃u([F]u & Numbers(z,[F]) & Numbers(x,[F]-u))› by (rule "∃I"; "cqt:2")
AOT_hence Px1: ‹[«?P¬]xz› using"beta-C-cor:2"[THEN"→E", OF pred_den, THEN tuple_forall[THEN"≡dfE"], THEN"∀E"(2), THEN"∀E"(2), THEN"≡E"(2)] by simp
AOT_hence ‹[λy [«?P¬]yz]x› by (safe intro!: "β←C""cqt:2")
AOT_hence ‹[λy [«?P¬]yz]y› by (safe intro!: indist[THEN"∀E"(1), THEN"≡E"(1)] "cqt:2")
AOT_hence Py1: ‹[«?P¬]yz› using"β→C"by blast
AOT_hence ‹∃F∃u([F]u & Numbers(z,[F]) & Numbers(y,[F]-u))› using"β→C"by fast then AOT_obtain G where ‹∃u([G]u & Numbers(z,[G]) & Numbers(y,[G]-u))› using"∃E"[rotated] by blast then AOT_obtain v where 2: ‹[G]v & Numbers(z,[G]) & Numbers(y,[G]-v)› using"Ordinary.∃E"[rotated] by meson with12 AOT_have ‹[λz z =E u] ≈E G› by (auto intro!: "hume-strict:1"[unvarify F, THEN"≡E"(1), rotated,
OF "∃I"(2)[where β=z], OF "&I"] "cqt:2"
dest: "&E")
AOT_hence 3: ‹[λz z =E u]-u≈E [G]-v› using12 by (safe_step intro!: "eqP'"[unvarify F, THEN"→E"])
(auto dest: "&E" intro!: "cqt:2""&I") with12 AOT_have ‹x = y› by (auto intro!: "pre-Hume"[unvarify G H, THEN"→E", THEN"≡E"(2), rotated 3, OF 3] "F-u[den]"[unvarify F] "cqt:2""&I"
dest: "&E")
} ultimately AOT_have ‹x = y› using"∨E"(1) "→I""reductio-aa:1"by blast text‹Now since x numbers F, so does y.›
AOT_hence ‹Numbers(y,F)› using numxF "rule=E"by fast
} note0 = this text‹The only thing left is to generalize this result to a biconditional.›
AOT_modally_strict { fix x y
AOT_assume ‹[«?P¬]↓› moreover AOT_assume ‹∀F([F]x ≡ [F]y)› moreover AOT_have ‹∀F([F]y ≡ [F]x)› by (metis "cqt-basic:11""intro-elim:3:a" calculation(2)) ultimately AOT_show ‹Numbers(x,F) ≡ Numbers(y,F)› using0"≡I""→I"by auto
} qed ultimately AOT_show ‹[λx Numbers(x,F)]↓› using"kirchner-thm:1"[THEN"≡E"(2)] "→E"by fast next text‹The converse can be shown by coexistence.›
AOT_assume ‹∀F [λx Numbers(x,F)]↓›
AOT_hence ‹[λx Numbers(x,F)]↓›for F using"∀E"(2) by blast
AOT_hence ‹◻[λx Numbers(x,F)]↓›for F using"exist-nec"[THEN"→E"] by blast
AOT_hence ‹∀F ◻[λx Numbers(x,F)]↓› by (rule GEN)
AOT_hence ‹◻∀F [λx Numbers(x,F)]↓› using BF[THEN"→E"] by fast moreover AOT_have ‹◻∀F [λx Numbers(x,F)]↓→ ◻∀x ∀y (∃F ∃u ([F]u & [λz Numbers(z,F)]y & [λz Numbers(z,[F]-u)]x) ≡ ∃F ∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u)))› proof(rule RM; safe intro!: "→I" GEN)
AOT_modally_strict { fix x y
AOT_assume 0: ‹∀F [λx Numbers(x,F)]↓›
AOT_show ‹∃F ∃u ([F]u & [λz Numbers(z,F)]y & [λz Numbers(z,[F]-u)]x) ≡ ∃F ∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))› proof(safe intro!: "≡I""→I")
AOT_assume ‹∃F ∃u ([F]u & [λz Numbers(z,F)]y & [λz Numbers(z,[F]-u)]x)› then AOT_obtain F where ‹∃u ([F]u & [λz Numbers(z,F)]y & [λz Numbers(z,[F]-u)]x)› using"∃E"[rotated] by blast then AOT_obtain u where ‹[F]u & [λz Numbers(z,F)]y & [λz Numbers(z,[F]-u)]x› using"Ordinary.∃E"[rotated] by meson
AOT_hence ‹[F]u & Numbers(y,F) & Numbers(x,[F]-u)› by (auto intro!: "&I" dest: "&E""β→C")
AOT_thus ‹∃F ∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))› using"∃I""Ordinary.∃I"by fast next
AOT_assume ‹∃F ∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))› then AOT_obtain F where ‹∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))› using"∃E"[rotated] by blast then AOT_obtain u where ‹[F]u & Numbers(y,F) & Numbers(x,[F]-u)› using"Ordinary.∃E"[rotated] by meson
AOT_hence ‹[F]u & [λz Numbers(z,F)]y & [λz Numbers(z,[F]-u)]x› by (auto intro!: "&I""β←C"0[THEN"∀E"(1)] "F-u[den]"
dest: "&E" intro: "cqt:2")
AOT_hence ‹∃u([F]u & [λz Numbers(z,F)]y & [λz Numbers(z,[F]-u)]x)› by (rule "Ordinary.∃I")
AOT_thus ‹∃F∃u([F]u & [λz Numbers(z,F)]y & [λz Numbers(z,[F]-u)]x)› by (rule "∃I") qed
} qed ultimately AOT_have ‹◻∀x ∀y (∃F ∃u ([F]u & [λz Numbers(z,F)]y & [λz Numbers(z,[F]-u)]x) ≡ ∃F ∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u)))› using"→E"by blast
AOT_thus ‹[λxy ∃F ∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))]↓› by (rule "safe-ext[2]"[axiom_inst, THEN"→E", OF "&I", rotated]) "cqt:2" qed
text‹The following is not part of PLM, but a consequence of extended relation
comprehension and can be used to @{emph ‹derive›} the predecessor axiom.›
AOT_theorem numbers_prop_den: ‹[λx Numbers(x,G)]↓› proof (rule "safe-ext"[axiom_inst, THEN"→E", OF "&I"])
AOT_show ‹[λx A!x & [λx ∀F (x[F] ≡ [λz \A[F]z] ≈E G)]x]↓› by"cqt:2" next
AOT_have 0: ‹\⊨\◻ [λx ∀F (x[F] ≡ [λz \A[F]z] ≈E G)]↓› proof(safe intro!: Comprehension_3[THEN"→E"] "→I" RN GEN)
AOT_modally_strict { fix F H
AOT_assume ‹◻H ≡E F›
AOT_hence ‹◻∀u ([H]u ≡ [F]u)› by (AOT_subst (reverse) ‹∀u ([H]u ≡ [F]u)›‹H ≡E F›)
(safe intro!: "eqE"[THEN"≡Df", THEN"≡S"(1), OF "&I"] "cqt:2")
AOT_hence ‹∀u ◻([H]u ≡ [F]u)› by (metis "Ordinary.res-var-bound-reas[CBF]""→E")
AOT_hence ‹◻([H]u ≡ [F]u)›for u using"Ordinary.∀E"by fast
AOT_hence ‹\A([H]u ≡ [F]u)›for u by (metis "nec-imp-act""→E")
AOT_hence ‹\A([F]u ≡ [H]u)›for u by (metis "Act-Basic:5""Commutativity of ≡""intro-elim:3:b")
AOT_hence ‹[λz \A[F]z] ≡E [λz \A[H]z]› by (safe intro!: "eqE"[THEN"≡dfI"] "&I""cqt:2" Ordinary.GEN;
AOT_subst ‹[λz \A[F]z]u›‹\A[F]u›for: u F)
(auto intro!: "beta-C-meta"[THEN"→E"] "cqt:2" "Act-Basic:5"[THEN"≡E"(1)])
AOT_hence ‹[λz \A[F]z] ≈E [λz \A[H]z]› by (safe intro!: "apE-eqE:1"[unvarify F G, THEN"→E"] "cqt:2")
AOT_thus ‹[λz \A[F]z] ≈E G ≡ [λz \A[H]z] ≈E G› using"≡I""eq-part:2[terms]""eq-part:3[terms]""→E""→I" by metis
} qed
AOT_show ‹◻∀x (A!x & [λx ∀F (x[F] ≡ [λz \A[F]z] ≈E G)]x ≡ Numbers(x,G))› proof (safe intro!: RN GEN)
AOT_modally_strict { fix x
AOT_show ‹A!x & [λx ∀F (x[F] ≡ [λz \A[F]z] ≈E G)]x ≡ Numbers(x,G)› by (AOT_subst_def numbers; AOT_subst_thm "beta-C-meta"[THEN"→E", OF 0])
(auto intro!: "beta-C-meta"[THEN"→E", OF 0] "≡I""→I""&I""cqt:2"
dest: "&E")
} qed qed
text‹The two theorems above allow us to derive
the predecessor axiom of PLM as theorem.›
AOT_theorem "pred-thm:2": ‹ℙ↓› using pred "pred-thm:1""rule-id-df:2:b[zero]"by blast
AOT_theorem "pred-thm:3": ‹[ℙ]xy ≡∃F∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))› by (auto intro!: "beta-C-meta"[unvarify ν1νn, where τ=‹(_,_)›, THEN"→E",
rotated, OF pred, simplified]
tuple_denotes[THEN"≡dfI"] "&I""cqt:2" pred
intro: "=dfI"(2)[OF "pred-thm:1"])
AOT_theorem "pred-1-1:1": ‹[ℙ]xy →◻[ℙ]xy› proof(rule "→I")
AOT_assume ‹[ℙ]xy›
AOT_hence ‹∃F∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))› using"≡E"(1) "pred-thm:3"by fast then AOT_obtain F where ‹∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))› using"∃E"[rotated] by blast then AOT_obtain u where props: ‹[F]u & Numbers(y,F) & Numbers(x,[F]-u)› using"Ordinary.∃E"[rotated] by meson
AOT_obtain G where Ridigifies_G_F: ‹Rigidifies(G, F)› by (metis "instantiation""rigid-der:3")
AOT_hence ξ: ‹◻∀x([G]x →◻[G]x)›and ζ: ‹∀x([G]x ≡ [F]x)› using"df-rigid-rel:2"[THEN"≡dfE", THEN"&E"(1), THEN"≡dfE"[OF "df-rigid-rel:1"], THEN"&E"(2)] "df-rigid-rel:2"[THEN"≡dfE", THEN"&E"(2)] by blast+
AOT_have rigid_num_nec: ‹Numbers(x,F) & Rigidifies(G,F) →◻Numbers(x,G)› for x G F proof(rule "→I"; frule "&E"(1); drule "&E"(2)) fix G F x
AOT_assume Numbers_xF: ‹Numbers(x,F)›
AOT_assume ‹Rigidifies(G,F)›
AOT_hence ξ: ‹Rigid(G)›and ζ: ‹∀x([G]x ≡ [F]x)› using"df-rigid-rel:2"[THEN"≡dfE"] "&E"by blast+
AOT_thus ‹◻Numbers(x,G)› proof (safe intro!: "num-cont:2"[THEN"→E", OF ξ, THEN"qml:2"[axiom_inst, THEN"→E"], THEN"∀E"(2), THEN"→E"] "num-tran:3"[THEN"→E", THEN"≡E"(1), rotated, OF Numbers_xF]
eqE[THEN"≡dfI"] "&I""cqt:2[const_var]"[axiom_inst] Ordinary.GEN "→I")
AOT_show ‹[F]u ≡ [G]u›for u using ζ[THEN"∀E"(2)] by (metis "≡E"(6) "oth-class-taut:3:a") qed qed
AOT_have ‹◻Numbers(y,G)› using rigid_num_nec[THEN"→E", OF "&I", OF props[THEN"&E"(1), THEN"&E"(2)],
OF Ridigifies_G_F]. moreover {
AOT_have ‹Rigidifies([G]-u, [F]-u)› proof (safe intro!: "df-rigid-rel:1"[THEN"≡dfI"] "df-rigid-rel:2"[THEN"≡dfI"] "&I""F-u[den]" GEN "≡I""→I")
AOT_have ‹◻∀x([G]x →◻[G]x) →◻∀x([[G]-u]x →◻[[G]-u]x)› proof (rule RM; safe intro!: "→I" GEN)
AOT_modally_strict { fix x
AOT_assume 0: ‹∀x([G]x →◻[G]x)›
AOT_assume 1: ‹[[G]-u]x›
AOT_have ‹[λx [G]x & x ≠E u]x› apply (rule "F-u"[THEN"=dfE"(1), where τ1τn="(_,_)", simplified]) apply"cqt:2[lambda]" by (fact 1)
AOT_hence ‹[G]x & x ≠E u› by (rule "β→C"(1))
AOT_hence 2: ‹◻[G]x›and3: ‹◻x ≠E u› using"&E"0[THEN"∀E"(2), THEN"→E"] "id-nec4:1""≡E"(1) by blast+
AOT_show ‹◻[[G]-u]x› apply (AOT_subst ‹[[G]-u]x›‹[G]x & x ≠E u›) apply (rule "F-u"[THEN"=dfI"(1), where τ1τn="(_,_)", simplified]) apply"cqt:2[lambda]" apply (rule "beta-C-meta"[THEN"→E"]) apply"cqt:2[lambda]" using23"KBasic:3""≡S"(2) "≡E"(2) by blast
} qed
AOT_thus ‹◻∀x([[G]-u]x →◻[[G]-u]x)›using ξ "→E"by blast next fix x
AOT_assume ‹[[G]-u]x›
AOT_hence ‹[λx [G]x & x ≠E u]x› by (auto intro: "F-u"[THEN"=dfE"(1), where τ1τn="(_,_)", simplified]
intro!: "cqt:2")
AOT_hence ‹[G]x & x ≠E u› by (rule "β→C"(1))
AOT_hence ‹[F]x & x ≠E u› using ζ "&I""&E"(1) "&E"(2) "≡E"(1) "rule-ui:3"by blast
AOT_hence ‹[λx [F]x & x ≠E u]x› by (auto intro!: "β←C"(1) "cqt:2")
AOT_thus ‹[[F]-u]x› by (auto intro: "F-u"[THEN"=dfI"(1), where τ1τn="(_,_)", simplified]
intro!: "cqt:2") next fix x
AOT_assume ‹[[F]-u]x›
AOT_hence ‹[λx [F]x & x ≠E u]x› by (auto intro: "F-u"[THEN"=dfE"(1), where τ1τn="(_,_)", simplified]
intro!: "cqt:2")
AOT_hence ‹[F]x & x ≠E u› by (rule "β→C"(1))
AOT_hence ‹[G]x & x ≠E u› using ζ "&I""&E"(1) "&E"(2) "≡E"(2) "rule-ui:3"by blast
AOT_hence ‹[λx [G]x & x ≠E u]x› by (auto intro!: "β←C"(1) "cqt:2")
AOT_thus ‹[[G]-u]x› by (auto intro: "F-u"[THEN"=dfI"(1), where τ1τn="(_,_)", simplified]
intro!: "cqt:2") qed
AOT_hence ‹◻Numbers(x,[G]-u)› using rigid_num_nec[unvarify F G, OF "F-u[den]", OF "F-u[den]", THEN"→E",
OF "&I", OF props[THEN"&E"(2)]] by blast
} moreover AOT_have ‹◻[G]u› using props[THEN"&E"(1), THEN"&E"(1), THEN ζ[THEN"∀E"(2), THEN"≡E"(2)]]
ξ[THEN"qml:2"[axiom_inst, THEN"→E"], THEN"∀E"(2), THEN"→E"] by blast ultimately AOT_have ‹◻([G]u & Numbers(y,G) & Numbers(x,[G]-u))› by (metis "KBasic:3""&I""≡E"(2))
AOT_hence ‹∃u (◻([G]u & Numbers(y,G) & Numbers(x,[G]-u)))› by (rule "Ordinary.∃I")
AOT_hence ‹◻∃u ([G]u & Numbers(y,G) & Numbers(x,[G]-u))› using"Ordinary.res-var-bound-reas[Buridan]""→E"by fast
AOT_hence ‹∃F ◻∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))› by (rule "∃I")
AOT_hence 0: ‹◻∃F∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))› using Buridan "vdash-properties:10"by fast
AOT_show ‹◻[ℙ]xy› by (AOT_subst ‹[ℙ]xy›‹∃F∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))›;
simp add: "pred-thm:3"0) qed
AOT_theorem "pred-1-1:2": ‹Rigid(ℙ)› by (safe intro!: "df-rigid-rel:1"[THEN"≡dfI"] "pred-thm:2""&I"
RN tuple_forall[THEN"≡dfI"];
safe intro!: GEN "pred-1-1:1")
AOT_theorem "pred-1-1:3": ‹1-1(ℙ)› proof (safe intro!: "df-1-1:1"[THEN"≡dfI"] "pred-thm:2""&I" GEN "→I";
frule "&E"(1); drule "&E"(2)) fix x y z
AOT_assume ‹[ℙ]xz›
AOT_hence ‹∃F∃u ([F]u & Numbers(z,F) & Numbers(x,[F]-u))› using"pred-thm:3"[THEN"≡E"(1)] by blast then AOT_obtain F where ‹∃u ([F]u & Numbers(z,F) & Numbers(x,[F]-u))› using"∃E"[rotated] by blast then AOT_obtain u where u_prop: ‹[F]u & Numbers(z,F) & Numbers(x,[F]-u)› using"Ordinary.∃E"[rotated] by meson
AOT_assume ‹[ℙ]yz›
AOT_hence ‹∃F∃u ([F]u & Numbers(z,F) & Numbers(y,[F]-u))› using"pred-thm:3"[THEN"≡E"(1)] by blast then AOT_obtain G where ‹∃u ([G]u & Numbers(z,G) & Numbers(y,[G]-u))› using"∃E"[rotated] by blast then AOT_obtain v where v_prop: ‹[G]v & Numbers(z,G) & Numbers(y,[G]-v)› using"Ordinary.∃E"[rotated] by meson
AOT_show ‹x = y› proof (rule "pre-Hume"[unvarify G H, OF "F-u[den]", OF "F-u[den]", THEN"→E", OF "&I", THEN"≡E"(2)])
AOT_show ‹Numbers(x, [F]-u)› using u_prop "&E"by blast next
AOT_show ‹Numbers(y, [G]-v)› using v_prop "&E"by blast next
AOT_have ‹F ≈E G› using u_prop[THEN"&E"(1), THEN"&E"(2)] using v_prop[THEN"&E"(1), THEN"&E"(2)] using"num-tran:2"[THEN"→E", OF "&I"] by blast
AOT_thus ‹[F]-u≈E [G]-v› using u_prop[THEN"&E"(1), THEN"&E"(1)] using v_prop[THEN"&E"(1), THEN"&E"(1)] using eqP'[THEN"→E", OF "&I", OF "&I"] by blast qed qed
AOT_theorem "pred-1-1:4": ‹Rigid1-1(ℙ)› by (meson "≡dfI""&I""df-1-1:2""pred-1-1:2""pred-1-1:3")
AOT_theorem "assume-anc:3": ‹[ℙ*]xy ≡∀F((∀z([ℙ]xz → [F]z) & ∀x'∀y'([ℙ]x'y' → ([F]x' → [F]y'))) → [F]y)› proof -
AOT_have prod_den: ‹\⊨\◻«(AOT_term_of_var x1,AOT_term_of_var x2)¬↓› for x1 x2 :: ‹κ AOT_var› by (simp add: "&I""ex:1:a" prod_denotesI "rule-ui:3")
AOT_have den: ‹[λxy ∀F((∀z([ℙ]xz → [F]z) & Hereditary(F,ℙ)) → [F]y)]↓› by"cqt:2[lambda]"
AOT_have 1: ‹[ℙ*]xy ≡∀F((∀z([ℙ]xz → [F]z) & Hereditary(F,ℙ)) → [F]y)› apply (rule "rule=E"[rotated, OF "assume-anc:1"[symmetric]]) by (rule "beta-C-meta"[unvarify ν1νn, OF prod_den, THEN"→E",
simplified, OF den, simplified]) show ?thesis apply (AOT_subst (reverse) ‹∀x'∀y' ([ℙ]x'y' → ([F]x' → [F]y'))› ‹Hereditary(F,ℙ)›for: F :: ‹<\<kappa>>›) using"hered:1"[THEN"≡Df", THEN"≡S"(1), OF "&I", OF "pred-thm:2",
OF "cqt:2[const_var]"[axiom_inst]] apply blast by (fact 1) qed
AOT_theorem "no-pred-0:1": ‹¬∃x [ℙ]x 0› proof(rule "raa-cor:2")
AOT_assume ‹∃x [ℙ]x 0› then AOT_obtain a where ‹[ℙ]a 0› using"∃E"[rotated] by blast
AOT_hence ‹∃F∃u ([F]u & Numbers(0, F) & Numbers(a, [F]-u))› using"pred-thm:3"[unvarify y, OF "zero:2", THEN"≡E"(1)] by blast then AOT_obtain F where ‹∃u ([F]u & Numbers(0, F) & Numbers(a, [F]-u))› using"∃E"[rotated] by blast then AOT_obtain u where ‹[F]u & Numbers(0, F) & Numbers(a, [F]-u)› using"Ordinary.∃E"[rotated] by meson
AOT_hence ‹[F]u›and num0_F: ‹Numbers(0, F)› using"&E""&I"by blast+
AOT_hence ‹∃u [F]u› using"Ordinary.∃I"by fast moreover AOT_have ‹¬∃u [F]u› using num0_F "≡E"(2) "0F:1"by blast ultimately AOT_show ‹p & ¬p›for p by (metis "raa-cor:3") qed
AOT_theorem "no-pred-0:2": ‹¬∃x [ℙ*]x 0› proof(rule "raa-cor:2")
AOT_assume ‹∃x [ℙ*]x 0› then AOT_obtain a where ‹[ℙ*]a 0› using"∃E"[rotated] by blast
AOT_hence ‹∃z [ℙ]z 0› using"anc-her:5"[unvarify R y, OF "zero:2",
OF "pred-thm:2", THEN"→E"] by auto
AOT_thus ‹∃z [ℙ]z 0 & ¬∃z [ℙ]z 0› by (metis "no-pred-0:1""raa-cor:3") qed
AOT_theorem "no-pred-0:3": ‹¬[ℙ*]0 0› by (metis "existential:1""no-pred-0:2""reductio-aa:1""zero:2")
AOT_theorem "0-n": ‹[ℕ]0› proof (safe intro!: "nnumber:3"[unvarify x, OF "zero:2", THEN"≡E"(2)] "assume1:5"[unvarify x y, OF "zero:2", OF "zero:2", THEN"≡E"(2)] "∨I"(2) "assume1:2"[unvarify x y, OF "zero:2", OF "zero:2", THEN"≡E"(2)]) fix u
AOT_have den: ‹[λx O!x & x =E u]↓›by"cqt:2[lambda]"
AOT_obtain a where a_prop: ‹Numbers(a, [λx O!x & x =E u])› using"num:1"[unvarify G, OF den] "∃E"[rotated] by blast
AOT_have ‹[ℙ]0a› proof (safe intro!: "pred-thm:3"[unvarify x, OF "zero:2", THEN"≡E"(2)] "∃I"(1)[where τ=‹«[λx O!x & x =E u]¬›] "Ordinary.∃I"[where β=u] "&I" den "0F:1"[unvarify F, OF "F-u[den]", unvarify F,
OF den, THEN"≡E"(1)])
AOT_show ‹[λx [O!]x & x =E u]u› by (auto intro!: "β←C"(1) "cqt:2""&I""ord=Eequiv:1"[THEN"→E"]
Ordinary.ψ) next
AOT_show ‹Numbers(a,[λx [O!]x & x =E u])› using a_prop. next
AOT_show ‹¬∃v [[λx [O!]x & x =E u]-u]v› proof(rule "raa-cor:2")
AOT_assume ‹∃v [[λx [O!]x & x =E u]-u]v› then AOT_obtain v where ‹[[λx [O!]x & x =E u]-u]v› using"Ordinary.∃E"[rotated] "&E"by blast
AOT_hence ‹[λz [λx [O!]x & x =E u]z & z ≠E u]v› apply (rule "F-u"[THEN"=dfE"(1), where τ1τn="(_,_)", simplified, rotated]) by"cqt:2[lambda]"
AOT_hence ‹[λx [O!]x & x =E u]v & v ≠E u› by (rule "β→C"(1))
AOT_hence ‹v =E u›and‹v ≠E u› using"β→C"(1) "&E"by blast+
AOT_hence ‹v =E u & ¬(v =E u)› by (metis "≡E"(4) "reductio-aa:1""thm-neg=E")
AOT_thus ‹p & ¬p›for p by (metis "raa-cor:1") qed qed
AOT_thus ‹∃z ([ℙ]0z & [ℙ]0z)› by (safe intro!: "&I""∃I"(2)[where β=a]) qed
AOT_theorem "mod-col-num:1": ‹[ℕ]x →◻[ℕ]x› proof(rule "→I")
AOT_have nec0N: ‹[λx ◻[ℕ]x]0› by (auto intro!: "β←C"(1) "cqt:2" simp: "zero:2" RN "0-n")
AOT_have 1: ‹[λx ◻[ℕ]x]0 & ∀x∀y ([[ℙ]+]0x & [[ℙ]+]0y → ([ℙ]xy → ([λx ◻[ℕ]x]x → [λx ◻[ℕ]x]y))) → ∀x ([[ℙ]+]0x → [λx ◻[ℕ]x]x)› by (auto intro!: "cqt:2"
intro: "pre-ind"[unconstrain R, unvarify β, OF "pred-thm:2", THEN"→E", OF "pred-1-1:4", unvarify z, OF "zero:2",
unvarify F])
AOT_have ‹∀x ([[ℙ]+]0x → [λx ◻[ℕ]x]x)› proof (rule 1[THEN"→E"]; safe intro!: "&I" GEN "→I" nec0N;
frule "&E"(1); drule "&E"(2)) fix x y
AOT_assume ‹[ℙ]xy›
AOT_hence 0: ‹◻[ℙ]xy› by (metis "pred-1-1:1""→E")
AOT_assume ‹[λx ◻[ℕ]x]x›
AOT_hence ‹◻[ℕ]x› by (rule "β→C"(1))
AOT_hence ‹◻([ℙ]xy & [ℕ]x)› by (metis "0""KBasic:3" Adjunction "≡E"(2) "→E") moreover AOT_have ‹◻([ℙ]xy & [ℕ]x) →◻[ℕ]y› proof (rule RM; rule "→I"; frule "&E"(1); drule "&E"(2))
AOT_modally_strict {
AOT_assume 0: ‹[ℙ]xy›
AOT_assume ‹[ℕ]x›
AOT_hence 1: ‹[[ℙ]+]0x› by (metis "≡E"(1) "nnumber:3")
AOT_show ‹[ℕ]y› apply (rule "nnumber:3"[THEN"≡E"(2)]) apply (rule "assume1:5"[unvarify x, OF "zero:2", THEN"≡E"(2)]) apply (rule "∨I"(1)) apply (rule "w-ances-her:3"[unconstrain R, unvarify β, OF "pred-thm:2", THEN"→E", OF "pred-1-1:4", unvarify x,
OF "zero:2", THEN"→E"]) apply (rule "&I") apply (fact 1) by (fact 0)
} qed ultimately AOT_have ‹◻[ℕ]y› by (metis "→E")
AOT_thus ‹[λx ◻[ℕ]x]y› by (auto intro!: "β←C"(1) "cqt:2") qed
AOT_hence 0: ‹[[ℙ]+]0x → [λx ◻[ℕ]x]x› using"∀E"(2) by blast
AOT_assume ‹[ℕ]x›
AOT_hence ‹[[ℙ]+]0x› by (metis "≡E"(1) "nnumber:3")
AOT_hence ‹[λx ◻[ℕ]x]x› using0[THEN"→E"] by blast
AOT_thus ‹◻[ℕ]x› by (rule "β→C"(1)) qed
AOT_theorem "mod-col-num:2": ‹Rigid(ℕ)› by (safe intro!: "df-rigid-rel:1"[THEN"≡dfI"] "&I" RN GEN "mod-col-num:1""nnumber:2")
AOT_register_rigid_restricted_type
Number: ‹[ℕ]κ› proof
AOT_modally_strict {
AOT_show ‹∃x [ℕ]x› by (rule "∃I"(1)[where τ=‹«0¬›]; simp add: "0-n""zero:2")
} next
AOT_modally_strict {
AOT_show ‹[ℕ]κ → κ↓›for κ by (simp add: "→I""cqt:5:a[1]"[axiom_inst, THEN"→E", THEN"&E"(2)])
} next
AOT_modally_strict {
AOT_show ‹∀x([ℕ]x →◻[ℕ]x)› by (simp add: GEN "mod-col-num:1")
} qed
AOT_register_variable_names
Number: m n k i j
AOT_theorem "0-pred": ‹¬∃n [ℙ]n 0› proof (rule "raa-cor:2")
AOT_assume ‹∃n [ℙ]n 0› then AOT_obtain n where ‹[ℙ]n 0› using"Number.∃E"[rotated] by meson
AOT_hence ‹∃x [ℙ]x 0› using"&E""∃I"by fast
AOT_thus ‹∃x [ℙ]x 0 & ¬∃x [ℙ]x 0› using"no-pred-0:1""&I"by auto qed
AOT_theorem "no-same-succ": ‹∀n∀m∀k([ℙ]nk & [ℙ]mk → n = m)› proof(safe intro!: Number.GEN "→I") fix n m k
AOT_assume ‹[ℙ]nk & [ℙ]mk›
AOT_thus ‹n = m› by (safe intro!: "cqt:2[const_var]"[axiom_inst] "df-1-1:3"[
unvarify R, OF "pred-thm:2", THEN"→E", OF "pred-1-1:4", THEN"qml:2"[axiom_inst, THEN"→E"], THEN"≡dfE"[OF "df-1-1:1"], THEN"&E"(2), THEN"∀E"(1), THEN"∀E"(1), THEN"∀E"(1)[where τ=‹AOT_term_of_var (Number.Rep k)›], THEN"→E"]) qed
AOT_theorem induction: ‹∀F([F]0 & ∀n∀m([ℙ]nm → ([F]n → [F]m)) →∀n[F]n)› proof (safe intro!: GEN[where 'a=‹<\<kappa>>›] Number.GEN "&I""→I";
frule "&E"(1); drule "&E"(2)) fix F n
AOT_assume F0: ‹[F]0›
AOT_assume 0: ‹∀n∀m([ℙ]nm → ([F]n → [F]m))›
{ fix x y
AOT_assume ‹[[ℙ]+]0x & [[ℙ]+]0y›
AOT_hence ‹[ℕ]x›and‹[ℕ]y› using"&E""≡E"(2) "nnumber:3"by blast+ moreover AOT_assume ‹[ℙ]xy› moreover AOT_assume ‹[F]x› ultimately AOT_have ‹[F]y› using0[THEN"∀E"(2), THEN"→E", THEN"∀E"(2), THEN"→E", THEN"→E", THEN"→E"] by blast
} note1 = this
AOT_have 0: ‹[[ℙ]+]0n› by (metis "≡E"(1) "nnumber:3" Number.ψ)
AOT_show ‹[F]n› apply (rule "pre-ind"[unconstrain R, unvarify β, THEN"→E", OF "pred-thm:2",
OF "pred-1-1:4", unvarify z, OF "zero:2", THEN"→E", THEN"∀E"(2), THEN"→E"];
safe intro!: 0"&I" GEN "→I" F0) using1by blast qed
AOT_theorem "suc-num:1": ‹[ℙ]nx → [ℕ]x› proof(rule "→I")
AOT_have ‹[[ℙ]+]0 n› by (meson Number.ψ "≡E"(1) "nnumber:3") moreover AOT_assume ‹[ℙ]nx› ultimately AOT_have ‹[[ℙ]*]0 x› using"w-ances-her:3"[unconstrain R, unvarify β, OF "pred-thm:2", THEN"→E",
OF "pred-1-1:4", unvarify x, OF "zero:2", THEN"→E", OF "&I"] by blast
AOT_hence ‹[[ℙ]+]0 x› using"assume1:5"[unvarify x, OF "zero:2", THEN"≡E"(2), OF "∨I"(1)] by blast
AOT_thus ‹[ℕ]x› by (metis "≡E"(2) "nnumber:3") qed
AOT_theorem "suc-num:2": ‹[[ℙ]*]nx → [ℕ]x› proof(rule "→I")
AOT_have ‹[[ℙ]+]0 n› using Number.ψ "≡E"(1) "nnumber:3"by blast
AOT_assume ‹[[ℙ]*]n x›
AOT_hence ‹∀F (∀z ([ℙ]nz → [F]z) & ∀x'∀y' ([ℙ]x'y' → ([F]x' → [F]y')) → [F]x)› using"assume-anc:3"[THEN"≡E"(1)] by blast
AOT_hence θ: ‹∀z ([ℙ]nz → [ℕ]z) & ∀x'∀y' ([ℙ]x'y' → ([ℕ]x' → [ℕ]y')) → [ℕ]x› using"∀E"(1) "nnumber:2"by blast
AOT_show ‹[ℕ]x› proof (safe intro!: θ[THEN"→E"] GEN "→I""&I")
AOT_show ‹[ℕ]z›if‹[ℙ]nz›for z using Number.ψ "suc-num:1" that "→E"by blast next
AOT_show ‹[ℕ]y›if‹[ℙ]xy›and‹[ℕ]x›for x y using"suc-num:1"[unconstrain n, THEN"→E"] that "→E"by blast qed qed
AOT_theorem "suc-num:3": ‹[ℙ]+nx → [ℕ]x› proof (rule "→I")
AOT_assume ‹[ℙ]+nx›
AOT_hence ‹[ℙ]*nx ∨ n =\ℙ x› by (metis "assume1:5""≡E"(1)) moreover {
AOT_assume ‹[ℙ]*nx›
AOT_hence ‹[ℕ]x› by (metis "suc-num:2""→E")
} moreover {
AOT_assume ‹n =\ℙ x›
AOT_hence ‹n = x› using"id-R-thm:3"[unconstrain R, unvarify β, OF "pred-thm:2", THEN"→E", OF "pred-1-1:4", THEN"→E"] by blast
AOT_hence ‹[ℕ]x› by (metis "rule=E" Number.ψ)
} ultimately AOT_show ‹[ℕ]x› by (metis "∨E"(3) "reductio-aa:1") qed
AOT_theorem "pred-num": ‹[ℙ]xn → [ℕ]x› proof (rule "→I")
AOT_assume 0: ‹[ℙ]xn›
AOT_have ‹[[ℙ]+]0 n› using Number.ψ "≡E"(1) "nnumber:3"by blast
AOT_hence ‹[[ℙ]*]0 n ∨ 0 =\ℙ n› using"assume1:5"[unvarify x, OF "zero:2"] by (metis "≡E"(1)) moreover {
AOT_assume ‹0 =\ℙ n›
AOT_hence ‹∃z ([ℙ]0z & [ℙ]nz)› using"assume1:2"[unvarify x, OF "zero:2", THEN"≡E"(1)] by blast then AOT_obtain a where ‹[ℙ]0a & [ℙ]na›using"∃E"[rotated] by blast
AOT_hence ‹0 = n› using"pred-1-1:3"[THEN"df-1-1:1"[THEN"≡dfE"], THEN"&E"(2), THEN"∀E"(1), OF "zero:2", THEN"∀E"(2), THEN"∀E"(2), THEN"→E"] by blast
AOT_hence ‹[ℙ]x 0› using0"rule=E" id_sym by fast
AOT_hence ‹∃x [ℙ]x 0› by (rule "∃I")
AOT_hence ‹∃x [ℙ]x 0 & ¬∃x [ℙ]x 0› by (metis "no-pred-0:1""raa-cor:3")
} ultimately AOT_have ‹[[ℙ]*]0n› by (metis "∨E"(3) "raa-cor:1")
AOT_hence ‹∃z ([[ℙ]+]0z & [ℙ]zn)› using"w-ances-her:7"[unconstrain R, unvarify β, OF "pred-thm:2", THEN"→E", OF "pred-1-1:4", unvarify x,
OF "zero:2", THEN"→E"] by blast then AOT_obtain b where b_prop: ‹[[ℙ]+]0b & [ℙ]bn› using"∃E"[rotated] by blast
AOT_hence ‹[ℕ]b› by (metis "&E"(1) "≡E"(2) "nnumber:3") moreover AOT_have ‹x = b› using"pred-1-1:3"[THEN"df-1-1:1"[THEN"≡dfE"], THEN"&E"(2), THEN"∀E"(2), THEN"∀E"(2), THEN"∀E"(2), THEN"→E",
OF "&I", OF 0, OF b_prop[THEN"&E"(2)]]. ultimately AOT_show ‹[ℕ]x› using"rule=E" id_sym by fast qed
AOT_theorem "nat-card": ‹[ℕ]x → NaturalCardinal(x)› proof(rule "→I")
AOT_assume ‹[ℕ]x›
AOT_hence ‹[[ℙ]+]0x› by (metis "≡E"(1) "nnumber:3")
AOT_hence ‹[[ℙ]*]0x ∨ 0 =\ℙ x› using"assume1:5"[unvarify x, OF "zero:2", THEN"≡E"(1)] by blast moreover {
AOT_assume ‹[[ℙ]*]0x› then AOT_obtain a where ‹[ℙ]ax› using"anc-her:5"[unvarify R x, OF "zero:2", OF "pred-thm:2", THEN"→E"] "∃E"[rotated] by blast
AOT_hence ‹∃F∃u ([F]u & Numbers(x,F) & Numbers(a,[F]-u))› using"pred-thm:3"[THEN"≡E"(1)] by blast then AOT_obtain F where ‹∃u ([F]u & Numbers(x,F) & Numbers(a,[F]-u))› using"∃E"[rotated] by blast then AOT_obtain u where ‹[F]u & Numbers(x,F) & Numbers(a,[F]-u)› using"Ordinary.∃E"[rotated] by meson
AOT_hence ‹NaturalCardinal(x)› using"eq-num:6"[THEN"→E"] "&E"by blast
} moreover {
AOT_assume ‹0 =\ℙ x›
AOT_hence ‹0 = x› using"id-R-thm:3"[unconstrain R, unvarify β, OF "pred-thm:2", THEN"→E", OF "pred-1-1:4", unvarify x,
OF "zero:2", THEN"→E"] by blast
AOT_hence ‹NaturalCardinal(x)› by (metis "rule=E""zero-card")
} ultimately AOT_show ‹NaturalCardinal(x)› by (metis "∨E"(2) "raa-cor:1") qed
AOT_theorem "pred-func:1": ‹[ℙ]xy & [ℙ]xz → y = z› proof (rule "→I"; frule "&E"(1); drule "&E"(2))
AOT_assume ‹[ℙ]xy›
AOT_hence ‹∃F∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))› using"pred-thm:3"[THEN"≡E"(1)] by blast then AOT_obtain F where ‹∃u ([F]u & Numbers(y,F) & Numbers(x,[F]-u))› using"∃E"[rotated] by blast then AOT_obtain a where
Oa: ‹O!a› and a_prop: ‹[F]a & Numbers(y,F) & Numbers(x,[F]-a)› using"∃E"[rotated] "&E"by blast
AOT_assume ‹[ℙ]xz›
AOT_hence ‹∃F∃u ([F]u & Numbers(z,F) & Numbers(x,[F]-u))› using"pred-thm:3"[THEN"≡E"(1)] by blast then AOT_obtain G where ‹∃u ([G]u & Numbers(z,G) & Numbers(x,[G]-u))› using"∃E"[rotated] by blast then AOT_obtain b where Ob: ‹O!b› and b_prop: ‹[G]b & Numbers(z,G) & Numbers(x,[G]-b)› using"∃E"[rotated] "&E"by blast
AOT_have ‹[F]-a≈E [G]-b› using"num-tran:2"[unvarify G H, OF "F-u[den]", OF "F-u[den]", THEN"→E", OF "&I", OF a_prop[THEN"&E"(2)],
OF b_prop[THEN"&E"(2)]].
AOT_hence ‹F ≈E G› using"P'-eq"[unconstrain u, THEN"→E", OF Oa, unconstrain v, THEN"→E",
OF Ob, THEN"→E", OF "&I", OF "&I"]
a_prop[THEN"&E"(1), THEN"&E"(1)]
b_prop[THEN"&E"(1), THEN"&E"(1)] by blast
AOT_thus ‹y = z› using"pre-Hume"[THEN"→E", THEN"≡E"(2), OF "&I",
OF a_prop[THEN"&E"(1), THEN"&E"(2)],
OF b_prop[THEN"&E"(1), THEN"&E"(2)]] by blast qed
AOT_theorem "pred-func:2": ‹[ℙ]nm & [ℙ]nk → m = k› using"pred-func:1".
AOT_theorem being_number_of_den: ‹[λx x = #G]↓› proof (rule "safe-ext"[axiom_inst, THEN"→E"]; safe intro!: "&I" GEN RN)
AOT_show ‹[λx Numbers(x,[λz \A[G]z])]↓› by (rule numbers_prop_den[unvarify G]) "cqt:2[lambda]" next
AOT_modally_strict {
AOT_show ‹Numbers(x,[λz \A[G]z]) ≡ x = #G›for x using"eq-num:2".
} qed
axiomatization ψ_nat :: ‹ψ → nat› where ψ_nat: ‹surj ψ_nat› text‹Unfortunately, since the axiom requires the type @{typ ψ}
to have an infinite domain, @{command nitpick} can only find a potential model
and no genuine model.
However, since we could trivially choose @{typ ψ} as a copy of @{typ nat},
we can still be assured that above axiom is consistent.› lemma‹True› nitpick[satisfy, user_axioms, card nat=1, expect = potential] ..
AOT_axiom "modal-axiom": ‹∃x([ℕ]x & x = #G) →♢∃y([E!]y & ∀u (\A[G]u → u ≠E y))› proof(rule AOT_model_axiomI) AOT_modally_strict { text‹The actual extension on the ordinary objects of a property is the
set of ordinary urelements that exemplifies the property in the
designated actual world.› define act_ψext :: ‹<\<kappa>> → ψ set› where ‹act_ψext ≡ λ Π . {x :: ψ . [w0⊨ [Π]«ψκ x¬]}› text‹Encoding a property with infinite actual extension on the ordinary objects
denotes a property by extended relation comprehension.›
AOT_have enc_finite_act_ψext_den: ‹\⊨\◻ [λx ∃F(¬«ε\o w. finite (act_ψext F)¬ & x[F])]↓› proof(safe intro!: Comprehension_1[THEN"→E"] RN GEN "→I")
AOT_modally_strict { fix F G
AOT_assume ‹◻G ≡E F›
AOT_hence ‹\AG ≡E F› using"nec-imp-act"[THEN"→E"] by blast
AOT_hence ‹\A(G↓ & F↓ & ∀u([G]u ≡ [F]u))› by (AOT_subst_def (reverse) eqE) hence‹[w0⊨ [G]«ψκ x¬] = [w0⊨ [F]«ψκ x¬]›for x by (auto dest!: "∀E"(1) "→E"
simp: AOT_model_denotes_κ_def AOT_sem_denotes AOT_sem_conj
AOT_model_ψκ_ordinary AOT_sem_act AOT_sem_equiv)
AOT_thus ‹¬«ε\o w. finite (act_ψext (AOT_term_of_var F))¬≡ ¬«ε\o w. finite (act_ψext (AOT_term_of_var G))¬› by (simp add: AOT_sem_not AOT_sem_equiv act_ψext_def
AOT_model_proposition_choice_simp)
} qed text‹By coexistence, encoding only properties with finite actual extension
on the ordinary objects denotes.›
AOT_have ‹[λx ∀F(x[F] →«ε\o w. finite (act_ψext F)¬)]↓› proof(rule "safe-ext"[axiom_inst, THEN"→E"]; safe intro!: "&I" RN GEN)
AOT_show ‹[λx ¬[λx ∃F(¬«ε\o w. finite (act_ψext F)¬ & x[F])]x]↓› by"cqt:2" next
AOT_modally_strict { fix x
AOT_show ‹¬[λx ∃F (¬«ε\o w. finite (act_ψext F)¬ & x[F])]x ≡ ∀F(x[F] →«ε\o w. finite (act_ψext F)¬)› by (AOT_subst ‹[λx ∃F (¬«ε\o w. finite (act_ψext F)¬ & x[F])]x› ‹∃F (¬«ε\o w. finite (act_ψext F)¬ & x[F])›;
(rule "beta-C-meta"[THEN"→E"])?)
(auto simp: enc_finite_act_ψext_den AOT_sem_equiv AOT_sem_not
AOT_sem_forall AOT_sem_imp AOT_sem_conj AOT_sem_exists)
} qed text‹We show by induction that any property encoded by a natural number
has a finite actual extension on the ordinary objects.›
AOT_hence ‹[λx ∀F(x[F] →«ε\o w. finite (act_ψext F)¬)]n›for n proof(rule induction[THEN"∀E"(1), THEN"→E", THEN"Number.∀E"];
safe intro!: "&I""Number.GEN""β←C""zero:2""→I""cqt:2"
dest!: "β→C")
AOT_show ‹∀F(0[F] →«ε\o w. finite (act_ψext F)¬)› proof(safe intro!: GEN "→I") fix F
AOT_assume ‹0[F]›
AOT_actually {
AOT_hence ‹¬∃u [F]u› using"zero=:2""intro-elim:3:a" AOT_sem_enc_nec by blast
AOT_hence ‹∀x ¬(O!x & [F]x)› using"cqt-further:4""vdash-properties:10"by blast hence‹¬([w0⊨ [F]«ψκ x¬])›for x by (auto dest!: "∀E"(1)[where τ=‹ψκ x›]
simp: AOT_sem_not AOT_sem_conj AOT_model_ψκ_ordinary "russell-axiom[exe,1].ψ_denotes_asm")
}
AOT_thus ‹«ε\o w. finite (act_ψext (AOT_term_of_var F))¬› by (auto simp: AOT_model_proposition_choice_simp act_ψext_def) qed next fix n m
AOT_assume ‹[ℙ]nm›
AOT_hence ‹∃F∃u ([F]u & Numbers(m,F) & Numbers(n,[F]-u))› using"pred-thm:3"[THEN"≡E"(1)] by blast then AOT_obtain G where ‹∃u ([G]u & Numbers(m,G) & Numbers(n,[G]-u))› using"∃E"[rotated] by blast then AOT_obtain u where 0: ‹[G]u & Numbers(m,G) & Numbers(n,[G]-u)› using"Ordinary.∃E"[rotated] by meson
AOT_assume n_prop: ‹∀F(n[F] →«ε\o w. finite (act_ψext F)¬)›
AOT_show ‹∀F(m[F] →«ε\o w. finite (act_ψext F)¬)› proof(safe intro!: GEN "→I") fix F
AOT_assume ‹m[F]›
AOT_hence 1: ‹[λx \A[F]x] ≈E G› using0[THEN"&E"(1), THEN"&E"(2), THEN numbers[THEN"≡dfE"], THEN"&E"(2), THEN"∀E"(2), THEN"≡E"(1)] by auto
AOT_show ‹«ε\o w. finite (act_ψext (AOT_term_of_var F))¬› proof(rule "raa-cor:1")
AOT_assume ‹¬«ε\o w. finite (act_ψext (AOT_term_of_var F))¬› hence inf: ‹infinite (act_ψext (AOT_term_of_var F))› by (auto simp: AOT_sem_not AOT_model_proposition_choice_simp) then AOT_obtain v where act_F_v: ‹\A[F]v› unfolding AOT_sem_act act_ψext_def by (metis AOT_term_of_var_cases AOT_model_ψκ_ordinary
AOT_model_denotes_κ_def Ordinary.Rep_cases κ.disc(7)
mem_Collect_eq not_finite_existsD)
AOT_hence ‹[λx \A[F]x]v› by (safe intro!: "β←C""cqt:2")
AOT_hence ‹[λx \A[F]x]-v≈E [G]-u› by (safe intro!: eqP'[unvarify F, THEN"→E"] "&I""cqt:2"1 0[THEN"&E"(1), THEN"&E"(1)]) moreover AOT_have ‹[λx \A[F]x]-v≈E [λx \A[λy [F]y & y ≠E v]x]› proof(safe intro!: "apE-eqE:1"[unvarify F G, THEN"→E"] "cqt:2" "F-u[den]"[unvarify F] eqE[THEN"≡dfI"] "&I"
Ordinary.GEN) fix u
AOT_have ‹[λx [λx \A[F]x]x & x ≠E v]u ≡ [λx \A[F]x]u & u style='font-size: 18px;'>≠E v› by (safe intro!: "beta-C-meta"[THEN"→E"] "cqt:2") also AOT_have ‹[λx \A[F]x]u & u ≠E v ≡\A[F]u & u 'font-size: 18px;'>≠E v› by (AOT_subst ‹[λx \A[F]x]u›‹\A[F]u›)
(safe intro!: "beta-C-meta"[THEN"→E"] "cqt:2" "oth-class-taut:3:a") also AOT_have ‹\A[F]u & u ≠E v ≡\A([F]u & u ≠E v)› using"id-act2:2" AOT_sem_conj AOT_sem_equiv AOT_sem_act by auto also AOT_have ‹\A([F]u & u ≠E v) ≡\A[λy [F]y & y 'font-size: 18px;'>≠E v]u› by (AOT_subst ‹[λy [F]y & y ≠E v]u›‹[F]u & u ≠E v›)
(safe intro!: "beta-C-meta"[THEN"→E"] "cqt:2" "oth-class-taut:3:a") also AOT_have ‹\A[λy [F]y & y ≠E v]u ≡ [λx \A[λy [F]y & y style='font-size: 18px;'>≠E v]x]u› by (safe intro!: "beta-C-meta"[THEN"→E", symmetric] "cqt:2") finally AOT_show ‹[[λx \A[F]x]-v]u ≡ [λx \A[λy [F]y & y ≠Ev]x]u› by (auto intro!: "cqt:2"
intro: "rule-id-df:2:b"[OF "F-u", where τ1τn=‹(_,_)›, simplified]) qed ultimately AOT_have ‹[λx \A[λy [F]y & y ≠E v]x] ≈E [G]-u› using"eq-part:2[terms]""eq-part:3[terms]""→E"by blast
AOT_hence ‹n[λy [F]y & y ≠E v]› by (safe intro!: 0[THEN"&E"(2), THEN numbers[THEN"≡dfE"], THEN"&E"(2), THEN"∀E"(1), THEN"≡E"(2)] "cqt:2") hence finite: ‹finite (act_ψext «[λy [F]y & y ≠E v]¬)› by (safe intro!: n_prop[THEN"∀E"(1), THEN"→E",
simplified AOT_model_proposition_choice_simp] "cqt:2") obtain y where y_def: ‹ψκ y = AOT_term_of_var (Ordinary.Rep v)› by (metis AOT_model_ordinary_ψκ Ordinary.restricted_var_condition)
AOT_actually { fix x
AOT_assume ‹[λy [F]y & y ≠E v]«ψκ x¬›
AOT_hence ‹[F]«ψκ x¬› by (auto dest!: "β→C""&E"(1))
} moreover AOT_actually {
AOT_have ‹[F]«ψκ y¬› unfolding y_def using act_F_v AOT_sem_act by blast
} moreover AOT_actually { fix x assume noteq: ‹x ≠ y›
AOT_assume ‹[F]«ψκ x¬› moreover AOT_have ψκ_x_den: ‹«ψκ x¬↓› using AOT_sem_exe calculation by blast moreover {
AOT_have ‹¬(«ψκ x¬ =E v)› proof(rule "raa-cor:2")
AOT_assume ‹«ψκ x¬ =E v›
AOT_hence ‹«ψκ x¬ = v› using"=E-simple:2"[unvarify x, THEN"→E", OF ψκ_x_den] by blast hence‹ψκ x = ψκ y› unfolding y_def AOT_sem_eq by meson hence‹x = y› by blast
AOT_thus ‹p & ¬p›for p using noteq by blast qed
AOT_hence ‹«ψκ x¬≠E v› by (safe intro!: "thm-neg=E"[unvarify x, THEN"≡E"(2)] ψκ_x_den)
} ultimately AOT_have ‹[λy [F]y & y ≠E v]«ψκ x¬› by (auto intro!: "β←C""cqt:2""&I")
} ultimatelyhave‹(insert y (act_ψext «[λy [F]y & y ≠E v]¬)) =
(act_ψext (AOT_term_of_var F))› unfolding act_ψext_def by auto hence‹finite (act_ψext (AOT_term_of_var F))› using finite finite.insertI by metis
AOT_thus ‹p & ¬p›for p using inf by blast qed qed qed
AOT_hence nat_enc_finite: ‹∀F(n[F] →«ε\o w. finite (act_ψext F)¬)›for n using"β→C"(1) by blast
text‹The main proof can now generate a witness, since we required
the domain of ordinary objects to be infinite.›
AOT_show ‹∃x ([ℕ]x & x = #G) →♢∃y (E!y & ∀u (\A[G]u → u ≠E y))› proof(safe intro!: "→I")
AOT_assume ‹∃x ([ℕ]x & x = #G)› then AOT_obtain n where ‹n = #G› using"Number.∃E"[rotated] by meson
AOT_hence ‹Numbers(n,[λx \A[G]x])› using"eq-num:3""rule=E" id_sym by fast
AOT_hence ‹n[G]› by (auto intro!: numbers[THEN"≡dfE", THEN"&E"(2), THEN"∀E"(2), THEN"≡E"(2)] "eq-part:1"[unvarify F] "cqt:2")
AOT_hence ‹«ε\o w. finite (act_ψext (AOT_term_of_var G))¬› using nat_enc_finite[THEN"∀E"(2), THEN"→E"] by blast hence finite: ‹finite (act_ψext (AOT_term_of_var G))› by (auto simp: AOT_model_proposition_choice_simp)
AOT_have ‹∃u ¬\A[G]u› proof(rule "raa-cor:1")
AOT_assume ‹¬∃u ¬\A[G]u›
AOT_hence ‹∀x ¬(O!x & ¬\A[G]x)› by (metis "cqt-further:4""→E")
AOT_hence ‹\A[G]x›if‹O!x›for x using"∀E"(2) AOT_sem_conj AOT_sem_not that by blast hence‹[w0⊨ [G]«ψκ x¬]›for x by (metis AOT_term_of_var_cases AOT_model_ψκ_ordinary
AOT_model_denotes_κ_def AOT_sem_act κ.disc(7)) hence‹(act_ψext (AOT_term_of_var G)) = UNIV› unfolding act_ψext_def by auto moreoverhave‹infinite (UNIV::ψ set)› by (metis ψ_nat finite_imageI infinite_UNIV_char_0) ultimatelyhave‹infinite (act_ψext (AOT_term_of_var G))› by simp
AOT_thus ‹p & ¬p›for p using finite by blast qed then AOT_obtain x where x_prop: ‹O!x & ¬\A[G]x› using"∃E"[rotated] by blast
AOT_hence ‹♢E!x› by (metis "betaC:1:a""con-dis-i-e:2:a" AOT_sem_ordinary) moreover AOT_have ‹◻∀u (\A[G]u → u ≠E x)› proof(safe intro!: RN GEN "→I")
AOT_modally_strict { fix y
AOT_assume ‹O!y›
AOT_assume 0: ‹\A[G]y›
AOT_show ‹y ≠E x› proof (safe intro!: "thm-neg=E"[THEN"≡E"(2)] "raa-cor:2")
AOT_assume ‹y =E x›
AOT_hence ‹y = x› by (metis "=E-simple:2""vdash-properties:10") hence‹y = x› by (simp add: AOT_sem_eq AOT_term_of_var_inject)
AOT_hence ‹¬\A[G]y› using x_prop "&E" AOT_sem_not AOT_sem_act by metis
AOT_thus ‹\A[G]y & ¬\A[G]y› using0"&I"by blast qed
} qed ultimately AOT_have ‹♢(∀u (\A[G]u → u ≠E x) & E!x)› using"KBasic:16"[THEN"→E", OF "&I"] by blast
AOT_hence ‹♢(E!x & ∀u (\A[G]u → u ≠E x))› by (AOT_subst ‹E!x & ∀u (\A[G]u → u ≠E x)›‹∀u (\A[G]u → u ≠E x) & E!x›)
(auto simp: "oth-class-taut:2:a")
AOT_hence ‹∃y ♢(E!y & ∀u (\A[G]u → u ≠E y))› using"∃I"by fast
AOT_thus ‹♢∃y (E!y & ∀u (\A[G]u → u ≠E y))› using"CBF♢"[THEN"→E"] by fast qed
} qed
AOT_theorem "modal-lemma": ‹♢∀u(\A[G]u → u ≠E v) →∀u(\A[G]u → u ≠E v)› proof(safe intro!: "→I" Ordinary.GEN)
AOT_modally_strict { fix u
AOT_assume act_Gu: ‹\A[G]u›
AOT_have ‹∀u (\A[G]u → u ≠E v) → u ≠E v› proof(rule "→I")
AOT_assume ‹∀u (\A[G]u → u ≠E v)›
AOT_hence ‹\A[G]u → u ≠E v› using"Ordinary.∀E"by fast
AOT_thus ‹u ≠E v› using act_Gu "→E"by blast qed
} note0 = this
AOT_have θ: ‹◻(∀u (\A[G]u → u ≠E v) → u ≠E v)›if‹◻\A[G]u›for u proof -
AOT_have ‹◻\A[G]u →◻(∀u (\A[G]u → u ≠E v) → u ≠E v)› apply (rule RM) using0"&E""→I"by blast thus ?thesis using that "→E"by blast qed fix u
AOT_assume 1: ‹♢∀u(\A[G]u → u ≠E v)›
AOT_assume ‹\A[G]u›
AOT_hence ‹◻\A[G]u› by (metis "Act-Basic:6""≡E"(1))
AOT_hence ‹◻(∀u (\A[G]u → u ≠E v) → u ≠E v)› using Ordinary.ψ θ by blast
AOT_hence ‹♢u ≠E v› using1"K♢"[THEN"→E", THEN"→E"] by blast
AOT_thus ‹u ≠E v› by (metis "id-nec4:2""≡E"(1)) qed
AOT_theorem "th-succ": ‹∀n∃!m [ℙ]nm› proof(safe intro!: Number.GEN "→I""uniqueness:1"[THEN"≡dfI"]) fix n
AOT_have ‹NaturalCardinal(n)› by (metis "nat-card" Number.ψ "→E")
AOT_hence ‹∃G(n = #G)› by (metis "≡dfE" card) then AOT_obtain G where n_num_G: ‹n = #G› using"∃E"[rotated] by blast
AOT_hence ‹∃n (n = #G)› by (rule "Number.∃I")
AOT_hence ‹♢∃y ([E!]y & ∀u(\A[G]u → u ≠E y))› using"modal-axiom"[axiom_inst, THEN"→E"] by blast
AOT_hence ‹∃y ♢([E!]y & ∀u(\A[G]u → u ≠E y))› using"BF♢"[THEN"→E"] by auto then AOT_obtain y where ‹♢([E!]y & ∀u(\A[G]u → u ≠E y))› using"∃E"[rotated] by blast
AOT_hence ‹♢E!y›and2: ‹♢∀u(\A[G]u → u ≠E y)› using"KBasic2:3""&E""→E"by blast+
AOT_hence Oy: ‹O!y› by (auto intro!: "β←C"(1) "cqt:2" intro: AOT_ordinary[THEN"=dfI"(2)])
AOT_have 0: ‹∀u(\A[G]u → u ≠E y)› using2"modal-lemma"[unconstrain v, THEN"→E", OF Oy, THEN"→E"] by simp
AOT_have 1: ‹[λx \A[G]x ∨ x =E y]↓› by"cqt:2"
AOT_obtain b where b_prop: ‹Numbers(b, [λx \A[G]x ∨ x =E y])› using"num:1"[unvarify G, OF 1] "∃E"[rotated] by blast
AOT_have Pnb: ‹[ℙ]nb› proof(safe intro!: "pred-thm:3"[THEN"≡E"(2)] "∃I"(1)[where τ=‹«[λx \A[G]x ∨ x =E y]¬›] 1"∃I"(2)[where β=y] "&I" Oy b_prop)
AOT_show ‹[λx \A[G]x ∨ x =E y]y› by (auto intro!: "β←C"(1) "cqt:2""∨I"(2) "ord=Eequiv:1"[THEN"→E", OF Oy]) next
AOT_have equinum: ‹[λx \A[G]x ∨ x =E y]-y≈E [λx \A[G]x]› proof(rule "apE-eqE:1"[unvarify F G, THEN"→E"];
("cqt:2[lambda]" | rule "F-u[den]"[unvarify F]; "cqt:2[lambda]")?)
AOT_show ‹[λx \A[G]x ∨ x =E y]-y≡E [λx \A[G]x]› proof (safe intro!: eqE[THEN"≡dfI"] "&I""F-u[den]"[unvarify F]
Ordinary.GEN "→I"; "cqt:2"?) fix u
AOT_have ‹[[λx \A[G]x ∨ [(=E)]xy]-y]u ≡ ([λx \A[G]x ∨ x =E y]u) & u ≠E y› apply (rule "F-u"[THEN"=dfI"(1)[where τ1τn=‹(_,_)›], simplified]; "cqt:2"?) by (rule "beta-C-cor:2"[THEN"→E", THEN"∀E"(2)]; "cqt:2") also AOT_have ‹…≡ (\A[G]u ∨ u =E y) & u ≠E y› apply (AOT_subst ‹[λx \A[G]x ∨ [(=E)]xy]u›‹\A[G]u ∨ u =E y›) apply (rule "beta-C-cor:2"[THEN"→E", THEN"∀E"(2)]; "cqt:2") using"oth-class-taut:3:a"by blast also AOT_have ‹…≡\A[G]u› proof(safe intro!: "≡I""→I")
AOT_assume ‹(\A[G]u ∨ u =E y) & u ≠E y›
AOT_thus ‹\A[G]u› by (metis "&E"(1) "&E"(2) "∨E"(3) "≡E"(1) "thm-neg=E") next
AOT_assume ‹\A[G]u›
AOT_hence ‹u ≠E y›and‹\A[G]u ∨ u =E y› using0[THEN"∀E"(2), THEN"→E", OF Ordinary.ψ, THEN"→E"] "∨I"by blast+
AOT_thus ‹(\A[G]u ∨ u =E y) & u ≠E y› using"&I"by simp qed also AOT_have ‹…≡ [λx \A[G]x]u› by (rule "beta-C-cor:2"[THEN"→E", THEN"∀E"(2), symmetric]; "cqt:2") finally AOT_show ‹[[λx \A[G]x ∨ [(=E)]xy]-y]u ≡ [λx \A[G]x]u›. qed qed
AOT_have 2: ‹[λx \A[G]x]↓›by"cqt:2[lambda]"
AOT_show ‹Numbers(n,[λx \A[G]x ∨ x =E y]-y)› using"num-tran:1"[unvarify G H, OF 2, OF "F-u[den]"[unvarify F, OF 1], THEN"→E", OF equinum, THEN"≡E"(2),
OF "eq-num:2"[THEN"≡E"(2), OF n_num_G]]. qed
AOT_show ‹∃α ([ℕ]α & [ℙ]nα & ∀β ([ℕ]β & [ℙ]nβ → β = α))› proof(safe intro!: "∃I"(2)[where β=b] "&I" Pnb "→I" GEN)
AOT_show ‹[ℕ]b›using"suc-num:1"[THEN"→E", OF Pnb]. next fix y
AOT_assume 0: ‹[ℕ]y & [ℙ]ny›
AOT_show ‹y = b› apply (rule "pred-func:1"[THEN"→E"]) using0[THEN"&E"(2)] Pnb "&I"by blast qed qed
(* Note the use of a bold '. *)
AOT_define Successor :: ‹τ → κs› (‹_''› [100] 100) "def-suc": ‹n' =df\ιm([ℙ]nm)›
text‹Note: not explicitly in PLM›
AOT_theorem "def-suc[den1]": ‹\ιm([ℙ]nm)↓› using"A-Exists:2""RA[2]""≡E"(2) "th-succ"[THEN"Number.∀E"] by blast text‹Note: not explicitly in PLM›
AOT_theorem "def-suc[den2]": shows‹n'↓› by (rule "def-suc"[THEN"=dfI"(1)])
(auto simp: "def-suc[den1]")
(* TODO: not in PLM *)
AOT_theorem suc_eq_desc: ‹n' = \ιm([ℙ]nm)› by (rule "def-suc"[THEN"=dfI"(1)])
(auto simp: "def-suc[den1]""rule=I:1")
AOT_theorem "suc-fact": ‹n = m → n' = m'› proof (rule "→I")
AOT_assume 0: ‹n = m›
AOT_show ‹n' = m'› apply (rule "rule=E"[rotated, OF 0]) by (rule "=I"(1)[OF "def-suc[den2]"]) qed
AOT_theorem "ind-gnd": ‹m = 0 ∨∃n(m = n')› proof -
AOT_have ‹[[ℙ]+]0m› using Number.ψ "≡E"(1) "nnumber:3"by blast
AOT_hence ‹[[ℙ]*]0m ∨ 0 =\ℙ m› using"assume1:5"[unvarify x, OF "zero:2", THEN"≡E"(1)] by blast moreover {
AOT_assume ‹[[ℙ]*]0m›
AOT_hence ‹∃z ([[ℙ]+]0z & [ℙ]zm)› using"w-ances-her:7"[unconstrain R, unvarify β x, OF "zero:2",
OF "pred-thm:2", THEN"→E", OF "pred-1-1:4", THEN"→E"] by blast then AOT_obtain z where θ: ‹[[ℙ]+]0z›and ξ: ‹[ℙ]zm› using"&E""∃E"[rotated] by blast
AOT_have Nz: ‹[ℕ]z› using θ "≡E"(2) "nnumber:3"by blast moreover AOT_have ‹m = z'› proof (rule "def-suc"[THEN"=dfI"(1)];
safe intro!: "def-suc[den1]"[unconstrain n, THEN"→E", OF Nz] "nec-hintikka-scheme"[THEN"≡E"(2)] "&I"
GEN "→I""Act-Basic:2"[THEN"≡E"(2)])
AOT_show ‹\A[ℕ]m›using Number.ψ by (meson "mod-col-num:1""nec-imp-act""→E") next
AOT_show ‹\A[ℙ]zm›using ξ by (meson "nec-imp-act""pred-1-1:1""→E") next fix y
AOT_assume ‹\A([ℕ]y & [ℙ]zy)›
AOT_hence ‹\A[ℕ]y›and‹\A[ℙ]zy› using"Act-Basic:2""&E""≡E"(1) by blast+
AOT_hence 0: ‹[ℙ]zy› by (metis RN "≡E"(1) "pred-1-1:1""sc-eq-fur:2""→E")
AOT_thus ‹y = m› using"pred-func:1"[THEN"→E", OF "&I"] ξ by metis qed ultimately AOT_have ‹[ℕ]z & m = z'› by (rule "&I")
AOT_hence ‹∃n m = n'› by (rule "∃I") hence ?thesis by (rule "∨I")
} moreover {
AOT_assume ‹0 =\ℙ m›
AOT_hence ‹0 = m› using"id-R-thm:3"[unconstrain R, unvarify β x, OF "zero:2", OF "pred-thm:2", THEN"→E", OF "pred-1-1:4", THEN"→E"] by auto hence ?thesis using id_sym "∨I"by blast
} ultimatelyshow ?thesis by (metis "∨E"(2) "raa-cor:1") qed
AOT_theorem "suc-thm": ‹[ℙ]n n'› proof -
AOT_obtain x where m_is_n: ‹x = n'› using"free-thms:1"[THEN"≡E"(1), OF "def-suc[den2]"] using"∃E"by metis
AOT_have ‹\A([ℕ]n' & [ℙ]n n')› apply (rule "rule=E"[rotated, OF suc_eq_desc[symmetric]]) apply (rule "actual-desc:4"[THEN"→E"]) by (simp add: "def-suc[den1]")
AOT_hence ‹\A[ℕ]n'›and‹\A[ℙ]n n'› using"Act-Basic:2""≡E"(1) "&E"by blast+
AOT_hence ‹\A[ℙ]nx› using m_is_n[symmetric] "rule=E"by fast+
AOT_hence ‹[ℙ]nx› by (metis RN "≡E"(1) "pred-1-1:1""sc-eq-fur:2""→E") thus ?thesis using m_is_n "rule=E"by fast qed
AOT_theorem "prec-facts:1": ‹[ℙ]0 1› by (auto intro: "numerals:1"[THEN"rule-id-df:2:b[zero]",
OF "def-suc[den2]"[unconstrain n, unvarify β,
OF "zero:2", THEN"→E", OF "0-n"]] "suc-thm"[unconstrain n, unvarify β, OF "zero:2", THEN"→E", OF "0-n"])
AOT_theorem "inf-card-exist:2": ‹Infinite(#O!)› proof (safe intro!: "inf-card:2"[THEN"≡dfI"] "&I""inf-card-exist:1")
AOT_show ‹¬Finite(#O!)› proof(rule "raa-cor:2")
AOT_assume ‹Finite(#O!)›
AOT_hence 0: ‹[ℕ]#O!› using"inf-card:1"[THEN"≡dfE"] "&E"(2) by blast
AOT_have ‹Numbers(#O!, [λz \AO!z])› using"eq-num:3"[unvarify G, OF "oa-exist:1"].
AOT_hence ‹#O! = #O!› using"eq-num:2"[unvarify x G, THEN"≡E"(1), OF "oa-exist:1",
OF "num-def:2"[unvarify G], OF "oa-exist:1"] by blast
AOT_hence ‹[ℕ]#O! & #O! = #O!› using0"&I"by blast
AOT_hence ‹∃x ([ℕ]x & x = #O!)› using"num-def:2"[unvarify G, OF "oa-exist:1"] "∃I"(1) by fast
AOT_hence ‹♢∃y ([E!]y & ∀u (\A[O!]u → u ≠E y))› using"modal-axiom"[axiom_inst, unvarify G, THEN"→E", OF "oa-exist:1"] by blast
AOT_hence ‹∃y ♢([E!]y & ∀u (\A[O!]u → u ≠E y))› using"BF♢"[THEN"→E"] by blast then AOT_obtain b where ‹♢([E!]b & ∀u (\A[O!]u → u ≠E b))› using"∃E"[rotated] by blast
AOT_hence ‹♢[E!]b›and2: ‹♢∀u (\A[O!]u → u ≠E b)› using"KBasic2:3"[THEN"→E"] "&E"by blast+
AOT_hence ‹[λx ♢[E!]x]b› by (auto intro!: "β←C"(1) "cqt:2") moreover AOT_have ‹O! = [λx ♢[E!]x]› by (rule "rule-id-df:1[zero]"[OF "oa:1"]) "cqt:2" ultimately AOT_have b_ord: ‹O!b› using"rule=E" id_sym by fast
AOT_hence ‹\AO!b› by (meson "≡E"(1) "oa-facts:7") moreover AOT_have 2: ‹∀u (\A[O!]u → u ≠E b)› using"modal-lemma"[unvarify G, unconstrain v, OF "oa-exist:1", THEN"→E", OF b_ord, THEN"→E", OF 2]. ultimately AOT_have ‹b ≠E b› using"Ordinary.∀E"[OF 2, unconstrain α, THEN"→E",
OF b_ord, THEN"→E"] by blast
AOT_hence ‹¬(b =E b)› by (metis "≡E"(1) "thm-neg=E") moreover AOT_have ‹b =E b› using"ord=Eequiv:1"[THEN"→E", OF b_ord]. ultimately AOT_show ‹p & ¬p›for p by (metis "raa-cor:3") qed qed
(*<*) end (*>*)
Messung V0.5 in Prozent
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.771Bemerkung:
(vorverarbeitet am 2026-09-07)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
