From Undecidability.FOL Require Import Syntax.Core.
From Undecidability.FOL.Arithmetics Require Export Signature FA Robinson PA.
Require Import Undecidability.FOL.Deduction.FullND.
Require Import Undecidability.FOL.Semantics.Tarski.FullCore.
Import Vector.VectorNotations.
Require Import List.

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


Definition entailment_FA phi :=
  valid_ctx FAeq phi.


Definition deduction_FA phi :=
  FAeq ⊢I phi.


Definition entailment_Q phi :=
  valid_ctx Qeq phi.


Definition deduction_Q phi :=
  Qeq ⊢I phi.


Definition entailment_PA phi :=
  forall D (I : interp D) rho, (forall psi rho, PAeq psi -> rho ⊨ psi) -> rho ⊨ phi.


Definition ext_entailment_PA phi :=
  forall D (I : interp D) rho, extensional I -> (forall psi rho, PA psi -> rho ⊨ psi) -> rho ⊨ phi.


Definition deduction_PA phi :=
  PAeq ⊢TI phi.