Vergleich von Ansätzen zur Verwaltung freier und gebundener Variablen.

Question

Vergleich von Ansätzen zur Verwaltung freier und gebundener Variablen.

Gregor Nisbet

Korrekturen:

Ich sagte ursprünglich $\varphi(x, w_1 \cdots w_n, a)$ war eine geschlossene wohlgeformte Formel. Es ist nicht. Das wollte ich innerlich sagen $\varphi$ die einzigen freien Variablen kommen aus $x, w_1 \cdots w_n, a$ , dh $\text{FV}(\varphi) \subset \{x, w_1 \cdots w_n, a\}$ .

Vergleich von Ansätzen zur Verwaltung freier und gebundener Variablen.

Was sind die verschiedenen Ansätze zur Verwaltung freier und gebundener Variablen in wohlgeformten Formeln? Gibt es Referenzen, die mehrere Möglichkeiten explizit vergleichen und über ihre Vor- und Nachteile sprechen?

Hier ist zum Beispiel das Axiom-Schema der Spezifikation von Z(F)(C), wie es von Wikipedia präsentiert wird, aber mit allen Variablen in Kleinbuchstaben und einigen geringfügigen Notationsänderungen.

\forall w_{1} \dots w_{N} . \forall A . \exists B . \forall X . (X \in B) \leftrightarrow (X \in A \land φ (X_{1}, w_{1} \dots w_{N}, A))

$\forall w_1\cdots w_n \mathop. \forall a \mathop. \exists b \mathop. \forall x \mathop. (x \in b) \leftrightarrow (x \in a \land \varphi(x_1, w_1 \cdots w_n, a))$

Beachten Sie, dass alle Variablensymbole gebunden sind.

In der im Artikel verwendeten Konvention $\varphi$ ist eine wohlgeformte Formel. $\varphi(x_1, w_1 \cdots w_n, a)$ ist eine wohlgeformte Formel und die Tatsache, dass $b$ taucht nicht auf $(x_1, w_1 \cdots w_n, a)$ ist wichtig. Die Tatsache, dass $b$ nicht vorkommt bedeutet, dass $b$ kommt nicht frei vor $\varphi$ . Ich bin mir nicht sicher, wie ich es definieren soll $\varphi(\vec{v})$ für eine Willkür $\vec{v}$ in dieser Notation ... Ich denke normalerweise daran, Abhängigkeiten in gewissem Sinne zu erklären, wo die genaue Interpretation vom Kontext abhängt.

Ich denke, es gibt einige technische Vorteile bei der Definition der Syntax, um gebundene und freie Variablensymbole disjunkt zu machen. Ich bin nicht auf die Idee gekommen, freie und gebundene Variablen zu trennen, aber ich weiß nicht mehr, wo ich es gesehen habe.

Ein lateinischer Kleinbuchstabe sei ein gebundenes Variablensymbol und ein lateinischer Großbuchstabe ein freies Variablensymbol. Lassen $\psi[M:=\chi]$ ein einfangvermeidender Ersatz sein $M$ mit $\chi$ in der wohlgeformten Formel $\psi$ .

Unter Verwendung dieser Konvention kann die obige Formel wie folgt geschrieben werden.

\exists B . \forall X . (X \in B) \leftrightarrow (X \in A \land φ [X := X])

$\exists b \mathop. \forall x \mathop. (x \in b) \leftrightarrow (x \in A \land \varphi[X:=x])$

In diesem Fall, $\varphi$ ist eine gewöhnliche wohlgeformte Formel ohne Einschränkungen. $A$ könnte vorkommen in $\varphi$ oder vielleicht auch nicht. $X$ könnte vorkommen in $\varphi$ oder vielleicht auch nicht. Indem man wohlgeformt ist $b$ kann nicht frei in auftreten $\varphi$ da es sich um eine gebundene Variable handelt. Etwas merkwürdig ist allerdings, dass die Namen freier Variablen in $\varphi$ sind nicht irrelevant; $X$ Und $A$ beide haben wegen der genauen Formulierung des Axiomenschemas besondere Bedeutungen.

In diesem einen speziellen Fall scheint die Verwendung einer unterschiedlichen Sammlung von Symbolen für freie und gebundene Variablen einen Teil meiner Aufgabe bei der Definition eines Axiomenschemas zu vereinfachen, aber es ist im Allgemeinen möglicherweise nicht bequemer.

Thorimur

Sie könnten de Bruijn-Indizes relevant finden! Es könnte Literatur geben, die de Bruijn-Indizes mit anderen Bindungsmethoden vergleicht, was einen Ausgangspunkt bieten könnte.

Alex Kruckmann

Bist du sicher, dass du das sagen willst

φ

$\varphi$ ist eine geschlossene Formel? „Geschlossene Formel“ bedeutet in der Regel dasselbe wie „Satz“: keine freien Variablen. Aber

x, w_{1}, \dots, w_{n}, a

$x,w_1,\dots,w_n,a$ können alle frei in auftreten

