Diskussion:Prädikatenlogik zweiter Stufe

Definition von Gleichheit

Ich finde die Defintion von Gleichheit nicht wieder. Also ich meine

$\forall A,B:((A=B)<=>\forall$ Prädikat $P:P(A)<=>P(B))$

, oder so. Ich dachte, sie stände hier irgendwo. Kann sie aber leider nicht mehr wiederfinden. Weder hier noch auf dem Artikel zu Gleichheit.

Thomas Limberg (Schmogrow) 93.197.33.150 10:06, 20. Sep. 2015 (CEST)

Gleichheit gehört zur Sprache, siehe Prädikatenlogik erster Stufe. --FerdiBf (Diskussion) 13:11, 20. Sep. 2015 (CEST)

Ach, und was sagst du hierzu? Zitat von "http://webcache.googleusercontent.com/search?q=cache:eGhUAfn_ZOwJ:www.informatik.uni-ulm.de/ki/Edu/Vorlesungen/Inferenzsysteme/WS0203/r4.pdf+&cd=3&hl=de&ct=clnk&gl=de":

"In der Logik höherer Stufe läßt sich die Gleichheit auf einem Typ S definieren: (x = y) := [∀ P : (S →Bool). (P(x) ⇔ P(y))]"

Noch eine kleine Änderung meiner Formulierung (Klammern vergessen): $\forall A,B:((A=B)<=>\forall$ Prädikat $P:(P(A)<=>P(B)))$.

Thomas Limberg (Schmogrow) 93.197.33.150 13:40, 20. Sep. 2015 (CEST)

Ich bin hier im Wesentlichen der Darstellung aus "H.-D. Ebbinghaus, J. Flum, W. Thomas: Einführung in die mathematische Logik" gefolgt. In dieser Darstellung gehört Gleichheit zur Sprache, siehe auch entsprechende Ausführungen zur Prädikatenlogik erster Stufe. Du könntest doch ganz am Ende dieses Artikels einen neuen Unterparagraphen einfügen, etwa mit der Überschrift "Prädikatenlogik zweiter Stufe ohne Gleichheit" und dort dann entsprechende Auführungen platzieren. Davon könnte der Artikel profitieren.--FerdiBf (Diskussion) 18:23, 20. Sep. 2015 (CEST)

Man kann sich auch auf der englischen Wikipedia umschauen: "https://en.wiki.x.io/wiki/Equality_%28mathematics%29#Logical_formulations". Da steht im Wesentlichen das, was ich vorgeschlagen habe.

Thomas Limberg (Schmogrow) 93.197.6.61 08:20, 22. Sep. 2015 (CEST)

Hallo Thomas. So ist Deine Ergänzung ein Fremdkörper. Du solltest schon die bereits vorhandenen Bezeichnungen wählen. Demnach würdest Du definieren wollen $x=y:\Leftrightarrow \forall X(Xx\leftrightarrow Xy)$. Mit Prädikat meinst Du "einstellige Relation". In jeder Interpretation sind dies dann Teilmengen des Grundraums und die rechte Seite bedeutet dann, dass die Interpretationen von x und y in genau denselben Teilmengen liegen und daher gleich sind. Daraus ergibt sich, dass man genau dieselben Modelle erhält. Das ist ok und sollte irgendwie ausgeführt werden. Kannst Du bitte auch Literatur angeben, in der die Prädikatenlogik zweiter Stufe genau so aufgebaut ist. Damit die Formel nicht ganz so isoliert dasteht, solltest Du im Artikel noch ergänzen, dass man damit eine Prädikatenlogik zweiter Stufe ohne Gleichheit aufbauen kann, in der Gleichheit dann definiert wird, dass man dieselben Modelle hat, usw. Vielleicht könnte man noch die Peano-Axiome (s.o. im Artikel) in dieser Sprache angeben, um dem Leser ein Gefühl für den Verzicht auf Gleichheit zu geben.--FerdiBf (Diskussion) 07:39, 24. Sep. 2015 (CEST)

Modell

Bei den letzten beiden Zeilen scheint mir etwas zu fehlen. Was meint: 'Für alle R auf A'? Sind hier 'alle' beliebig-stelligen Relationen R auf A gemeint? Wie sieht dann ein Ausdruck mit so einer Relationsvariablen mit variabler Stelligkeit aus? Kann ich mir nicht vorstellen. Man kann doch nicht in einen Ausdruck rechts gleichzeitig n- und m-stellige Relationen auf A einsetzen mitt m<>n? "Alle R auf A"" kann nicht heißen $R\in \bigcup _{n\in \mathbb {N} _{0}}{\mathcal {P}}(A^{n})$ (Menge der beliebigstelligen Relationen auf A).

