| |
| Autor |
 semantische Beweise als Kalkül darstellbar? |
|
carlox
Aktiv 
Dabei seit: 22.02.2007
Mitteilungen: 1623
 |  Themenstart: 2023-09-16
|
Hallo allerseits,
die Semantik einer Sprache der Prädikatenlogik wird bekanntlich induktiv definiert.
Die „normalen“ Beweise in der Mathematik sind "semantische Beweise" (über die Wahrheit).
In diesen semantischen Beweisen wird auch oft der Begriff „daraus folgt“ benutzt.
Deswegen könnte man auf die Idee kommen, diese semantischen Beweise auch als Kalküle (Semantikkalkül) darzustellen.
Definition:
$\models_\mathfrak{A} a$
bedeutet: Die Formel a ist in der Struktur $\mathfrak{A}$ für alle Belegungen h wahr.
Als Regeln des Kalküls könnte man z.B. wählen:
\( \frac {\models_\mathfrak{A} ({a \rightarrow b)} \; , \; \models_\mathfrak{A} a} {\models_\mathfrak{A} b}\)
\( \frac {\models_\mathfrak{A} {a}} {\models_\mathfrak{A} {a \lor b}} \)
\( \frac {\models_\mathfrak{A} B_x^t} {\models_\mathfrak{A} \exists x \; B}\)
\( \frac {\models_\mathfrak{A} B} {\models_\mathfrak{A} \forall x \; B}\)
….
Das wird aber nicht funktionieren, da dann die Menge der wahren arithmetischen Formeln rekursiv aufzählbar wäre.
(siehe im Buch „Theoretische Informatik kurz gefasst“ S. 140 den Beweis des Gödelschen Unvollständigkeitssatz )
Frage:
Welche Anforderung könnte man nicht als Regel formulieren?
Ich vermute so etwas (wo unendlich viele Voraussetzungen benötigt werden):
\( \frac {\models_\mathfrak{A} {B(1)} \; , \; \models_\mathfrak{A} B(2), ...} {\models_\mathfrak{A} \forall i \; B}\)
\( \frac {\models_\mathfrak{A} B_x^t} {\models_\mathfrak{A} \exists x \; B}\)
\( \frac {\models_\mathfrak{A} B} {\models_\mathfrak{A} \forall x \; B}\)
1)
Was meint ihr dazu?
2)
Könnte man einen Semantikkalkül definieren, wenn keine Quantoren in den Formeln vorkommen ?
mfg
cx
|
 Profil