φ

$\varphi$ .

Gregor Nisbet

Ich wollte sagen, dass die Argumente dazu

φ

$\varphi$ Erfassen Sie alle Abhängigkeiten, die

φ

$\varphi$ hat (und damit das Fehlen von

b

$b$ ist aussagekräftig). Geschlossen ist definitiv nicht das richtige Wort, aber ich weiß nicht, was es ist.

Alex Kruckmann

Die Notation

φ (v_{1}, \dots, v_{n})

$\varphi(v_1,\dots,v_n)$ wird normalerweise verwendet, um die freien Variablen der Formel anzugeben

φ

$\varphi$ gehören dazu

v_{1}, \dots, v_{n}

$v_1,\dots,v_n$ . Das heißt, jede freie Variable in

φ

$\varphi$ ist eines der

v_{i}

$v_i$ , aber nicht alle

v_{i}

$v_i$ frei in auftreten müssen

φ

$\varphi$ . Dies ist eine sehr nützliche Notation, weil wir dann schreiben können

φ (a_{1}, \dots, a_{n})

$\varphi(a_1,\dots,a_n)$ für die Substitutionsoperation

a_{i}

$a_i$ für jede kostenlose Instanz von

v_{i}

$v_i$ . Und das macht es deutlich

φ

$\varphi$ definiert natürlich eine Teilmenge von

A^{n}

$A^n$ / ein

n

$n$ -ary Beziehung auf

A

$A$ , für jede Struktur

A

$A$ .

Alex Kruckmann

Es besteht normalerweise keine Notwendigkeit, die gebundenen Variablen in einer Formel auf ähnliche Weise anzugeben

φ

$\varphi$ , denn einmal gebunden, sind ihre Identitäten irrelevant. Das heißt, Sie können eine gebundene Variable (in ihrem Quantor und in jedem Fall innerhalb des Geltungsbereichs dieses Quantors) gegen eine andere Variable austauschen, ohne die Bedeutung der Formel zu ändern.

Gregor Nisbet

Danke schön. Was ich immer verwirrend fand

φ (\vec{v})

$\varphi(\vec{v})$ ist, dass es verwendet wurde, um beides zu sagen

FV (φ) \subset \vec{v}

$\text{FV}(\varphi) \subset \vec{v}$ und zu sagen

φ [x_{1} := {\vec{v}}_{1} \dots x_{n} := {\vec{v}}_{n}]

$\varphi[x_1 := \vec{v}_1 \cdots x_n := \vec{v}_n]$ Wo

x_{i}

$x_i$ ist der

i

$i$ te freie Variable ... daher habe ich mich immer gefragt, ob der "Name" des Parameters oder seine Position in der Argumentliste wichtiger ist. // De Bruijn-Indizes sind eine weitere gute Alternative. Ich habe sie schon einmal in Diskussionen über Lambda-Kalkül gesehen, Substitution ist jedoch nicht trivial und erfordert, dass Sie hinzufügen.

Mauro ALLEGRANZA

Es gibt den von Gentzen (dem Vater von ND und Sequent Calc) verwendeten Ansatz, um Variablen zu trennen:

x, y

$x,y$ nur gebunden verwendet , von Parametern :

a, b

$a,b$ nur kostenlos genutzt. Beispiel mit

\forall

$\forall$ -Einführungsregel:

\frac{φ}{\forall x φ [x / a]}

$\dfrac {\varphi} {\forall x \varphi [x/a]}$

Markus S.

Ich denke, einige verwandte (aber nicht umfassende) Lektüren könnten über die Metamath Proof Explorer-Dokumentation verstreut sein, z. B. ZFC Axioms Without Distinct Variable Conditions .

Antworten (1)

Vergleich von Ansätzen zur Verwaltung freier und gebundener Variablen.

