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

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

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

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

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

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

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

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

Кроме того, можно определить функциональные предикаты после доказательства соответствующей теоремы. (Если вы работаете в формальной системе, которая не позволяет вам вводить новые символы после доказательства теорем, вам придется использовать символы отношений, чтобы обойти это, как в следующем разделе.) В частности, если вы можете доказать что для каждого X (или любого X определенного типа), существует с уникальной Y, удовлетворяющей некоторым условием Р, то вы можете ввести символ функции 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 ). Наглядно, Р ( Х, 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 в одной переменной:

${\ Displaystyle \ forall A, \ существует B, \ forall C, C \ in A \ rightarrow F (C) \ in B.}$

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

${\ Displaystyle \ forall A, \ существует B, \ forall C, C \ in A \ rightarrow D \ in B.}$

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

${\ Displaystyle \ forall A, \ существует B, \ forall C, \ forall D, C \ in A \ rightarrow D \ in B.}$

Мы все еще должны ввести P для защиты этой количественной оценки:

${\ Displaystyle \ forall A, \ существует B, \ forall C, \ forall D, P (C, D) \ rightarrow (C \ in A \ rightarrow D \ in B).}$

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

${\ Displaystyle (\ forall X, \ существует! Y, P (X, Y)) \ rightarrow (\ forall A, \ существует B, \ forall C, \ forall D, P (C, D) \ rightarrow (C \ в A \ rightarrow D \ в B)).}$

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

• Функциональный символ (логика)
• Логическая связка
• Логическая константа