From Undecidability.FOL Require Export Semantics Kripke Deduction.

(* Definitions concerning first-order logic *)

(* On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem. Yannick Forster, Dominik Kirst, and Gert Smolka. CPP '19. https://www.ps.uni-saarland.de/extras/fol-undec *)

About prv_min.   (* Minimal provability *)
About prv_into.  (* Intuitionistic provability *)
About prv_class. (* Classical provability *)

About valid.  (* Tarski validity *)
About kvalid. (* Kripke validity *)

About satis.  (* Tarksi satisfiability *)
About ksatis. (* Kripke satisfiability *)
