Question in consideration: Mathematics as several Type-0 Grammars

I've asked the question above because I've been trying to understand the way mathematicians do mathematics from a formalist perspective.

I'm soon to do my thesis, and I really like the concept of formal grammars, formal languages, etc. It's very likely that I will have the chance to do my thesis about this stuff and so I want to iron out some misconceptions about it that I might have.

Unfortunately for me, this question was closed as being opinion based.

I provided some context along the question to help the possible answerer understand my level of understanding - I also provided a link to something called an "Infinitary Logic" that would provide as a possible counterexample to my ideas. I also explained why I think it's not a counterexample of my ideas.

I really want some kind of closure for this question, perhaps I could have reworded it better or split it up into smaller questions.

Furthermore, I received which I assume is a well-meaning comment about how my description of mathematics is a "cartoon version" of actual mathematics. It'd be great if this were the case, but looking back at all the mathematics that was taught to me - I just don't see it.

Any constructive criticism is welcome, please don't hold back.

  • $\begingroup$ I was taught a heck of a lot of different sports in my schooling, and speaking with actual athletes I've come to realize that my understanding is at best a cartoon version of what they do. Perhaps your understanding of how people do math is at a similar level? $\endgroup$ – JonathanZ supports MonicaC Jul 14 '20 at 16:44
  • $\begingroup$ @JonathanZsupportsMonicaC Well, perhaps. But then it begs the question - I have done math at the undergraduate level. I progressively passed and am now closer and closer to finishing the degree, and to pass you are given a finite exam with finite statements in it and you produce back a finite answer to every statement in it. The person marking the exam then gets to decide whether or not the blob of symbols I gave them is what they expect as correct. If I show you Chinese, assuming none of us know Chinese, I could have showed you an alien language. $\endgroup$ – Threnody Jul 14 '20 at 16:48
  • $\begingroup$ @JonathanZsupportsMonicaC And that's precisely what I'm asking here. I think the question has an objective answer - any counterexample will do. My question is begging for a reference to that alien language for which one cannot write down and devise a finite algorithm to understand it. $\endgroup$ – Threnody Jul 14 '20 at 16:49
  • $\begingroup$ As a general sidenote, automatic theorem proving algorithms have existed since a long long time. To build an ATP you need to know what statements are "ok" (well defined grammar), what proof system you'll be using and what you consider to be true with no justification (the axioms). It's another monster of its own whether or not it's a tractable solution but that's not the point here $\endgroup$ – Threnody Jul 14 '20 at 16:52
  • $\begingroup$ @XanderHenderson It does in a way, although the answer doesn't have a "clause" for opinion based as a reason, and even though I did try to engage with the commenters, I still understood why it was ultimately closed. I suppose for such a broad question, I failed to explain why it is of interest as well. $\endgroup$ – Threnody Jul 14 '20 at 23:11
  • $\begingroup$ I would say that a question closed for being opinion based is one which has, in my opinion, been closed for a deficit of quality. $\endgroup$ – Xander Henderson Jul 14 '20 at 23:14
  • $\begingroup$ @XanderHenderson Understood - I think the question does have some pitfalls. From hindsight - It would've been better to split it up. $\endgroup$ – Threnody Jul 14 '20 at 23:16

You most likely have a strong intuition about doing mathematics in "formal grammars, formal languages, etc." that motivated your Question. But having gone through it twice, it seems a long way from being suitable content for Math.SE.

Calling it "opinion based" may be the best peg to hang this Question on, but that is something of an ironic understatement. The notion of "type-0 grammars" is introduced without particular motivation or context, but you almost surely know that this is perhaps the broadest possible class of grammars that one might call formal.

The gist of your Question then seems to be whether some field of mathematics would not be amenable to such a treatment ("where one cannot sit down and think through").

Generally fields of mathematics are presented with sufficient rigor that formalizing definitions and proofs proceeds with general consensus that the underlying semantics are being properly captured. However it is unquestionably a matter (like beauty) of "in the eye of the beholder." You need someone who both understands the topic to be formalized and has the facility to use the formal tools properly. Lacking one or the other of these, one necessarily would rely on the opinion of those who have both, as to the adequacy of the formalization.

An interesting topic is looking for useful areas of mathematics where the Community is not wholly satisfied with existing formalizations. After much study one might contribute either by improving the formalization or by clarifying the mismatch between topic and tools.

Trying to discuss this from a 30,000 foot level seems ambitious and too broad for a Math.SE Question. Your Question suggests that you want to pursue studies in this area, and that is admirable. But a more tractable problem would involve asking for details of formalizing a particular mathematical argument.

  • $\begingroup$ You have a point here, I am very glad you wrote this answer. Yes, this topic interests me too much to be considered healthy. On the comment about "type-0 grammars" - I assume mathematicians study them as well? I've been introduced to them through my cs studies, not through my mathematics units. The idea I was trying to capture is that mathematics usually starts from an idea and is then written, you know, strings. I'm not going to go into it again because I understand now that is possibly too broad and imprecise to answer in a way that doesn't seem dismissive. $\endgroup$ – Threnody Jul 14 '20 at 23:07
  • 1
    $\begingroup$ I think, hardmath, that what you've written here would be a good answer to the question on main. $\endgroup$ – Gerry Myerson Jul 14 '20 at 23:14
  • $\begingroup$ Also another point, I did use the "formal-languages" tag, where type-0 grammars are typically introduced in the literature. $\endgroup$ – Threnody Jul 14 '20 at 23:14
  • $\begingroup$ @GerryMyerson I think so too. $\endgroup$ – Threnody Jul 14 '20 at 23:14

Not the answer you're looking for? Browse other questions tagged .