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.) Benoît On Saturday, June 4, 2022 at 3:23:25 AM UTC+2 [email protected] wrote: > On Fri, Jun 3, 2022 at 7:47 PM 'Philip White' via Metamath < > [email protected]> wrote: > >> > 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. >> > > One of the things that came out of the research which resulted in the > "Models" paper was the "syntax" $j command. In set.mm you can find the > following declarations: > > $( $j > syntax 'wff'; > syntax '|-' as 'wff'; > syntax 'setvar'; > syntax 'class'; > $) > > These correspond to the "Syn" function from the paper. In short, there is > one of these syntax lines for every legal typecode (that can appear as the > initial constant on any $e $f $a $p statement), and the ones that have an > 'as' are the logical typecodes (and the thing after the 'as' is the > typecode by which to parse the contents) while those that don't have 'as' > are grammatical typecodes. So if you wanted to generalize the "is it '|-'?" > check, you would instead check if it is a logical typecode. This does > require $j parsing however, which is optional for metamath verifiers (since > this was intended to be a backward-compatible addition). > -- 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/bf9ee925-e677-4c58-baa6-61fa933a9180n%40googlegroups.com.