Sie könnten de Bruijn-Indizes relevant finden! Es könnte Literatur geben, die de Bruijn-Indizes mit anderen Bindungsmethoden vergleicht, was einen Ausgangspunkt bieten könnte.
Bist du sicher, dass du das sagen willst $\varphi$ ist eine geschlossene Formel? „Geschlossene Formel“ bedeutet in der Regel dasselbe wie „Satz“: keine freien Variablen. Aber $x,w_1,\dots,w_n,a$ können alle frei in auftreten $\varphi$ .
Ich wollte sagen, dass die Argumente dazu $\varphi$ Erfassen Sie alle Abhängigkeiten, die $\varphi$ hat (und damit das Fehlen von $b$ ist aussagekräftig). Geschlossen ist definitiv nicht das richtige Wort, aber ich weiß nicht, was es ist.
Die Notation $\varphi(v_1,\dots,v_n)$ wird normalerweise verwendet, um die freien Variablen der Formel anzugeben $\varphi$ gehören dazu $v_1,\dots,v_n$ . Das heißt, jede freie Variable in $\varphi$ ist eines der $v_i$ , aber nicht alle $v_i$ frei in auftreten müssen $\varphi$ . Dies ist eine sehr nützliche Notation, weil wir dann schreiben können $\varphi(a_1,\dots,a_n)$ für die Substitutionsoperation $a_i$ für jede kostenlose Instanz von $v_i$ . Und das macht es deutlich $\varphi$ definiert natürlich eine Teilmenge von $A^n$ / ein $n$ -ary Beziehung auf $A$ , für jede Struktur $A$ .
Es besteht normalerweise keine Notwendigkeit, die gebundenen Variablen in einer Formel auf ähnliche Weise anzugeben $\varphi$ , denn einmal gebunden, sind ihre Identitäten irrelevant. Das heißt, Sie können eine gebundene Variable (in ihrem Quantor und in jedem Fall innerhalb des Geltungsbereichs dieses Quantors) gegen eine andere Variable austauschen, ohne die Bedeutung der Formel zu ändern.
Danke schön. Was ich immer verwirrend fand $\varphi(\vec{v})$ ist, dass es verwendet wurde, um beides zu sagen $\text{FV}(\varphi) \subset \vec{v}$ und zu sagen $\varphi[x_1 := \vec{v}_1 \cdots x_n := \vec{v}_n]$ Wo $x_i$ ist der $i$ te freie Variable ... daher habe ich mich immer gefragt, ob der "Name" des Parameters oder seine Position in der Argumentliste wichtiger ist. // De Bruijn-Indizes sind eine weitere gute Alternative. Ich habe sie schon einmal in Diskussionen über Lambda-Kalkül gesehen, Substitution ist jedoch nicht trivial und erfordert, dass Sie hinzufügen.
Es gibt den von Gentzen (dem Vater von ND und Sequent Calc) verwendeten Ansatz, um Variablen zu trennen: $x,y$ nur gebunden verwendet , von Parametern : $a,b$ nur kostenlos genutzt. Beispiel mit $\forall$ -Einführungsregel: $\dfrac {\varphi} {\forall x \varphi [x/a]}$
Ich denke, einige verwandte (aber nicht umfassende) Lektüren könnten über die Metamath Proof Explorer-Dokumentation verstreut sein, z. B. ZFC Axioms Without Distinct Variable Conditions .

Peter Schmidt · Answer 1

"Ich denke, es gibt einige technische Vorteile bei der Definition der Syntax, um gebundene und freie Variablensymbole disjunkt zu machen. Ich bin nicht auf die Idee gekommen, freie und gebundene Variablen zu trennen, aber ich erinnere mich nicht, wo ich es gesehen habe." Die Methode, unterschiedliche Buchstaben für gebundene Variablen [dh Variablen, die dazu dienen, Quantoren-Präfixe an Stellen in einfachen oder komplexen Prädikaten zu binden] und für freie Variablen [Ausdrücke, deren Hauptverwendung als Parameter/Dummy-Namen/"willkürliche" Namen ist, je nachdem, was Sie bevorzugen, zu verwenden um es auszudrücken] ist in Gentzens ursprünglichen Untersuchungen über natürliche Deduktion aus den 1930er Jahren und dann wieder in Prawitz' klassischem Buch von 1965 enthalten. Es wird in einigen späteren einflussreichen Logiklehrbüchern aufgegriffen, beginnend mit denen von Lemmon und Thomason.

Je nachdem, wie Sie die Dinge genau einrichten, können Sie mit dem Gerät unter anderem vermeiden, sich um die unbeabsichtigte Erfassung von Variablen zu kümmern. Aber vielleicht ist der wichtigste positive Grund für die Übernahme des Geräts kein technischer, sondern [im weitesten Sinne] philosophischer oder konzeptioneller: Es hält an dem sehr guten Fregeschen Prinzip fest, wichtige Unterschiede der semantischen Rolle in der Syntax deutlich zu markieren .

Vergleich von Ansätzen zur Verwaltung freier und gebundener Variablen.

Gregor Nisbet

Thorimur

Alex Kruckmann

Gregor Nisbet

Alex Kruckmann

Alex Kruckmann

Gregor Nisbet

Mauro ALLEGRANZA

Markus S.

Antworten (1)

Peter Schmidt

Artikel über Ideen in der Geschichte der mathematischen Notation?

Ist die Summe zweier linearer Ausdrücke immer ein linearer Ausdruck?

Kann man die Set-Builder-Notation offiziell in ZFC einführen?

Ist die Theorie regulärer formaler Sprachen endlich axiomatisierbar?

Ist diese Intervallnotation zur Lösung eines Ungleichungsproblems korrekt?

Eine Projektarbeit zur algebraischen Topologie (mit kategorischem Flair): Vorschläge für Themen.

Satz, der Dennis Sullivan dazu inspirierte, zur Mathematik zu wechseln

Highschool-Geometrie-Text?

Wie übersetze ich „kein Philosophenstudent bewundert irgendeinen faulen Dozenten“ in eine quantifizierende Logikformel?

Definition des Rangs von Begriffen in der Sprache erster Ordnung