Используя формальные языки, логики записывают математические
утверждения в виде последовательностей символов ("формул").
Доказательства при этом становятся последовательностями формул,
подчинающимися определённым "правилам вывода".

Мы рассказываем о языке пропозицональных формул (исчисление
высказываний, в том числе интуиционистское --- доказывается его
полнота относительно моделей Крипке) и о языках первого порядка
(исчисление предикатов). Попутно разбираются вопросы сложности
булевых функций, выразимости (элиминация кванторов в арифметике
сложения и в элементарной теории вещественных чисел), начала
теории моделей (теоремы о полноте и компактности, о повыщении и
понижении мощности, об устойчивости при ограничениях,
расширениях и объединениях цепей), элементы нестандартного
анализа (учения о бесконечно малых).

Предварительных знаний не требуется --- мы рассчитываем на
читателя, заинтересовавшегося математической логикой, но ещё не
знакомого с ней.