Правила для кванторов всеобщности



 
  G |– F(v)
(В")  
  G |– " v F(v)

 

 

 
  G |– " v F(v)
(У")  
  G |– F (t)

 

 

где v не является свободной где t является
переменной для любой формулы в G подстановочным для v в F(v)
   

В каждой из следующих задач выведите данную формулу из пустого множества посылок.

3.19(P(a) & " x (P(x) Й Q(x))) Й Q(a).

3.20" xy P(x, y) Й " x P (x, x).

Правила для кванторов существования

 
  G |– F(t)
(В$)  
  G |– $ v F(v)

 

 

 
  G |– $ v F(v) G И { F(v) }|– C
(У$)  
  G |– C

 

 

где t – подстановочный где для C и любой формулы из G
для v в F(v) v не является свободной переменной
   

В каждой из следующих задач выведите данную формулу из пустого множества посылок.

3.21(P(a) Ъ P(b)) Й $ x P(x).

3.22$ x P(x) є " x P(x).

Корректность и полнота логики предикатов

Множество правил вывода для логики предикатов обладает свойством корректности и полноты подобно свойствам пропозициональных выводов.

Теорема корректности.Если существует вывод замкнутой формулы F из множества формул G, тогда G влечёт F.

Теорема полноты.Для любой замкнутой формулы F и любого множества предложений G, если G влечёт F, то существует вывод F из некоторого подмножества G.

Полнота логики предикатов для случая счётного G и для другого множества правил вывода была доказана Куртом Гёделем в 1930 году.

Функциональные символы и равенство: синтаксис

Логика предикатов, определённая выше немного более ограничена, чем что обыкновенно называется ``логикой первого порядка'', и наша следующая цель – удалить эти ограничения. Во-первых, мы обобщим понятие терма. В дополнение к объектным константам и объектным переменным, мы разрешим построение термов с использованием символов для функций, ``функциональных констант''. Во-вторых, мы добавим к языку знак равенства, и уравнения будут включены как новый тип атомарных формул.

Наше наиболее общее понятие сигнатуры определяется следующим образом.

Определение 28 (Сигнатура,константы).Сигнатура – это множество символов двух типов – функциональных констант и предикатных констант – с неотрицательным целым числом, называемым арностью, связанным с каждым символом. Объектная константа – это функциональная константа арности 0. Функциональная константа унарна, если её арность равна 1, и бинарна, если её арность равна 2. Пропозициональная константы, так же как унарные и бинарные предикатные константы, определены как выше.

Определение 29 (Терм).Возьмём сигнатуру s, не включающую ни дополнительных символов, указанных в начале данной части, ни знака равенства. Множество X строк замкнуто относительно правил построения термов, если

  • каждая объектная константа принадлежит X,
  • каждая объектная переменная принадлежит X,
  • для каждой функциональной константы h арности n (n > 0) и любой строки t1, ... , tn, если t1, ... , tn принадлежит X, тогда также принадлежит h(t1, ... , tn).

Строка является термом, если она принадлежит все множествам, которые замкнуты относительно правил построения.*

3.23Каждый терм содержит объектную константу или объектную переменную. Верно или нет ?

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

  • пропозициональные константы,
  • строки вида R(t1, ... , tn) где R – предикатная константа арности n (n > 0) и t1, ..., tn – термы,
  • строки вида (t1 = t2), где t1, t2 – термы.

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

Для любых термов t1 и t2, t1 t2 обозначает формулу (t1 = t2).

Функциональные символы и равенство: семантика

 

Выводы в логике первого порядка

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

Новые аксиомы выражают рефлексивность равенства и имеют вид Ж |– t = t , где t – произвольный терм. Новые правила вывода – правила замены:

 
  G |– t1 = t2 G |– F(t1)
(З=)  
  G |– F(t2)

 

 

 
G |– t1 = t2 G |– F(t2)
 
G |– F(t1)

 

 

где t1 и t2 свободные для v в F(v).*

Для каждой из следующих формул найдите вывод из пустого множества посылок.

3.27x = y Й f(x, y) = f(y, x).

см. Решение

3.28" x $ y (y = f(x)).

3.29$ y (x = y & y = z) Й x = z.

3.30$ x (x = a & P (x)) є P (a).

Теории первого порядка

Теория первого порядка сигнатуры s определяется с помощью аксиом. Интерпретация, при которой истинны все аксиомы теории первого порядка G, называется моделью G. Если теория первого порядка G выполнима, мы также говорим что она непротиворечива. Логические следствия теории первого порядка называется её теоремами. Доказательство предложения F в теории первого порядка G есть вывод F из подмножества аксиом из G.

Теоремы корректности и полноты выполняются для логик предикатов с функциональными символами и равенством и могут быть сформулированы в рамках теорий первого порядка следующим образом. В соответствие с теоремой корректности, если существует доказательство предложения F в теории первого порядка G, тогда F является теоремой G. В соответствие с теоремой полноты Гёделя, обратное также верно: для любой теоремы F теории первого порядка G, существует доказательство F в G.

Однако, добавление правил вывода для кванторов второго порядка ведёт к формальной системе которая корректна, но не полна.


Дата добавления: 2018-02-28; просмотров: 508; Мы поможем в написании вашей работы!

Поделиться с друзьями:






Мы поможем в написании ваших работ!