|
Pippen
Aktiv 
Dabei seit: 06.07.2021
Mitteilungen: 244
| Beitrag No.1, eingetragen 2023-09-18
|
Das gibt es doch schon. Jeder korrekte Kalkül ist auch ein semantischer Kalkül in deinem Sinne. Denn wenn du dort folgerst $\Gamma \vdash A$, dann ist das automatisch auch die semantische Folgerung $\Gamma \vDash A$.
|
Profil
|
carlox
Aktiv
Dabei seit: 22.02.2007
Mitteilungen: 1623
| Beitrag No.2, vom Themenstarter, eingetragen 2023-09-18
|
\quoteon(2023-09-18 01:41 - Pippen in Beitrag No. 1)
Das gibt es doch schon. Jeder korrekte Kalkül ist auch ein semantischer Kalkül in deinem Sinne. Denn wenn du dort folgerst $\Gamma \vdash A$, dann ist das automatisch auch die semantische Folgerung $\Gamma \vDash A$.
\quoteoff
Das ist etwas anderes:
$\Gamma \vDash A$
bedeutet:
Jede Interpretation $\mathfrak{A}$, die Modell von $\Gamma$ ist, ist auch Modell von A
$\models_\mathfrak{A} A$
dagegen bedeutet:
Die Formel A ist in der _vorgegebenen_ Struktur $\mathfrak{A}$ für alle Belegungen h wahr (aber nicht notwendig für alle Strukturen).
$\mathfrak{A}$ könnte z.B. das Standardmodell der natürlichen Zahlen sein.
Der Gödelsche Unvollständigkeizssatz sagt dann, dass es eine wahre arithmetische Aussage gibt, die sich nicht beweisen läßt.
Bzw. siehe "Theoretische Informatik kurz gefasst" von Uwe Schöning:
Jedes Beweissystem für die Menge der wahren arithmetischen Formeln ist notwendigerweise unvollständig.
mfg
cx
|
Profil
|
tobit09
Aktiv 
Dabei seit: 24.04.2018
Mitteilungen: 86
| Beitrag No.3, eingetragen 2023-09-18
|
Hallo carlox,
ein geeignetes "Modell" für normale Beweise in der Mathematik ist aus meiner Sicht ein Kalkül des natürlichen Schließens. Die Beweise in diesem Kalkül würde ich als syntaktisch, nicht als semantisch einordnen.
Man schlussfolgert in der Mathematik üblicherweise aus Axiomen und trifft keine Aussagen für nur eine bestimmte den Axiomen genügende Struktur, sondern für alle den Axiomen genügende Strukturen gleichzeitig.
Der Gödelsche Unvollständigkeitssatz liefert in der Tat, dass es dir nicht gelingen wird, einen Kalkül (mit rekursiv aufzählbarer Menge der bewiesenen Formeln) anzugeben, der genau die im Standardmodell der natürlichen Zahlen gültigen Sätze beweist.
Daher wird es schwierig sein, dir eine konkrete Regel zu benennen, die in dem von dir intendierten Kalkül fehlt; könnte ich sagen "nur die und die Regel fehlt", dann wäre der Kalkül erweitert um diese Regel ja vermutlich ein "Gegenbeispiel zum Gödelschen Unvollständigkeitssatz".
Mir ist im Übrigen unklar, welche Schlussregeln in deinem Kalkül für die atomaren Formeln gelten sollen.
Mir sieht es so aus, als würdest du im Grunde eigentlich einen syntaktischen Kalkül des natürlichen Schließens aufstellen, nur dass du statt des üblichen $\vdash$ die Notation $\models_\mathfrak{A}$ wählst, aber in Wahrheit die speziellen Eigenheiten des Modells $\mathfrak{A}$ ignorierst.
Viele Grüße
Tobias
|
Profil
|
Zwerg_Allwissend
Senior 
Dabei seit: 02.12.2013
Mitteilungen: 354
| Beitrag No.4, eingetragen 2023-09-18
|
Ein Kalkül besteht aus einer formalen Sprache, einem Regelsystem sowie einem Herleitungsbegriff mittels dessen aus Ausdrücken der Sprache unter Verwendung der Regeln weitere Ausdrücke gebildet werden können, also durch reine Symbolmanipulation. Einen Sinn bekommt das ganze durch Definition einer Semantik mittels deren den sparchlichen Ausdrücken eine Bedeutung zugewiesen wird. Damit können "Wahrheiten" durch reine Symbolmanipulation mittels der Herleitungen berechnet werden.
Was soll jetzt ein "semantischer Kalkül" sein? Wie lautet die zugrundeliegende formale Sprache? Was wäre deren Semantik? Was würde man durch solch einen Kalkül gewinnen?
|
Profil
|
carlox
Aktiv 
Dabei seit: 22.02.2007
Mitteilungen: 1623
| Beitrag No.5, vom Themenstarter, eingetragen 2023-09-18
|
\quoteon(2023-09-18 09:50 - tobit09 in Beitrag No. 3)
ein geeignetes "Modell" für normale Beweise in der Mathematik ist aus meiner Sicht ein Kalkül des natürlichen Schließens. Die Beweise in diesem Kalkül würde ich als syntaktisch, nicht als semantisch einordnen.
Man schlussfolgert in der Mathematik üblicherweise aus Axiomen und trifft keine Aussagen für nur eine bestimmte den Axiomen genügende Struktur, sondern für alle den Axiomen genügende Strukturen gleichzeitig.
\quoteoff
Die "Beweise" in den meisten Vorlesungen bzw. Lehrbüchern (Analysis, lineare Algebra, Numerik, usw.) sind doch "semantische Beweise".
In diesem wird auch argumentiert, d.h. es werden Begriffe, wie
also, daraus folgt, usw. benutzt.
Ein "semantischer Beweis" kann etwas beweisen, was man mit einem Beweis (eines Kalküls) nicht beweisen kann (Menge aller wahren arithmetischen Formel - siehe meinen letzten Beitrag).
\quoteon
Der Gödelsche Unvollständigkeitssatz liefert in der Tat, dass es dir nicht gelingen wird, einen Kalkül (mit rekursiv aufzählbarer Menge der bewiesenen Formeln) anzugeben, der genau die im Standardmodell der natürlichen Zahlen gültigen Sätze beweist.
Daher wird es schwierig sein, dir eine konkrete Regel zu benennen, die in dem von dir intendierten Kalkül fehlt; könnte ich sagen "nur die und die Regel fehlt", dann wäre der Kalkül erweitert um diese Regel ja vermutlich ein "Gegenbeispiel zum Gödelschen Unvollständigkeitssatz".
\quoteoff
Ja, man kann keine Regel nennen, die fehlt.
Aber vielleicht kann man angeben, warum man in der induktiv definierten Semantik etwas formulieren kann, was sich nicht in einem Kalkül darstellen läßt.
\quoteon
Mir ist im Übrigen unklar, welche Schlussregeln in deinem Kalkül für die atomaren Formeln gelten sollen.
\quoteoff
Wenn man z.B. in der Gruppentheorie den Beweis eines Satzes angeben will,
sind die Axiome (der Gruppentheorie) wahr, also:
Für alle $g \in G \models_\mathfrak{A} g$
Als Regel:
\( \frac {} {\models_\mathfrak{A} g}\)
\quoteon
Mir sieht es so aus, als würdest du im Grunde eigentlich einen syntaktischen Kalkül des natürlichen Schließens aufstellen,
\quoteoff
Ich suche ein konkretes einfaches Beispiel, an dem man erkennt, dass die induktiv definierte Semantik nicht durch ein Kalkül ersetzt werden kann.
D.h. Ich suche in einem "semantischen Beweis" die Stelle, die sich nicht in einen syntaktischen Beweis transformieren läßt.
mfg
cx
|
Profil
|
carlox
Aktiv
Dabei seit: 22.02.2007
Mitteilungen: 1623
| Beitrag No.6, vom Themenstarter, eingetragen 2023-09-18
|
\quoteon(2023-09-18 12:44 - Zwerg_Allwissend in Beitrag No. 4)
Was soll jetzt ein "semantischer Kalkül" sein? Wie lautet die zugrundeliegende formale Sprache? Was wäre deren Semantik? Was würde man durch solch einen Kalkül gewinnen?
\quoteoff
Die meisten "Beweise" in den Vorlesungen sind "semantische Beweise".
In diesen wird auch argumentiert (eben über den Wahrheitsbegriff), d.h. es werden Begriffe, wie also, daraus folgt, usw. benutzt, die mich an ein Regelsystem und einen Herleitungsbegriff erinnern.
Meine Idee ist, dies durch etwas "Kalkülähnliches" zu formalisieren
(man könnte es einen "semantischen Pseudokalkül" nennen).
Dieser braucht keine Semantik, sondern nur eine formalen Sprache, ein Regelsystem und einen Herleitungsbegriff
mfg
cx
|
Profil
|
carlox
Aktiv
Dabei seit: 22.02.2007
Mitteilungen: 1623
| Beitrag No.7, vom Themenstarter, eingetragen 2023-09-19
|
Hallo allerseits,
Vielleicht zur Verdeutlichung das folgendes Beispiel:
Angenommen man hätte für die Goldbachsche Vermutung einen "semantischen Beweis" gefunden, d.h. diese Vermutung mit Hilfe der induktiven Definition der Semantik des Standardmodells der natürlichen Zahlen bewiesen.
Könnte es dann trotzdem sein, dass es keinen "syntaktischen Beweis" in einem Kalkül gibt?
mfg
cx
|
Profil
|
tobit09
Aktiv 
Dabei seit: 24.04.2018
Mitteilungen: 86
| Beitrag No.8, eingetragen 2023-09-20
|
Hallo carlox,
entschuldige bitte, dass ich erst jetzt zum Antworten komme.
\quoteon(2023-09-18 18:49 - carlox in Beitrag No. 5)
Die "Beweise" in den meisten Vorlesungen bzw. Lehrbüchern (Analysis, lineare Algebra, Numerik, usw.) sind doch "semantische Beweise".
In diesem wird auch argumentiert, d.h. es werden Begriffe, wie
also, daraus folgt, usw. benutzt.
\quoteoff
Ich würde diese Beweise als syntaktische Beweise bezeichnen. Jeder vernünftige (im Sinne von: rein logisch und nicht anschaulich argumentierende) solche Beweis lässt sich prinzipiell (mit genügend Aufwand) in einen Beweis in einem (üblicherweise als syntaktisch angesehenen) Kalkül des natürlichen Schließens übersetzen.
Eine Sichtweise dieser Beweise als semantische Beweise wäre mir neu.
Aber selbst, wenn man eine solche Sichtweise sinnvoll vertreten können sollte: Dann wird eben z.B. statt $\operatorname{ZFC}\vdash A$ für irgendwelche Formeln A stattdessen $\operatorname{ZFC}\models A$ begründet.
Da $\operatorname{ZFC}\vdash A$ und $\operatorname{ZFC}\models A$ nach Gödelschem Vollständigkeitssatz ohnehin äquivalent sind (bzw. für jeden vernünftigen syntaktischen Kalkül sein sollten), sollte auch diese Sichtweise keinen wesentlichen Unterschied machen.
Einen wesentlichen Unterschied würde es hingegen machen, wenn man stattdessen irgendwie $\models_\mathfrak{A} A$ für ein bestimmtes ZFC-Modell $\mathfrak{A}$ zeigen würde.
So einen Beweis habe ich jedoch (außerhalb von Mengenlehrevorlesungen) noch nicht gesehen; solche Beweise scheinen im mathematischen Alltag keine nennenswerte Rolle zu spielen.
\quoteon(2023-09-18 18:49 - carlox in Beitrag No. 5)
Ein "semantischer Beweis" kann etwas beweisen, was man mit einem Beweis (eines Kalküls) nicht beweisen kann (Menge aller wahren arithmetischen Formel - siehe meinen letzten Beitrag).
\quoteoff
Das ist eine sehr optimistische Sichtweise, die ich nicht teile. Glaubst du wirklich, dass man jede wahre arithmetische Formel mit einem (semantischen) Beweis beweisen kann? Ich glaube das nicht. (Natürlich ist diese Frage unpräzise, solange nicht klar ist, was ein semantischer Beweis genau ist.)
\quoteon(2023-09-18 18:49 - carlox in Beitrag No. 5)
Wenn man z.B. in der Gruppentheorie den Beweis eines Satzes angeben will,
sind die Axiome (der Gruppentheorie) wahr, also:
Für alle $g \in G \models_\mathfrak{A} g$
Als Regel:
\( \frac {} {\models_\mathfrak{A} g}\)
\quoteoff
$G$ bezeichnet hier offensichtlich die Menge der Gruppentheorie-Axiome und $\mathfrak{A}$ eine Struktur in der Sprache der Gruppentheorie (also im Grunde eine Gruppe)?
Dann berücksichtigt dein Kalkül doch anscheinend nirgendwo spezielle Eigenschaften der speziellen Gruppe $\mathfrak{A}$? Warum schreibst du dann nicht gleich $\operatorname{Gruppen-Axiome}\models A$ oder $\operatorname{Gruppen-Axiome}\vdash A$ für Gruppentheoretische Sätze statt $\models_\mathfrak{A}A$, wenn dich die konkrete Gruppe $\mathfrak{A}$ ohnehin kaum interessiert?
\quoteon(2023-09-18 18:49 - carlox in Beitrag No. 5)
Ich suche ein konkretes einfaches Beispiel, an dem man erkennt, dass die induktiv definierte Semantik nicht durch ein Kalkül ersetzt werden kann.
D.h. Ich suche in einem "semantischen Beweis" die Stelle, die sich nicht in einen syntaktischen Beweis transformieren läßt.
\quoteoff
Jeder "normale" mathematische Beweis lässt sich prinzipiell (mit genügend Aufwand) entsprechend transformieren.
\quoteon(2023-09-19 21:28 - carlox in Beitrag No. 7)
Angenommen man hätte für die Goldbachsche Vermutung einen "semantischen Beweis" gefunden, d.h. diese Vermutung mit Hilfe der induktiven Definition der Semantik des Standardmodells der natürlichen Zahlen bewiesen.
Könnte es dann trotzdem sein, dass es keinen "syntaktischen Beweis" in einem Kalkül gibt?
\quoteoff
Ich würde sagen, das kommt darauf an.
Die aus meiner Sicht wahrscheinlichere Möglichkeit 1: Der Beweis wäre ein ganz "normaler" Beweis. Vermutlich wäre also so etwas wie $ZFC\vdash \operatorname{Goldbachsche Vermutung}$ oder (wohl unwahrscheinlicher) $PA\vdash\operatorname{Goldbachsche Vermutung}$ herleitbar. Damit wäre die Goldbachsche Vermutung insbesondere nicht exklusiv für das Standardmodell der natürlichen Zahlen gezeigt, sondern insbesondere auch für Modelle von von ZFC bzw. PA mit Nichtstandardzahlen. Aber es wäre ein syntaktischer Beweis gefunden, der sich sicherlich prinzipiell mit genügend großem Aufwand in einem Kalkül des natürlichen Schließens darstellen ließe.
Die ebenfalls denkbare Möglichkeit 2: Es werden völlig neue Methoden entwickelt, um Aussagen über die gewöhnlichen natürlichen Zahlen ohne Nichtstandardzahlen zu beweisen. Das könnte z.B. ein neues Axiom oder eine neue Schlussregel sein, die für plausibel für die gewöhnlichen natürlichen Zahlen befunden werden. Mit einer solchen Methode gelingt der Beweis der Goldbachschen Vermutung. Dann wäre es wohl nicht in offensichtlicher Weise möglich, den Beweis in einen der alten Kalküle zu übersetzen. Es wären jedoch neue Kalküle denkbar, die den syntaktischen Beweis erlauben. Wenn einem nichts Besseres einfiele, könnte man z.B. einen bestehenden alten Kalkül um ein zusätzliches Axiom erweitern, dass die Goldbachsche Vermutung stimme und erhielte so einen neuen Kalkül, in dem die Goldbachsche Vermutung beweisbar ist.
Viele Grüße
Tobias
|
Profil
|
Zwerg_Allwissend
Senior
Dabei seit: 02.12.2013
Mitteilungen: 354
| Beitrag No.9, eingetragen 2023-09-20
|
\quoteon(2023-09-18 18:58 - carlox in Beitrag No. 6)
Die meisten "Beweise" in den Vorlesungen sind "semantische Beweise".
In diesen wird auch argumentiert (eben über den Wahrheitsbegriff), d.h. es werden Begriffe, wie also, daraus folgt, usw. benutzt, die mich an ein Regelsystem und einen Herleitungsbegriff erinnern.
\quoteoff
Das sind keine "semantischen" Beweise sondern Argumentationen in natürlicher Sprache. Deshalb, weil dies besser verständlich ist als eine formaler bzw. Kalkülbeweis.
\quoteon(2023-09-18 18:58 - carlox in Beitrag No. 6)
Meine Idee ist, dies durch etwas "Kalkülähnliches" zu formalisieren
(man könnte es einen "semantischen Pseudokalkül" nennen).
Dieser braucht keine Semantik, sondern nur eine formalen Sprache, ein Regelsystem und einen Herleitungsbegriff
\quoteoff
"semantischen Pseudokalkül" das ist so eine Wischi-Waschi Begriff unter dem sich jeder vorstellen kann, was er mag.
Man stelle sich vor Du hast in Deinem "semantischen Pseudokalkül" den Ausdruck "Μαλακίες" hergeleitet. Was weißt Du jetzt? Nix. Denn es gibt ja keine Semantik für die Sprache Deines Kalküls.
|
Profil
|
carlox
Aktiv
Dabei seit: 22.02.2007
Mitteilungen: 1623
| Beitrag No.10, vom Themenstarter, eingetragen 2023-09-21
|
@ZA und tobit09
Danke dass ihr euch an der Diskussion beteiligt.
1)
\quoteon(2023-09-20 22:04 - Zwerg_Allwissend in Beitrag No. 9)
\quoteon(2023-09-18 18:58 - carlox in Beitrag No. 6)
Die meisten "Beweise" in den Vorlesungen sind "semantische Beweise".
In diesen wird auch argumentiert (eben über den Wahrheitsbegriff), d.h. es werden Begriffe, wie also, daraus folgt, usw. benutzt, die mich an ein Regelsystem und einen Herleitungsbegriff erinnern.
\quoteoff
Das sind keine "semantischen" Beweise sondern Argumentationen in natürlicher Sprache. Deshalb, weil dies besser verständlich ist als eine formaler bzw. Kalkülbeweis.
\quoteoff
Willst du behaupten, dass alle semantischen Argumentationen durch einen Kalkül darstellen sind?
Ich vermute nicht.
Welchen Teil der Semantik kann man nicht durch einen Kalkül darstellen?
2)
Zum "semantischen Beweis":
Ein "semantischer Beweis" ist ein "Beweis", in dem die (induktiv definierte) Semantik benutzt wird.
Beispiel 1)
Wenn z.B. in der Vorlesung Analysis eine Behauptung der Form „Aus A folgt B“ bewiesen werden soll, nimmt man in dem "semantischen Beweis" an, dass A für eine beliebige Belegung wahr ist und zeigt dann dass auch B für diese Belegung wahr wird.
Beispiel 2)
Sei $\mathfrak{N}$ das Standardmodell der natürlichen Zahlen und GV die Abkürzung für die Goldbachsche Vermutung.
Vermutung:
$\models_\mathfrak{N} GV$
Um diese Vermutung beweisen zu können, ist ein "semantischer Beweis" nötig.
(also ein Beweis, in dem die Wahrheit vorkommt).
Kann man diese Behauptung mit einem Kalkül beweisen?
Beispiel 3)
Behauptung: Für jede Formel $\phi$ ohne freie Variablen und jeder Struktur $\mathfrak{A}$ gilt:
$\models_\mathfrak{A} \phi$ oder $\models_\mathfrak{A} \neg \phi$
Wie will man das "beweisen", ohne die Semantik (Wahrheit) zu verwenden?
Kann man diese Behauptung mit einem Kalkül beweisen?
3)
Meine Idee ist nun, wie und ob man man diese semantischen Argumentationen formaliseren kann.
mfg
cx
|
Profil
|
tobit09
Aktiv
Dabei seit: 24.04.2018
Mitteilungen: 86
| Beitrag No.11, eingetragen 2023-09-21
|
Hallo carlox!
Beispiel 1) ist ein sehr einfaches Beispiel in einem geeigneten Kalkül des natürlichen Schließens: Gezeigt werden soll $\Gamma\vdash A\rightarrow B$. Dafür genügt es nach einer Schlussregel, $\Gamma,A\vdash B$ zu zeigen. Genau das nutzt man in Analysis und anderen Vorlesungen ständig innerhalb von in natürlicher Sprache formulierten Beweisen, wenn man A voraussetzt und B schlussfolgert, um $A\rightarrow B$ zu zeigen.
Auf Beispiel 2) bin ich in meinem vorherigen Beitrag ausführlich eingegangen.
Zu Beispiel 3): Wenn wir Begriffe und Notationen wie "Struktur" und $\models_\mathfrak{A}\phi$ in naheliegender Weise in einer geeigneten Mengenlehre (z.B. ZFC) formalisieren und die Formalisierung deiner Aussage aus Beispiel 3 mit BSP3 abkürzen, können wir natürlich prinzipiell $ZFC\vdash BSP3$ zeigen.
(Wenn wir diese Formalisierung hingegen nicht möchten und die Aussage aus Beispiel 3) lieber als metamathematische Aussage ansehen wollen, macht die Frage nach einer Beweisbarkeit in einem Kalkül keinen Sinn, solange wir nicht anfangen, über Kalküle zum Beweis metamathematischer Aussagen nachzudenken.)
(Beispiel 3) hat aus meiner Sicht im Übrigen nichts mit alltäglicher Mathematik wie z.B. Analysis zu tun. Alltäglicher wäre da wohl die Frage nach der Beweisbarkeit von $\phi\vee\neg\phi$. Diese ist natürlich in klassischer Logik und damit in entsprechenden syntaktischen Kalkülen mit "Ja" zu beantworten.)
Viele Grüße
Tobias
|
Profil
|
Zwerg_Allwissend
Senior
Dabei seit: 02.12.2013
Mitteilungen: 354
| Beitrag No.12, eingetragen 2023-09-21
|
\quoteon(2023-09-21 10:39 - carlox in Beitrag No. 10)
Behauptung: Für jede Formel $\phi$ ohne freie Variablen und jeder Struktur $\mathfrak{A}$ gilt:
$\models_\mathfrak{A} \phi$ oder $\models_\mathfrak{A} \neg \phi$
Wie will man das "beweisen", ohne die Semantik (Wahrheit) zu verwenden?
Kann man diese Behauptung mit einem Kalkül beweisen?
\quoteoff
Wie ist $\models_\mathfrak{A} \phi$ definiert?
|
Profil
|
carlox
Aktiv
Dabei seit: 22.02.2007
Mitteilungen: 1623
| Beitrag No.13, vom Themenstarter, eingetragen 2023-09-21
|
\quoteon(2023-09-21 16:30 - Zwerg_Allwissend in Beitrag No. 12)
\quoteon(2023-09-21 10:39 - carlox in Beitrag No. 10)
Behauptung: Für jede Formel $\phi$ ohne freie Variablen und jeder Struktur $\mathfrak{A}$ gilt:
$\models_\mathfrak{A} \phi$ oder $\models_\mathfrak{A} \neg \phi$
Wie will man das "beweisen", ohne die Semantik (Wahrheit) zu verwenden?
Kann man diese Behauptung mit einem Kalkül beweisen?
\quoteoff
Wie ist $\models_\mathfrak{A} \phi$ definiert?
\quoteoff
siehe Startbeitrag
mfg
cx
|
Profil
|
carlox
Aktiv
Dabei seit: 22.02.2007
Mitteilungen: 1623
| Beitrag No.14, vom Themenstarter, eingetragen 2023-09-23
|
Da ich einige Zeit zum Überlegen brauchte und Denkfehler bei mir entdeckte, kann ich leider jetzt erst antworten.
1)
\quoteon
\quoteon(2023-09-18 18:49 - carlox in Beitrag No. 5)
Ein "semantischer Beweis" kann etwas beweisen, was man mit einem Beweis (eines Kalküls) nicht beweisen kann (Menge aller wahren arithmetischen Formel - siehe meinen letzten Beitrag).
\quoteoff
Das ist eine sehr optimistische Sichtweise, die ich nicht teile. Glaubst du wirklich, dass man jede wahre arithmetische Formel mit einem (semantischen) Beweis beweisen kann? Ich glaube das nicht. (Natürlich ist diese Frage unpräzise, solange nicht klar ist, was ein semantischer Beweis genau ist.)
\quoteoff
Ich glaube nicht, dass man jede wahre arithmetische Formel mit einem "semantischen Beweis" beweisen kann. Und ihr habt recht: Ich habe noch nicht geklärt, was ein „semantischer Beweis“ ist.
Unter einem „semantischem Beweis“ des Wahrheitswerts einer Formel A verstehe ich die „Ableitbarkeit“ des Wahrheitswerts mit Hilfe der induktiven Definition.
Diese „Ableitbarkeit“ kann formalisiert werden, siehe Skript Ekkart Kindler:
https://drive.google.com/file/d/1Kr_3_T3obZUYygXvJyYDJ9assAaE3VNa/view?usp=sharing
Ein „semantischem Beweis“ ist also ein "Beweis", den man mit (durch) Hilfe der induktiven Definition erbringen kann.
Der "semantische Beweis" ist aber sehr armselig, da er in vielen Fällen nicht hilft (wenn z.B. ein Quantor dabei ist).
Aber besser als gar nichts.
Beispiel 1 (informal):
$\neg 1+1=3$
$1+1=3$ falsch.
Mit der Regel:
$1+1=3$ falsch
------------------
$\neg 1+1=3$ wahr
folgt dann:
$\neg 1+1=3$ wahr
$\neg 1+1=3$ wahr wird also durch einen "semantischen Beweis" (durch Anwendung und Benutzung der induktiven Definition) geliefert.
Beispiel 2 (informal):
Axiome: 3 und 5
Regel:
a,b
---
a+b
Damit (durch Anwendung und Benutzung der induktiven Definition) bekommt man die folgenden Zahlen geliefert:
3,5,8,11,13,16, usw.
Das kann man alles formaler gestalten (siehe Link auf Skript von Kindler)
Vermutlich kann das, was man mit einem „semantischen Beweis“ zeigen kann auch mit einem synatktischen Beweis (eines Kalküls) auch zeigen.
Frage: Ist das richtig?
2)
\quoteon
Die ebenfalls denkbare Möglichkeit 2: Es werden völlig neue Methoden entwickelt, um Aussagen über die gewöhnlichen natürlichen Zahlen ohne Nichtstandardzahlen zu beweisen. Das könnte z.B. ein neues Axiom oder eine neue Schlussregel sein, die für plausibel für die gewöhnlichen natürlichen Zahlen befunden werden. Mit einer solchen Methode gelingt der Beweis der Goldbachschen Vermutung. Dann wäre es wohl nicht in offensichtlicher Weise möglich, den Beweis in einen der alten Kalküle zu übersetzen. Es wären jedoch neue Kalküle denkbar, die den syntaktischen Beweis erlauben. Wenn einem nichts Besseres einfiele, könnte man z.B. einen bestehenden alten Kalkül um ein zusätzliches Axiom erweitern, dass die Goldbachsche Vermutung stimme und erhielte so einen neuen Kalkül, in dem die Goldbachsche Vermutung beweisbar ist.
\quoteoff
Mit dem neuen Axiom hätte man zwar die Goldbachschen Vermutung bewiesen.
Allerdings gibt es in dem neuen Axiomensystem auch wieder (wegen des Gödelschen Unvollständigkeitssatz) nicht beweisbare wahre Aussagen.
3) Evtl. off topic
In dem Skript von Kindler wird bei den Regeln vorausgesetzt, dass es in einer Regel nur endlich viele Voraussetzungen geben darf.
Allerdings werden bei der Definition der Semantik des Allquantors in der Prädikatenlogik unendlich viele Voraussetzungen angegeben.
Was stimmt da nicht?
4)
Die Definition einer Mengen (z.B: Menge aller wahren arithmetischen Aussagen, Menge aller stetigen Funktionen, Menge aller differenzierbaren Funktionen, Menge aller integrierbaren Funktionen, usw.) bedeutet nicht, dass man auch beweisen kann ob man zu einem beliebigen vorgegebenen x feststellen (beweisen) kann, ob es auch Element einer vorgegeben Menge ist.
In der Analysis bzw. anderen "üblichen" Vorlesungen hat man (zumindest) in diesen Vorlesungen „Glück“:
Man kann dann von allen dort vorgestellten Funktionen (bzw. Objekten) zeigen, ob sie stetig, differenzierbar, integrierbar, usw. ist oder nicht.
Frage:
Gibt es auch Funktionen, von denen man nicht entscheiden kann, es also keinen Beweis gibt, ob diese stetig/nicht stetig bzw. differenzierbar/nicht differenzierbar bzw. integrierbar/nicht integrierbar , usw. sind oder wird so etwas in einer "üblichen" Vorlesung nicht behandelt (unterschlagen)?
mfg
cx
|
Profil
|
tobit09
Aktiv
Dabei seit: 24.04.2018
Mitteilungen: 86
| Beitrag No.15, eingetragen 2023-09-24
|
Hallo carlox,
zu 1):
Beim groben Überfliegen des von dir verlinkten Skripts habe ich nicht den Eindruck, dass ein "semantischer" Kalkül (was auch immer das genau heißen soll) beschrieben wird.
Solange ein Kalkül für die Prädikatenlogik der ersten Stufe nur semantisch korrekte Schlussfolgerungen herleiten kann, können sämtliche im Kalkül herleitbare Schlussfolgerungen auch in jedem vollständigen Kalkül der Prädikatenlogik der ersten Stufe (z.B. ein geeigneter Kalkül des natürlichen Schließens) hergeleitet werden.
Zu 2): Genau.
Zu 3): In der induktiven Definition der Semantik des Allquantors innerhalb der Prädikatenlogik der ersten Stufe tauchen nirgendwo unendlich viele Voraussetzungen auf.
Zu 4):
Betrachte irgendeine Aussage A, die im betrachteten Kontext weder bewiesen noch widerlegt werden kann, z.B. die Kontinuumshypothese im Rahmen von ZFC.
Dann ist die Funktion
$f\colon \mathbb{R}\to\mathbb{R},\quad x\mapsto\begin{cases}1&\text{ falls }x=0\wedge A\\0&\text{sonst}\end{cases}$
genau dann stetig, wenn A falsch ist.
Somit kann die Stetigkeit von f weder bewiesen noch widerlegt werden.
Viele Grüße
Tobias
|
Profil
|
carlox
Aktiv
Dabei seit: 22.02.2007
Mitteilungen: 1623
| Beitrag No.16, vom Themenstarter, eingetragen 2023-09-25
|
Hallo tobit09,
\quoteon(2023-09-24 12:25 - tobit09 in Beitrag No. 15)
Zu 3): In der induktiven Definition der Semantik des Allquantors innerhalb der Prädikatenlogik der ersten Stufe tauchen nirgendwo unendlich viele Voraussetzungen auf.
\quoteoff
Da bin ich anderer Meinung:
Definitionen:
$W_\mathfrak{A}(\phi,h)$ ist der Warheitswert einer Formel $\phi$ bei der Belegung h in der Struktur $\mathfrak{A}$
$h_x^\kappa(z)=\begin{cases} h(z), & z\neq x \\ \kappa, & z=x \end{cases}$.
T: Trägermenge
$W_\mathfrak{A}(\forall x \phi,h)=W$ gdw
$W_\mathfrak{A}(\phi,h_x^\kappa)=W$ für alle $\kappa \in$T
oder als Regel formuliert:
$\frac{\{(W_\mathfrak{A}(\phi,h_x^\kappa),W) \; \vert \; \kappa \in T \}} {(W_\mathfrak{A}(\forall x \phi,h),W)} $
Man sieht, wenn T unendlich groß ist, besteht die Menge
$\{(W_\mathfrak{A}(\phi,h_x^\kappa),W) \; \vert \; \kappa \in T \}$
aus unendlich vielen Elementen (Voraussetzungen)
mfg
cx
|
Profil
|
tobit09
Aktiv
Dabei seit: 24.04.2018
Mitteilungen: 86
| Beitrag No.17, eingetragen 2023-09-25
|
Hallo carlox!
\quoteon(2023-09-25 08:38 - carlox in Beitrag No. 16)
$W_\mathfrak{A}(\phi,h_x^\kappa)=W$ für alle $\kappa \in$T
\quoteoff
Genau diese Bedingung ist für mich eine Voraussetzung und nicht unendlich viele Voraussetzungen; auch wenn ich deine Idee, diese eine Bedingung in unendlich viele separate Voraussetzungen aufzuspalten, meine nachvollziehen zu können. Im Hinblick auf praktisch anwendbare Kalküle (deren Herleitungen ja von endlicher Länge sein sollten) erscheint mir eine solche Aufspaltung aber nicht sinnvoll.
\quoteon(2023-09-25 08:38 - carlox in Beitrag No. 16)
oder als Regel formuliert:
$\frac{\{(W_\mathfrak{A}(\phi,h_x^\kappa),W) \; \vert \; \kappa \in T \}} {(W_\mathfrak{A}(\forall x \phi,h),W)} $
Man sieht, wenn T unendlich groß ist, besteht die Menge
$\{(W_\mathfrak{A}(\phi,h_x^\kappa),W) \; \vert \; \kappa \in T \}$
aus unendlich vielen Elementen (Voraussetzungen)
\quoteoff
Da meinst du offenbar etwas Anderes als du schreibst: Die Menge $\{(W_\mathfrak{A}(\phi,h_x^\kappa),W) \; \vert \; \kappa \in T \}$ ist eine Teilmenge von $\{(W,W),(F,W)\}$ und somit höchstens zweielementig und damit nicht unendlich.
Viele Grüße
Tobias
|
Profil
|
carlox
Aktiv
Dabei seit: 22.02.2007
Mitteilungen: 1623
| Beitrag No.18, vom Themenstarter, eingetragen 2023-09-25
|
\quoteon(2023-09-25 15:41 - tobit09 in Beitrag No. 17)
\quoteon(2023-09-25 08:38 - carlox in Beitrag No. 16)
$W_\mathfrak{A}(\phi,h_x^\kappa)=W$ für alle $\kappa \in$T
\quoteoff
Genau diese Bedingung ist für mich eine Voraussetzung und nicht unendlich viele Voraussetzungen; auch wenn ich deine Idee, diese eine Bedingung in unendlich viele separate Voraussetzungen aufzuspalten, meine nachvollziehen zu können. Im Hinblick auf praktisch anwendbare Kalküle (deren Herleitungen ja von endlicher Länge sein sollten) erscheint mir eine solche Aufspaltung aber nicht sinnvoll.
\quoteoff
Ich vermute leider, dass ich eine solche Aufspaltung, d.h. unendlich viele Voraussetzungen brauche, denn wenn man nur endlich viele Vorraussetzungen in den Regeln zuläßt, ist - unter bestimmten Voraussetzungen – (vermutlich X ist rekursiv aufzählbar und noch irgendwas mir Unbekanntes, siehe meine Frage unten), die induktiv definierte Menge $I_R$ auch rekursiv aufzählbar.
Das könnte dann bedeuten, dass z.B. die induktiv definierte Menge der wahren arithmetischen Ausdrücke rekursiv aufzählbar wäre. Das ist aber falsch!
\quoteon
Da meinst du offenbar etwas Anderes als du schreibst: Die Menge $\{(W_\mathfrak{A}(\phi,h_x^\kappa),W) \; \vert \; \kappa \in T \}$ ist eine Teilmenge von $\{(W,W),(F,W)\}$ und somit höchstens zweielementig und damit nicht unendlich.
\quoteoff
Du hast Recht. Vielen Dank für deine kritische Durchsicht!
Ich korrigiere mich (und habe - wenn T unendlich groß ist - uendlich viele Vorausetzungen) in der Regel:
$\frac{\{(\phi,\mathfrak{A},h_x^\kappa,W) \; \vert \; \kappa \in T \}} {(\forall x \phi,\mathfrak{A},h,W)} $
wobei W den Wahrheitswert wahr bedeutet.
Frage:
Unter welchen Bedingungen ist eine induktiv definierte Menge (nach der Definition von Kindler) rekursiv aufzählbar?
Vermutung:
Wenn die Regeln auf entscheidbare Regeln mit endlich vielen Voraussetzungen einschränkt wird, dann ist die induktiv definierte Menge rekursiv aufzählbar.
Oder soll das in einen neuen Thread?
mfg
cx
|
Profil
|
carlox
Aktiv
Dabei seit: 22.02.2007
Mitteilungen: 1623
| Beitrag No.19, vom Themenstarter, eingetragen 2023-09-26
|
Behauptung:
Wenn:
1) X ist rekursiv aufzählbar und
2) Jede Regel hat nur endlich viele Voraussetzungen und
3) Jede Regel ist entscheidbar.
Dann:
ist die induktiv definierte Menge $I_R$ rekursiv aufzählbar.
Bem (siehe Skript von Kindler)
$I_R=\bigcup_{i=0}^\infty {Q}_{i}$
Beweisskizze:
Definiere für jedes n>0 und die Regelmenge R:
$Q_0=\{x \in X \; \vert \; (\emptyset,x) \in R\}=\{q_1, q_2, q_3, ... \}$
$\bar{Q}_{0,n}=\{q_1, q_2, q_3, ... q_n\}$
$\bar{Q}_{1,n}=\{x \in X \; \vert \; (Y,x) \in R \land Y \subset \bar{Q}_{0,n}\}$
$\bar{Q}_{2,n}=\{x \in X \; \vert \; (Y,x) \in R \land Y \subset \bar{Q}_{1,n}\}$
...
Unterbehauptung 1:
$Q_0$ ist rekursiv berechenbar.
Begründung:
Da X rekursiv berechenbar ist, kann man X als Liste $X=x_1, x_2, x_3, ...$ darstellen und durchlaufen. Entscheide dabei ob für jedes $x_i \in X$ dann $(\emptyset,x_i)$ eine Regel ist. Wenn ja, füge x der Menge $Q_0$ hinzu, die am Anfang auf die leere Menge gesetzt wird.
Unterbehauptung 2:
$\bar{Q}_{0,n}$ ist für jedes n>0 rekursiv berechenbar.
Begründung: trivial
Unterbehauptung 3:
$\bar{Q}_{1,n}$ ist für jedes n>0 rekursiv berechenbar.
Begründung:
Bilde die Potenzmenge $P(\bar{Q}_{0,n})$ von $\bar{Q}_{0,n}$.
Bilde das cartesische Produkt $P(\bar{Q}_{0,n}) \times X$
Durchlaufe dieses cartesische Produkt nach dem Cantorschen Diagonalverfahren und entscheide für jedes (T,x) ob es eine Regel ist.
Wenn ja, füge x der Menge $\bar{Q}_{1,n}$ hinzu, die am Anfang auf die leere Menge gesetzt wird.
Jedes Element von $\bar{Q}_{1,n}$ kann also konstruiert werden.
Unterbehauptung 4:
$\bar{Q}_{2,n}$ ist für jedes n>0 rekursiv berechenbar.
Jedes Element von $\bar{Q}_{2,n}$ kann also konstruiert werden.
usw.
Unterbehauptung 5:
Es gilt:
$I_R=\bigcup_{i=1}^\infty \bigcup_{j=1}^\infty {\bar{Q}_{i,j}}$
ohne Begründung
Unterbehauptung 6:
$I_R$ ist rekursiv aufzählbar.
Begründung:
Schreibe
$\bar{Q}_{0,1}$ , $\bar{Q}_{0,2}$, $\bar{Q}_{0,3}$, ...
$\bar{Q}_{1,0}$, $\bar{Q}_{1,1}$, $\bar{Q}_{1,2}$, ...
$\bar{Q}_{2,0}$, $\bar{Q}_{2,1}$, $\bar{Q}_{2,2}$, ...
...
Vereinige alle diese einzelnen Elemente (Mengen) dieser "Matrix" nach dem Cantorschen Diagonalverfahren.
mfg cx
|
Profil
|
| carlox hat die Antworten auf ihre/seine Frage gesehen. | | carlox wird per Mail über neue Antworten informiert. |
|
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2023 by Matroids Matheplanet
This web site was originally made with PHP-Nuke, a former web portal system written in PHP that seems no longer to be maintained nor supported. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die
Nutzungsbedingungen,
die Distanzierung,
die Datenschutzerklärung und das Impressum.
[Seitenanfang]
|
Home / Seite ohne Frame
Wie unterstütze ich den Matheplaneten mit Geld?
