(**************************************************************)
(*   Copyright Dominique Larchey-Wendling *                 *)
(*                                                            *)
(*                             * Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List.

From Undecidability.Shared.Libs.DLW.Utils
  Require Import finite.

From Undecidability.Shared.Libs.DLW.Vec
  Require Import pos vec.

From Undecidability.TRAKHTENBROT
  Require Import notations utils decidable fol_ops fo_sig fo_terms fo_logic.

Set Implicit Arguments.

Definition of first order satisfiability


Section satisfiability.

  Variable (Σ : fo_signature) (e : rels Σ) (E : ar_rels Σ e = 2) (A : fol_form Σ).

A first order formula over signature Σ is finitely satisfiable over type X if there exists a model M interpreting the signature Σ over type X which is both finite (strongly listable) and strongly decidable, and a valuation φ : nat -> X in which A is satisfied

  Definition fo_form_fin_SAT_in X :=
    exists (M : fo_model Σ X)
           (_ : finite_t X)
           (φ : nat -> X),
           fol_sem M φ A.

  Definition fo_form_fin_dec_SAT_in X :=
    exists (M : fo_model Σ X)
           (_ : finite_t X)
           (_ : fo_model_dec M)
           (φ : nat -> X),
           fol_sem M φ A.

  Definition fo_form_fin_dec_eq_SAT_in X :=
    exists (M : fo_model Σ X)
           (_ : finite_t X)
           (_ : fo_model_dec M)
           (_ : forall x y, fom_rels M e (cast (x##y##ø) (eq_sym E)) <-> x = y)
           (φ : nat -> X),
           fol_sem M φ A.

  Definition fo_form_fin_discr_dec_SAT_in X :=
    exists (_ : discrete X),
           fo_form_fin_dec_SAT_in X.

  Definition fo_form_fin_SAT := ex fo_form_fin_SAT_in.
  Definition fo_form_fin_dec_SAT := ex fo_form_fin_dec_SAT_in.
  Definition fo_form_fin_dec_eq_SAT := ex fo_form_fin_dec_eq_SAT_in.
  Definition fo_form_fin_discr_dec_SAT := ex fo_form_fin_discr_dec_SAT_in.

  Fact fo_form_fin_discr_dec_SAT_fin_dec : fo_form_fin_discr_dec_SAT -> fo_form_fin_dec_SAT.
  Proof. intros (X & _ & ?); exists X; trivial. Qed.

  Fact fo_form_fin_dec_SAT_fin : fo_form_fin_dec_SAT -> fo_form_fin_SAT.
  Proof. intros (X & M & H & _ & ?); exists X, M, H; trivial. Qed.

End satisfiability.