Diskussion:Freie Variable und gebundene Variable

Ausdruck vs. Formel

@Wasseralm,

gibt es einen Grund, warum Du "Ausdruck" durch "Formel" ersetzt hast? Ich kenne "formula" aus englischsprachiger Literatur, die mit bekannte deutsche Literatur (im Wesentlichen Ebbinghaus) benutzt aber den Begriff "Ausdruck". --Digamma 15:12, 5. Jan. 2008 (CET)

Hallo Digamma, ich habe "Formel" gelernt (ist schon lange her) und immer "Formel" benutzt und gehört. In dem Skript von Ebbinghaus/Flum/Thomas wird aber tatsächlich durchgängig "Ausdruck" verwendet. Ein Nachweis für "Formel" wäre z. B. O. Deiser, Einführung in die Mengenlehre. Ob das eine Entwicklung in neueren deutschen Büchern ist, "Ausdruck" zu benutzen, weiß ich nicht. Da müsste man vielleicht noch einige weitere Bücher zu Rate ziehen. In der Wikipedia scheint mir "Formel" eher benutzt zu werden, siehe z. B. Aussagenlogik oder Bereinigte Normalform oder Pränexform. Der Artikel Prädikatenlogik drückt sich da irgendwie drum herum, es kommt aber auch "Formel" drin vor. Gruß, Wasseralm 17:39, 5. Jan. 2008 (CET)

Herzlichsten Dank --Digamma 17:41, 5. Jan. 2008 (CET)

zu spezielle Definition

Die Definition ist viel zu speziell auf die Prädikatenlogik bezogen. Gebundene Variablen sind - wie der Artikel ja andeutet - ein viel allgemeineres Phänomen. Darauf sollte bereits die Definition eingehen. Die Prädikatenlogik ist dann als einfachster Sonderfall zu behandeln. Ich werde mich in nächster Zeit darum kümmern.--Wilfried Neumaier 18:55, 25. Jul. 2009 (CEST)

Die Sache ist jetzt besser. Unglücklich bin ich nur über den "Bereich eines Operators". Es gibt ja viel Operatoren mit freien Variablen, etwa der Potenzmengen-Operator. Es sind also spezielle Operatoren gemeint, verschiedenste Sorten von Quantoren und vor allem der zentrale, überall in der Mathematik gebrauchte Klassenoperator und alle von ihm abgeleiteten Operatoren mit gebundener Variable.--Wilfried Neumaier 22:03, 11. Aug. 2009 (CEST)

Gebunde Variablen in Beispielen

In den Beispielen im letzten Abschnitt letzten Abschnitt sollte man klar benennen, welche Variablen nun gebunden oder frei sind. Diese Formeln stehen hier kommentarlos da. Das ist eine Zumutung.--Wilfried Neumaier 11:16, 15. Jul. 2010 (CEST)

Der Meinung bin ich auch. Ich versuche mich mal daran. -- Digamma 20:12, 15. Jul. 2010 (CEST)

Andere Logiken und Integral

Ich haette bitte gerne die freien und gebundenen Variablen in anderen Kaluelen erlaeutert, da es dort nicht undbedingt an den Quantoren abzulesen ist, z. B. Gentzens Kalkuel. Andereseits ist beim Integral nicht dx die Variable? Bei der Integration, ist x doch festgehalten, auf jeden Fall hinkt dann das Beispiel je nach Betrachtungsweise. -- Room 608 22:46, 28. Aug. 2010 (CEST)

Beim Integral ist dx keine Variable, sondern nur der Textteil, der anzeigt, dass x die gebundene Variable ist.

Beim Gentzenkalkül, der ja ein prädikatenlogischer Kalkül ist, stehen gebundene Variablen immer nach Quantoren. Andere Kontexte können höchstens definierte Abkürzungen für Quantorenformeln sein. In diesen Fällen sieht man am Definiens, welche Variablen gebundenen sind und welche frei sind. Genauso ist es auch in Klassen- oder Mengenkalkülen: Am Definiens einer definierten Formel sieht man immer, welche Variablen gebunden sind und welche nicht. Man muss also immer nur die Definitionskette zurückgehen, bis man auf eine Formel kommt, an der man die Variablenart klar erkennen kann. Soll man eine derartige Bemerkung in den Artikel einfügen?--Wilfried Neumaier 11:47, 29. Aug. 2010 (CEST)

