> The divide between ALL and ESSENTIAL is that the latter only shows
> the steps with typecode '|-' (and the final step, whatever its
> typecode is). The other steps, those constructing the formulas and
> classes, are "syntactic", that is, their typecodes are wff, set,
> class (and indeed, their leaves are $f-statements).
Ohhh, yeah, that makes complete sense. I was expecting that metamath
somehow had an internal concept of what is merely syntactic and what is
essential, but I guess it's just by convention. In other words, if I
were to make a file with different typecodes, then ESSENTIAL mode would
not work so well? (that's easy to verify I guess)
Probably what I should do is give the user control over the typecodes
they want to consider essential.
Mario: I had been wondering about something for a while: in Models for Metamath, you define "weakly grammatical" as a property and "grammatical" as an extra structure (the function Syn is part of the data). One could define a system \Gamma to be *uniquely grammatical* if there exists a unique Syn: TC \to VT such that (\Gamma, Syn) is grammatical. It is not hard to see that set.mm-like systems are uniquely grammatical. In general, I haven't found non-trivial necessary or sufficient conditions to be uniquely grammatical. Have you thought about these questions ?
It looks like if you know beforehand that a system is uniquely grammatical, these $j commands are not necessary: upon reading the first assertion with a non-VT typecode, say $a T expr $., the system tries to prove $p S expr $= ? $. for all variable types S, and it will succeed for a unique one, which is then Syn(T). (This assumes that a typecode which first appears in an assertion does not appear later in an $f-statement.)
--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4932d6bf-c373-42df-9301-1640a060768dn%40googlegroups.com.
Forbidding that may be "aesthetically desirable" but it would probably be too cumbersome for practical developments.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/bdb5fc53-1629-427f-ba7c-667f8aa2b00an%40googlegroups.com.
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.
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.
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).