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 *)