Студопедия
Случайная страница | ТОМ-1 | ТОМ-2 | ТОМ-3
АрхитектураБиологияГеографияДругоеИностранные языки
ИнформатикаИсторияКультураЛитератураМатематика
МедицинаМеханикаОбразованиеОхрана трудаПедагогика
ПолитикаПравоПрограммированиеПсихологияРелигия
СоциологияСпортСтроительствоФизикаФилософия
ФинансыХимияЭкологияЭкономикаЭлектроника

Исчисление предикатов первого порядка

Логический смысл исчислений | Классическое натуральное исчисление высказываний. Правила вывода | Выводы и доказательства | V Пример | V Пример | V Пример | Язык классической логики предикатов | V Пример | V Пример | V Пример |


Читайте также:
  1. Dj Первого сексуального Рома «SuperHair» Ромовый
  2. I. Из первого издания поэмы
  3. VIII. Враг порядка — человек
  4. VIII. Выполнение внутреннего распорядка личным составом подразделения
  5. VIII. Что за упразднением первого плотского обрезания постановится второе — духовное
  6. Билет 32. Политические реформы (1905-1907). Манифест об усовершенствовании государственного порядка от 17 октября 1905 г. основные законы российской империи
  7. Билет 36 Свержение монархии в России (март 1917)Двоевластие. Приказ №1 Петроградского совета. Преобразования Временного правительствапервого состава.

Вывод в исчислении предикатов — это не пустая и конечная последовательность формул, каждая из которых является либо посылкой, либо получена из предыдущих формул согласно одному из дедуктивных принципов так, что после применения правил Éв и Øв все формулы, начиная с последней посылки и вплоть до результата применения данного правила, не используются в дальнейших шагах построения вывода, при этом ни одна переменная не ограничивает сама себя и ни одна индивидуальная переменная не ограничивается абсолютно более одного раза. В том случае, если никакая абсолютно ограничивавшаяся в выводе переменная не встречается свободно в неисключённых посылках и заключении, имеет место завершённый вывод.

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

Пошаговый переход от одной формулы к другой осуществляется в исчислении предикатов посредством выполнения всех правил вывода, применяемых в исчислении высказываний, к которым добавляются кванторные правила вывода, а именно: 1) введения, 2) исключения кванторов.

К дедуктивным принципам введения кванторов относятся правила:

1.1. — введения квантора общности (обозначим символом «"в»), выражаемое схемой:

А (x/ y, z1, …, zn)

______________________ , гдеy— абсолютное ограничение, z1, …, zn — ограничение.

"x A (x, z1, …, zn)

1.2. — введения квантора существования (обозначим символом «$в»), выражаемое схемой:

А (x/ t)

___________ .

$x А (x)

2.1.— исключения квантора общности (обозначим символом «"и»), выражаемое схемой:

"x А (x)

___________ .

А (x/ t)

2.2. — исключения квантора существования (обозначим символом «$и»), выражаемое схемой:

$x А (x, z1, …, zn)

______________________ , гдеy— абсолютное ограничение, z1, …, zn — ограничение.

А (x/ y, z1, …, zgn)

В правилах «введения квантора существования» и «исключения квантора общности» запись A(x/t) означает результат правильного замещения термом t всех имеющихся в формуле A(x) свободных вхождений предметной переменной x.

 


Дата добавления: 2015-09-05; просмотров: 40 | Нарушение авторских прав


<== предыдущая страница | следующая страница ==>
V Пример| V Пример

mybiblioteka.su - 2015-2024 год. (0.006 сек.)