Дискуссионный математический форумМатематический форум

Математический форум Math Help Planet

Обсуждение и решение задач по математике, физике, химии, экономике

Теоретический раздел
Часовой пояс: UTC + 4 часа [ Летнее время ]
MathHelpPlanet.com RSS-лента Математического форума

Часовой пояс: UTC + 4 часа [ Летнее время ]


Независимость системы аксиом формализованного исчисления высказываний

Независимость системы аксиом формализованного исчисления высказываний


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


Понятие независимости аксиом


После того как теория построена и установлен ряд ее свойств, следует обратиться к ее истокам — к системе аксиом — для решения ряда вопросов. Почему в качестве аксиом выбраны именно эти формулы? Можно ли взять другие формулы в качестве аксиом? (Уже отмечалось, что имеется множество других аксиоматик для аксиоматической теории высказываний.) Можно ли сократить число аксиом до двух или одной? Можно ли из данной системы аксиом безболезненно исключить одну или две формулы? Ответу на последний вопрос и посвящается настоящая лекция.


Определение 17.1. Аксиома [math]A[/math] из системы аксиом [math]\Sigma[/math] называется независящей от остальных аксиом этой системы, если ее нельзя вывести (доказать) из множества [math]\Sigma\setminus\{A\}[/math] всех остальных аксиом системы [math]\Sigma[/math]. Система аксиом [math]\Sigma[/math] называется независимой, если каждая ее аксиома не зависит от остальных.


Из определения следует, как нужно доказывать независимость той или иной аксиомы от остальных аксиом данной системы. Нужно смоделировать одновременно все аксиомы данной системы, кроме той, независимость которой доказывается, т.е. построить модель, в которой бы выполнялись все аксиомы данной системы, кроме анализируемой аксиомы. Это означает, что каждому первоначальному понятию и отношениям между понятиями нужно придать конкретное содержание посредством каких-то конкретных предметов и отношений между ними. Причем сделать это нужно так, чтобы выбранные конкретные предметы и отношения между ними обладали свойствами, сформулированными в аксиомах из системы [math]\Sigma\setminus\{A\}[/math], и не обладали бы свойством [math]A[/math]. Такая совокупность конкретных предметов и отношений между ними называется моделью системы аксиом [math]\Sigma\setminus\{A\}[/math]. Наличие ее доказывает независимость аксиомы [math]A[/math] от аксиом из [math]\Sigma\setminus\{A\}[/math]. В самом деле, ведь если [math]A[/math] можно было бы вывести из [math]\Sigma\setminus\{A\}[/math], то во всякой модели, в которой выполнялись бы все аксиомы из [math]\Sigma\setminus\{A\}[/math], непременно выполнялась бы и аксиома [math]A[/math], и такой модели, в которой выполнялись бы все аксиомы из [math]\Sigma\setminus\{A\}[/math] и не выполнялась [math]A[/math], просто не существовало бы.


Докажем, что система аксиом (A1), (A2), (A3) формализованного исчисления высказываний независима с помощью построения соответствующих моделей.


Независимость аксиомы (A1). Доказательство осуществляется построением модели, в которой выполняются аксиомы (A2) и (A3), но не выполняется аксиома (A1).


Лемма 17.2. Аксиома (A1) не зависит от остальных аксиом (A2) и (A3) формализованного исчисления высказываний.


Доказательство. Рассмотрим трехэлементное множество [math]M=\{0;1;2\}[/math] и введем в нем две операции. Первая операция — унарная, сопоставляющая каждому элементу [math]A\in M[/math] элемент из [math]M[/math], обозначаемый [math]\lnot A[/math]; вторая — бинарная, сопоставляющая любым двум элементам [math]A[/math], [math]B\in M[/math] элемент из [math]M[/math], обозначаемый [math]A\to B[/math]. Причем сопоставление осуществляется по правилам, определяемым следующими таблицами:


