Require Export Undecidability.FOL.Utils.FullSyntax.
From Undecidability.FOL.Sets Require Export ZF minZF binZF Signatures.
Import Vector.VectorNotations.
Require Import List.

Declare Scope syn.
Open Scope syn.


Import ZFSignature.
Export ZFSignature.

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.



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.



Definition entailment_binZF phi :=
  forall D (M : @interp sig_empty _ D) (rho : nat -> D), (forall psi, In psi binZF -> rho ⊨ psi) -> rho ⊨ phi.


Definition deduction_binZF phi :=
  binZF ⊢I phi.