Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы (стр. 3 )

p	p →p
0	1
1	0

Противоречивость

Формула называется противоречивой логической формулой тогда и только тогда, когда она обозначает функцию равнозначную константе 1 . Примером противоречивой формулы является формула (p ~P).

P	(p ~P)
0	0
1	0

Нейтральность

Формула, не являющаяся ни общезначимой, ни противоречивой, называется нейтральной. Примером нейтральной формулы является формула (P).

P	(p)
0	1
1	0

Следование и равносильность формул

Одна формула следует из другой тогда и только тогда, когда для любой интерпретации, для которой значение обозначаемой второй формулой функции равнозначно 1 , значение обозначаемой первой формулой функции также равнозначно 1 .Например, формула ( P →Q) следует из формулы (P^Q). Это записывается так ((P^Q)' (P →Q)). Если формула следует из любой формулы, т. е. является общезначимой, то это записывается так: (' (P →P)). Формула следует из формулы тогда и только тогда когда множество невыполнимо.

Две формулы равносильны тогда и только тогда, когда следуют друг из друга. Например, формулы (PvQ) и (P→Q) равносильны, так как: ((PvQ)'(P→Q)) и ((P→Q) '(PvQ)). Равносильность формул записывается так: ((P→Q)ó(PvQ)). Следовательно, две формулы равносильны тогда и только тогда, когда обозначают функции, для которых существует каждой из них равнозначная или равная функция.

11.  Понятие метатеоремы. Метатеорема дедукции.

Метатеорема - теорема относительно объектов (понятий, определений, аксиом, доказательств, правил вывода, теорем и др.) какой-либо научной теории (т. н. предметной, или объектной, теории), доказываемая средствами метатеории этой теории. Термин «метатеорема» употребляется преимущественно в применении к теоремам об объектах формализованных теорий (т. е. в случае, когда предметная теория является исчислением, или формальной системой). Если метатеорема, относящаяся к какому-либо логико-математическому исчислению, доказывается т. н. финитными средствами, ни в какой форме не использующими абстракции актуальной бесконечности, то её относят к метаматематике; таковы, напримертеорема Гёделя о неполноте формальной арифметики и более богатых систем.

Теорема дедукции, доказанная Эрбраном, по-видимому, самый эффективный прием в классическом исчислении высказываний. Хотя она и называется "теоремой" дедукции – это метод, который применяется для доказательства теорем. То есть, как говорят, метатеорема. Метатеорема дедукции (МТД): G1, G2,..., Gβ-1, Gβ R, то можно составить доказательство G1, G2,..., Gβ-1 Gβ R. Проще говоря, значок можно переносить справа налево, на место запятой, оставляя вместо него на каждом шаге символ :

Обратное движение также допустимо, причем, обоснование этого (в отличие от метатеоремы дедукции) элементарно. Пусть у нас имеется старое доказательство: G1, G2,..., Gβ-1 Gβ R. Построим на его основе новое доказательство: G1, G2,..., Gβ-1, Gβ R. Если R - аксиома, или одна из гипотез G1, G2,..., Gβ, то новое доказательство получится сразу (длиной в 0 строк). Иначе возьмем старое доказательство целиком и добавим в его конец одну дополнительную строку:

Gβ, Gβ R R // MP - старое доказательство плюс одна эта строка как раз и составят новое доказательство. Самое крайнее положение значка при движении вправо - перед последней формулой R (дальше modus ponens двигать значок не позволяет). Самое крайнее положение значка при движении влево - с краю формулы. При движении значка вправо символ должен ставится на место операции , которая обрабатывается (согласно скобкам и приоритетам) самой последней. Если в формуле последней обрабатывается другая операция, то дальнейшее движение значка невозможно. При движении влево надо не забывать расставлять скобки, чтобы в образовавшейся формуле новый символ обрабатывался (согласно скобкам и приоритетам) самым последним.

12.  Связь тождественно-истинных высказываний и теорем исчисления высказываний, формальной теории высказываний.

13.  Формальное доказательство двойного отрицания ( {}).

14.  Формальное доказательство перехода от прямого заключения к заключению от обратного ({}  {}).

15.  Формальное доказательство закона исключенного третьего ( {}).

16.  Категоричность, a-категоричность, непротиворечивость и полнота формальных теорий. Эрбранова модель.

Математическую теорию, изучающую данную аксиоматическую теорию как единое целое, устанавливающую свойства данной аксиоматической теории, называют метатеорией по отношению к изучаемой теории, и методы математической логики являются основными методами этой науки. Факты, устанавливаемые в ней относительно изучаемой аксиоматической теории, называют метатеоремами.

Непротиворечивость. Аксиоматическая теория называется непротиворечивой, если ни для какого утверждения А, сформулированного в терминах этой теории, само утверждение А и его отрицание! А не могут быть одновременно теоремами этой теории. Чтобы установить непротиворечивость аксиомат. теории, необходимо проверить систему аксиом на противоречия и истинность логических умозаключений.

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

Пусть α – какое-нибудь кардинальное число (мощность). Теория первого порядка Т называется α-категоричной, если Т имеет хотя бы одну модель мощности α и любые две ее модели мощности α изоморфны.

Полнота. Аксиоматическая теория называется абсолютно полной, если для любого утверждения А, сформулированного в терминах этой теории, точно одно из утверждений А и! А является ее теоремой. Аксиоматическая теория называется полной в узком смысле (или в смысле Поста), если добавление к ее аксиомам любого недоказуемого в ней утверждения с сохранением всех правил вывода приводит к противоречивой теории. Всякая абсолютно полная теория будет полна в узком смысле. Классическим примером неполной системы аксиом является система аксиом и постулатов «Начал» Евклида (так, для обоснования наличия точки пересечения у двух прямых требуется аксиома непрерывности). Всякая полная и непротиворечивая аксиоматическая теория категорична. Не всякая категоричная теория полна.

Вероятностной Эрбрановой моделью сигнатуры W будем называть пару M = áU, mñ, где m – вероятность на Â. Функциональные символы интерпретируются на U обычным образом. Эрбрановой моделью сигнатуры W будем называть вероятностную Эрбранову модель M = áU, Iñ, где I : Â ® {0, I}.

17.  Правило введения отрицания. (Справедливость метода доказательства от противного в исчислении высказываний).

Суть метода доказательства от противного. Для того, чтобы доказать утверждение X→Y, предполагается, что верно утверждение Х. Отсюда нужно логическими рассуждениями прийти к утверждению Y. Вместо этого делается предположение, противное тому, которое требуется доказать, т. е. предполагается Y. Далее, рассуждая на основании этого предположения, мы приходим к нелепому выводу Х. «Нелепость» вывода состоит в том, что он противоречит исходному данному утверждению Х. Получение такого вывода заставляет нас отвергнуть сделанное предположение Y и принять то, которое требовалось доказать, – Y. Это возможно, потому что в этом состоит логический закон контрапозиции X → Y≡ Y → X устанавливающий равносильность этих утверждений.