Mathematical logic (theoretical logic, symbolic logic) is a branch of mathematics that studies proofs and questions of the foundations of mathematics. “The subject matter of modern mathematical logic is varied.” Mathematical logic is logic by subject, mathematics by method.
Application in logic of mathematical methods becomes possible when judgments are formulated in some exact language. Such precise languages have two sides: syntax and semantics. Syntax is the set of rules for constructing language objects (usually called formulas). Semantics is called the set of conventions that describe our understanding of formulas (or some of them) and allow us to regard some formulas as true and others as not.
The concepts of deductive theory and calculus play an important role in mathematical logic. A calculus is a set of rules of inference that allow some formulas to be considered deductible. The rules of inference are divided into two classes. One of them directly qualifies some formulas as deducible. Such rules of deduction are called axioms.
The relation of calculi to semantics is expressed by the notions of semantic fitness and semantic completeness of a calculus. An AND calculus is called semantically suitable for the language I if any formula inferred in AND is true. Similarly, an AND calculus is called semantically complete in the language Y if any true formula of Y is derivable in Y.
Many of the languages considered in mathematical logic have semantically complete and semantically correct calculi. In particular, C. Gödel’s result that the so-called classical predicate calculus is semantically complete and semantically suitable for the language of classical first-order predicate logic is well known. On the other hand, there are many languages for which the construction of a semantically complete and semantically suitable calculus is impossible. In this area a classical result is Gödel’s incompleteness theorem, which asserts the impossibility of a semantically complete and semantically suitable calculus for a language of formal arithmetic.
It is worth noting that in practice the set of elementary logic operations is a mandatory part of the instruction set of all modern microprocessors and is accordingly included in programming languages. This is one of the most important practical applications of mathematical logic methods studied in modern computer science textbooks.
Of particular interest to mathematical logic are the technologies of evidentiary programming by V. A. Kaymin, which involves the development of algorithms and programs with proofs of the correctness of algorithms. The peculiarity of technologies of evidentiary programming is the need to write not only algorithms and programs, but also to write together with them proofs of the absence of errors in them. Which has always been considered a purely mathematical activity.