Kategorien
Logik Paradoxe

Currys Paradoxon

Currys Paradoxon ist ein Paradoxon, bei dem eine willkürliche Behauptung F aus der bloßen Existenz eines Satzes C bewiesen wird, der von sich selbst sagt: „Wenn C, dann F“ und nur wenige scheinbar harmlose logische Ableitungsregeln erfordert. Da F willkürlich ist, beweist jede Logik mit diesen Regeln alles. Das Paradoxon kann in natürlicher Sprache und in verschiedenen Logiken ausgedrückt werden, einschließlich bestimmter Formen der Mengenlehre, der Lambda-Rechnung und der kombinatorischen Logik.

Das Paradoxon ist nach dem Logiker Haskell Curry benannt. Aufgrund seiner Beziehung zum Satz von Löb wurde es nach Martin Hugo Löb auch Löbs Paradoxon genannt.

In natürlicher Sprache
Ansprüche der Form „wenn A, dann B“ werden bedingte Ansprüche genannt. Currys Paradoxon verwendet eine bestimmte Art von selbstreferenziellem bedingten Satz, wie in diesem Beispiel gezeigt:

Wenn dieser Satz wahr ist, dann grenzt Deutschland an China.

Obwohl Deutschland nicht an China grenzt, ist der Beispielsatz sicherlich ein Satz in natürlicher Sprache, und so kann die Wahrheit dieses Satzes analysiert werden. Das Paradoxon ergibt sich aus dieser Analyse. Die Analyse besteht aus zwei Schritten.

Erstens können übliche Beweisverfahren in natürlicher Sprache verwendet werden, um zu beweisen, dass der Beispielsatz wahr ist.

Zweitens kann die Wahrheit des Beispielsatzes verwendet werden, um zu beweisen, dass Deutschland an China grenzt. Da Deutschland nicht an China grenzt, deutet dies darauf hin, dass in einem der Beweise ein Fehler aufgetreten ist.

Die Behauptung „Deutschland grenzt an China“ könnte durch jede andere Behauptung ersetzt werden, und das Urteil wäre immer noch nachweisbar. Somit scheint jeder Satz beweisbar zu sein. Da der Beweis nur gut akzeptierte Abzugsmethoden verwendet und keine dieser Methoden falsch zu sein scheint, ist diese Situation paradox.

Informeller Beweis
Die Standardmethode zum Nachweis von bedingten Sätzen (Sätze der Form „wenn A, dann B“) wird als „bedingter Beweis“ bezeichnet. Bei dieser Methode wird zuerst A angenommen, um zu beweisen, dass „wenn A, dann B“, und dann wird mit dieser Annahme gezeigt, dass B wahr ist.

Um Currys Paradoxon zu erzeugen, wie in den beiden obigen Schritten beschrieben, wenden Sie diese Methode auf den Satz „Wenn dieser Satz wahr ist, grenzt Deutschland an China“ an. Hier bezieht sich A, „dieser Satz ist wahr“, auf den Gesamtsatz, während B „Deutschland grenzt an China“ ist. Die Annahme von A ist also die gleiche wie die Annahme von „Wenn A, dann B“. Daher haben wir bei der Annahme von A sowohl A als auch „Wenn A, dann B“ angenommen. Daher ist B durch modus ponens wahr, und wir haben bewiesen: „Wenn dieser Satz wahr ist, dann ist ‚Deutschland grenzt an China‘ wahr.“ in üblicher Weise durch Annahme der Hypothese und Ableitung der Schlussfolgerung.

Nun, da wir bewiesen haben, dass „Wenn dieser Satz wahr ist, dann ist“ Deutschland grenzt an China „wahr ist“, können wir wieder modus ponens anwenden, weil wir wissen, dass die Behauptung „dieser Satz ist wahr“ richtig ist. Auf diese Weise können wir schließen, dass Deutschland an China grenzt.

Formeller Beweis

