In der formalen Logik und den verwandten Zweigen der Mathematik ist ein funktionelles Prädikat oder Funktionssymbol, ein logisches Symbol, das auf einen Gegenstand-Begriff angewandt werden kann, um einen anderen Gegenstand-Begriff zu erzeugen.

Funktionelle Prädikate werden auch manchmal mappings genannt, aber dieser Begriff hat andere Bedeutungen ebenso.

In einem Modell wird ein Funktionssymbol durch eine Funktion modelliert.

Spezifisch ist das Symbol F auf einer formellen Sprache ein funktionelles Symbol, wenn in Anbetracht eines Symbols das X Darstellen eines Gegenstands auf der Sprache, F (X) wieder ein Symbol ist, das einen Gegenstand auf dieser Sprache vertritt.

In der getippten Logik ist F ein funktionelles Symbol mit dem Bereichstyp T und codomain Typ U, wenn in Anbetracht eines Symbols das X Darstellen eines Gegenstands des Typs T, F (X) ein Symbol ist, das einen Gegenstand des Typs U vertritt.

Man kann Funktionssymbole von mehr als einer Variable ähnlich definieren, die Funktionen von mehr als einer Variable analog ist; ein Funktionssymbol in Nullvariablen ist einfach ein unveränderliches Symbol.

Betrachten Sie jetzt ein Modell der formellen Sprache, mit den Typen T und U als modelliert durch Sätze [T] und [U] und jedes Symbol X des Typs T modelliert durch ein Element [X] in [T].

Dann kann F durch den Satz modelliert werden

der einfach eine Funktion mit dem Gebiet [T] und codomain [U] ist.

Es ist eine Voraussetzung eines konsequenten Modells dass [F (X)] = [F (Y)] wann auch immer [X] = [Y].

Das Einführen neuer Funktionssymbole

In einer Behandlung der Prädikat-Logik, die erlaubt, neue Prädikat-Symbole einzuführen, wird man auch im Stande sein wollen, neue Funktionssymbole einzuführen.

Das Einführen neuer Funktionssymbole von alten Funktionssymbolen ist leicht; gegebene Funktionssymbole F und G, es gibt ein neues Funktionssymbol F o G, die Zusammensetzung von F und G, (F o G) (X) = F (G (X)) für alle X befriedigend.

Natürlich hat die richtige Seite dieser Gleichung in der getippten Logik keinen Sinn, wenn der Bereichstyp von F den codomain Typ von G nicht vergleicht, so ist das für die Zusammensetzung erforderlich, definiert zu werden.

Man bekommt auch bestimmte Funktionssymbole automatisch.

In der ungetippten Logik gibt es ein Identitätsprädikat id, der id (X) = X für alle X befriedigt.

In der getippten Logik, in Anbetracht jedes Typs T, gibt es ein Identitätsprädikat id mit dem Gebiet und codomain Typ T; es befriedigt id (X) = X für alle X des Typs T.

Ähnlich, wenn T ein Subtyp von U ist, dann gibt es ein Einschließungsprädikat des Bereichstyps T und codomain Typs U, der dieselbe Gleichung befriedigt; es gibt zusätzliche mit anderen Weisen vereinigte Funktionssymbole, neue Typen aus alten zu bauen.

Zusätzlich kann man funktionelle Prädikate nach dem Beweis eines passenden Lehrsatzes definieren.

(Wenn Sie in einem formellen System arbeiten, das Ihnen nicht erlaubt, neue Symbole nach dem Beweis von Lehrsätzen einzuführen, dann werden Sie Beziehungssymbole verwenden müssen, um darum, als in der folgenden Abteilung herumzukommen.)

Spezifisch, wenn Sie beweisen können, dass für jeden X (oder alle X eines bestimmten Typs), dort ein einzigartiger Y besteht, der etwas Bedingung P befriedigt, dann können Sie ein Funktionssymbol F einführen, um das anzuzeigen.

Bemerken Sie, dass P selbst ein Verwandtschaftsprädikat sein wird, das sowohl X als auch Y einschließt.

So, wenn es solch ein Prädikat P und einen Lehrsatz gibt:

: Für alle X des Typs T, für einen einzigartigen Y des Typs U, P (X, Y),

dann können Sie ein Funktionssymbol F vom Bereichstyp T und codomain Typ U einführen, der befriedigt:

