Diskussion:Prädikatenlogik zweiter Stufe

aus Wikipedia, der freien Enzyklopädie

Definition von Gleichheit

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

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \forall A, B: ( ( A = B ) <=> \forall } Prädikat Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle 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): Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \forall A, B: ( ( A = B ) <=> \forall } Prädikat Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle 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.wikipedia.org/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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle 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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle R \in \bigcup_{n \in \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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle n \in \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 ∈ VARn, dann sind ∃X.φ und ∀X.φ Formeln" mit VARn = n-stellige Relationsvariablen", und: "A,β |= ∃X.φ mit X∈VARn gdw. ein R⊆An existiert mit A,β[X/R] |= φ"

usw.

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

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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle X} wird dabei zuvor per Deklaration Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \nu} eine Stelligkeit Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle n = \nu(X)} zugewiesen. Den Relationssymbolen muss die Interpretationsfunktion dann eine Relation der deklarierten Stelligkeit zuweisen: Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \beta(X) \sube A^{\nu(X)}} . Man braucht also in irgendeiner Form Symbole für die natürlichen Zahlen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle i \in n} und eine um diese erweiterte Interpretationsfunktion Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \alpha:I \N_0} . Im einfachsten Fall reicht ein Strichsystem, d. h. | als weiteres Symbol, Zeichenketten Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle i = \underbrace{||\dots|}_{n\text{-mal}}} aus n dieser Symbole wird ihre Wortlänge zugeordnet: Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle 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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle X:i} angedeutet werden: Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \forall X:i\varphi, \exists X:i\varphi} . Die rechten Seiten sind dann mit Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle n = \alpha(i)} zu lesen als: Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \dots\mbox{ für alle } n\mbox{-stelligen Relationen } B \text { auf } A}
bzw.
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \alpha(i) = n} durch den Argumenttyp Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \nu(R) = t = (t1,\dots t_n) \in T^*} mit den Argumentsorten Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle t_i \in T} mit der Menge der Sortensymbole T zu ersetzen. Das Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle 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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \beta'} , sondern auch - zuerst mal - ihres Typs Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \beta\frac{a}{x}} benutzt, Stefan Brass (2005) verwendet Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \beta' = \beta\langle{x/a}\rangle} (für die Variablendeklaration, was analog geht), C. Lutz ganz ähnlich Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \beta[{x/a}]} , und Klaus Grue (1995) ganz im Allgemeinen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \beta_{\langle x \mapsto a\rangle}} (und baut mit diesen Maplets Funktionen mit endlichem Definitionsbereich ausgehend von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \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)

Abgerufen von „https://de.wikiup.org/index.php?title=Diskussion:Prädikatenlogik_zweiter_Stufe&oldid=209062765“