Спирина, М.С. Дискретная математика

P4: Ух Л(х) => А; Р5\ Ух (А => В) => (А => Vx Д). Выражения Р{—Р5 называют формальными схемами аксиом, так как из математической логики нам известна их общезначи­ мость. Эти схемы выражают те логические законы, которые вместе с правилами вывода и собственно математическими аксиомами образуют логику теории S. В качестве исходных примем правила вывода: 1. Из А и А => В выводимо В ( modusponens ): /?,: (А(А => В)) =» В. 2. Из А выводимо УхА (правило обобщения): R2: А =>УхА. К собственным аксиомам теории S относятся следующие фор­ мулы: 5,: х, = х2 => (х, = х 3 => х 2 = х3); S2: х, = х2 => х'| = х'2; 53: х', * 0 ; S4: х \ = х'2 => Xj = х2; S5: Х( + 0 = х^ 56: Xj + х 2 = (х, + х2)'; S7: xi ■ 0 = 0; S . #^ • 59 : /1(0) => Vx(/l(x) => Л(хО => Vx/l(x) (или /1(0) л Vx(/l(x) -> /l(x ')) => Vx/l(x), где A(x) — произвольная формула теории S. Формулу S9 называют аксиомой индукции. 9 . Какой семантический смысл вкладывается в эти аксиомы? Аксиомы ^ и S2 выражают свойства отношения равенства с учетом отношения «непосредственно следовать». Аксиомы 5 3 и 5 4 соответствуют аксиомам Пеано и выражают отношение «непосредственно не следуют ни за каким натураль­ ным числом». Аксиомы S 5 и S6 дают возможность индуктивно (рекурсивно) ввести операцию сложения. Аксиомы S7 и S 8 дают возможность индуктивно ввести опера­ цию умножения. В логику теории S принято вводить два важных понятия: опре­ деления формального доказательства и вывода. Тогда с помощью правил вывода можно получать любые новые. Сформулируем аксиомы Пеано. 1. Для каждого натурального числа а существует одно и только одно следующее за ним число. Новое число принято обозначать а'. 2. Единица является натуральным числом, причем она не сле­ дует ни за каким натуральным числом: а' Ф 1 (Уа е N). 3. Ни одно натуральное число не следует за двумя различными числами (а = Ь) => ( а' = Ь’) Уа' е N, УЬ' е N. 269