Логика предикатов . Пример формальной теории первого порядка

Формальные теории первого порядка представляют собой яркий пример формальных теорий с аксиоматикой и правилами вывода и обладают следующим свойством: в них кванторы могут связывать только предметные константы, а не предикаты. Будем рассматривать теорию, в которой используются две логические связки ( ך,→) и кванторные символы (,). Множество аксиом представлено следующими схемами:

A1.      A → (A →B),

A2.      (A → (B → C)) → ((A → B) → (A → C)),

A3.      (ךA → ךB) → (B → A),

A4.      xF(x) →F(y),

A5.      F(y)→ xF(x).

В схеме 4 должен быть свободен для переменной в формуле .

В любой теории первого порядка имеются следующие правила вывода:

A,A → B (R1)                B → A(x) (R2)                A(x) → B (R3)

B                                    B →xA(x)                          xA(x)→ B

Правило R1 является знаментитым и называется modus ponens, или правилом заключения. Покажем на примере, как с помощью нашей теории доказывается знаменитый аристотелевский силлогизм:

Все люди смертны. Сократ – человек. Следовательно, Сократ смертен.

Этот силлогизм является частным случаем более общего силлогизма:

Все, кто обладает свойством P, обладает свойством Q. y обладает свойством P. Следовательно, y обладает свойством Q.

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

x(P(x) → Q(x))

P(y)         .

Q(y)

Формальный вывод заключения из посылок состоит в следующем:

1. В первую аксиому A₄ вместо F(x) подставим P(x)→Q(x). Получим:x(P(x)→Q(x))→(P(y)→Q(y)).

2. Из предыдущей формулы и первой посылки по правилу заключения R₁ следует, что формула: P(y)→Q(y).

3. Из предыдущей формулы и второй посылки по правилу заключения R1 выводима формула Q(y), ч.т.д.