Require Import Undecidability.FOL.Util.Syntax.
Require Import Undecidability.FOL.Util.FullTarski.
Require Import Undecidability.FOL.Util.FullDeduction.
Import Vector.VectorNotations.
Require Import List.
Existing Instance falsity_on.
Inductive ZF_Funcs : Type :=
| eset : ZF_Funcs
| pair : ZF_Funcs
| union : ZF_Funcs
| power : ZF_Funcs
| om : ZF_Funcs.
Definition ZF_fun_ar (f : ZF_Funcs) : nat :=
match f with
| eset => 0
| pair => 2
| union => 1
| power => 1
| om => 0
end.
Inductive ZF_Preds : Type :=
| elem : ZF_Preds
| equal : ZF_Preds.
Definition ZF_pred_ar (P : ZF_Preds) : nat :=
match P with _ => 2 end.
Instance ZF_func_sig : funcs_signature :=
{| syms := ZF_Funcs; ar_syms := ZF_fun_ar; |}.
Instance ZF_pred_sig : preds_signature :=
{| preds := ZF_Preds; ar_preds := ZF_pred_ar; |}.
Notation "x ∈ y" := (atom _ ZF_pred_sig elem ([x; y])) (at level 35) : syn.
Notation "x ≡ y" := (atom (Σ_preds := ZF_pred_sig) equal ([x; y])) (at level 35) : syn.
Notation "∅" := (func ZF_func_sig eset ([])) : syn.
Notation "'ω'" := (func ZF_func_sig om ([])) : syn.
Notation "{ x ; y }" := (func ZF_func_sig pair ([x; y])) (at level 31) : syn.
Notation "⋃ x" := (func ZF_func_sig union ([x])) (at level 32) : syn.
Notation "'PP' x" := (func ZF_func_sig power ([x])) (at level 31) : syn.
Notation "x ∪ y" := (⋃ {x; y}) (at level 32) : syn.
Notation "'σ' x" := (x ∪ {x; x}) (at level 32) : syn.
Definition sub x y :=
∀ $0 ∈ x`[↑] ~> $0 ∈ y`[↑].
Notation "x ⊆ y" := (sub x y) (at level 34) : syn.
Definition ax_ext :=
∀ ∀ $1 ⊆ $0 ~> $0 ⊆ $1 ~> $1 ≡ $0.
Definition ax_eset :=
∀ ¬ ($0 ∈ ∅).
Definition ax_pair :=
∀ ∀ ∀ $0 ∈ {$1; $2} <~> $0 ≡ $1 ∨ $0 ≡ $2.
Definition ax_union :=
∀ ∀ $0 ∈ ⋃ $1 <~> ∃ $0 ∈ $2 ∧ $1 ∈ $0.
Definition ax_power :=
∀ ∀ $0 ∈ PP $1 <~> $0 ⊆ $1.
Definition inductive x :=
∅ ∈ x ∧ ∀ $0 ∈ x`[↑] ~> σ $0 ∈ x`[↑].
Definition ax_om1 :=
inductive ω.
Definition ax_om2 :=
∀ inductive $0 ~> ω ⊆ $0.
Definition ax_sep phi :=
∀ ∃ ∀ $0 ∈ $1 <~> $0 ∈ $2 ∧ phi[$0.: Nat.add 3 >> var].
Definition fun_rel phi :=
∀ ∀ ∀ phi[$2 .: $1 .: Nat.add 3 >> var] ~> phi[$2 .: $0 .: Nat.add 3 >> var] ~> $1 ≡ $0.
Definition ax_rep phi :=
fun_rel phi ~> ∀ ∃ ∀ $0 ∈ $1 <~> ∃ $0 ∈ $3 ∧ phi[$0 .: $1 .: Nat.add 4 >> var].
Definition HF :=
ax_ext :: ax_eset :: ax_pair :: ax_union :: ax_power :: nil.
Definition ax_no_inductive :=
∀ ¬ inductive $0.
Definition HFN :=
ax_no_inductive :: HF.
Definition ZF' :=
ax_ext :: ax_eset :: ax_pair :: ax_union :: ax_power :: ax_om1 :: ax_om2 :: nil.
Inductive Z : form -> Prop :=
| Z_base phi : In phi ZF' -> Z phi
| Z_sep phi : Z (ax_sep phi).
Inductive ZF : form -> Prop :=
| ZF_base phi : In phi ZF' -> ZF phi
| ZF_sep phi : ZF (ax_sep phi)
| ZF_rep phi : ZF (ax_rep phi).
Definition ax_refl :=
∀ $0 ≡ $0.
Definition ax_sym :=
∀ ∀ $1 ≡ $0 ~> $0 ≡ $1.
Definition ax_trans :=
∀ ∀ ∀ $2 ≡ $1 ~> $1 ≡ $0 ~> $2 ≡ $0.
Definition ax_eq_elem :=
∀ ∀ ∀ ∀ $3 ≡ $1 ~> $2 ≡ $0 ~> $3 ∈ $2 ~> $1 ∈ $0.
Definition HFeq :=
ax_refl :: ax_sym :: ax_trans :: ax_eq_elem :: HF.
Definition HFNeq :=
ax_refl :: ax_sym :: ax_trans :: ax_eq_elem :: HFN.
Definition ZFeq' :=
ax_refl :: ax_sym :: ax_trans :: ax_eq_elem :: ZF'.
Inductive Zeq : form -> Prop :=
| Zeq_base phi : In phi ZFeq' -> Zeq phi
| Zeq_sep phi : Zeq (ax_sep phi).
Inductive ZFeq : form -> Prop :=
| ZFeq_base phi : In phi ZFeq' -> ZFeq phi
| ZFeq_sep phi : ZFeq (ax_sep phi)
| ZFeq_rep phi : ZFeq (ax_rep phi).
Notation extensional M :=
(forall x y, @i_atom _ ZF_pred_sig _ M equal ([x; y]) <-> x = y).
Definition entailment_ZFeq' phi :=
forall D (M : interp D) (rho : nat -> D), (forall sigma psi, In psi ZFeq' -> sigma ⊨ psi) -> rho ⊨ phi.
Definition entailment_HF phi :=
forall D (M : interp D) (rho : nat -> D), extensional M -> (forall sigma psi, In psi HF -> sigma ⊨ psi) -> rho ⊨ phi.
Definition entailment_HFN phi :=
forall D (M : interp D) (rho : nat -> D), extensional M -> (forall sigma psi, In psi HFN -> sigma ⊨ psi) -> rho ⊨ phi.
Definition entailment_ZF' phi :=
forall D (M : interp D) (rho : nat -> D), extensional M -> (forall sigma psi, In psi ZF' -> sigma ⊨ psi) -> rho ⊨ phi.
Definition entailment_Z phi :=
forall D (M : interp D) (rho : nat -> D), extensional M -> (forall sigma psi, Z psi -> sigma ⊨ psi) -> rho ⊨ phi.
Definition entailment_ZF phi :=
forall D (M : interp D) (rho : nat -> D), extensional M -> (forall sigma psi, ZF psi -> sigma ⊨ psi) -> rho ⊨ phi.
Definition deduction_HF phi :=
HFeq ⊢I phi.
Definition deduction_HFN phi :=
HFNeq ⊢I phi.
Definition deduction_ZF' phi :=
ZFeq' ⊢I phi.
Definition deduction_Z phi :=
Zeq ⊢TI phi.
Definition deduction_ZF phi :=
ZFeq ⊢TI phi.