Sententielle Logik
Im Beispiel im vorherigen Abschnitt wurde unformalisiertes Denken in natürlicher Sprache verwendet. Currys Paradoxon tritt auch in einigen Varianten der formalen Logik auf. In diesem Zusammenhang zeigt es, dass wir Y mit einem formalen Beweis beweisen können, wenn wir annehmen, dass es einen formalen Satz (X → Y) gibt, in dem X selbst äquivalent zu (X → Y) ist. Ein Beispiel für einen solchen formalen Beweis ist wie folgt. Eine Erläuterung der in diesem Abschnitt verwendeten Logiknotation finden Sie in der Liste der Logiksymbole.

X: = (X → Y)
Annahme, der Ausgangspunkt, äquivalent zu „Wenn dieser Satz wahr ist, dann Y“

X → X.
Gesetz der Identität

X → (X → Y)
Ersetzen Sie die rechte Seite von 2, da X X → Y durch 1 entspricht

X → Y.
von 3 durch Kontraktion

X.
Ersetzen Sie 4 durch 1

Y.
von 5 und 4 von modus ponens

Ein alternativer Beweis ist das Peirce-Gesetz. Wenn X = X → Y, dann (X → Y) → X. Dies impliziert zusammen mit dem Peirce-Gesetz ((X → Y) → X) → X und modus ponens X und anschließend Y (wie im obigen Beweis).

Wenn Y eine unbeweisbare Aussage in einem formalen System ist, gibt es in diesem System keine Aussage X, so dass X der Implikation entspricht (X → Y). Im Gegensatz dazu zeigt der vorherige Abschnitt, dass es in natürlicher (nicht formalisierter) Sprache für jede natürliche Sprachaussage Y eine natürliche Sprachaussage Z gibt, so dass Z in natürlicher Sprache (Z → Y) entspricht. Z ist nämlich „Wenn dieser Satz wahr ist, dann Y“.

In bestimmten Fällen, in denen die Klassifizierung von Y bereits bekannt ist, sind nur wenige Schritte erforderlich, um den Widerspruch aufzudecken. Wenn beispielsweise Y „Deutschland grenzt an China“ ist, ist bekannt, dass Y falsch ist.

X = (X → Y)
Annahme

X = (X → falsch)
Ersetzen Sie den bekannten Wert von Y.

X = (¬X ∨ falsch)
Implikation

X = ¬X
Identität

Naive Mengenlehre
Selbst wenn die zugrunde liegende mathematische Logik keine selbstreferenziellen Sätze zulässt, sind bestimmte Formen der naiven Mengenlehre immer noch anfällig für Currys Paradoxon. In Mengen-Theorien, die ein uneingeschränktes Verständnis ermöglichen, können wir dennoch jede logische Aussage Y beweisen, indem wir die Menge untersuchen

X = def {x ∣ x ∈ x → Y}.
Unter der Annahme, dass ∈ Vorrang vor → und ↔ hat, läuft der Beweis wie folgt ab:

X = {x ∣ x ∈ x → Y}
Definition von X.

x = X → (x ∈ x ↔ X ∈ X)
Ersetzung gleicher Mitgliederzahlen

x = X → ((x ∈ x → Y) ↔ (X ∈ X → Y))
Hinzufügung einer Konsequenz zu beiden Seiten eines Biconditional (von 2)

X ∈ X ↔ (X ∈ X → Y)
Gesetz der Konkretion (von 1 und 3)

X ∈ X → (X ∈ X → Y)
Bikonditionale Eliminierung (von 4)

X ∈ X → Y.
Kontraktion (von 5)

(X ∈ X → Y) → X ∈ X.
Bikonditionale Eliminierung (von 4)

X ∈ X.
Modus ponens (von 6 und 7)

Y.
Modus ponens (von 8 und 6)

