On Sat, Jun 4, 2022 at 9:36 AM Benoit <[email protected]> wrote:
> 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 ? > Well, it's easy enough to determine which typecodes are syntax typecodes since they are the typecodes of variables, but I don't think it is very simple to figure out the mapping '|-' -> 'wff' for the logical typecodes. Especially if there are no axioms (yet) the problem is underdetermined. > 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.) > More to the point, it is my opinion that these kinds of things "feel" like they should be declarations. This prevents syntax errors like using ')' as a typecode, because you know what the legal typecodes are, and it allows you to parse expressions without guessing the typecodes. In fact, the example where we truncate a grammatical database before the first axiom is actually true in general: It could be that ')' is a typecode of set.mm, and we simply have not introduced the first axiom using it. That is, the definition of "grammatical database" includes not just the data "Syn" but also "TC". (In the paper TC is inferred from the existence of axioms, but in the $j syntax approach TC is declared in advance of use, and I think this is the right approach as mentioned in the previous paragraph. In MM0 these are declared using the "sort" command.) Even if we take the paper definition of TC, there is another example of a grammatical database that is not uniquely grammatical: $c A B |- * $. $v a b $. va $f A a $. vb $f B b $. as $a A * $. bs $a B * $. ax $a |- * $. Here we have two variable typecodes A and B, and one logical typecode |-, and the question is: is Syn(|-) = A or Syn(|-) = B? It parses either way. This is actually an unambiguous formal system, because we require only that there are no two ways to derive the proof of the *same* syntax theorem, and "A *" and "B *" are different theorems. 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/CAFXXJSv_UJTTYcyf7ANOfrMspVt05MsVQtPgFyLcbnyGVvjmyg%40mail.gmail.com.
