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



страница2/11
Дата03.12.2012
Размер0.93 Mb.
ТипДокументы
1   2   3   4   5   6   7   8   9   10   11

Интерпретация логических формул. Таблицы интерпретаций. Зависимость мощности множества интерпретаций от мощности носителя модели формальной теории.

Модель логики предикатов задается множеством элементов (носителей) и множеством отношений на этом множестве элементов (сигнатурой). Любое множество предикатов задает хотя бы одну модель.

Каждая формула языка логики предикатов обозначает некоторой предикат. Интерпретацией формулы логики предикатов называется функция, которая каждой предметной переменной ставит в соответствие ее значение. Как можно будет увидеть из последующих примеров число интерпретаций формулы в модели равно mn, где n – есть число свободных предметных переменных в формуле, а m – мощность носителя модели. Число моделей, которые можно построить равно , где p – число предикатов (мощность сигнатуры модели), qi – число аргументов (арность) предиката i, m – мощность носителя модели.

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

Рассмотрим пример:

a

b

c





gif" name="object5" align=bottom width=110 height=19>

0

0

0

0

1

0

0

0

1

0

1

0

0

1

0

1

1

1

0

1

1

1

1

1

1

0

0

1

0

0

1

0

1

1

0

0

1

1

0

1

1

1

1

1

1

1

1

1

  1. Семантическая классификация логических формул. Общезначимость, нейтральность, противоречивость. Отношение равносильности формул.

Общезначимость

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

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)). Следовательно, две формулы равносильны тогда и только тогда, когда обозначают функции, для которых существует каждой из них равнозначная или равная функция.

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

Метод доказательства от противного применяется также и в других формах. Например, вместо импликации X → У доказывают равносильную ей импликацию (X ^¬ Y) → ¬X, т.е. предполагая, что истинны утверждения Х и ¬У, выводят истинность утвержде­ния ¬X в противоречие с предположением. На основании равно­сильности Х→ Y≡ (X ^¬ Y) → ¬X. Сделается вывод об истинности импликации X → Y. Вторая равносильность Х→ Y≡ (X ^¬ Y) → Y дает возможность заменить доказательство импликации X → Y доказательством импликации (X ^¬ Y) → Y, т.е. предположив, что истинны утверждения X и ¬Y, вывести отсюда истинность утверждения К в противоречие с предположением. Наконец еще одна форма этого метода, являющаяся также одной из форм мето­да приведения к абсурду, основа­на на равносильности X → Y≡ (X ^¬ Y) → (Z ^¬ Z) Предполагая, что истинны утверждения Хи ¬Y, выводим из них некоторое ут­верждение и его отрицание.

Метод доказательства от противного имеет две модификации: метод приведения противоположного утверждения к абсурду и метод приведения данного утверждения к абсурду.

Первый метод состоит в следующем. Пусть требуется доказать утверждение Х. Допускается противоположное ему утверждение ¬Х и из него выводятся два противоречащих друг другу утверждения Y и ¬Y: ¬X → Y и ¬X → ¬Y. Из этого делается вывод о том, что справедливо исходное утверждение Х. Оправданием этому методу служит тавтология:. (¬X→¬Y) → ((¬X→Y)→X).

Второй метод состоит в следующем. Пусть требуется опровергнуть Х, т.е. доказать ¬Х. В этом случае два противоречащих друг другу утверждения Y и ¬Y выводятся не из утверждения ¬Х, а из самого данного утвреждения Х: Х→Y и X→¬Y. Из этого делается вывод о том, что справедливо !Х, т.е. данное утверждение Х опровергнуто. Оправданием этому методу служит тавтология: (X→¬Y) → ((X→Y)→¬X).
1   2   3   4   5   6   7   8   9   10   11

Похожие:

Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы icon1 формальные теории 1 Основные положения
Мы рассмотрели две логических системы: алгебру высказываний и логику предикатов. Это было содержательное рассмотрение. Попытаемся...
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconЗаконы (принципы) формальной логики Логическая культура. Значение логики. Язык логики. Семантические категории языка
Отношения между понятиями (сравнимые и несравнимые, совместимые и несовместимые понятия)
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconФормальные теории
Язык формальной арифметики. Выразимость в этом языке любого разрешимого отношения. β-функция Гёделя
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconСписок экзаменационных вопросов по курсу «Системное программное обеспечение»
Понятие формальной грамматики и языка. Выводимость. Язык, порождаемый грамматикой
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconПлан занятий по онтологическому инжинирингу Введение в онтологический инжиниринг
Пропозициональная (ПЛ) или Булева логика (синтаксис: атомарные (пропозициональный символ P, Q, r и т д.) и сложные (на основе простых)...
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconЭквивалентность двух определений элементарной формальной системы
«Исчисления и формальные системы» (стр. 267) и «Основания математической логики» (стр. 68). Ясно, что эти два определения в некотором...
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconВычислительные Машины и Системы Математическое Обеспечение Вычислительных Систем Разработка формальной грамматики

Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconСинтаксис английского языка синтаксис
При всех существующих пониманиях предмета синтаксиса раздел соответствующей теории (языкознания, семиотики), занимающийся изучением...
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы icon1. Синтаксис и семантика языков программирования. Алфавит языка Borland Pascal. Описание синтаксиса языка: синтаксические диаграммы
Синтаксис языка совокупность правил, определяющих допустимые конструкции (слова, предложения) языка, его форму
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconОтношение семантического включения в свете аналитических тенденций л. В. Воронина Белгородский гу, Белгород, Россия
Все три подхода нашли отражение в исследованиях по лингвистике, однако чаще ученые обращаются к данной проблеме при исследовании...
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org