Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

называть примитивными связками, а Ai,A2, A3,... - пропозициональными буквами. 2. Формулы теории L определим индуктивным образом: 1) все буквы • суть формулы; 2) если^ и В формулы, то( ^ ) и {А^В) тоже формулы; 3) выражение теории L является формулой только тогда, когда это следует из 1) и 2). Будем считать, что: А&В служит обозначением для формулы ( —I(A^(—B))), А у В служит обозначением для формулы ((—А)^В), А=В служит обозначением для формулы ( —i((A^B)^(—i(B^A)))). Из определения формул видно, что всякая формула из L есть пропозициональная форма, построенная из пропозициональных букв Ai,A2... с помощью связок —1 и Будем придерживаться тех же правил опускания скобок в формулах, что и раньше для пропозициональных форм. 3. Аксиомы теории L. Каковы бы ни были формулы А, В Я С теории L, следующие формулы суть аксиомы теории L: А1:А^(В^А); А2: (А^(В^>С))^((А^В)^(А^>С)); A3: (—В^—А)^(( —IB^A)^B). Заметим, что А1 - A3 являются схемами аксиом, т.е. указывают, как строятся аксиомы для произвольных формул 5 и С. В силу произвольности формул А, В Я С схемы аксиом А1-АЗ порождают бесчисленное множество аксиом. Легко убедиться, например, с помощью таблиц истинности, что каждая аксиома, полученная по схемам ^7-^5, является тавтологией. 4. Единственным правилом вывода теории L служит правило modus ponens: В есть непосредственное следствие^ яА^В. Это правило сокращенно обозначают MP. Modus ponens в переводе означает «правило отделения». Отметим, что теорема 1.1 утверждает, что если А и А^В тавтологии, то и 5 тоже тавтология. Следовательно, правило modus ponens из тавтологий получает тавтологию. Очевидно, правило MP означает, что А,А^В \-В. Таким образом, задали некоторую формальную аксиоматическую теорию, которая и называется исчислением высказываний. Рассмотрим некоторые доказательства в этой теории. То, что начала существуют, необходимо принять, прочее следует доказать. Аристотель 109