Schritt 4 ist der einzige Schritt, der in einer konsistenten Mengenlehre ungültig ist. In der Zermelo-Fraenkel-Mengenlehre wäre eine zusätzliche Hypothese erforderlich, die besagt, dass X eine Menge ist, was in ZF oder in seiner Erweiterung ZFC (mit dem Axiom der Wahl) nicht beweisbar ist.

Daher existiert in einer konsistenten Mengenlehre die Menge {x ∣ x ∈ x → Y} nicht für falsches Y. Dies kann als eine Variante von Russells Paradox angesehen werden, ist aber nicht identisch. Einige Vorschläge für die Mengenlehre haben versucht, mit Russells Paradoxon umzugehen, indem sie nicht die Regel des Verstehens einschränkten, sondern die Regeln der Logik so einschränkten, dass sie den Widerspruch der Menge aller Mengen tolerierten, die nicht Mitglieder ihrer selbst sind. Das Vorhandensein von Beweisen wie dem oben genannten zeigt, dass eine solche Aufgabe nicht so einfach ist, da mindestens eine der im obigen Beweis verwendeten Abzugsregeln weggelassen oder eingeschränkt werden muss.

Lambda-Kalkül
Das Curry-Paradoxon kann in einem untypisierten Lambda-Kalkül ausgedrückt werden, das durch eine eingeschränkte Minimallogik angereichert ist. Um mit den syntaktischen Einschränkungen des Lambda-Kalküls fertig zu werden, bezeichnet m die Implikationsfunktion mit zwei Parametern, dh der Lambda-Term ((m A) B) muss der üblichen Infixnotation A → B entsprechen. Eine beliebige Formel Z kann sein bewiesen durch Definition einer Lambda-Funktion N: = λ p. ((mp) Z) und X: = (YN), wobei Y Currys Festkommakombinator bezeichnet. Dann ist X = (NX) = ((m X) Z) durch Definition von Y und N, daher kann der obige sententiale logische Beweis im Kalkül dupliziert werden:

⊢ ((m X) X) durch das minimale logische Axiom A → A ⊢ ((m X) ((m X) Z)), da X = ((m X) Z) ⊢ ((m X) Z) durch das Satz (A → (A → B)) ⊢ (A → B) der minimalen Logik ⊢ X, da X = ((m X) Z) ⊢ Z nach Modus ponens A, (A → B) ⊢ B aus X und (( m X) Z)

In der einfach getippten Lambda-Rechnung können Festkomma-Kombinatoren nicht typisiert werden und sind daher nicht zugelassen.

Kombinatorische Logik
Currys Paradoxon kann auch in kombinatorischer Logik ausgedrückt werden, die eine äquivalente Ausdruckskraft wie Lambda-Kalkül hat. Jeder Lambda-Ausdruck kann in eine kombinatorische Logik übersetzt werden, sodass eine Übersetzung der Implementierung des Curry-Paradoxons in den Lambda-Kalkül ausreichen würde.

Der obige Term X bedeutet in der kombinatorischen Logik (rr), wobei

r = S (S (K m) (SII)) (KZ);
daher
(rr) = ((m (rr)) Z).

Diskussion
Currys Paradoxon kann in jeder Sprache formuliert werden, die grundlegende Logikoperationen unterstützt, die es auch ermöglichen, eine selbstrekursive Funktion als Ausdruck zu konstruieren. Zwei Mechanismen, die die Konstruktion des Paradoxons unterstützen, sind die Selbstreferenz (die Fähigkeit, innerhalb eines Satzes auf „diesen Satz“ zu verweisen) und das uneingeschränkte Verständnis in der naiven Mengenlehre. Natürliche Sprachen enthalten fast immer viele Merkmale, die zur Konstruktion des Paradoxons verwendet werden könnten, ebenso wie viele andere Sprachen. Normalerweise werden durch Hinzufügen von Metaprogrammierfunktionen zu einer Sprache die erforderlichen Funktionen hinzugefügt. In der mathematischen Logik wird im Allgemeinen nicht explizit auf eigene Sätze Bezug genommen. Das Herzstück von Gödels Unvollständigkeitssätzen ist jedoch die Beobachtung, dass eine andere Form der Selbstreferenz hinzugefügt werden kann; siehe Gödel-Nummer.

