Функциональный предикат

В формальной логике и связанных с ней разделах математики функциональный предикат или символ функции — это логический символ, который можно применить к термину объекта для создания другого термина объекта.Функциональные предикаты также иногда называют отображениями , но этот термин имеет дополнительные значения в математике .В модели функциональный символ будет моделироваться функцией .

В частности, символ F на формальном языке является функциональным символом, если для любого символа X, представляющего объект на языке, F ( X ) снова является символом, представляющим объект на этом языке.В типизированной логике F является функциональным символом с домена типом T и кодомена типом U , если для любого символа X представляющего объект типа T , F ( X ) является символом, представляющим объект типа U. , Аналогичным образом можно определить функциональные символы более чем одной переменной, аналогично функциям более чем одной переменной; символ функции в нулевых переменных — это просто постоянный символ.

Теперь рассмотрим модель формального языка, в которой типы T и U моделируются множествами [ T ] и [ U ], а каждый символ X типа T моделируется элементом [ X ] в [ T ].Тогда F можно смоделировать множеством

$[F]:={\big \{}([X],[F(X)]):[X]\in [\mathbf {T} ]{\big \}},$

это просто функция с доменом [ T ] и кодоменом [ U ].Требование непротиворечивой модели заключается в том, что [ F ( X )] = [ F ( Y )] всякий раз, когда [ X ] = [ Y ].

Представляем новые функциональные символы

При рассмотрении логики предикатов , которая позволяет вводить новые символы предикатов, необходимо также иметь возможность вводить новые функциональные символы. Учитывая функциональные символы F и G , можно ввести новый функциональный символ F ∘ G , композицию F ( и G , удовлетворяющую ( ∘ G ) ( X ) = F ( G F X )), для всех X .Конечно, правая часть этого уравнения не имеет смысла в типизированной логике, если тип домена F не соответствует типу кодомена G , поэтому это необходимо для определения композиции.

Определенные функциональные символы также получаются автоматически.В нетипизированной логике существует предикат id , который удовлетворяет условию id( X ) = X для всех X .В типизированной логике для любого типа T существует предикат идентичности id _T с типом домена и кодомена T ; он удовлетворяет id _T ( X ) = для всех X типа T. X Аналогично, если T является подтипом U ; , то существует предикат включения типа домена T и типа кодомена U , который удовлетворяет тому же уравнению существуют дополнительные функциональные символы, связанные с другими способами создания новых типов из старых.

Кроме того, можно определить функциональные предикаты после доказательства соответствующей теоремы .(Если вы работаете в формальной системе , которая не позволяет вам вводить новые символы после доказательства теорем, то вам придется использовать символы отношений, чтобы обойти это, как описано в следующем разделе.)В частности, если вы можете доказать, что для каждого X (или каждого X определенного типа) существует уникальный удовлетворяющий Y, некоторому условию P , то вы можете ввести функциональный символ F , чтобы указать это.Обратите внимание, что P сам по себе будет реляционным предикатом, включающим как X , так и Y .Итак, если существует такой предикат P и теорема:

Для всех X типа T , для некоторого уникального Y типа U , P ( X , Y ),

тогда вы можете ввести функциональный символ F типа домена T и типа кодомена U , который удовлетворяет:

Для всех X типа T , для всех Y типа U , P ( X , Y ) тогда и только тогда, когда Y = F ( X ).

Обходимся без функциональных предикатов

Многие трактовки логики предикатов не допускают использования функциональных предикатов, а только реляционных предикатов .Это полезно, например, в контексте доказательства металогических теорем (таких как теоремы Гёделя о неполноте ), когда нежелательно допускать введение новых функциональных символов (как и любых других новых символов, если уж на то пошло).Но существует метод замены функциональных символов реляционными символами, где бы они ни встречались; более того, это алгоритмический подход и, следовательно, подходящий для применения к результату большинства металогических теорем.

В частности, если F имеет тип домена T и кодомена тип U , то его можно заменить предикатом P типа ( T , U ).Интуитивно P ( X , Y ) означает ( X ) = Y. F Тогда всякий раз, когда F ( X ) появляется в операторе, вы можете заменить его новым символом Y типа U и включить другой оператор P ( X , Y ).Чтобы иметь возможность сделать такие же выводы, нужно дополнительное предложение:

Для всех X типа T , для некоторого единственного Y типа U , P ( X , Y ).

(Конечно, это то же самое утверждение, которое нужно было доказать как теорему, прежде чем вводить новый символ функции в предыдущем разделе.)

Поскольку исключение функциональных предикатов одновременно удобно и возможно для некоторых целей, многие трактовки формальной логики не имеют дело явно с функциональными символами, а вместо этого используют только символы отношений; Другой способ подумать об этом состоит в том, что функциональный предикат — это особый вид предиката, в частности тот, который удовлетворяет приведенному выше предложению.Это может показаться проблемой, если вы хотите указать схему предложения , применимую только к функциональным предикатам F ; как заранее узнать, удовлетворяет ли он этому условию?Чтобы получить эквивалентную формулировку схемы, сначала замените что-нибудь в форме F ( X новой переменной Y. ) Затем выполните универсальную количественную оценку каждого Y соответствующего X сразу после введения (то есть после количественной оценки X или в начале утверждения, если X свободен) и защитите количественную оценку с помощью P ( X , Y ).Наконец, сделайте все утверждение материальным следствием условия уникальности функционального предиката, приведенного выше.

Возьмем в качестве примера схему аксиом замены в теории множеств Цермело–Френкеля .(В этом примере используются математические символы .)Эта схема утверждает (в одной форме) для любого функционального предиката F в одной переменной:

$\forall A,\exists B,\forall C,C\in A\rightarrow F(C)\in B.$

Во-первых, мы должны заменить F ( C ) какой-то другой переменной D :

$\forall A,\exists B,\forall C,C\in A\rightarrow D\in B.$

Конечно, это утверждение неверно; D должен быть определен количественно сразу после C :

$\forall A,\exists B,\forall C,\forall D,C\in A\rightarrow D\in B.$

Нам все равно придется ввести P , чтобы защитить эту количественную оценку:

$\forall A,\exists B,\forall C,\forall D,P(C,D)\rightarrow (C\in A\rightarrow D\in B).$

Это почти правильно, но это применимо к слишком большому количеству предикатов; на самом деле мы хотим:

$(\forall X,\exists !Y,P(X,Y))\rightarrow (\forall A,\exists B,\forall C,\forall D,P(C,D)\rightarrow (C\in A\rightarrow D\in B)).$

Эта версия схемы аксиом замены теперь пригодна для использования в формальном языке, который не позволяет вводить новые функциональные символы. Альтернативно, можно интерпретировать исходное утверждение как утверждение на таком формальном языке; это было просто сокращение заявления, приведенного в конце.

См. также

• Символ функции (логика)
• Логическая связка
• Логическая константа