[math]\begin{array}{|c||c|}\hline A& \lnot A\\\hline 0&1\\ 1&1\\ 2&0\\\hline \end{array}\qquad\qquad \begin{array}{|c|c||c|} \hline A& B& A\to B\\\hline 0&0&0\\ 0&1&2\\ 0&2&2\\ 1&0&2\\ 1&1&2\\ 1&2&0\\ 2&0&0\\ 2&1&0\\ 2&2&0\\\hline \end{array}[/math]

Если теперь всем переменным, входящим в формулу формализованного исчисления высказываний, придать некоторые значения из [math]M[/math], то согласно введенным правилам сама формула примет некоторое значение из [math]M[/math]. Формулу, всегда принимающую значение 0, назовем выделенной.


Во-первых, можно показать, что всякая формула, получающаяся по схеме аксиомы (A2), является выделенной. Для этого составим таблицу значений формулы (A2) (предпоследний столбец соответствует формуле [math]K\equiv (F\to G)\to (F\to H)[/math]


[math]\dpi{100}\begin{array}{|c|c|c||c|c|c|c|c|c|}\hline \begin{matrix}{}\\[-8pt]{}\end{matrix} F& G& H& G\to H& F\to(G\to H)& F\to G& F\to H& K& (A2)\\\hline 0&0&0&0&0&0&0&0&0\\ 0&0&1&2&2&0&2&2&0\\ 0&0&2&2&2&0&2&2&0\\ 0&1&0&2&2&2&0&0&0\\ 0&1&1&2&2&2&2&0&0\\ 0&1&2&0&0&2&2&0&0\\ 0&2&0&0&0&2&0&0&0\\ 0&2&1&0&0&2&2&0&0\\ 0&2&2&0&0&2&2&0&0\\ 1&0&0&0&2&2&2&0&0\\ 1&0&1&2&0&2&2&0&0\\ 1&0&2&2&0&2&0&0&0\\ 1&1&0&2&0&2&2&0&0\\ 1&1&1&2&0&2&2&0&0\\ 1&1&2&0&2&2&0&0&0\\ 1&2&0&0&2&0&2&2&0\\ 1&2&1&0&2&0&2&2&0\\ 1&2&2&0&2&0&0&2&0\\ 2&0&0&0&0&0&0&0&0\\ 2&0&1&2&0&0&0&0&0\\ 2&0&2&2&0&0&0&0&0\\ 2&1&0&2&0&0&0&0&0\\ 2&1&1&2&0&0&0&0&0\\ 2&1&2&0&0&0&0&0&0\\ 2&2&0&0&0&0&0&0&0\\ 2&2&1&0&0&0&0&0&0\\ 2&2&2&0&0&0&0&0&0\\\hline \end{array}[/math]

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


В-третьих, покажем, что правило вывода modus ponens сохраняет свойство выделенное, т.е. если формулы [math]F[/math] и [math]F\to G[/math] выделенные, то и формула [math]G[/math] — выделенная. В самом деле, в таблице, определяющей операцию [math]\to[/math] над элементами множества [math]M=\{0;1;2\}[/math], видим, что формулы [math]F[/math] и [math]F\to G[/math] принимают одновременно значение 0 только в первой строке. Но в этой строке и формула [math]G[/math] также принимает значение 0.


Итак, на основании трех доказанных утверждений можно сделать следующий вывод: всякая формула, выводимая из аксиом (A2) и (A3) с помощью правила modus ponens, является выделенной.


Теперь, чтобы убедиться, что формула (A1) не может быть выведена из аксиом (A2) и (A3) с помощью правила modus ponens, нужно установить, что она не является выделенной. В самом деле, если, например, [math]F[/math] принимает значение 1, a [math]G[/math] принимает значение 2, то вычисляем значение формулы (A1):


[math]F\to (G\to F)= 1\to (2\to1)= 1\to 0= 2\ne 0.[/math]

Требуемая модель построена, и лемма тем самым полностью доказана.




Независимость аксиомы (A2). Здесь строится модель, в которой выполняются аксиомы (A1) и (A3), но не выполняется аксиома (A2).


Лемма 17.3. Аксиома (A2) не зависит от аксиом (A1) и (A3) формализованного исчисления высказываний.


Доказательство. Снова рассмотрим трехэлементное множество [math]M=\{0;1;2\}[/math], но операции [math]\lnot[/math] и [math]\to[/math] над его элементами зададим по-другому, с помощью следующих таблиц:


[math]\begin{array}{|c||c|}\hline A& \lnot B\\\hline 0&1\\ 1&0\\ 2&1\\\hline \end{array} \qquad\qquad \begin{array}{|c|c||c|}\hline A& B& A\to B\\\hline 0&0&0\\ 0&1&2\\ 0&2&1\\ 1&0&0\\ 1&1&2\\ 1&2&0\\ 2&0&0\\ 2&1&0\\ 2&2&0\\\hline \end{array}[/math]

Снова назовем формулу исчисления высказываний выделенной, если при всякой подстановке вместо ее переменных любых элементов из [math]M[/math] она принимает значение 0. Предлагается самостоятельно проверить, что всякая формула, построенная как по схеме аксиом (A1), так и по схеме аксиом (A3), является выделенной. Нетрудно также видеть, что правило вывода modus ponens сохраняет свойство выделенное, т.е. если формулы [math]F[/math] и [math]F\to G[/math] выделенные, то и формула [math]G[/math] — выделенная. Следовательно, всякая формула, выводимая из аксиом (A1) и (A3) с помощью правила modus ponens, является выделенной.


Теперь, чтобы убедиться, что формула (A2) не может быть выведена из аксиом (A1) и (A3) с помощью правила modus ponens, нужно установить, что (A2) не является выделенной. Действительно, если, например, [math]F[/math] придать значение О, [math]G[/math] — 0 и [math]H[/math] — 1, то (A2) примет значение 2.




Независимость аксиомы (A3). Метод построения соответствующей модели не единственный путь доказательства независимости той или иной аксиомы от остальных аксиом данной системы. Покажем независимость аксиомы (A3) другим методом.


Лемма 17.4. Аксиома (A3) не зависит от остальных аксиом (A1) и (A2) формализованного исчисления высказываний.


Доказательство. Пусть [math]F[/math] — произвольная формула формализованного исчисления высказываний. Обозначим через [math]h(F)[/math] формулу, полученную из [math]F[/math] стиранием всех вхождений знака [math]\lnot[/math] в формуле [math]F[/math]. Легко понять, что для всякого частного случая [math]F[/math] схем (Al) и (A2) формула [math]h(F)[/math] есть тавтология алгебры высказываний. Далее, правило вывода modus ponens обладает следующим свойством: если [math]h(F\to G)[/math] и [math]h(F)[/math] — тавтологии, то и [math]h(G)[/math] — тавтология (так как [math]h(F\to G)[/math] совпадает с формулой [math]h(F)\to h(G)[/math]). Следовательно, всякая формула [math]F[/math], выводимая из (A1) и (A2) с помощью правила modus ponens, имеет в качестве [math]h(F)[/math] тавтологию.


Убедимся, что формула (A3) не выводима из (Al), (A2) с помощью правила modus ponens. Для этого нужно проверить, что какая-либо конкретная формула [math]F[/math], получающаяся по схеме (A3), имеет в качестве [math]h(F)[/math] формулу, не являющуюся тавтологией. Действительно, формула


[math]h\bigl[(\lnot X\to\lnot X)\to \bigl((\lnot X\to X)\to X\bigr)\bigr][/math]

есть следующая [math](X\to X)\to \bigl((X\to X)\to X\bigr)[/math]. Нетрудно проверить, что последняя формула не является тавтологией. (Найдите ее значение при [math]X=0[/math].) Следовательно, формула (A3) не выводима из (A1) и (A2).


Независимость системы аксиом. Из лемм 17.2–17.4 вытекает следующая теорема.


Теорема 17.5. Система аксиом (Al), (A2), (A3) формализованного исчисления высказываний независима.


Часовой пояс: UTC + 4 часа [ Летнее время ]


Яндекс.Метрика

Copyright © 2010-2016 MathHelpPlanet.com. All rights reserved