# ZF set theory with Skolem function symbols

## Axiomatisations

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.