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 `Compute`

commands), like `(A /\x B)`

for `(notH _ (impH _ (notH _ (notH _ A)) (notH _ B)))`

?

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