# Theory AOT_Axioms

```(*<*)
theory AOT_Axioms
imports AOT_Definitions
begin
(*>*)

section‹Axioms of PLM›

AOT_axiom "pl:1": ‹φ → (ψ → φ)›
by (auto simp: AOT_sem_imp AOT_model_axiomI)
AOT_axiom "pl:2": ‹(φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))›
by (auto simp: AOT_sem_imp AOT_model_axiomI)
AOT_axiom "pl:3": ‹(¬φ → ¬ψ) → ((¬φ → ψ) → φ)›
by (auto simp: AOT_sem_imp AOT_sem_not AOT_model_axiomI)

AOT_axiom "cqt:1": ‹∀α φ{α} → (τ↓ → φ{τ})›
by (auto simp: AOT_sem_denotes AOT_sem_forall AOT_sem_imp AOT_model_axiomI)

AOT_axiom "cqt:2[const_var]": ‹α↓›
using AOT_sem_vars_denote by (rule AOT_model_axiomI)
AOT_axiom "cqt:2[lambda]":
assumes ‹INSTANCE_OF_CQT_2(φ)›
shows ‹[λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]↓›
by (auto intro!: AOT_model_axiomI AOT_sem_cqt_2[OF assms])
AOT_axiom "cqt:2[lambda0]":
shows ‹[λ φ]↓›
by (auto intro!: AOT_model_axiomI
simp: AOT_sem_lambda_denotes "existence:3"[unfolded AOT_model_equiv_def])

AOT_axiom "cqt:3": ‹∀α (φ{α} → ψ{α}) → (∀α φ{α} → ∀α ψ{α})›
by (simp add: AOT_sem_forall AOT_sem_imp AOT_model_axiomI)
AOT_axiom "cqt:4": ‹φ → ∀α φ›
by (simp add: AOT_sem_forall AOT_sem_imp AOT_model_axiomI)
AOT_axiom "cqt:5:a": ‹[Π]κ⇩1...κ⇩n → (Π↓ & κ⇩1...κ⇩n↓)›
by (simp add: AOT_sem_conj AOT_sem_denotes AOT_sem_exe
AOT_sem_imp AOT_model_axiomI)
AOT_axiom "cqt:5:a[1]": ‹[Π]κ → (Π↓ & κ↓)›
using "cqt:5:a" AOT_model_axiomI by blast
AOT_axiom "cqt:5:a[2]": ‹[Π]κ⇩1κ⇩2 → (Π↓ & κ⇩1↓ & κ⇩2↓)›
by (rule AOT_model_axiomI)
(metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes AOT_sem_exe
AOT_sem_imp case_prodD)
AOT_axiom "cqt:5:a[3]": ‹[Π]κ⇩1κ⇩2κ⇩3 → (Π↓ & κ⇩1↓ & κ⇩2↓ & κ⇩3↓)›
by (rule AOT_model_axiomI)
(metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes AOT_sem_exe
AOT_sem_imp case_prodD)
AOT_axiom "cqt:5:a[4]": ‹[Π]κ⇩1κ⇩2κ⇩3κ⇩4 → (Π↓ & κ⇩1↓ & κ⇩2↓ & κ⇩3↓ & κ⇩4↓)›
by (rule AOT_model_axiomI)
(metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes AOT_sem_exe
AOT_sem_imp case_prodD)
AOT_axiom "cqt:5:b": ‹κ⇩1...κ⇩n[Π] → (Π↓ & κ⇩1...κ⇩n↓)›
using AOT_sem_enc_denotes
by (auto intro!: AOT_model_axiomI simp: AOT_sem_conj AOT_sem_denotes AOT_sem_imp)+
AOT_axiom "cqt:5:b[1]": ‹κ[Π] → (Π↓ & κ↓)›
using "cqt:5:b" AOT_model_axiomI by blast
AOT_axiom "cqt:5:b[2]": ‹κ⇩1κ⇩2[Π] → (Π↓ & κ⇩1↓ & κ⇩2↓)›
by (rule AOT_model_axiomI)
(metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes
AOT_sem_enc_denotes AOT_sem_imp case_prodD)
AOT_axiom "cqt:5:b[3]": ‹κ⇩1κ⇩2κ⇩3[Π] → (Π↓ & κ⇩1↓ & κ⇩2↓ & κ⇩3↓)›
by (rule AOT_model_axiomI)
(metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes
AOT_sem_enc_denotes AOT_sem_imp case_prodD)
AOT_axiom "cqt:5:b[4]": ‹κ⇩1κ⇩2κ⇩3κ⇩4[Π] → (Π↓ & κ⇩1↓ & κ⇩2↓ & κ⇩3↓ & κ⇩4↓)›
by (rule AOT_model_axiomI)
(metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes
AOT_sem_enc_denotes AOT_sem_imp case_prodD)

AOT_axiom "l-identity": ‹α = β → (φ{α} → φ{β})›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_eq AOT_sem_imp)

AOT_act_axiom "logic-actual": ‹❙𝒜φ → φ›
by (rule AOT_model_act_axiomI)
(simp add: AOT_sem_act AOT_sem_imp)

AOT_axiom "logic-actual-nec:1": ‹❙𝒜¬φ ≡ ¬❙𝒜φ›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_act AOT_sem_equiv AOT_sem_not)
AOT_axiom "logic-actual-nec:2": ‹❙𝒜(φ → ψ) ≡ (❙𝒜φ → ❙𝒜ψ)›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_act AOT_sem_equiv AOT_sem_imp)

AOT_axiom "logic-actual-nec:3": ‹❙𝒜(∀α φ{α}) ≡ ∀α ❙𝒜φ{α}›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_act AOT_sem_equiv AOT_sem_forall AOT_sem_denotes)
AOT_axiom "logic-actual-nec:4": ‹❙𝒜φ ≡ ❙𝒜❙𝒜φ›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_act AOT_sem_equiv)

AOT_axiom "qml:1": ‹□(φ → ψ) → (□φ → □ψ)›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_box AOT_sem_imp)
AOT_axiom "qml:2": ‹□φ → φ›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_box AOT_sem_imp)
AOT_axiom "qml:3": ‹◇φ → □◇φ›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_box AOT_sem_dia AOT_sem_imp)

AOT_axiom "qml:4": ‹◇∃x (E!x & ¬❙𝒜E!x)›
using AOT_sem_concrete AOT_model_contingent
by (auto intro!: AOT_model_axiomI
simp: AOT_sem_box AOT_sem_dia AOT_sem_imp AOT_sem_exists
AOT_sem_denotes AOT_sem_conj AOT_sem_not AOT_sem_act
AOT_sem_exe)+

AOT_axiom "qml-act:1": ‹❙𝒜φ → □❙𝒜φ›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_act AOT_sem_box AOT_sem_imp)
AOT_axiom "qml-act:2": ‹□φ ≡ ❙𝒜□φ›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_act AOT_sem_box AOT_sem_equiv)

AOT_axiom descriptions: ‹x = ❙ιx(φ{x}) ≡ ∀z(❙𝒜φ{z} ≡ z = x)›
proof (rule AOT_model_axiomI)
AOT_modally_strict {
AOT_show ‹x = ❙ιx(φ{x}) ≡ ∀z(❙𝒜φ{z} ≡ z = x)›
by (induct; simp add: AOT_sem_equiv AOT_sem_forall AOT_sem_act AOT_sem_eq)
(metis (no_types, opaque_lifting) AOT_sem_desc_denotes AOT_sem_desc_prop
AOT_sem_denotes)
}
qed

AOT_axiom "lambda-predicates:1":
‹[λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]↓ → [λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}] = [λμ⇩1...μ⇩n φ{μ⇩1...μ⇩n}]›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_denotes AOT_sem_eq AOT_sem_imp)
AOT_axiom "lambda-predicates:1[zero]": ‹[λ p]↓ → [λ p] = [λ p]›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_denotes AOT_sem_eq AOT_sem_imp)
AOT_axiom "lambda-predicates:2":
‹[λx⇩1...x⇩n φ{x⇩1...x⇩n}]↓ → ([λx⇩1...x⇩n φ{x⇩1...x⇩n}]x⇩1...x⇩n ≡ φ{x⇩1...x⇩n})›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_equiv AOT_sem_imp AOT_sem_lambda_beta AOT_sem_vars_denote)
AOT_axiom "lambda-predicates:3": ‹[λx⇩1...x⇩n [F]x⇩1...x⇩n] = F›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_lambda_eta AOT_sem_vars_denote)
AOT_axiom "lambda-predicates:3[zero]": ‹[λ p] = p›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_eq AOT_sem_lambda0 AOT_sem_vars_denote)

AOT_axiom "safe-ext":
‹([λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]↓ & □∀ν⇩1...∀ν⇩n (φ{ν⇩1...ν⇩n} ≡ ψ{ν⇩1...ν⇩n})) →
[λν⇩1...ν⇩n ψ{ν⇩1...ν⇩n}]↓›
using AOT_sem_lambda_coex
by (auto intro!: AOT_model_axiomI simp: AOT_sem_imp AOT_sem_denotes AOT_sem_conj
AOT_sem_equiv AOT_sem_box AOT_sem_forall)
AOT_axiom "safe-ext[2]":
‹([λν⇩1ν⇩2 φ{ν⇩1,ν⇩2}]↓ & □∀ν⇩1∀ν⇩2 (φ{ν⇩1, ν⇩2} ≡ ψ{ν⇩1, ν⇩2})) →
[λν⇩1ν⇩2 ψ{ν⇩1,ν⇩2}]↓›
using "safe-ext"[where φ="λ(x,y). φ x y"]
by (simp add: AOT_model_axiom_def AOT_sem_denotes AOT_model_denotes_prod_def
AOT_sem_forall AOT_sem_imp AOT_sem_conj AOT_sem_equiv AOT_sem_box)
AOT_axiom "safe-ext[3]":
‹([λν⇩1ν⇩2ν⇩3 φ{ν⇩1,ν⇩2,ν⇩3}]↓ & □∀ν⇩1∀ν⇩2∀ν⇩3 (φ{ν⇩1, ν⇩2, ν⇩3} ≡ ψ{ν⇩1, ν⇩2, ν⇩3})) →
[λν⇩1ν⇩2ν⇩3 ψ{ν⇩1,ν⇩2,ν⇩3}]↓›
using "safe-ext"[where φ="λ(x,y,z). φ x y z"]
by (simp add: AOT_model_axiom_def AOT_model_denotes_prod_def AOT_sem_forall
AOT_sem_denotes AOT_sem_imp AOT_sem_conj AOT_sem_equiv AOT_sem_box)
AOT_axiom "safe-ext[4]":
‹([λν⇩1ν⇩2ν⇩3ν⇩4 φ{ν⇩1,ν⇩2,ν⇩3,ν⇩4}]↓ &
□∀ν⇩1∀ν⇩2∀ν⇩3∀ν⇩4 (φ{ν⇩1, ν⇩2, ν⇩3, ν⇩4} ≡ ψ{ν⇩1, ν⇩2, ν⇩3, ν⇩4})) →
[λν⇩1ν⇩2ν⇩3ν⇩4 ψ{ν⇩1,ν⇩2,ν⇩3,ν⇩4}]↓›
using "safe-ext"[where φ="λ(x,y,z,w). φ x y z w"]
by (simp add: AOT_model_axiom_def AOT_model_denotes_prod_def AOT_sem_forall
AOT_sem_denotes AOT_sem_imp AOT_sem_conj AOT_sem_equiv AOT_sem_box)

AOT_axiom "nary-encoding[2]":
‹x⇩1x⇩2[F] ≡ x⇩1[λy [F]yx⇩2] & x⇩2[λy [F]x⇩1y]›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_conj AOT_sem_equiv AOT_enc_prod_def AOT_proj_enc_prod_def
AOT_sem_unary_proj_enc AOT_sem_vars_denote)
AOT_axiom "nary-encoding[3]":
‹x⇩1x⇩2x⇩3[F] ≡ x⇩1[λy [F]yx⇩2x⇩3] & x⇩2[λy [F]x⇩1yx⇩3] & x⇩3[λy [F]x⇩1x⇩2y]›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_conj AOT_sem_equiv AOT_enc_prod_def AOT_proj_enc_prod_def
AOT_sem_unary_proj_enc AOT_sem_vars_denote)
AOT_axiom "nary-encoding[4]":
‹x⇩1x⇩2x⇩3x⇩4[F] ≡ x⇩1[λy [F]yx⇩2x⇩3x⇩4] &
x⇩2[λy [F]x⇩1yx⇩3x⇩4] &
x⇩3[λy [F]x⇩1x⇩2yx⇩4] &
x⇩4[λy [F]x⇩1x⇩2x⇩3y]›
by (rule AOT_model_axiomI)
(simp add: AOT_sem_conj AOT_sem_equiv AOT_enc_prod_def AOT_proj_enc_prod_def
AOT_sem_unary_proj_enc AOT_sem_vars_denote)

AOT_axiom encoding: ‹x[F] → □x[F]›
using AOT_sem_enc_nec
by (auto intro!: AOT_model_axiomI simp: AOT_sem_imp AOT_sem_box)

AOT_axiom nocoder: ‹O!x → ¬∃F x[F]›
by (auto intro!: AOT_model_axiomI
simp: AOT_sem_imp AOT_sem_not AOT_sem_exists AOT_sem_ordinary
AOT_sem_dia
AOT_sem_lambda_beta[OF AOT_sem_ordinary_def_denotes,
OF AOT_sem_vars_denote])
(metis AOT_sem_nocoder)

AOT_axiom "A-objects": ‹∃x (A!x & ∀F(x[F] ≡ φ{F}))›
proof(rule AOT_model_axiomI)
AOT_modally_strict {
AOT_obtain κ where ‹κ↓ & □¬E!κ & ∀F (κ[F] ≡ φ{F})›
using AOT_sem_A_objects[of _ φ]
by (auto simp: AOT_sem_imp AOT_sem_box AOT_sem_forall AOT_sem_exists
AOT_sem_conj AOT_sem_not AOT_sem_dia AOT_sem_denotes
AOT_sem_equiv) blast
AOT_thus ‹∃x (A!x & ∀F(x[F] ≡ φ{F}))›
unfolding AOT_sem_exists
by (auto intro!: exI[where x=κ]
simp: AOT_sem_lambda_beta[OF AOT_sem_abstract_def_denotes]
AOT_sem_box AOT_sem_dia AOT_sem_not AOT_sem_denotes
AOT_var_of_term_inverse AOT_sem_conj
AOT_sem_equiv AOT_sem_forall AOT_sem_abstract)
}
qed

AOT_theorem universal_closure:
assumes ‹for arbitrary α: φ{α} ∈ Λ⇩□›
shows ‹∀α φ{α} ∈ Λ⇩□›
using assms
by (metis AOT_term_of_var_cases AOT_model_axiom_def AOT_sem_denotes AOT_sem_forall)

AOT_theorem act_closure:
assumes ‹φ ∈ Λ⇩□›
shows ‹❙𝒜φ ∈ Λ⇩□›
using assms by (simp add: AOT_model_axiom_def AOT_sem_act)

AOT_theorem nec_closure:
assumes ‹φ ∈ Λ⇩□›
shows ‹□φ ∈ Λ⇩□›
using assms by (simp add: AOT_model_axiom_def AOT_sem_box)

AOT_theorem universal_closure_act:
assumes ‹for arbitrary α: φ{α} ∈ Λ›
shows ‹∀α φ{α} ∈ Λ›
using assms
by (metis AOT_term_of_var_cases AOT_model_act_axiom_def AOT_sem_denotes
AOT_sem_forall)

text‹The following are not part of PLM and only hold in the extended models.
They are a generalization of the predecessor axiom.›
context AOT_ExtendedModel
begin
AOT_axiom indistinguishable_ord_enc_all:
‹Π↓ & A!x & A!y & ∀F □([F]x ≡ [F]y) →
((∀G(∀z(O!z → □([G]z ≡ [Π]z)) → x[G])) ≡
∀G(∀z(O!z → □([G]z ≡ [Π]z)) → y[G]))›
by (rule AOT_model_axiomI)
(auto simp: AOT_sem_equiv AOT_sem_imp AOT_sem_conj
AOT_sem_indistinguishable_ord_enc_all)
AOT_axiom indistinguishable_ord_enc_ex:
‹Π↓ & A!x & A!y & ∀F □([F]x ≡ [F]y) →
((∃G(∀z(O!z → □([G]z ≡ [Π]z)) & x[G])) ≡
∃G(∀z(O!z → □([G]z ≡ [Π]z)) & y[G]))›
by (rule AOT_model_axiomI)
(auto simp: AOT_sem_equiv AOT_sem_imp AOT_sem_conj
AOT_sem_indistinguishable_ord_enc_ex)
end

(*<*)
end
(*>*)```