Require Export Undecidability.FOL.Syntax.Core.
Require Export Undecidability.FOL.Semantics.Tarski.FullFacts.
Require Export Undecidability.FOL.Deduction.FullNDFacts.
Require Export Undecidability.FOL.Sets.Signatures.
Require Export Undecidability.FOL.Sets.ZF.
Import Vector.VectorNotations.
Require Import List.

Declare Scope syn.
Open Scope syn.


Import BinSig.
Import ZFSignature.
Export BinSig.
Export ZFSignature.

#[global]
Existing Instance ZF_pred_sig | 0.

#[global]
Existing Instance sig_empty | 0.

Notation "x ∈' y" := (atom sig_empty ZF_pred_sig elem ([x; y])) (at level 35) : syn.
Notation "x ≡' y" := (atom sig_empty ZF_pred_sig equal ([x; y])) (at level 35) : syn.


Fixpoint shift `{funcs_signature} `{preds_signature} n (t : term) :=
  match n with
  | O => t
  | S n => subst_term ↑ (shift n t)
  end.

Definition is_eset (t : term) :=
  ∀ ¬ ($0 ∈ t`[↑]).

Definition is_pair (x y t : term) :=
  ∀ $0 ∈ t`[↑] ↔ $0 ≡ x`[↑] ∨ $0 ≡ y`[↑].

Definition is_union (x t : term) :=
  ∀ $0 ∈ t`[↑] ↔ ∃ $0 ∈ shift 2 x ∧ $1 ∈ $0.

Definition sub' (x y : term) :=
  ∀ $0 ∈ x`[↑] → $0 ∈ y`[↑].

Definition is_power (x t : term) :=
  ∀ $0 ∈ t`[↑] ↔ sub' $0 x`[↑].

Definition is_sigma (x t : term) :=
  ∀ $0 ∈ t`[↑] ↔ $0 ∈ x`[↑] ∨ $0 ≡ x`[↑].

Definition is_inductive (t : term) :=
  (∃ is_eset $0 ∧ $0 ∈ t`[↑]) ∧ ∀ $0 ∈ t`[↑] → (∃ is_sigma $1 $0 ∧ $0 ∈ shift 2 t).

Definition is_om (t : term) :=
  is_inductive t ∧ ∀ is_inductive $0 → sub' t`[↑] $0.


Definition ax_ext' :=
  ∀ ∀ sub' $1 $0 → sub' $0 $1 → $1 ≡' $0.

Definition ax_eset' :=
  ∃ is_eset $0.

Definition ax_pair' :=
  ∀ ∀ ∃ is_pair $2 $1 $0.

Definition ax_union' :=
  ∀ ∃ is_union $1 $0.

Definition ax_power' :=
  ∀ ∃ is_power $1 $0.

Definition ax_om' :=
  ∃ is_om $0.

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 minZF' :=
  ax_ext' :: ax_eset' :: ax_pair' :: ax_union' :: ax_power' :: ax_om' :: nil.


Definition minZFeq' :=
  ax_refl' :: ax_sym' :: ax_trans' :: ax_eq_elem' :: minZF'.

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].


Inductive minZ : form -> Prop :=
| minZ_base phi : In phi minZF' -> minZ phi
| minZ_sep phi : minZ (ax_sep' phi).


Inductive minZeq : form -> Prop :=
| minZeq_base phi : In phi minZFeq' -> minZeq phi
| minZeq_sep phi : minZeq (ax_sep' phi).


Inductive minZF : form -> Prop :=
| minZF_base phi : In phi minZF' -> minZF phi
| minZF_sep phi : minZF (ax_sep' phi)
| minZF_rep phi : minZF (ax_rep' phi).


Inductive minZFeq : form -> Prop :=
| minZFeq_base phi : In phi minZFeq' -> minZFeq phi
| minZFeq_sep phi : minZFeq (ax_sep' phi)
| minZFeq_rep phi : minZFeq (ax_rep' phi).



Definition entailment_minZFeq' phi :=
  forall D (M : interp D) (rho : nat -> D), (forall sigma psi, In psi minZFeq' -> sigma ⊨ psi) -> rho ⊨ phi.


Definition entailment_minZF' phi :=
  forall D (M : @interp sig_empty _ D) (rho : nat -> D), extensional M -> (forall sigma psi, In psi minZF' -> sigma ⊨ psi) -> rho ⊨ phi.


Definition entailment_minZ phi :=
  forall D (M : @interp sig_empty _ D) (rho : nat -> D), extensional M -> (forall sigma psi, minZ psi -> sigma ⊨ psi) -> rho ⊨ phi.


Definition entailment_minZF phi :=
  forall D (M : @interp sig_empty _ D) (rho : nat -> D), extensional M -> (forall sigma psi, minZF psi -> sigma ⊨ psi) -> rho ⊨ phi.


Definition deduction_minZF' phi :=
  minZFeq' ⊢I phi.


Definition deduction_minZ phi :=
  minZeq ⊢TI phi.


Definition deduction_minZF phi :=
  minZFeq ⊢TI phi.