Warren — Thanks for pointing me to Mizar. I didn't know about it, and will investigate. If it's syntax is annoying, then it's a call to arms to make a better language! Designing a good formal proof language that is easy for humans to read is similar to the problem of designing a good programming language that is easy for humans to read. Brent — Of course language is important, and we shouldn't operate just in formal language. The practical problem is that the gulf between English and mathematical notation is so wide that many young students fail to cross it (I'm developing math games for kids ages 6-10). I'm therefore designing intermediate forms to bridge the gap. These will not be formal notations, but will likely to visual templates for expressing mathematical ideas — a better user interface for math, so to speak. Allan — Loved your hilarious geological analogy. Arguing that the content and the form of math should necessarily be alike is clearly a losing battle. Nonetheless I would like to see more of the elegance of thought that is so core to practice of math be applied to the presentation of mathematical ideas. On Sun, Dec 3, 2017 at 9:57 AM, Allan Wechsler <acwacw@gmail.com> wrote:
Mathematics is the study of form.
We define formal systems and then ask questions about them. The questions are not part of the systems, and I don't feel like they ought to be. One could define a formal system that contained something question-like embedded in its structure, but doing mathematics with this system would still involve asking external questions about that system.
I do not feel that this is a flaw. Geology is the study of rocks, but geological questions, the things that geologists investigate all the time, are not themselves rocks. Nobody complains about that.
On Sun, Dec 3, 2017 at 12:31 PM, Brent Meeker <meekerdb@verizon.net> wrote:
Of course the main reason for using natural language is that we apply mathematics and so an important part of learning is the interpretation of the symbolic notation for application. You can't ask questions in symbols just because you haven't introduced the necessary meta-mathematical symbolic language. But you easily could and write something like ?x[13+78=x]. But then you would still need to teach the natural language interpretation.
Brent
On 12/2/2017 11:06 PM, Scott Kim wrote:
I'm thinking about teaching the problem solving process in mathematics, and have run into a curious question: can one ask a mathematical question purely in mathematical notation? I believe the answer is no — mathematical questions always require human language in addition to mathematical notation. Problem statements are therefore always extramathematical in nature.
In practice, school kids frequently see problems stated in forms like: 13+78 = ___, which means "what is the sum of thirteen and seventy eight?" But that involves a nonmathematical symbol (the blank), AND ends up misleading kids to think that the equals sign means "the answer is". Very sloppy. We can do better.
This is an extension of something that has always bothered me: if mathematics is so rigorous, then how come it is conducted in a mish mosh of English and formal notation? The practical reason for mixing in human language is clear…like a computer program, a formal mathematical proof is more readable if it is annotated with comments. But too much reliance on human language means that formal proofs are not checkable by computer — a weird situation at best. I suppose that makes me a formalist, or a computer scientist…I've certainly got the latter bias because I don't trust anything I can't program.
— Scott _______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun