Formal grammar for a logic? The rules of logic seem like they could be expressed as a recursively enumerable grammar, but I have never seen someone actually do that. Is there somewhere I could find an example of an important mathematical  universe, say ZFC or a constructive topos, expressed as a formal grammar that can generate every provable statement but no unprovable statements?
The reason I think this might exist is, proofs can be checked with Turing machines, and Turing machines correspond to RE grammars. So a mathematical universe could be written as an RE grammar that corresponded to a Turing machine that checked proofs in that universe. (I'm a bit fuzzy about what the TM-REG correspondence actually is so maybe this doesn't really exist.)
 A: I do not really have a reference, just an argument why maybe none might exist.
Examples for grammars are usually from the regular and context-free classes. One main reason for this is that beyond that they usually do not work any more in the way one imagines a grammar. Rather, they work more or less like a Turing machine, simulating something like transitions on the sentential form and doing some kind of computation. This is necessarily so, when we look at complicated problems. Otherwise a TM simulating the grammar would have low running time. But why should I think in turns of grammar, when I actually have to design a computation, and a TM is a more intuitive way to do this.
Thus probably the best way to obtain a grammar for a complex problem is to design a TM and then convert it by the standard procedure to a grammar. But why would anyone do the last step, if everyone knows it is straightforward? And who would publish this?
If you have a TM which checks proofs in a universe, you can design a grammar that generates a random string. Then it checks wether it is a syntactically correct statement and finally simulates the TM on it in the standard way. If the TM accepts, you delete all the extra space you have used and leave the terminal word consisting of the input statement. This grammar will indeed generate every provable statement from your universe and nothing else.
A: Here I'm giving a type-0 grammar of the propositional logic (in the end):
Thoughts on generative grammars and their use in automated theorem proving based on neural networks
The grammar contains 60 non-terminal symbols and 264 production rules. I think this is just a routine to construct a "real" grammar of some first-order theory (say, group theory). Meanwhile, this is actually important, since, how I've shown in the article, this gives us a good arrangement of our data to prove theorems automatically by machine learning.
