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

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

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

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

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

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

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

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

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

Для всех Икс типа Т, для некоторых уникальных Y типа U, п(Икс,Y),

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

Для всех Икс типа Т, для всех Y типа U, п(Икс,Y) если и только если Y = F(Икс).

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

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

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

Для всех Икс типа Т, для некоторых уникальный Y типа U, п(Икс,Y).

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

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

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

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

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

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

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

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

Смотрите также