: Für alle X des Typs T, für den ganzen Y des Typs U, P (X, Y) wenn und nur wenn Y = F (X).

Das Auskommen ohne funktionelle Prädikate

Viele Behandlungen der Prädikat-Logik erlauben funktionelle Prädikate, nur Verwandtschaftsprädikate nicht.

Das ist zum Beispiel im Zusammenhang nützlich, metalogical Lehrsätze zu beweisen (wie die Unvollständigkeitslehrsätze von Gödel), wo man die Einführung von neuen funktionellen Symbolen (noch irgendwelchen anderen neuen Symbolen, was das betrifft) nicht erlauben will.

Aber es gibt eine Methode, funktionelle Symbole durch Verwandtschaftssymbole zu ersetzen, wo auch immer der erstere vorkommen kann; außerdem ist das algorithmisch und so passend, um die meisten metalogical Lehrsätze auf das Ergebnis anzuwenden.

Spezifisch, wenn F Bereichstyp T und codomain Typ U hat, dann kann es durch ein Prädikat P vom Typ (T, U) ersetzt werden.

Intuitiv, P (X, Y) bedeutet F (X) = Y.

Dann, wann auch immer F (X) in einer Behauptung erscheinen würde, können Sie ihn durch ein neues Symbol Y vom Typ U ersetzen und eine andere Behauptung P (X, Y) einschließen.

Um im Stande zu sein, dieselben Abzüge zu machen, brauchen Sie einen zusätzlichen Vorschlag:

: Für alle X des Typs T, für einen einzigartigen Y des Typs U, P (X, Y).

(Natürlich ist das derselbe Vorschlag, der als ein Lehrsatz vor dem Einführen eines neuen Funktionssymbols in der vorherigen Abteilung bewiesen werden musste.)

Weil die Beseitigung von funktionellen Prädikaten zu einigen Zwecken sowohl günstig als auch möglich ist, befassen sich viele Behandlungen der formalen Logik ausführlich mit Funktionssymbolen nicht, aber verwenden stattdessen nur Beziehungssymbole; eine andere Weise, daran zu denken, besteht darin, dass ein funktionelles Prädikat eine spezielle Art des Prädikats, spezifisch dasjenige ist, das den Vorschlag oben befriedigt.

Das kann scheinen, ein Problem zu sein, wenn Sie ein Vorschlag-Diagramm angeben möchten, das nur für funktionelle Prädikate F gilt; wie wissen Sie vorzeitig, ob es diese Bedingung befriedigt?

Um eine gleichwertige Formulierung des Diagramms zu bekommen, ersetzen Sie zuerst irgendetwas der Form F (X) mit einer neuen Variable Y.

Messen Sie dann allgemein über jeden Y sofort, nachdem das Entsprechen X eingeführt wird (d. h. nachdem X, oder am Anfang der Behauptung gemessen wird, wenn X frei ist), und schützen Sie die Quantifizierung mit P (X, Y).

Geben Sie schließlich die komplette Erklärung eine materielle Folge der Einzigartigkeitsbedingung für ein funktionelles Prädikat oben ab.

Lassen Sie uns als ein Beispiel das Axiom-Diagramm des Ersatzes in der Zermelo-Fraenkel Mengenlehre nehmen.

(Dieses Beispiel verwendet mathematische Symbole.)

Dieses Diagramm Staaten (in einer Form), für jedes funktionelle Prädikat F in einer Variable:

Erstens müssen wir F (C) durch eine andere Variable D ersetzen:

Natürlich ist diese Behauptung nicht richtig; D muss gerade danach C gemessen werden:

Wir müssen noch P einführen, um diese Quantifizierung zu schützen:

Das ist fast richtig, aber es gilt für zu viele Prädikate; was wir wirklich wollen, ist:

Diese Version des Axiom-Diagramms des Ersatzes ist jetzt für den Gebrauch auf einer formellen Sprache passend, die die Einführung von neuen Funktionssymbolen nicht erlaubt. Wechselweise kann man die ursprüngliche Behauptung als eine Behauptung auf solch einer formellen Sprache interpretieren; es war bloß eine Abkürzung für die am Ende erzeugte Behauptung.

Siehe auch

• Logischer verbindender
• Logischer unveränderlicher