Система аксиом II.

ІI 1. A®(B®A);

II 2. (A®(B®C))®((A®B)®(A®C);

II 3. (ùA®ùB)®((ùA®B)®A).

Приведенные системы аксиом равносильны в том смысле, что порождают одно и то же множество формул. Какая из систем лучше? Это зависит от точки зрения. Система II компактнее и обозримее; соответственно более компактны и доказательства различных её свойств. С другой стороны, в более богатой системе I короче выводы различных формул.

Правила вывода.

1) Правило подстановки. Если u – выводимая формула, содержащая букву А (обозначим это факт u ( А ) ), то выводимая формула u(β), получаю­щаяся из u заменой всех вхождений А на произвольную формулу

U(A)

U: ——— ;

u(β)

2) правило заключения (Modus Ponens). Если u и u Þβ – выводимые формулы, то β выводима:

u, u Þ β

U: ——— .

β

В этом описании исчисления высказываний аксиомы являются форму­лами исчисления (соответствующими определению формулы); формулы же использованные в правилах вывода (u, u Þ β и т. д.), это ”метаформулы“ или схемы формул. Схема формул, например uÞ β обозначает множество всех тех формул исчисления, которые получаются, если её метапеременные заменить формулами исчисления: скажем, если u заменить на А, а β – на A&B и, то из схемы формул u Þ β получим формулу АÞA&B.

Исчисления предикатов и теории первого порядка.