Das Axiom des uneingeschränkten Verstehens fügt die Fähigkeit hinzu, eine rekursive Definition in der Mengenlehre zu konstruieren. Dieses Axiom wird von der modernen Mengenlehre nicht unterstützt.

Die bei der Konstruktion des Beweises verwendeten logischen Regeln sind die Annahme-Regel für den bedingten Beweis, die Kontraktionsregel und der Modus ponens. Diese sind in den gängigsten logischen Systemen enthalten, z. B. in der Logik erster Ordnung.

Konsequenzen für eine formale Logik
In den 1930er Jahren spielten Currys Paradoxon und das damit verbundene Kleene-Rosser-Paradoxon eine wichtige Rolle, um zu zeigen, dass formale Logiksysteme, die auf selbstrekursiven Ausdrücken basieren, inkonsistent sind. Dazu gehören einige Versionen des Lambda-Kalküls und der kombinatorischen Logik.

Curry begann mit dem Kleene-Rosser-Paradoxon und folgerte, dass das Kernproblem in diesem einfacheren Curry-Paradoxon zum Ausdruck kommen könnte. Seine Schlussfolgerung kann so formuliert werden, dass kombinatorische Logik und Lambda-Kalkül nicht als deduktive Sprachen konsistent gemacht werden können, während dennoch eine Rekursion möglich ist.

Bei der Untersuchung der illativen (deduktiven) kombinatorischen Logik erkannte Curry 1941 die Implikation des Paradoxons als impliziten, dass die folgenden Eigenschaften einer kombinatorischen Logik ohne Einschränkungen nicht kompatibel sind:

Kombinatorische Vollständigkeit. Dies bedeutet, dass ein Abstraktionsoperator im System definierbar (oder primitiv) ist, was eine Voraussetzung für die Ausdruckskraft des Systems ist.

Deduktive Vollständigkeit. Dies ist eine Voraussetzung für die Ableitbarkeit, nämlich das Prinzip, dass in einem formalen System mit materieller Implikation und Modus ponens, wenn Y aus der Hypothese X beweisbar ist, auch ein Beweis für X → Y vorliegt.

Terminologie
Natürliche Sprache und mathematische Logik basieren beide auf der Behauptung, dass einige Aussagen wahr sind. Die Anweisung kann als logischer (oder boolescher) Ausdruck (oder Formel) dargestellt werden, der ausgewertet werden kann, um den Wert true oder false zu erhalten. Eine Anweisung ist eine Anweisung oder ein logischer Ausdruck, von dem behauptet wird, dass er bei der Auswertung einen wahren Wert ergibt.

Demonstrationen können auch auf komplexere Weise betrachtet werden. Aussagen können durch das, was Sie behaupten oder an sie glauben, und durch das Maß an Sicherheit qualifiziert werden. Für die Logik ist jedoch die oben angegebene einfache Definition ausreichend.

Existenzproblem
Dieses Paradoxon ähnelt:

Lügnerparadoxon
Russells Paradoxon
in dem jedes Paradoxon versucht, etwas zu benennen, das nicht existiert. Diese Paradoxien versuchen alle, einer Lösung der Gleichung einen Namen oder eine Darstellung zu geben.

X = ¬X
Beachten Sie, dass das Paradoxon nicht aus der Durchsetzung der Aussage von ¬X entsteht, da eine solche Aussage eine Lüge wäre. Sie ergibt sich aus der Prüfung und Benennung der Erklärung. Das Paradoxon entsteht, indem ein Ausdruck der Form ¬X als X bezeichnet oder dargestellt wird. Im Fall des Curry-Paradoxons wird die Negation aus der Implikation konstruiert.

