FOL Encoding

[Durbatuluk1701]

Create (or find a library) for First Order Logic encodings in Coq.

The following main theorems should be provable within it:

• Soundness $\forall \Gamma, A, \Gamma \vdash A \implies \Gamma \vDash A$
• Particularly we want stuff regarding closed terms since that is what we would likely use a lot

The following book "Sets, Logic, Computation: An Open Introduction to Metalogic" (free online I think) chapters 6-8 has a very good guiding principle for FOL, its syntax, and semantics if encoding our own is the decision