Suppose you and I are writing a book that develops (classical) mathematics from scratch.

In the course of writing this book, we'll need to define a variety of formal systems, like a system for propositional logic, one for predicate logic; a system for PA, and a system for ZFC.

Now. To carry out all this specification with maximal ease, we should probably settle on a convenient specification language for formal systems, right at the outset.

Question. Suppose we're prioritizing practical usability (as opposed to, say, meta-theoretic simplicity). What would be a good specification language for formal systems?

For instance, I've heard of Post Systems. Would these be a good choice?


If you want "practical usability", then I suspect you don't want to look like you're specifying formal systems at all! Instead you want to provide an abstraction layer that looks better resembles the practice and thought process of mathematicians and machinery that can turn them into formal systems "under the hood".

Compare with computer programming; people very rarely write programs with the understanding that it will be turned into assembly language or machine code. Sure, in the back of their mind they usually know it happens, but treat that as being mostly irrelevant to the practice of writing programs.

  • $\begingroup$ I agree. In trying to document my own formal system, I didn't find the specification notations commonly used to be all that useful for my own system. But maybe that's more a comment on me and my system. In any case, it will be interesting to see what if anything the pro's here recommend. $\endgroup$ – Dan Christensen Aug 16 '13 at 19:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.