X = X → falsch = ¬X ∨ falsch = ¬X
Die Domäne einer booleschen Variablen X ist die Menge {true, false}. Weder wahr noch falsch ist jedoch eine Lösung für die obige Gleichung. Es muss also falsch sein, die Existenz von X zu behaupten, und es ist eine Lüge, den ¬X-Ausdruck als X zu bezeichnen.

Das Paradoxon dort ist immer ein Ausdruck, der konstruiert werden kann, dessen Wert nicht existiert. Dies kann mit „dieser Aussage“ erreicht werden, aber es gibt viele andere sprachliche Merkmale, die die Konstruktion eines Ausdrucks ermöglichen, der nicht existiert.

Sprachressourcen, um das Paradox auszudrücken
Currys Paradoxon kann in jeder Sprache formuliert werden, die grundlegende logische Operationen unterstützt, mit denen auch eine automatisch rekursive Funktion als Ausdruck konstruiert werden kann. Die folgende Liste enthält einige Mechanismen, die die Konstruktion des Paradoxons unterstützen, die Liste ist jedoch nicht vollständig.

Selbstreferenz; „dieser Satz“.
Durch die Nomenklatur eines Ausdrucks, der den Namen enthält.
Wenden Sie die naive Mengenlehre an (uneingeschränktes Verständnis).
Lambda-Ausdrücke.
Eine Eval-Funktion in einem Wort.

Die logischen Regeln für die Erstellung von Beweismitteln sind:

Annahmeregel
Kontraktion
Modus Ponens

Die automatisch rekursive Funktion kann dann verwendet werden, um eine Abbruchberechnung zu definieren, deren Wert nicht die Lösung einer Gleichung ist. In Currys Paradoxon verwenden wir Implikation, um eine Negation zu konstruieren, die eine Gleichung ohne Lösung erstellt.

Der rekursive Ausdruck repräsentiert dann einen Wert, der nicht existiert. Die Gesetze der Logik gelten nur für Boolesche Werte in {true, false}, sodass eine Beibehaltung des Ausdrucks möglicherweise fehlerhaft ist.

Natürliche Sprachen enthalten fast immer viele der Ressourcen, die zur Konstruktion des Paradoxons verwendet werden könnten, genau wie viele andere Sprachen. Normalerweise werden durch Hinzufügen von Meta-Programmierfunktionen für eine Sprache die erforderlichen Funktionen hinzugefügt.

Die mathematische Logik toleriert im Allgemeinen keine explizite Bezugnahme auf ihre eigenen Sätze. Das Herzstück von Gödels Unvollständigkeitssätzen ist jedoch die Beobachtung, dass Selbstreferenz hinzugefügt werden kann; siehe die Gödel-Nummer.

Das Axiom des uneingeschränkten Verstehens fügt die Fähigkeit hinzu, eine rekursive Definition in der Mengenlehre zu konstruieren. Dieses Axiom wird von der modernen Mengenlehre nicht unterstützt.

Konsequenzen für eine formale Logik
In den 1930er Jahren spielten das Curry-Paradoxon und das verwandte Kleene-Rosser-Paradoxon eine wichtige Rolle, um zu zeigen, dass formale Logiksysteme, die auf selbstrekursiven Ausdrücken basieren, inkonsistent sind.

Lambda-Kalkül
kombinatorische Logik

Curry begann mit dem Kleene-Rosser-Paradoxon und folgerte, dass das zentrale Problem in diesem einfacheren Paradoxon von Curry zum Ausdruck kommen könnte. Seine Schlussfolgerung lässt sich sagen, dass kombinatorische Logik und Lambda-Berechnung als deduktive Sprache nicht kohärent sein könnten, was eine Rekursion ermöglicht.

Bei der Untersuchung der illativen (deduktiven) kombinatorischen Logik erkannte Curry 1941 die Implikation des Paradoxons als implizierend, dass die folgenden Eigenschaften einer kombinatorischen Logik ohne Einschränkungen nicht kompatibel sind:

