Grammatical databases and logical typecodes

[Marlo Bruder]

Hello everyone,

I'm currently trying to understant what exactly makes a metamath database "grammatical" and I have run into a question I wanted to ask: Is it possible for a grammatical database to have more than one logical typecode? So far I've only seen databases with one logical typecode (usually ' |- '), but I don't really see a reason why this shouldn't be possible.

Much thanks for any answer in advance!

Best regards,

Marlo Bruder

[Matthew House]

There's no reason there can't be more than one logical typecode. E.g., in iset.mm, one might add a new typecode |= for classical theorems, with axioms making |= ph equivalent to |- -. -. ph. It mainly isn't done because it would require every theorem to be written multiple times with the different typecodes. For grammar checking, you'd just want to make sure to add a $( $j syntax '|=' as 'wff'; $) comment, as described in the Metamath $j commands page.

Matthew House

--
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 visit https://groups.google.com/d/msgid/metamath/4a02c164-1ba7-4356-8e9c-1f0fd9205aa2n%40googlegroups.com.