Георгий Рузавин - Логика и аргументация - Учебн. пособие для вузов.

Правило дизъюнкции(∨) разрешает перейти от строки, в которой встречается она, к другой, где вместо дизъюнкции встречаются два списка, в одном из которых находится один дизъюнктивный член, во втором - другой:

Это правило основывается на том, что дизъюнкция является истинной, если по крайней мере один из ее членов истинен, а поэтому при переходе от одной строки к другой мы получаем два списка, отделенных вертикальной чертой, в одном из которых встречается один член, во втором - другой.

Правило импликации(→) разрешает переходить от строки, где она встречается, к другой, в которой встречаются два списка формул, в одной из них содержится отрицание антецедента, в другой - консеквент импликации:

Действительно, импликация будет истинна, если ложен ее антецедент или истинен консеквент, что и представлено в заключении вывода.

Правило отрицания конъюнкцииразрешает в заключении переходить к отрицанию конъюнктивных членов, поскольку отрицание конъюнкции означает отрицание этих членов.

Г, ¬ (А ∧В)

Г, ¬ А, Δ ¬ Г, ¬ В, Δ

Правило отрицания дизъюнкцииразрешает в заключении переходить от отрицания дизъюнкции к отрицательным членам дизъюнкции, ибо дизъюнкция является ложной только тогда, когда ложны все члены дизъюнкции:

Г, ¬ ( А ∨ В ), Δ

Г, ¬ А, ¬ В, Δ

Правило отрицания импликацииразрешает в заключении переходить от отрицания импликации к утверждению ее антецедента и отрицанию консеквента, так как импликация оказывается ложной только тогда, когда антецедент истинен, а консеквент ложен:

Г, ¬ (А → В), Δ

Г, А, ¬ В, Δ

Двойное отрицание в одной строке может быть заменено утверждением в другой:

Г, ¬ ¬ А, Δ

Г, А, Δ

Квантор существования, который стоит перед формулой А, указывает на наличие объекта, удовлетворяющего

А. Назовем этот объект константой к. Очевидно, что А(к) будет истинно, ибо к удовлетворяет условию А:

Г, (Е х ) А , Δ

Г, А, (к), Δ

Квантор общности, встречающийся перед формулой, свидетельствует о том, что формула (х) А истинна тогда и только тогда, когда каждый индивид из универсума рассуждения удовлетворяет условию А, Тогда истинной оказывается любая формула вида А (т), получающаяся путем замены всех свободных вхождений переменной на любой замкнутый терм:

Г, (х) А, Δ

Г, (х) А, А(т), Δ

Формула с квантором общности (х) А сохраняется для того, чтобы в дальнейшем можно было применить его к другим термам.

Более строгий подход к доказательству формул достигается с помощью аксиоматического построения исчисления предикатов. Для доказательства формул логики, как и для доказательства теорем геометрии, необходимо указать некоторые исходные формулы, которые принимаются в качестве аксиом. В принципе в качестве аксиом могут быть взяты любые тождественно истинные или общезначимые формулы, которые играют роль законов логики. Но обычно при выборе аксиом руководствуются разного рода дополнительными требованиями: простоты получаемой формальной системы, минимального числа аксиом, их интуитивной очевидности и т.п. Чтобы вывести из исходных формул новые формулы, т.е. доказать последние как теоремы логики, необходимо ясно и точно перечислить также правила вывода или доказательства. К их числу относится правило заключения по схеме modus ponens: из двух формул А и А → В следует новая формула В. Кроме того, для получения новых формул используются различные правила подстановки. Например, свободная предметная переменная может быть заменена другой предметной переменной, если эта замена проводится одновременно на всех местах, где встречается свободная переменная. То же самое относится к переменной, обозначающей высказывание.

В качестве аксиом исчисления предикатов берутся, во-первых, аксиомы исчисления высказываний, во-вторых, к ним присоединяют две аксиомы, относящиеся к использованию кванторов общности и существования:

1) x v x → x;

2) х → (х v у);

3) (х v у) → (у v х);

4) (х → у) → [z v х → z v у].

К аксиомам, регулирующим использование кванторов, относятся:

5) (х) А (х) → А (у);

6) В (у) → (Ех) B (х).

Первая из них постулирует: если предикат А выполняется для всех х, то он выполняется также для какого-либо у. Вторая утверждает, что если предикат В, выполняется для какого-либо у, то существует х, для которого выполняется В.