Isn't there a completely worked out example of using Coq to implement a multi-sorted first-order theory, with sorted variables, constants, function symbols, relation symbols, axioms, and proofs of theorems? (F

or example, single-sorted Tarski's axioms for Euclidean geometry; or, two-sorted axioms for a vector space.)

I think there is, and I suppose @Dominik Kirst can tell you the details.

We so far don't have multi-sorted FOL, but for single sorted FOL we have axiomatisations of PA, ZF, and the like:

https://www.ps.uni-saarland.de/extras/axiomatisations/

Regarding your examples, the mechanisation of FOL we developed is parametric in the signature, so you can use it for Tarski's Euclidean geometry. It shouldn't be too much work to add support for multiple sorts, then you could use it also for vector spaces.

Some relevant meta-theoretic results included in our library are soundness, enumerability, completeness, undecidability, and incompleteness.

Last updated: Oct 03 2023 at 21:01 UTC