Require Export Undecidability.FOL.Syntax.Core.
Require Import Undecidability.FOL.Syntax.Theories.
From Undecidability Require Import Shared.ListAutomation.
Import ListAutomationNotations.
Require Import Vector.

Local Set Implicit Arguments.
Local Unset Strict Implicit.

Set Default Proof Using "Type".

Local Notation vec := Vector.t.

Import FragmentSyntax.
Export FragmentSyntax.


Section Tarski.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.


  Section Semantics.

    Variable domain : Type.

    Class interp := B_I
      {
        i_func : forall f : syms, vec domain (ar_syms f) -> domain ;
        i_atom : forall P : preds, vec domain (ar_preds P) -> Prop
      }.

    Definition env := nat -> domain.

    Context {I : interp}.

    Fixpoint eval (rho : env) (t : term) : domain :=
      match t with
      | var s => rho s
      | func f v => i_func (Vector.map (eval rho) v)
      end.

    Fixpoint sat {ff : falsity_flag} (rho : env) (phi : form) : Prop :=
      match phi with
      | atom P v => i_atom (Vector.map (eval rho) v)
      | falsity => False
      | bin Impl phi psi => sat rho phi -> sat rho psi
      | quant All phi => forall d : domain, sat (d .: rho) phi
      end.

  End Semantics.

  Notation "rho ⊨ phi" := (sat rho phi) (at level 20).

End Tarski.

Arguments sat {_ _ _ _ _} _ _, {_ _ _} _ {_} _ _.
Arguments interp {_ _} _, _ _ _.

Notation "p ⊨ phi" := (sat _ p phi) (at level 20).
Notation "I ⊨= phi" := (forall p, sat I p phi) (at level 20).
Notation "p ⊫ A" := (forall psi, psi el A -> sat _ p psi) (at level 20).

Section Defs.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ff : falsity_flag}.

  Definition classical D (I : interp D) :=
    forall rho phi psi, rho ⊨ (((phi → psi) → phi) → phi).

  Definition valid_theory_C (C : forall D (I:interp D), Prop) (T:theory) phi :=
      forall D (I : interp D) rho, C D I -> (forall psi, T psi -> rho ⊨ psi) -> rho ⊨ phi.
  Definition valid_ctx_C (C : forall D (I:interp D), Prop) A phi :=
      forall D (I : interp D) rho, C D I -> rho ⊫ A -> rho ⊨ phi.
  Definition valid_C (C : forall D (I:interp D), Prop) phi :=
      forall D (I : interp D) rho, C D I -> rho ⊨ phi.
  Definition valid_ctx A phi := forall D (I : interp D) rho, rho ⊫ A -> rho ⊨ phi.
  Definition valid_theory (T:theory) phi := forall D (I : interp D) rho, (forall psi, T psi -> rho ⊨ psi) -> rho ⊨ phi.
  Definition valid phi := forall D (I : interp D) rho, rho ⊨ phi.
  Definition valid_L A := forall D (I : interp D) rho, rho ⊫ A.
  Definition satis phi := exists D (I : interp D) rho, rho ⊨ phi.
  Definition satis_L A := exists D (I : interp D) rho, rho ⊫ A.

End Defs.