On Wed, Jun 8, 2022 at 4:39 PM Benoit <[email protected]> wrote:
> Coming back to your example from set.mm where you introduce
> ${ $e |- x e. y $. $a INHAB y $. $}
> one could argue that this is bad practice and that one should have
> introduced instead
> ${ $e |- x e. A $. $a INHAB A $. $}
> which is the "correct" level of generality. With that new axiom, the
> system remains uniquely grammatical.
Sure, but it's also semantically different. Maybe it was actually supposed
to be a predicate that only applies to set variables. Using set.mm for this
example is somewhat limiting since there just aren't that many syntactic
categories (and introducing new ones is discouraged anyway) - obviously
this "INHAB" typecode would be rejected in review.
What I'm trying to do is find a criterion that would make more precise the
> fact that "reasonable", or "currently encountered" databases are uniquely
> grammatical.
I suspect that in practice the most common reason why currently encountered
databases are uniquely grammatical is that the very first theorem is often
(the analogue of) idi, which has the form "|- ph => |- ph" where "ph" is a
wff metavariable, so it essentially specifies the Syn(|-) = wff mapping
right there. Some other good examples are hol.mm (which introduces the
necessary axioms "for mmj2 compatibility"):
$c wff $. $( Not used; for mmj2 compatibility $)
$( Internal axiom for mmj2 use. $)
wffMMJ2 $a wff A |= B $.
$( Internal axiom for mmj2 use. $)
wffMMJ2t $a wff A : al $.
as well as dtt.mm (which uses multiple typecodes for precedence parsing).
But I just can't shake the feeling that these are uniquely grammatical "by
coincidence": clearly hol.mm has those axioms because mmj2 was acting up in
some way without the ability to do grammar parsing, so that might be one
explanation for why you find this property in the wild. Note that in hol.mm
the idi theorem(s) are spelled
${ $e |- R |= A $. $p |- R |= A $. $}
${ $e |- A : al $. $p |- A : al $. $}
which is to say, they don't ever use the wff axioms (there isn't even a
variable of type wff, which means that the paper definition would not
consider this a variable typecode and that would disqualify it as a
grammatical database). Looking at this definition, there is really nothing
at all that connects the wff typecode to anything that is going on in the
rest of the file. You could introduce a wff2 typecode which is similarly
unused and then it would obviously not be a uniquely grammatical database
even ignoring the wff e. VT situation.
Or one could require that the types under coercions form a set of rooted
> trees, so that if there are no "partially duplicate" types (as in the
> example above with $a A * $. etc), then, even if the system is grammatical
> but not uniquely grammatical, there is a "most stringent" Syn function
> making it grammatical (in the example above with INHAB, this means taking
> Syn(INHAB)=setvar).
>
The drawback of choosing the "most stringent" Syn function is that it is
not monotonic under adding axioms. With the "INHAB x" example, we might
first decide Syn(INHAB)=setvar and then the second axiom is about "INHAB
{x}" and now we think that Syn(INHAB)=class. This is not good if we are
trying to build a model incrementally; we would instead want to say
Syn(INHAB)>=setvar and then Syn(INHAB)>=class to reflect our increasingly
precise information, but now this becomes difficult to model since we don't
know what type Syn(INHAB) is but we still have to give it some semantics
(which is consistent with any coercions that may be introduced in the
future).
Mario
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSv5-nN7c1Jj8q_SX_KoK9736Tw5Kp6_KNAwgMUf9U-yUw%40mail.gmail.com.