Ja, das ist allgemeiner und hilfreich. -- Room 608 20:46, 3. Sep. 2010 (CEST)

Gut, ich bereite einen entsprechenden Text vor mit Beispielen vor.----Wilfried Neumaier 06:12, 6. Sep. 2010 (CEST) Ich habe es am Beispiel der Vereinigung von Mengen, die vorher in der Liste weiter unten stand, erklärt. Ist es so verständlich?--Wilfried Neumaier 07:55, 6. Sep. 2010 (CEST)

Soweit ist das schoen klar. Wenn aber in Formeln am Schluss alles gebunden sein muss, was passiert mit den letzten freien Variablen, koennten da beispielsweise die Voraussetzungen eingehen? Das gehoert ja nicht mehr ganz hierher.

A ist in der ersten Zweile frei aber eine vorgegebene (sinnvolle) Formel.

Oder anders ausgedrueckt, was will man mit den freien Variablen erreichen? Sie einfuehren fuer spaetere Verwendung, bis sie schliesslich gebunden sind?

-- Room 608 10:24, 6. Sep. 2010 (CEST)

In Formeln müssen nicht alle Variablen gebunden sein. Nur in sogenannten geschlossenen Formeln sind alle Variablen gebunden, in offenen dagegen nicht. Freie Variablen nennt man zuweilen auch Platzhalter. In sie darf man beliebige Terme einsetzen, also gegebene sinnvolle Terme nach eigener Wahl bei irgendwelchen Andwendungen, etwa Zahlen oder Mengen oder dergleichen. Wenn man einen Satz mit freien Variablen beweisen kann, dann kann man sie zwar auch mit einem Allquantor versehen, das ist die sogenanntne Allquantor-Einführung. Wenn sie aber so gebunden ist, darf man sie nicht mehr belegen mit irgendwelchen Termen, sonst entstehen sinnlose Formeln, denn hinter einem Quantor kann zum Beispiel keine Zahl stehen. Will man eine Formel mit gebundener Variable auf konkrete Objekte anwenden, dann muss man sich einer Quantoren-Beseitigungs-Regel bedienen, die dem Namen entsprechend den Quantor verschwinden lässt und die Variable wieder frei macht, so dass sie belegbar wird. Soll ich auch noch einige Bemerkungen in dieser Richtung in den Artikel einbauen?--Wilfried Neumaier 11:14, 6. Sep. 2010 (CEST)

Variable als "Platzhalter" sollte erwaehnt werden, der Rest in knapper Form ist auch hilfreich. -- Room 608 19:06, 15. Sep. 2010 (CEST)

Ich werde einen Verbesserungsvorschlag erarbeiten, der den Zweck der freien und gebundenen Variablen benennt, aber erst zusammen mit einigen Punkten, die der folgende Diskussionspunkt anspricht.--Wilfried Neumaier 08:11, 16. Sep. 2010 (CEST)

Definitionsprobleme

Weiter oben wurde schon genannt, dass es Operatoren gibt, die Variablen binden und auch solche, die dies nicht tun. Das unterschlägt die Definition. Sehr misslich ist auch die bisherige Definition der gebundenen Variable, weil das Definiens schon gebundene Variablen voraussetzt: "Sind hingegen alle Vorkommen der Variable innerhalb der Formel an Operatoren gebunden, bezeichnet man die Variable als in dieser Formel gebunden". So ein Definitionsfehler muss unbedingt beseitigt werden. Diese Definition streitet auch gegen die weiter unten im Artikel gemachte Feststellung: "Ein und dieselbe Variable kann in einer Formel sowohl freie als auch gebundene Vorkommen haben". Danach müssen doch nicht alle Vorkommen gebunden sein.--Wilfried Neumaier 08:20, 16. Sep. 2010 (CEST)

Unfug?

Folgendes habe ich einfach mal aus dem "Beispiele"-Abschnitt entfernt, weil es keinen guten Sinn ergibt:

Bei abgeleiteten Formeln, die durch Definition eingeführt werden, erkennt man die freien und gebundenen Variablen am Definiens. Die Variablen des Definiens vererben nämlich ihre Eigenschaft, frei oder gebunden zu sein, auf die Variablen des Definiendum. Man muss dann die Definitionskette verfolgen, ausgehend von elementaren Formeln, an denen die freien und gebundenen Variablen sofort erkennbar sind. Als Beispiel diene die Definition der Vereinigung einer Familie von Mengen über folgende drei Schritte:

