Stream: Coq users

Topic: First Order Theory


view this post on Zulip Ellis D. Cooper (Sep 08 2021 at 17:53):

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

view this post on Zulip Christian Doczkal (Sep 09 2021 at 06:59):

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

view this post on Zulip Dominik Kirst (Sep 09 2021 at 15:24):

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: Feb 01 2023 at 13:03 UTC