Функциональный предикат
 |
В формальной логике и связанных с ней разделах математики функциональный предикат или символ функции — это логический символ, который можно применить к термину объекта для создания другого термина объекта.Функциональные предикаты также иногда называют отображениями , но этот термин имеет дополнительные значения в математике .В модели функциональный символ будет моделироваться функцией .
В частности, символ F на формальном языке является функциональным символом, если для любого символа X, представляющего объект на языке, F ( X ) снова является символом, представляющим объект на этом языке.В типизированной логике F является функциональным символом с домена типом T и кодомена типом U , если для любого символа X представляющего объект типа T , F ( X ) является символом, представляющим объект типа U. , Аналогичным образом можно определить функциональные символы более чем одной переменной, аналогично функциям более чем одной переменной; символ функции в нулевых переменных — это просто постоянный символ.
Теперь рассмотрим модель формального языка, в которой типы T и U моделируются множествами [ T ] и [ U ], а каждый символ X типа T моделируется элементом [ X ] в [ T ].Тогда F можно смоделировать множеством
![{\displaystyle [F]:={\big \{}([X],[F(X)]):[X]\in [\mathbf {T} ]{\big \}},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b4330f8ae04afd533c5bf1fbe3fc20c065056d4d)
это просто функция с доменом [ 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 в одной переменной:
Во-первых, мы должны заменить F ( C ) какой-то другой переменной D :
Конечно, это утверждение неверно; D должен быть определен количественно сразу после C :
Нам все равно придется ввести P , чтобы защитить эту количественную оценку:
Это почти правильно, но это применимо к слишком большому количеству предикатов; на самом деле мы хотим:
Эта версия схемы аксиом замены теперь пригодна для использования в формальном языке, который не позволяет вводить новые функциональные символы. Альтернативно, можно интерпретировать исходное утверждение как утверждение на таком формальном языке; это было просто сокращение заявления, приведенного в конце.
