Наше наиболее общее понятие сигнатуры определяется следующим образом.
Определение 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 |– t1 = t2 G |– F(t2) | |||
| (З=) | ||||
| G |– F(t2) | G |– F(t1) |
где t1 и t2 свободные для v в F(v).
Дата добавления: 2015-10-05; просмотров: 799;