that we more or less agree on the basic principles.

&gt;I would question whether every notation has to be explicitly mapped to FOL,

&gt;it might be sufficient to map to one or more other notations whose behaviour

&gt;with respect to FOL are well known and understood.

Yes. The main point is to identify how any proposed notation
relates to the ones that already exist.  For programming
languages, the ability to simulate a Turing machine is a key
test that separates the general-purpose languages from the
ve