Основные понятия и методы теории формальных систем. Волохович А.В. - 18 стр.

    Отметим, что для перевода предложений с русского языка на
язык исчисления предикатов не существует механических правил. В
каждом отдельном случае нужно сначала установить, каков смысл
переводимого предложения, а затем пытаться передать тот же смысл
с помощью предикатов, кванторов и термов.
    Формулы исчисления предикатов имеют смысл только тогда,
когда имеется какая-нибудь интерпретация входящих в нее
символов.
    Под интерпретацией в исчислении предикатов будем понимать
всякую систему, состоящую из непустого множества V, называемого
областью интерпретации и какого-либо соответствия, относящего
каждой предикатной букве A n i некоторое n-местное отношение в V
(т. е. V n a {И, Л}), каждой функциональной букве f n i – некоторую n-
местную функцию в V (т. е. V n a V ) и каждой предметной константе
a i – некоторый элемент из V. При заданной интерпретации
предметные переменные мыслятся пробегающими область V этой
интерпретации, а логическим связкам ¬ , → , ~, &, ∨ и кванторам
придается их обычный смысл.
    Для данной интерпретации любая формула без свободных
переменных представляет собой высказывание, которое может быть
истинным или ложным, а всякая формула со свободными
переменными       выражает    некоторое   отношение       на   области
интерпретации. Причем это отношение может быть истинным для
одних значений переменных из области интерпретации и ложным
для других.
    Если область интерпретации конечна, то можно выяснить
истинность или ложность формулы, перебрав все различные
элементы множества. Однако на практике мощность множества
бывает настолько велика, что об этом не может быть и речи.
    Понятия общезначимости и противоречивости формул исчисления
предикатов аналогичны этим понятиям в исчислении высказываний.
Кроме того, будем называть формулу выполнимой, если она истинна,
по крайней мере, в одной интерпретации.


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

   Рассмотрим формальную          аксиоматическую      систему   ФС       для
исчисления предикатов.

     1. Исходными элементами ФС являются:
     а) счетное множество предметных переменных x 1 , x 2 , …, x n , …;
     б) конечное (может быть и пустое) или счетное множество
     предметных констант a 1 , a 2 , …, a n , …;



18