Биохимия спиртового брожения: Основу технологии получения пива составляет спиртовое брожение, - при котором сахар превращается...
Автоматическое растормаживание колес: Тормозные устройства колес предназначены для уменьшения длины пробега и улучшения маневрирования ВС при...
Топ:
Процедура выполнения команд. Рабочий цикл процессора: Функционирование процессора в основном состоит из повторяющихся рабочих циклов, каждый из которых соответствует...
Отражение на счетах бухгалтерского учета процесса приобретения: Процесс заготовления представляет систему экономических событий, включающих приобретение организацией у поставщиков сырья...
Комплексной системы оценки состояния охраны труда на производственном объекте (КСОТ-П): Цели и задачи Комплексной системы оценки состояния охраны труда и определению факторов рисков по охране труда...
Интересное:
Финансовый рынок и его значение в управлении денежными потоками на современном этапе: любому предприятию для расширения производства и увеличения прибыли нужны...
Инженерная защита территорий, зданий и сооружений от опасных геологических процессов: Изучение оползневых явлений, оценка устойчивости склонов и проектирование противооползневых сооружений — актуальнейшие задачи, стоящие перед отечественными...
Принципы управления денежными потоками: одним из методов контроля за состоянием денежной наличности является...
Дисциплины:
2017-09-30 | 475 |
5.00
из
|
Заказать работу |
|
|
Определение 1.16
Формальным доказательством (в теории L) называется конечная последовательность формул , причем каждая формула этой последовательности либо аксиома, либо получена по правилу MP из каких-либо двух предшествующих формул этой последовательности. Формальное доказательство является доказательством своей последней формулы . Формула B называется формально доказуемой, или формальной (теории L), если она имеет формальное доказательство.
Утверждение “Формула B формально доказуема в теории L” обозначается .
Введем соглашения:
a) Индекс L опускать;
b) Говорить «формальное доказательство», «формально доказуема», «формальная теорема» - доказательство «доказуема», «теорема».
Пример 1
Установить, что
1. 1. AC2 C=A,
2. 2. AC1
3. 3. MP(2, 1)
4. 4. AC1
5. 5.MP(4, 3)
Пояснение AC2 A, , B, C означает, что записано AC2, в которой формула С заменила формулой А, а формула В – формулой , пояснение MP(2, 1) означает, что формула получена в результате применения правила MP к формулам с номерами 2 и 1.
Следует заметить, что в проверенном доказательстве каждая из пяти формул. Является теоремой, в том числе и выписывание первые две аксиомы: доказательство любой аксиомы состоит из этой аксиомы.
Определение 1.17
Формальным выводом формулы B из формул, которые называются посылками или гипотезами называется конечная последовательность формул , заканчивающаяся формулой , причем каждая формула этой последовательности:
1. или одна из посылок ;
2. или аксиома;
3. или формула, полученная из некоторых двух предшествующих формул этой последовательности по правилу MP.
Если формальный вывод B из формул , то формула B называется формально выводимой из формул и обозначается: , или , где .
|
Очевидно, что доказательство – частный случай формального вывода из пустого множества посылок.
Введем соглашение: вместо «формальный вывод», «формально-выводима» будем говорить «вывод», «выводима».
В определениях 1.16 и 1.17 употребляемые термины «формальное доказательство», «формально доказуема», «формальный вывод», «формально-выводима» для явного указания на то, что эти доказательства и выводы строятся в предметной языки. Используемые слева от доказательства или вывода нумерация и справа от доказательства или вывода пояснения уже относится к метаязыку.
Пример 2
Установить, что , .
1. 1. Посылка
2. 2. Посылка
3. 3. AC4
4. 4.MP (2, 3)
5. 5. AC5
6. 6. MP (2, 5)
7. 7. MP (4, 1)
8. 8. MP (6, 7)
9. , 9. ОФВ- определение формального вывода (1-8)
Запись 9 подытоживает формальный вывод формулы С из формул , . Запись 9 сделана на метаязыке.
Свойства отношения выводимости.
Метатеорема 1(МТ1).
a) .
b) Если и , то
Доказательство
a) Для построения вывода формула из формул достаточно записать последовательно все формулы (в произвольном порядке), поместив последней формулу .
b) Заменив в данном выводе формулы С из формул формулы их данными выводами из формул .
Метатеорема 2 (МТ2).
Пусть Г – любое множество формул.
Тогда:
a) Если Г , то Г, В частности
b) Если , то
Следствие:
a) Если , то .
b) Если , то .
Метатеорема 3(МТ3).
Теорема дедукции (ТД), правило введения импликации (ВИ).
Пусть Г – любое множество формул.
Тогда:
c) Если Г, , то Г . В частности
d) Если , то .
Доказательство
По условию МТ3 вывод (1) формула B из множества формул (данный вывод).
Требуется доказать существование вывода (2) формула из формул множества Г (результирующий вывод).
Опишем алгоритм превращения данного вывода (1) в результирующей вывод (2). К каждой формуле данного вывода (1) припишем слово «». Тогда получим последовательность формул: , (3) заканчивающуюся нужной формулой . Эта последовательность не является, вообще говоря, выводом из множества формул Г. Однако можно перед каждой формулой вставить дополнительные формулы так, чтобы превратить последовательность формул (3) в (2). Вывод дополнительных формул зависит от того, с каким обоснованием формула входит в данный вывод (1). Возможны 4 типа обоснований:
|
1. - посылка множества Г;
2. - посылка А;
3. - аксиома;
4. – формула, полученная по MP из двух предшествующих формул и (p,q<i).
Рассмотрим каждый из этих случаев:
1. Пусть и . В этом случае является посылкой не только в данном выводе (1), но и в результирующем выводе (2). Тогда перед формулой последовательности (3) вставим две формулы и , из которых получается по правилу MP:
l. l. посылка
l +1. l +1. AC1
l +2. l +2. MP(l, l+1)
2. Пусть . Тогда - посылка в данном выводе (1), но не является таковой в результирующем выводе (2). В последовательности (3) будет стоять формула , которая является доказуемой (пример 1). Поэтому перед вставляем первые четыре формулы из ее доказательства.
3. Пусть – аксиома. Тогда поступаем, как и в случае 1.
4. Пусть – формула, полученная по MP из формул и (p,q<i) последовательности (1). Тогда должна иметь вид (или имеет вид ). Итак, получена из и по MP. В последовательности (2) в этом случае будут формулы и с некоторыми номерами S и t(S,t<i), и нужно обосновать включение в вывод (2) формула . Но формулы и и являются частями AC2. Таким образом, перед в данном случае необходимо вставить две формулы с номерами и :
S. S
……… …
t. t
……… …
U. AC2
U+1. MP(S, U)
U+2. MP(t,
Следствия:
a) Если , то . В частности;
b) Если , то .
|
|
Таксономические единицы (категории) растений: Каждая система классификации состоит из определённых соподчиненных друг другу...
История развития хранилищ для нефти: Первые склады нефти появились в XVII веке. Они представляли собой землянные ямы-амбара глубиной 4…5 м...
Двойное оплодотворение у цветковых растений: Оплодотворение - это процесс слияния мужской и женской половых клеток с образованием зиготы...
Опора деревянной одностоечной и способы укрепление угловых опор: Опоры ВЛ - конструкции, предназначенные для поддерживания проводов на необходимой высоте над землей, водой...
© cyberpedia.su 2017-2024 - Не является автором материалов. Исключительное право сохранено за автором текста.
Если вы не хотите, чтобы данный материал был у нас на сайте, перейдите по ссылке: Нарушение авторских прав. Мы поможем в написании вашей работы!