Структура исчисления предикатов - построение логического вывода
Категория реферата: Рефераты по математике
Теги реферата: как лечить шпоры, реферат на тему земля
Добавил(а) на сайт: Ленин.
Предыдущая страница реферата | 1 2 3 4 5 6 7 8 | Следующая страница реферата
В связи с отмеченной неразрешимостью логики предикатов особое значение приобретает здесь формализация понятий следования и закона логики посредством построения логических исчислений. Именно исчисление дает возможность во многих случаях синтаксическим образом решать вопрос, является ли некоторая формула законом, или соответственно есть ли некоторое отношение следования, когда мы не можем решить этот вопрос посредством семантического анализа. Для логики высказываний исчисление высказываний, вообще говоря, не является необходимым. Оно скорее нужно как часть логического исчисления для формул ЯЛП.
Исчисление предикатов
В основе исчисления предикатов лежит язык логики предикатов. В остальном оно является расширением исчисления высказываний.
Аксиоматическую систему исчисления предикатов мы получим, добавив к перечисленным выше схемам аксиоматического исчисления высказываний (имея в виду, конечно, переход к языку логики предикатов) следующие четыре схемы и одно правило:
1. ∀x A(x) ⊃ A(t) — схема ∀и .
2. A(t) ⊃∃х А(х) — схема ∃в.
3. ∀x (В ⊃ С(х)) ⊃ (В ⊃∀x С(х)) схема введения ∀ в консеквент .
4. ∀x (С(х) ⊃ В) ⊃ (∃x⊃C(x) ⊃ В) — схема введения ∃ в антецедент.
A(t) — результат правильной подстановки терма ( вместо х в А(х); В — не содержит х свободно.
Правило ∀в (правило введения квантора общности, иное
A(t) название: правило обобщения): —— (из А непосредственно выводимо∀x A).
Формально мы сохраняем прежнее определение вывода и доказательства (ясно, что, по существу, изменение состоит в том, что теперь могут использоваться новые аксиомы и новое правило), однако, если мы хотим, чтобы отношение формальной выводимости было аналогом семантического понятия следования, необходимо ограничить применение ∀в : оно может применяться к некоторой формуле А(х) для обобщения лишь по таким переменным х, которые не содержатся свободно в допущениях, от которых зависит эта формула. Чтобы смысл этого ограничения был ясным, мы должны определить понятие зависимости некоторой формулы вывода от допущений (гипотез). Везде в дальнейшем будем иметь в виду выводы с анализом (то есть обоснованием каждого его шага ссылками либо на принадлежность формулы этого шага к множеству взятых гипотез или аксиом системы, либо на формулы, из которых она получатся, и используемые при этом правила).
Формула В данного вывода зависит от некоторого допущения А, если и только если: а) она есть само допущение А;
б) получается из некоторых формул по правилам системы (из С⊃В и С по m. р. или из С по ∀в), какая-нибудь из которых зависит от А. Более простым образом понятие зависимости разъясняется в описываемой далее системе натурального вывода, значительно проще осуществляются там сами выводы и доказательства.
Натуральная система исчисления предикатов
Постулатами системы (исходными правилами) являются все правила натуральной системы исчисления высказываний и правила для кванторов.
Правила вывода для выражений с кванторами:
|
при условии, что никакое допущение из Г не содержит x свободно; |
|
A[Г] ∀x A[Г] |
∀и :
|
Результат правильной подстановки терма t вместо x в A(x); |
|
∀x A(x) [Г] A(t) [Г] |
∃в :
|
Предыдущая страница реферата | 1 2 3 4 5 6 7 8 | Следующая страница реферата Поделитесь этой записью или добавьте в закладкиКатегории: |