Stream: Hydras & Co. universe

Topic: New notations


view this post on Zulip Pierre Castéran (Feb 26 2023 at 17:25):

I'm thinking about the design of simple notations for FOL-formulas.

In Ackermann+Gödel, a formula like (andH _ A B) can be reduced to (notH _ (orH _ (notH _ A) (notH _ B))), or worse,
to (notH _ (impH _ (notH _ (notH _ A)) (notH _ B))) (same stuff for all derived connectors and quantifiers).

I'm not sure if a given notation can be bound to several different terms.
A solution could be to bind A /\ B to (andH _ A B), and a specific notation to the most expanded form (in goals or results of Computecommands), like (A /\x B) for (notH _ (impH _ (notH _ (notH _ A)) (notH _ B))) ?

view this post on Zulip Karl Palmskog (Feb 26 2023 at 17:48):

maybe add some small marker to differentiate the deep embedding from Coq operators? like _/\. I wonder if we can take inspiration from https://github.com/dominik-kirst/coq-library-undecidability/tree/fol-library/theories/FOL


Last updated: Feb 22 2024 at 04:02 UTC