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

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

В частности, символ 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 F и G удовлетворяющую ( , ∘ 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 и теорема:

Для всех 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 ) означает F ( X = Y. ) Тогда всякий раз, когда 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)).$

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

См. также

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