Require Export Undecidability.FOL.Utils.FullSyntax.
From Undecidability.FOL.Sets Require Export FST binFST Signatures.
Import Vector.VectorNotations.
Require Import List.

Declare Scope syn.
Open Scope syn.


Import FSTSignature.
Export FSTSignature.


Notation extensional M :=
  (forall x y, @i_atom _ ZFSignature.ZF_pred_sig _ M equal ([x; y]) <-> x = y).

Definition entailment_FST phi :=
  forall D (M : interp D) (rho : nat -> D), extensional M -> (forall sigma psi, In psi FST -> sigma ⊨ psi) -> rho ⊨ phi.

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

Definition entailment_FSTI phi :=
  forall D (M : interp D) (rho : nat -> D), extensional M -> (forall sigma psi, FSTI psi -> sigma ⊨ psi) -> rho ⊨ phi.

Definition deduction_FST phi :=
  FSTeq ⊢I phi.

Definition deduction_FSTI phi :=
  FSTIeq ⊢TI phi.


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

Definition deduction_binFST phi :=
  binFST ⊢I phi.