• In der Definition $\exists x\in M\colon A(x):\iff \exists x\colon x\in M\land A(x)$ ist $\,x$ gebunden und $\,M$ frei.

• In der Definition $\bigcup M:=\{x\mid \exists y\in M\colon x\in y\}$ sind $\,x$ und $\,y$ gebunden und $\,M$ frei.

• In der Definition $\bigcup _{i\in I}A_{i}:=\bigcup \{x\mid \exists i\in I\colon x=A_{i}\}$ sind $\,i$ und $\,x$ gebunden und $\,I$ und $\,A$ frei.

Was hier in den Aufzählungspunkten definiert wird, sind Notationsmakros mit selbstverständlich (als formale Parameter) gebundenen Variablen (siehe Lambda-Kalkül; auch wenn der hier nicht direkt verwendet wird). Alle angeblich freien Variablen sind hier gebunden. Wäre dem nicht so, dann wären die Definitionen nicht sehr nützlich.

Keine Ahnung, was der Autor dieses Teiltextes uns mal sagen wollte... --Daniel5Ko 01:22, 6. Dez. 2010 (CET)

Möglicher Fehler?

Unter Beispiele ( https://de.wikipedia.org/wiki/Freie_Variable_und_gebundene_Variable#Beispiele ) liegt bei dem zweiten Beispiel möglicherweise ein Fehler vor. Wieso ist das zweite x in Q(x) ungebunden? Da keine Klammern gesetzt sind, bedeutet das, dass der Allquantor die schwächste Klammerung hat, folglich also im Syntaxbaum entsprechend an der Spitze steht und die stärkeren Operatoren unterhalb folgen. Alle x unterhalb vom Allquantor müssen daher gebunden und nicht frei sein. Ich hoffe, dass ich mich irre. Wenn ja, wäre eine Erklärung vielleicht hilfreich. --AloisIrlmaier (Diskussion) 17:13, 11. Okt. 2020 (CEST)

EDIT: Ich habe das ganze nun entsprechend geändert. Sollte es Einwände geben, bitte hier rein. Nochmal: So weit mir bekannt nehmen die Quantoren alles was nach ihnen steht, d.h. die Quantoren binden am schwächsten. Damit also das gilt, was ursprünglich im Artikel behauptet wurde (nämlich das x in P(x) gebunden und x in Q(x) ungebunden sei), müsste also geklammert werden:

$(\forall xP(x))\land Q(x)$

Da das im Artikel angegebenen Beispiel nicht der Fall ist, ist folglich auch sowohl das benutzende Auftreten von x in P(x) als auch das benutzende Auftreten von x in Q(x) gebunden an den Allquantor. --AloisIrlmaier (Diskussion) 20:00, 11. Okt. 2020 (CEST)

So wie ich die Syntax der Logik der ersten Stufe kenne, gibt es überhaupt keine Operatorrangfolge, d.h. nur Klammern binden. Der Allquantor bezieht sich auf die (geklammerte) Formel, die ihm unmittelbar folgt, das ist hier nur das $P(x)$. Wenn er sich auf $P(x)\land Q(x)$ erstrecken soll, dann muss die Konjunktion geklammert werden: $\forall x(P(x)\land Q(x))$ . --Digamma (Diskussion) 20:10, 11. Okt. 2020 (CEST)

Es gibt verschiedene Konventionen und natürlich ist "Logik der ersten Stufe" nicht an eine bestimmte konkrete Syntax gebunden. John Harrison schreibt in "Handbook of Practical Logic and Automated Reasoning" zum Beispiel

In our concrete syntax, the scope of a quantifier extends as far to the right as possible, e.g. $\forall x.P(x)\Rightarrow Q(x)$ means $\forall x.(P(x)\Rightarrow Q(x))$ and not $(\forall x.P(x))\Rightarrow Q(x)$. (Many, especially older, texts use exactly the opposite convention, making quantifiers bind tighter than propositional connectives. The reader should keep this in mind when consulting the literature.)

Viele Beweisassitenten (Coq, Agda, Epigram, Lean) verwenden die modernere Konvention "mit langen Skopen", weil sich wohl herausgestellt hat, dass sich damit in den meisten Fällen besser lesbare Formeln ergeben, und notwendige Klammern auf eine erhöhte inhaltliche Komplexität hinweisen. --Daniel5Ko (Diskussion) 22:46, 20. Sep. 2021 (CEST)