В формальной логике и смежных разделах математики функциональный предикат или символ функции — это логический символ, который может быть применен к объектному термину для получения другого объектного термина. Функциональные предикаты также иногда называют отображениями , но этот термин имеет дополнительные значения в математике . В модели символ функции будет смоделирован функцией .
В частности, символ F в формальном языке является функциональным символом, если для любого символа X, представляющего объект в языке, F ( X ) снова является символом, представляющим объект в этом языке. В типизированной логике F является функциональным символом с типом домена T и типом кодомена U , если для любого символа X, представляющего объект типа T , F ( X ) является символом, представляющим объект типа U . Аналогичным образом можно определить функциональные символы более чем одной переменной, аналогично функциям более чем одной переменной; функциональный символ в нулевых переменных является просто константным символом.
Теперь рассмотрим модель формального языка, в которой типы T и U моделируются множествами [ T ] и [ U ], а каждый символ X типа T моделируется элементом [ X ] в [ T ]. Тогда F может быть смоделирован множеством
которая является просто функцией с областью [ T ] и областью значений [ U ]. Требованием последовательной модели является то, что [ F ( X )] = [ F ( Y )] всякий раз, когда [ X ] = [ Y ].
При обработке логики предикатов , которая позволяет вводить новые символы предикатов, также захочется иметь возможность вводить новые символы функций. Учитывая символы функций F и G , можно ввести новый символ функции F ∘ G , композицию F и G , удовлетворяющую ( F ∘ G )( X ) = F ( G ( X )), для всех X . Конечно, правая часть этого уравнения не имеет смысла в типизированной логике, если тип домена F не совпадает с типом кодомена G , поэтому это требуется для определения композиции.
Также автоматически получаются определенные функциональные символы. В нетипизированной логике есть предикат тождества id, который удовлетворяет id( X ) = X для всех X . В типизированной логике, если задан любой тип T , есть предикат тождества id T с доменом и кодоменом типа T ; он удовлетворяет id T ( X ) = X для всех X типа T . Аналогично, если T является подтипом U , то есть предикат включения домена типа T и кодомена типа U , который удовлетворяет тому же уравнению ; есть дополнительные функциональные символы, связанные с другими способами построения новых типов из старых.
Кроме того, можно определить функциональные предикаты после доказательства соответствующей теоремы . (Если вы работаете в формальной системе , которая не позволяет вводить новые символы после доказательства теорем, то вам придется использовать символы отношений, чтобы обойти это, как в следующем разделе.) В частности, если вы можете доказать, что для каждого X (или каждого X определенного типа) существует уникальный Y, удовлетворяющий некоторому условию P , то вы можете ввести функциональный символ F, чтобы указать на это. Обратите внимание, что P сам по себе будет реляционным предикатом, включающим как X, так и Y. Так что если есть такой предикат P и теорема:
тогда можно ввести функциональный символ F доменного типа T и кодоменного типа U , который удовлетворяет:
Многие трактовки логики предикатов не допускают функциональных предикатов, только реляционные предикаты . Это полезно, например, в контексте доказательства металогических теорем (таких как теоремы Гёделя о неполноте ), где нежелательно допускать введение новых функциональных символов (или любых других новых символов, если на то пошло). Но существует метод замены функциональных символов реляционными везде, где могут встречаться первые; более того, это алгоритмично и, таким образом, подходит для применения большинства металогических теорем к результату.
В частности, если F имеет тип домена T и тип кодомена U , то его можно заменить предикатом P типа ( T , U ). Интуитивно P ( X , Y ) означает F ( X ) = Y . Тогда всякий раз, когда F ( X ) появляется в утверждении, вы можете заменить его новым символом Y типа U и включить другое утверждение P ( X , Y ). Чтобы иметь возможность сделать те же выводы, вам нужно дополнительное предложение:
(Разумеется, это то же самое утверждение, которое необходимо было доказать как теорему, прежде чем вводить новый символ функции в предыдущем разделе.)
Поскольку устранение функциональных предикатов удобно для некоторых целей и возможно, многие трактовки формальной логики не имеют дело явно с символами функций, а вместо этого используют только символы отношений; другой способ думать об этом заключается в том, что функциональный предикат — это особый вид предиката, в частности тот, который удовлетворяет приведенному выше предложению. Это может показаться проблемой, если вы хотите указать схему предложения , которая применяется только к функциональным предикатам F ; как вы узнаете заранее, удовлетворяет ли она этому условию? Чтобы получить эквивалентную формулировку схемы, сначала замените что-либо в форме F ( X ) новой переменной Y . Затем выполните универсальную квантификацию по каждому Y сразу после того, как будет введен соответствующий X (то есть после того, как X будет квантифицирован по, или в начале утверждения, если X является свободным), и защитите квантификацию с помощью P ( X , Y ). Наконец, сделайте все утверждение существенным следствием условия уникальности для приведенного выше функционального предиката.
Возьмем в качестве примера схему аксиом замены в теории множеств Цермело–Френкеля . (В этом примере используются математические символы .) Эта схема утверждает (в одной форме) для любого функционального предиката F от одной переменной:
Во-первых, мы должны заменить F ( C ) некоторой другой переменной D :
Конечно, это утверждение неверно; D должно быть количественно определено сразу после C :
Нам все еще необходимо ввести P , чтобы защитить эту количественную оценку:
Это почти правильно, но это применимо ко слишком большому количеству предикатов; на самом деле нам нужно следующее:
Эта версия схемы аксиомы замены теперь подходит для использования в формальном языке, который не допускает введения новых функциональных символов. В качестве альтернативы можно интерпретировать исходное утверждение как утверждение в таком формальном языке; это было просто сокращение для утверждения, полученного в конце.
![{\displaystyle [F]:={\big \{}([X],[F(X)]):[X]\in [\mathbf {T} ]{\big \}},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b4330f8ae04afd533c5bf1fbe3fc20c065056d4d)
