I've been interested in the subject of metalanguages and how (if) we can formalize them. Most metalanguages I've encountered use some variation of a natural language (such as English, German or French). Therefore, a relevant question is "how can we formalize natural languages" or at least, certain aspects of it. However, there are very few sources (As far as I've seen) that concern themselves with the subject. I've only seen two papers that have dealt with a similar subject, thus far; One from Richard Montague, and the other from Thomas Graf.
If you could kindly introduce me to references such as papers, books or any resources that deal with this subject itself and/or its prerequisites (such as syntax, semantics, formal languages), I'd be most thankful.
I'm an undergraduate student in my fourth semester; I'm not as familiar as I'd like to be in both logic and linguistics; So, even the most trivial resource would be most useful to me.
Thank you, very much.
Best Answer
So, here are a few directions you may wish to explore for formalizing natural language, which is a broad topic. From looking a bit, this question does not appear to be an exact duplicate of an earlier question, but there may be some other questions such as this one that will help.
One is formalized systems that resemble natural language.
This includes the Mizar system which is a piece of software that validates proofs written in a syntax that's like a cross between a programming language and mathematical prose. There is a Proof Assistants Stack Exchange with more information on Mizar and other proof assistants.
One direction might be studying metalogic.
Metalogic uses natural language to avoid circularity, but its use of language is different from natural language in other settings. In particular, metalogical if is the material conditional, usually.
One thing to check out might be the Open Logic Project which has a few free and open source textbooks on logic. Boxes and Diamonds, the book on modal logic, covers some approaches to formalizing the notions of possibility and necessity (and some other things like time and deontic status). It includes a lot of examples of explicit metalogical analysis using Kripke frames.
One direction might be cataloging the difficulties we would run into if we attempted to formalize natural language.
Aside from the difficulties with quantifiers mentioned in the comments, such as in the famous example someone loves everyone. The connectives themselves like and, or, not, and if are tough to formalize. A compelling account of all of their usages is elusive.
The Connectives by Lloyd Humberstone, has examples taken from natural language of different kinds of phenomena that defy a straightforward encoding in a logical system. This book is quite big and full of technical details about different logics, but the introductory sections on the chapters about specific connectives have good examples of natural language use.