Kombinatorische Vollständigkeit. Dies bedeutet, dass ein Abstraktionsoperator im System definierbar (oder primitiv) ist, was eine Voraussetzung für die Ausdruckskraft des Systems ist.
Deduktive Vollständigkeit. Dies ist eine Ableitungsanforderung, dh das Prinzip, dass in einem formalen System mit Implikation und materiellem Modus ponens, wenn Y von der Hypothese X abziehbar ist, auch ein Beweis für X → Y vorliegt.

Auflösung
In diesem Abschnitt werden keine Quellen genannt. Bitte helfen Sie, diesen Abschnitt zu verbessern, indem Sie Zitate zu zuverlässigen Quellen hinzufügen. Nicht bezogenes Material kann herausgefordert und entfernt werden.
Quellen finden: „Curry’s Paradoxon“ – Nachrichten • Zeitungen • Bücher • Gelehrter • JSTOR (August 2019) (Erfahren Sie, wie und wann Sie diese Vorlagennachricht entfernen können)

Die sachliche Richtigkeit dieses Abschnitts ist umstritten. Relevante Diskussionen finden Sie auf Talk: Currys Paradoxon. Bitte helfen Sie dabei, sicherzustellen, dass umstrittene Aussagen zuverlässig stammen. (August 2019) (Erfahren Sie, wie und wann Sie diese Vorlagennachricht entfernen können.)

Beachten Sie, dass Currys Paradoxon im Gegensatz zum Lügnerparadoxon oder Russells Paradoxon nicht davon abhängt, welches Negationsmodell verwendet wird, da es vollständig negationsfrei ist. Daher können parakonsistente Logiken immer noch für dieses Paradoxon anfällig sein, selbst wenn sie gegen das Lügnerparadoxon immun sind.

Keine Auflösung im Lambda-Kalkül
Der Ursprung des Lambda-Kalküls der Alonzo-Kirche könnte gewesen sein: „Wie können Sie eine Gleichung lösen, um eine Definition einer Funktion bereitzustellen?“. Dies drückt sich in dieser Äquivalenz aus,

fx = y ⟺ f = λ xy

Diese Definition ist gültig, wenn es eine und nur eine Funktion f gibt, die die Gleichung fx = y erfüllt, ansonsten jedoch ungültig. Dies ist der Kern des Problems, das Stephen Cole Kleene und dann Haskell Curry mit kombinatorischer Logik und Lambda-Rechnung entdeckten.

Die Situation kann mit der Definition verglichen werden
y = x 2 ⟺ x = y.

Diese Definition ist in Ordnung, solange nur positive Werte für die Quadratwurzel zulässig sind. In der Mathematik kann eine existenziell quantifizierte Variable mehrere Werte darstellen, jedoch jeweils nur einen. Die existenzielle Quantifizierung ist die Disjunktion vieler Instanzen einer Gleichung. In jeder Gleichung ist ein Wert für die Variable.

In der Mathematik muss ein Ausdruck ohne freie Variablen jedoch nur einen Wert haben. 4 kann also nur + 2 darstellen. Es gibt jedoch keine bequeme Möglichkeit, die Lambda-Abstraktion auf einen Wert zu beschränken oder sicherzustellen, dass es einen Wert gibt.

Die Lambda-Rechnung ermöglicht die Rekursion, indem dieselbe Funktion übergeben wird, die als Parameter aufgerufen wird. Dies ermöglicht Situationen, in denen fx = y mehrere oder keine Lösungen für f hat.

Der Lambda-Kalkül kann als Teil der Mathematik betrachtet werden, wenn nur Lambda-Abstraktionen zulässig sind, die eine einzige Lösung für eine Gleichung darstellen. Andere Lambda-Abstraktionen sind in der Mathematik falsch.

