The relevance of the study of the logic of predicates?

Question

Mathematics

Friends, welcome everyone! I ask people who know and understand mathematical logic, including the logic of predicates, to explain to me in simple words WHY it is needed? What is the relevance of the study of this section of logic?

We were given the topic of the final work to write educational software for the analysis of the record of predicate formulas. In this regard, I would like to understand what is the relevance of such a program, what would be useful for automating the analysis of such formulas. The functionality of the program will include the definition of bound and free variables, the presence of repetitions among variables, the proposal of options for transformation, finding the area of ​​action of quantifiers, and so on and so forth.
Thanks to this, a thousand and one questions arise in my head: why, for example, the connectivity of variables is determined and where it is used further ... In terms of definitions, I have already studied everything, it remains to understand why and why all this is needed))

Let's rewind a little, I want to to say that Google and other search engines did not save me, I studied many manuals and books, but everywhere they write in general terms that it is needed to formalize statements, etc. ... and then they describe the terminology and a bunch of formulas. And I would like to go into details: how exactly the predicate logic formulas contribute to this formalization, how they further develop into a program code, and in what areas (with details of HOW and WHY) they are used ...

I'm interested in your point of view, I really hope for advice, maybe someone knows the literature where you can go deep and read something interesting, or maybe someone can immediately give a detailed answer!

Thank you for your time and attention, all the best!)

Answer 1

First of all, the relevance for you is that this is a pretty good exercise that will teach you how to program not the most trivial things.
In real life, of course, there is nothing new in this. There is software that can do all this and much more, at a much more advanced level than the student is able to implement in the final work.

Google and other search engines did not save me

Well, I googled this in a few seconds, maybe you didn’t come across it, there is also about the real application.
https://en.wikipedia.org/wiki/Automated_proving...
the English version of the wiki describes in more detail: https://en.wikipedia.org/wiki/Automated_theorem_proving
and automatic translation from the English version: https://translated.turbopages. org/proxy_u/en-ru.ru...
https://habr.com/ru/post/519368/

and further they already describe the terminology and a bunch of formulas

Yes, here they are:
https://qudata.com/ds/ru/theory/theorem_proving.html
By the way, are you familiar with the Prolog language?
https://habr.com/en/post/124636/

Answer 2

In a nutshell, this allows you to organize lazy computing and parallel computing. If you can calculate the logical connection of instructions in a program, then you can optimize it, i.e. Compilers are the third direction.

Answer 3

Using
First-Order Logic as a Formal Model of Reasoning
Being a formalized analogue of ordinary logic, first-order logic makes it possible to strictly reason about the truth and falsity of statements and their interrelation, in particular, about the logical consequence of one statement from another, or, for example, about their equivalence. Consider a classic example of the formalization of natural language statements in first-order logic.
Let us take the reasoning “Every man is mortal. Socrates is a man. Therefore, Socrates is mortal." Let's denote "x is a man" through MAN(x) and "x is mortal" through MERTEN(x). Then the statement "every man is mortal" can be represented by the formula: x(MAN(x) → DEATH(x)) the statement "Socrates is a man" by the formula MAN(Socrates), and "Socrates is mortal" by the formula DEATH(Socrates). The statement as a whole can now be written as