
Re: Formal Proof Language Example  HumanReadable?
Posted:
Jun 23, 2009 2:37 PM


Yes, I can understand the meaning of the (assertion of) the theorem. I think a good formal proof language has to have the following features:
1. Be readable for people with general mathematical education, without having the study the language. Readability is of course relative and depends on the reader's experience. For some people a proof is readable if it looks like Lisp. For most mathematicians though the proof is readable if it looks similar to what they can see in a standard journal. I think your syntax does have this feature.
2. Provide ways to cope with excessive verbosity. Formal proofs are typically very verbose. A proof language should provide ways to structure the proofs so that at least in a web presentation the reader can choose how detailed the proof she wants to see. Your syntax is too verbose.
3. Should support LaTeXlike mathematical symbols and notation. This can be done by a presentation layer, but there has to be way to render the proofs so that they look like math. This is also needed for 2.
4. Should support some notion of context to be able to limit the scope of introduced notation, independent of the defined notions. For example you should be able to talk about groups using both multiplicative and additive notation (in different contexts), or use the same \cdot symbol to denote both general group operation and multiplication of real numbers (again in different contexts). How important this need is becomes obvious only when you reach certain scale.
Isar is a proof language that has all these features to some extent. <plug> See formalmath.org site for an examples </plug>.