Currys Paradoxon und andere Paradoxe entstehen im Lambda-Kalkül aufgrund der Inkonsistenz des Lambda-Kalküls, der als deduktives System betrachtet wird. Siehe auch deduktive Lambda-Rechnung.

Domäne der Lambda-Kalkülbegriffe

Die Lambda-Rechnung ist eine konsistente Theorie auf ihrem eigenen Gebiet. Es ist jedoch nicht konsistent, die Lambda-Abstraktionsdefinition zur allgemeinen Mathematik hinzuzufügen. Lambda-Begriffe beschreiben Werte aus der Lambda-Kalküldomäne. Jeder Lambda-Begriff hat einen Wert in dieser Domäne.

Bei der Übersetzung von Ausdrücken aus der Mathematik in den Lambda-Kalkül ist der Bereich der Lambda-Kalkülbegriffe nicht immer isomorph zum Bereich der mathematischen Ausdrücke. Dieser Mangel an Isomorphismus ist die Quelle der offensichtlichen Widersprüche.

Auflösung in uneingeschränkten Sprachen

Es gibt viele Sprachkonstrukte, die implizit eine Gleichung aufrufen, die möglicherweise keine oder viele Lösungen hat. Die Klangauflösung für dieses Problem besteht darin, diese Ausdrücke syntaktisch mit einer existenziell quantifizierten Variablen zu verknüpfen. Die Variable repräsentiert die mehreren Werte auf eine Weise, die für das allgemeine menschliche Denken von Bedeutung ist, aber auch für die Mathematik gilt.

Beispielsweise ist eine natürliche Sprache, die die Eval-Funktion ermöglicht, mathematisch nicht konsistent. Aber jeder Aufruf an Eval in dieser natürlichen Sprache kann auf konsistente Weise in Mathematik übersetzt werden. Die Übersetzung von Eval (s) in die Mathematik ist

sei x = Eval (s) in x.
Also wo s = „Eval (s) → y“,

sei x = x → y in x.
Wenn y falsch ist, dann ist x = x → y falsch, aber dies ist eine Lüge, kein Paradoxon.

Die Existenz der Variablen x war in der natürlichen Sprache implizit. Die Variable x wird erstellt, wenn die natürliche Sprache in Mathematik übersetzt wird. Dies ermöglicht es uns, natürliche Sprache mit natürlicher Semantik zu verwenden und gleichzeitig die mathematische Integrität aufrechtzuerhalten.

Auflösung in formaler Logik
Das Argument in der formalen Logik beginnt mit der Annahme der Gültigkeit der Benennung (X → Y) als X. Dies ist jedoch kein gültiger Ausgangspunkt. Zuerst müssen wir die Gültigkeit der Benennung ableiten. Der folgende Satz ist leicht zu beweisen und repräsentiert eine solche Benennung:

∀ A, ∃ X, X = A.
In der obigen Anweisung wird die Formel A als X bezeichnet. Versuchen Sie nun, die Formel mit (X → Y) für A zu instanziieren. Dies ist jedoch nicht möglich, da der Bereich von ∃ X innerhalb des Bereichs von ∀ A liegt. Die Reihenfolge der Quantifizierer können mit Skolemization umgekehrt werden:

∃ f, ∀ A, f (A) = A.
Jetzt gibt jedoch die Instanziierung

f (X → Y) = X → Y,
Dies ist nicht der Ausgangspunkt für den Beweis und führt nicht zu einem Widerspruch. Es gibt keine anderen Instanziierungen für A, die zum Ausgangspunkt des Paradoxons führen.

Auflösung in der Mengenlehre

In der Zermelo-Fraenkel-Mengenlehre (ZFC) wird das Axiom des uneingeschränkten Verständnisses durch eine Gruppe von Axiomen ersetzt, die die Konstruktion von Mengen ermöglichen. Currys Paradoxon kann also nicht in ZFC angegeben werden. ZFC entwickelte sich als Reaktion auf Russells Paradoxon.