Gibt es eine Definition für freie und gebundene Variablen in der Logik?

Freie und gebundene Variablen werden im Kontext der Syntax der Logik erster Ordnung unter Berücksichtigung von Begriffen (dh "Namen" für Objekte) und Formeln (dh Anweisungen) definiert.

Die formale Definition der Menge$\text {FV}(φ)$von freien Variablen einer Formel$φ$ist definiert durch:

alle in einem Term oder einer Atomformel vorkommenden Variablen sind frei.

$\text {FV}(¬φ) = \text {FV}(φ)$;

$\text {FV}(φ ∨ ψ) = \text {FV}(φ) \cup \text {FV}(ψ)$, (und das gleiche für die anderen binären Konnektoren);

$\text {FV}(∀xφ) = \text {FV}(∃xφ) = \text {FV}(φ) \setminus \{ x \}$.

Eine Variable, die nicht frei ist, wird gebunden .

Eine Formel$φ$heißt geschlossen wenn$\text {FV}(φ)=\emptyset$.

In Formel$\forall x P(x)$, Die Variable$x$ist gebunden.

In Formel$\forall x R(x,y)$Die Variable$x$gebunden ist, während die Variable$y$ist gratis.

Eine geschlossene Formel drückt, wenn sie interpretiert wird, einen Satz aus, dh hat einen bestimmten Tuth-Wert.

$\forall n (n \ge 0)$stimmt darin$\mathbb N$, während$\exists n (n < 0)$ist darin falsch.

Was ist der Wahrheitswert einer Formel mit einer freien Variablen, wie zB$(x > 0)$?

Es kommt darauf an... Es kommt darauf an, welchen Wert wir der Variablen zuweisen$x$.

Eine freie Variable fungiert als Pronomen der natürlichen Sprache : Ihre Referenz muss entsprechend dem Kontext identifiziert werden : Wenn ich sage "es ist rot", hängt der Wahrheitswert der Aussage von dem Objekt ab, auf das ich mit meinem Finger zeige : the rotes Buch oder der blaue Stift auf meinem Tisch.

Ebenso gibt es Möglichkeiten (definiert durch die formalen semantischen Spezifikationen der Sprache erster Ordnung : siehe Variablenzuweisungsfunktion ), um "temporär" auf freie Variablen einer Formel zu verweisen.

Betrachten Sie die Formel:

$x+2=5$;

wenn wir ersetzen$x$die (Name für die) Nummer$3$, erhalten wir einen wahren Satz (dh$3+2=5$).

Wenn wir stattdessen zu ersetzen$x$die (Name für die) Nummer$4$, erhalten wir einen falschen Satz (dh$4+2=5$).

Eine Formel mit freier Variable wird "offen" genannt, weil sie keine (feste) Bedeutung hat: Sie ist "offen für" verschiedene Interpretationen; Um ihm eine Bedeutung zu geben, müssen wir ihn in einen Satz (dh eine geschlossene Formel) umwandeln.

Leider sind Variablen wirklich fummelig.

Das Problem der Variablen taucht in der Informatik häufig in Bezug auf Theorien wie den Lambda-Kalkül auf, der Bindungen und Substitutionen sauber handhabt. Wenn Sie einen Rahmen mit mehrfach sortierter Logik höherer Ordnung zulassen, können Sie Quantoren im Sinne des einfach typisierten Lambda-Kalküls axiomisieren und definieren. Einem Quantor über einem Diskursbereich kann direkt ein Typ gegeben werden$\text{join} \colon (\text{domain} \rightarrow \text{prop}) \rightarrow \text{prop}$. Eine solche Grundlage der Simple Type Theory wird in der Praxis in Theorembeweisern wie Isabelle/HOL verwendet. Weitere Informationen finden Sie unter Die sieben Tugenden der Theorie einfacher Typen .

Die STLC löst die Variablenbindung nicht direkt, bietet aber ein schönes Beispiel für die Formalisierung und Verallgemeinerung. Eine der einfacheren Techniken, um mit der Hässlichkeit von Variablen umzugehen und Substitution zu vermeiden, die in der Praxis häufig in der Metatheorie verwendet wird, ist die Verwendung von de Bruijn-Indizes. Grundsätzlich werden Variablen wie Zahlen behandelt, die in den lokalen Geltungsbereich indizieren, also zum Beispiel die Konstantenfunktion$\lambda x y. x$wird$\lambda. \lambda. 1$. Wenn Sie an solchen Sachen interessiert sind, gibt es einen netten Blogbeitrag über Ordner von Jesper Cockx .

Wenn Sie mit dieser Art von Ansatz nicht zufrieden sind, können Sie die STLC zu kartesischen geschlossenen Kategorien zusammenstellen. Siehe Compiling to Categories von Conal Elliott . BCKW ist wahrscheinlich ein eher traditioneller Satz von Kombinatoren, auf den man sich kompilieren kann. Leider ist die vollständige kategorientheoretische Behandlung von abhängigen Typen und Quantifizierern in Bezug auf Slices und Unterobjekte ziemlich unheimlich. Ich denke, einer der wenigen Bereiche, in denen ein kombinatorischer Ansatz in der Praxis verwendet wird, ist das Klassenverständnis-Metatheorem der NBG-Mengentheorie, in dem Formeln für Klassen bis zu Permutationen von Tupeln und dergleichen kompiliert werden.

Direktere Zugänge zum Umgang mit Variablen sind das Gebiet der Algebraischen Logik. Sie möchten sich wahrscheinlich Alfred Tarskis Zylinderalgebren ansehen, wo Sie Existenzquantoren im Grunde als eine Art Modaloperator behandeln können. Es gibt auch andere Ansätze für das Problem wie polyadische Algebren, aber ich verstehe sie auch nicht.

Abschließend möchte ich Hilberts unbestimmten Beschreibungsoperator erwähnen, der einige Probleme mit Variablen durch das Verschachteln von Aussagen und Begriffen wohl verschlimmert, aber die Metatheorie vereinfachen kann.$\varepsilon x. P(x)$wird verwendet, um "einen unbestimmten Begriff zu beschreiben, so dass P wahr ist". Existenzielle Quantifizierung kann dann definiert werden als$\exists x. P(x) \equiv P(\varepsilon x. P(x))$.

Sie erwähnen das Problem nicht, aber neben freien und gebundenen Variablen gibt es auch die Probleme der globalen und lokalen Definitionen und der definitorischen Erweiterung. In einigen Fällen können Sie lokale Definitionen in Lambda-Ausdrücke desugaren$\textbf{let} \, x := e \, \textbf{in} \, e' \equiv (\lambda x. e) e'$obwohl dies aus technischen Gründen, die sehr spezifisch für Computerprogramme sind, nicht immer funktioniert. Die prägnanteste Methode, mit globalen Variablen umzugehen, könnte darin bestehen, einen eindeutigen Beschreibungsoperator zu missbrauchen .

Auch dies ist kein wirkliches Problem für die Logik erster Ordnung, aber die Informatik muss sich mit Kontrollfluss / Fortsetzungen als einer anderen Art von Variablen befassen. Die Fokussierung wie im Lambda-Bar-Mu-Mu-Tilde-Kalkül ist jedoch nicht deterministisch.

Ich hoffe, ich habe Sie davon überzeugt, dass es möglich, wenn nicht sogar tatsächlich ist, dass jemand die Erfassung formalisiert hat, um die Ersetzung von Variablen korrekt zu vermeiden, und dass Sie, wenn Sie ein Zylon sind, alles zu einem unlesbaren Durcheinander frei von Namensbindern schonfinkle können. Leider sind Variablen wirklich fummelig.