§ 7. Проблема установления вида формул алгебры высказываний.

Табличный способ установления вида формул алгебры высказываний при числе переменных n5 является громоздким, поэтому в математической логике был разработан другой способ установления вида формул алгебры высказываний, основанный на следующих двух теоремах - критериях.

Критерий 1. Формула алгебры высказываний F(x₁, x₂, ..., x_n) тогда будет ТИ, когда каждая дизъюнкция ее КН формы содержит хотя бы одну переменную с ее отрицанием, то есть имеет вид .

Доказательство. Пусть FИ и F^k ее КН форма, то есть , где есть ДО.

Так как FИ, то и F^kИ, что возможно в том случае, когда каждый ДО является истинным. То теореме 1 § 6 ДО будет ТИ только тогда, когда он содержит хотя бы одну дизъюнкцию вида .

Критерий 2. Формула алгебры высказываний F(x₁, x₂, ..., x_n) тогда будет ТЛ, когда каждая конъюнкция ее ДН формы содержит хотя бы одну переменную с ее отрицанием, то есть имеет вид .

Доказательство (аналогично критерию 1).

Пусть F  Л, и F^д - ее ДН форма, то есть , где есть КО.

Так как F  Л, то и F^д  Л, что возможно в том случае, когда каждый КО является ложным. По теореме 2 § 6 КО будет ТЛ тогда и только тогда, когда он содержит хотя бы одну конъюнкцию вида .

Из доказанных критериев следует второй способ установления вида формул алгебры высказываний, который представляет собой алгоритм установления вида формул алгебры высказываний.

1. Преобразуем данную формулу алгебры высказываний какой-либо равносильной ей КН форме, если она не задана в этом виде.

2. Если данная дизъюнкция этой формы имеет вид , то данная формула является ТИ.

3. Если второй шаг не выполняется, то преобразуем данную формулу к какой-либо равносильной ей ДН форме.

4. Если каждая конъюнкция этой формы имеет вид , то данная формула ТЛ.

5. Если четвертый шаг не выполняется, то данная формула является и выполнимой и опровержимой.