Habe mich mal in der online-Literatur umgeschaut, und bisher haben alle Autoren für jede Stelligkeit $n\in \mathbb {N} _{0}$ eine *eigene* Menge von Relationsvariablensymbolen definiert und die Quantoren laufen nur über diese mit festem n.

• [1] definiert "Für jede natürliche Zahl n ≥ 0 eine abzählbar unendliche Menge von n-stelligen Relationsvariablen"

• [2] "wenn φ eine Formel ist und X ∈ VARⁿ, dann sind ∃X.φ und ∀X.φ Formeln" mit VARⁿ = n-stellige Relationsvariablen", und: "A,β |= ∃X.φ mit X∈VARⁿ gdw. ein R⊆Aⁿ existiert mit A,β[X/R] |= φ"

usw.

Zum Vergleich: Mehrsortige Logik 1. Stufe wie in Deklaration von Variablen wie in

• Stefan Brass: Mathematische Logik mit Datenbank-Anwendungen. Martin-Luther-Universität Halle-Wittenberg, Institut für Informatik, Halle 2005, S. 176. 

auf S. 54 hat *eine* Menge von Variablensymbolen für alle Sorten und deklariert diese dann auf jeweils eine Sorte (keine Überladung von Variablensymbolen). Stelligkeit, Sorte und allg. Typ (im Sinn von Argumenttyp = n-Tupel von Argumentsorten, n=Stelligkeit) sind sehr verwandte Begriffe. Wäre es nicht möglich, mit *einer* Menge von Relationsvariablensymbolen zu arbeiten unddiese dann vor Benutzung auf eine bestimmte Stelligkeit zu deklarieren? Der feine Unterschied wäre der: Unter einem Quantor wäre des Symbol für eine gebundene Relationsvariable lokal auf die gerade benötigte Stelligkeit zu deklarieren. So wie die normalen Variablen gebunden unter einem Quantor in mehrsortiger Logik lokal auf eine benötigte Sorte umdeklariert werden (lokale Variante der Deklaration). Das sollte hier auch gehen! Dem Relationssymbol $X$ wird dabei zuvor per Deklaration $\nu$ eine Stelligkeit $n=\nu (X)$ zugewiesen. Den Relationssymbolen muss die Interpretationsfunktion dann eine Relation der deklarierten Stelligkeit zuweisen: $\beta (X)\subseteq A^{\nu (X)}$. Man braucht also in irgendeiner Form Symbole für die natürlichen Zahlen $i\in n$ und eine um diese erweiterte Interpretationsfunktion $\alpha :I\mathbb {N} _{0}$. Im einfachsten Fall reicht ein Strichsystem, d. h. | als weiteres Symbol, Zeichenketten $i=\underbrace {||\dots |} _{n{\text{-mal}}}$ aus n dieser Symbole wird ihre Wortlänge zugeordnet: $n\alpha (i)=len(i)$. Dies entspricht genau dem vielsortigen Fall mit nur einer Sorte |. Jedes g-al-System (g=2 Dual-, g=10 Dezimal-, … ist aber auch gut. Oder man führt ein Zeichen für die Null ein und eines für das Inkrement, siehe en: Second-order arithmetic, damit <matb>\alpha(SSSO) = 3</math>. Auf der linken Seite der beiden letzten Zeilen kann das durch ein Stelligkeitsurteil $X:i$ angedeutet werden: $\forall X:i\varphi ,\exists X:i\varphi$. Die rechten Seiten sind dann mit $n=\alpha (i)$ zu lesen als: $\dots {\mbox{ für alle }}n{\mbox{-stelligen Relationen }}B{\text{ auf }}A$
bzw.
${\text{es gibt eine }}n{\mbox{-stelligen Relation }}B{\text{ auf }}A{\text{ mit }}\dots$ Wahrscheinlich wäre es nur eine technische Rafinesse, und Beweisbarkeitsfragen nicht berührt. Literatur?

Noch eine Frage: Ramharter,Eder (Uni Wien) haben auch Funktionsvariablen. Was macht das für einen Unterschied?

BTW: Relationsvariablen der Stelligkeit 0 sind Aussagevariablen. Funktionsvariablen der Stelligkeit 0 sind gewöhnliche Variablen der PL 1. Stufe.

Bei mehrsortiger PL 2. Stufe muss man die Relationssymbole sowieso auf den Argumenttyp deklarieren, nicht? Es wäre die Stelligkeit n symbolisiert durch i mit $\alpha (i)=n$ durch den Argumenttyp $\nu (R)=t=(t1,\dots t_{n})\in T^{*}$ mit den Argumentsorten $t_{i}\in T$ mit der Menge der Sortensymbole T zu ersetzen. Das $R:t$ in der Zeichenkette auf der linken Seite ist dann ein modelliertes Typurteil wie es die Typentheorie fällt.

Resumee: Offenbar *kann* man für die Relationsvariablen zu jeder gegebenen Stelligkeit n > 0 (vielsortig: jeden Argumenttyps t), die normalen Variablen (vielsortig: jeder Sorte s), und ggf. zu den Funktionsvariablen jeder gegebene Stelligkeit n > 1 (wobei n=0 die normalen Variablen sind, vielsortig: jeden Argumenttyps t und jeder Wertesorte s) eine eigene Menge an Symbolen vorsehen. *Oder* man legt alles oder teilweise zusammen, im Prinzip reicht offenbar eine einzige Menge an Variablenzeichen. Dann wird der genaue Typ der benutzten Variablen per Deklaration $\nu$ festgelegt auf:

• Relationsvariable mit bestimmter Stelligkeit (bzw. Argumenttyp),
• Funktionsvariable mit bestimmter Stelligkeit (bzw. Argumenttyp + Bildsorte) mit immer vorhandenem Spezialfall
• normale Variable = Funktionsvariable mit Stelligkeit (ggf. mit Sorte)

Gebundene Variablen unter den Quantoren haben nicht nur eine lokale Variante des Werts $\beta '$, sondern auch - zuerst mal - ihres Typs $\nu '$. --Ernsts (Diskussion) 09:28, 27. Feb. 2018 (CET) Update/Ergänzung --Ernsts (Diskussion) 13:02, 1. Mär. 2018 (CET)

Was ist der Zus'hang Funktionsvariablen und en:Second order arithmetics? Scheint mir, da genau das bei Ramharter,Eder 2015/16 integriert ist, es geht dort wie im engl. Artikel viel um Peano... --Ernsts (Diskussion) 13:43, 1. Mär. 2018 (CET)

Lokal modifizierte Funktion - Notation

Im Artikel hier wird (zurzeit) die Notation $\beta {\frac {a}{x}}$ benutzt, Stefan Brass (2005) verwendet $\beta '=\beta \langle {x/a}\rangle$ (für die Variablendeklaration, was analog geht), C. Lutz ganz ähnlich $\beta [{x/a}]$, und Klaus Grue (1995) ganz im Allgemeinen $\beta _{\langle x\mapsto a\rangle }$ (und baut mit diesen Maplets Funktionen mit endlichem Definitionsbereich ausgehend von $\emptyset =\epsilon$ (=nirgends definierte Funktion, Nullfunktion) zusammen).
Für mich sprechen gegen die ersten beiden Notationen

• beide benutzen einen Bruchstrich, der allgemein eine ganz andere Bedeutung hat, was zu Konfliktsituationen führen kann
• haben im Vergleich miteinander Zähler und Nenner vertauscht.

Für die Maplet-Notation spricht, dass diese sowieso schon für Abbildungen benutzt wird, also keine große Erklärung braucht (statt Konfliktsituationen herauf zu beschwören). Zwecks besserer Lesbarkeit scheint mir diese Notation mit Tieferstellung $\beta _{\langle x\mapsto a\rangle }$ am geeignetsten. Hatte diese daher - ohne den Artikel hier bis dato in Augenschein genommen zu haben - in Lemma Term eigeführt.
Würde gern die Notation in WP:de vereinheitlicht sehen, aber wie? Daher bitte ich um Meinungen/Anregungen/Vorschläge! Meine eigene Präferenz ist nach wie vor 'Grue, tiefergestellt' :-) Anm.: die C-Syntax dafür für $\beta _{\langle x_{0}\mapsto a\rangle }(x)$ lautet (x=x0)?a:beta(x), die Visual-Basic-Syntax iif(x=x0,a,beta(x)), siehe en:IIf, en:?:, ?:, Bedingte_Anweisung_und_Verzweigung#Auswahloperator, Wikibooks: VBA in Excel/Wenn-Abfragen . --Ernsts (Diskussion) 01:17, 11. Mär. 2018 (CET)

Wir wollen

Ist es der gewollte Stil der Wikipedia sätze mit "wir wollen" in die Erklärung ein zu bauen? --Tavin (Diskussion) 13:56, 21. Feb. 2021 (CET)