Тождественно истинные формулы

Множество всевозможных формул логики высказываний с точки зрения принимаемых этими формулами значений разбивается на три класса:

1. Формулы, принимающие значения И при всех наборах входящих в них переменных называются тождественно истинными (ТИФ).

2. Формулы, принимающие значения Л на всех наборах значений переменных, входящих в них, называются тождественно ложными (ТЛФ).

3. Формулы, принимающие при некоторых наборах значений переменных значения И, при других – Л, называются выполнимыми.

Предложение «j - тождественно истинная формула» обозначают |‑j.

На практике мы ввели важное понятие равносильности формулы логики высказывания. Две формулы А и В равносильны (АºВ) тогда и только тогда, когда они представляют одну и ту же функцию от входящих в нее переменных, то есть для всех наборов значений переменных значения истинности формул А и В совпадают, в противном случае формулы не равносильны.

Таким образом, на первый взгляд может показаться, что для установления равносильности формул достаточно сравнить их значения на всевозможных наборах переменных. Однако кажущаяся простота решения проблемы наталкивается на ряд серьезных затруднений.

1. Во-первых, если число переменных не очень мало, то число наборов, которые нужно подставлять, будет очень велико и применение простого принципа сравнения формул А и В может стать практически невозможным. Уже для 30 переменных потребуется проверить 10⁹ наборов (это примерно соответствует 2³⁰). При этом для установления равносильности нужно для каждого набора провести вычисление значений обеих формул, а если эти формулы большой длины, то на это, в свою очередь, понадобится большое число операций.

2. Во-вторых, ‑ и это соображение, по видимому более важно – в логике высказываний, в логике предикатов и их приложениях речь пойдет о равносильности не двух каких-либо формул, а о равносильности бесконечного множества формул. Таким образом, нужны утверждения, согласно которым все формулы некоторого определенного вида равносильны соответственно формулам некоторого определенного вида, то есть нужны общие соображения, общие правила вывода одних формул из других.