Hilbert-Kalkül

11.11.2024, 02:19

Pippen

Hilbert-Kalkül

Fange bei Deiser gerade mit dem Hilbert-Kalkül an. Sind meine Notizen bis hierher richtig? Hinweis: Das Bild anklicken, dann wird’s größer. Besonders unsicher bin ich mir beim letzten Satz. Den habe ich blind von Deiser abgeschrieben, aber das sollte eigentlich kein Axiom sein, weil es kein entsprechendes Axiomschema dazu gibt, was passt.

[attach]57985[/attach]

11.11.2024, 09:30

Elvis

Auf diesen Beitrag antworten »

Deine Bemerkungen am Ende interpretieren den Zusammenhang zwischen Formeln und Axiomen nicht richtig.
Aus einer Formel wird durch Einsetzen in ein Axiomenschema kein Axiom. Vielmehr entsteht durch korrektes Einsetzen von Formeln in ein Axiomenschema aus dem Axiomenschema ein Axiom.
(Offensichtlich muss in einem formalen System vor dem Einsetzen von Formeln in ein Axiomenschema definiert werden, was Formeln sind. Das macht Oliver Deiser u.a. im vorangegangenen Kapitel "Die Sprache der Mengenlehre". Die Sprache L ist nicht mit dem logischen System PL1 identisch !)

12.11.2024, 00:33

Pippen

Auf diesen Beitrag antworten »

Zitat:

Original von Elvis
Deine Bemerkungen am Ende interpretieren den Zusammenhang zwischen Formeln und Axiomen nicht richtig.
Aus einer Formel wird durch Einsetzen in ein Axiomenschema kein Axiom. Vielmehr entsteht durch korrektes Einsetzen von Formeln in ein Axiomenschema aus dem Axiomenschema ein Axiom.
(Offensichtlich muss in einem formalen System vor dem Einsetzen von Formeln in ein Axiomenschema definiert werden, was Formeln sind. Das macht Oliver Deiser u.a. im vorangegangenen Kapitel "Die Sprache der Mengenlehre". Die Sprache L ist nicht mit dem logischen System PL1 identisch !)

WENN eine Formel in ein Axiomschema einsetzbar ist, DANN ist sie auch Axiom. Ich denke wir meinen dasselbe, nur mit anderen Worten.

Du hast recht, dass wohl L nicht mit PL1 identisch ist. Das muss ich ändern. Denn L kennt das Elementzeichen als Standardprädikat, was PL1 nicht kennt. Das ist der Unterschied, richtig?

Kannst du mit dem letzten Satz was anfangen? Ist wirklich jede All-Formel ein Axiom, wo die Formel in ein Schema passt? Ist das eine Anwendung des ersten Axiomachemas für Quantoren? Wie liest man das? Nicht jede Formel Phi ist doch automatisch eine Allformel?!? Und in dem Axiomschema steht nirgends, dass die Formel Phi selbst ein Axiom sein muss, nur dann würde es Sinn machen.

12.11.2024, 08:12

Elvis

Auf diesen Beitrag antworten »

1. Du irrst. Die Formel $\begin{eqnarray*} x=\emptyset \end{eqnarray*}$ kann man in jedes Axiom einsetzen, aber weder diese Formel noch $\begin{eqnarray*} \forall x\,x=\emptyset \end{eqnarray*}$ sind Axiome der Mengenlehre.
2. Die formale Sprache L ist etwas ganz anderes als das Axiomensystem PL1. PL1 benutzt L, um die Theorie Mengenlehre zu formulieren.
3. Man kann nicht nur Axiome sondern jedes Theorem als Formel in jedes Axiom einsetzen. Siehe Beweistheorie.

12.11.2024, 09:06

Finn_

Auf diesen Beitrag antworten »

Mir scheint, Pippen meint so etwas wie Jede Formel, die mit einem Axiomenschema bezüglich der Schemavariablen unifizierbar ist, ist ein Axiom. Ggf. vorhandene Nebenbedingungen bezüglich freier Variablen müssen dabei natürlich beachtet werden. Speziell handelt es sich hier um einen Musterabgleich, wobei das Schema die Rolle des Musters übernimmt.

Bspw. lässt sich die Formel $\begin{eqnarray*} x=y\to (x=z\to x=y) \end{eqnarray*}$ mit $\begin{eqnarray*} \varphi\to(\psi\to\varphi) \end{eqnarray*}$ abgleichen, mit dem Unifizierer $\begin{eqnarray*} [\varphi:=(x=y),\psi:=(x=z)]. \end{eqnarray*}$

12.11.2024, 09:21

Elvis

Auf diesen Beitrag antworten »

Vermutlich meint Pippen so etwas, aber er sagt, dass in deinem Beispiel die Formel $\begin{eqnarray*} x=y \end{eqnarray*}$ ein Axiom sei, weil sie in ein Axiomenschema eingesetzt werden kann. Und dann ist auch noch $\begin{eqnarray*} \forall x\forall y \,x=y \end{eqnarray*}$ ein Axiom. Diese Mengenlehre wäre etwas langweilig. Richtig gruselig wird es dann bei den "Axiomen" $\begin{eqnarray*} \forall x\, x=y \end{eqnarray*}$ und $\begin{eqnarray*} \forall x\forall x\,x=y \end{eqnarray*}$ .

12.11.2024, 22:50

Pippen

Auf diesen Beitrag antworten »

Zitat:

Original von Finn_
Mir scheint, Pippen meint so etwas wie Jede Formel, die mit einem Axiomenschema bezüglich der Schemavariablen unifizierbar ist, ist ein Axiom. Ggf. vorhandene Nebenbedingungen bezüglich freier Variablen müssen dabei natürlich beachtet werden. Speziell handelt es sich hier um einen Musterabgleich, wobei das Schema die Rolle des Musters übernimmt.

Bspw. lässt sich die Formel $\begin{eqnarray*} x=y\to (x=z\to x=y) \end{eqnarray*}$ mit $\begin{eqnarray*} \varphi\to(\psi\to\varphi) \end{eqnarray*}$ abgleichen, mit dem Unifizierer $\begin{eqnarray*} [\varphi:=(x=y),\psi:=(x=z)]. \end{eqnarray*}$

Genau das meine ich. Jede Formel, die man in eines der Axiomschemata einsetzen kann, ist ein Axiom. Ich gebe ja in meiner Notiz ein Beispiel, so dass klar ist, was ich wie meine.

Was mich umtreibt ist mein letzter Satz auf meinem Notizzettel. Stimmt der so und ergibt sich das aus dem ersten Axiomschema zu Quantoren? Denn dann könnte ich ihn löschen, er wäre überflüssig, weil er bereits aus dem vorhergehenden Satz folgte, dass jede L (= PL 1 mit dem Elementzeichen) Formel, die in ein Schema einsetzbar ist, ein Axiom ist. (das Axiom x = x ist eine Ausnahme, aber es ist klar, was es bedeutet: diesselben Elemente)

13.11.2024, 07:20

Elvis

Auf diesen Beitrag antworten »

L ist nicht PL1, denn eine Sprache ist keine Logik und eine Logik ist keine Sprache.
Eine Sprache braucht ein Alphabet, das sind Zeichen aus denen Worte gebildet werden. Eine Grammatik legt fest, welche Worte Formeln sind.
Von Formeln kommt man zu Aussagen, indem eine Interpretation gewissen Formeln Wahrheitswerte zuordnet und sie dadurch zu Aussagen macht.
Eine Logik legt mittels Junktoren fest, wie sich die Wahrheit von Aussagen auf zusammengesetzte Aussagen überträgt und welche logischen Ableitungen zulässig sind.
Eine Theorie wie z.B. die Mengenlehre braucht eine Sprache und eine Logik, hier z.B. L und PL1.
Die Formel x=x ist kein Axiom, Formeln sind i.a. keine Axiome. $\begin{eqnarray*} \forall x\,x=x \end{eqnarray*}$ ist ein Axiom der Gleichheit und wird in jeder Logik benutzt, die das Symbol "=" kennt. Schon Euklid hat gesagt: "Jedes Ding ist sich selbst gleich", und genau das bedeutet dieses Axiom. Diese logische Gleichheit von Dingen ist etwas völlig anderes als die extensionale Gleichheit von Mengen, die in einem Theorieaxiom der Mengenlehre formuliert wird.
Ich will nicht noch einmal alles erklären, das wird mir zu anstrengend. Wenn Finn_ mehr Nerven hat als ich darf er gerne übernehmen.

13.11.2024, 10:18

Finn_

Auf diesen Beitrag antworten »

In dem von Deiser beschriebenen System kommen anscheinend auch Formeln mit freien Variablen als Axiome vor. Zum Kontext, siehe den zurzeit aktiven Faden Hilbert-Kalkül und seine Axiome auf dem MP.

Die Schlussregel $\begin{eqnarray*} \frac{\vdash\varphi}{\vdash\forall x\,\varphi}, \end{eqnarray*}$ genauer $\begin{eqnarray*} \frac{\varphi\;\text{ist ein Axiom}}{\forall x\,\varphi\;\text{ist ein Axiom}}, \end{eqnarray*}$ lässt sich nicht vermittels des Modus ponens aus dem Schema $\begin{eqnarray*} \varphi\to\forall x\,\varphi \end{eqnarray*}$ ableiten. Weil das Schema die Nebenbedingung besitzt, dass $\begin{eqnarray*} x \end{eqnarray*}$ nicht frei in $\begin{eqnarray*} \varphi \end{eqnarray*}$ vorkommen darf, würde sich diese Einschränkung auf die Schlussregel vererben, die damit nutzlos wird.

13.11.2024, 23:10

Pippen

Auf diesen Beitrag antworten »

@Finn: Richtig. Ich poste mal meinen Beitrag aus dem Matheplandt hier rein, vllt. kannst du dazu was schreiben:

Deiser sagt wörtlich, dass $\begin{eqnarray*} \varphi \end{eqnarray*}$ (= eine L-Formel, also eine PL1+ $\begin{eqnarray*} \in \end{eqnarray*}$ -Formel) ein Axiom des Hilbert-Kalküls sei, wenn $\begin{eqnarray*} \varphi \end{eqnarray*}$ eine Generalisierung eines aussagelogischen Axioms, eines Identitätsaxioms oder Quantorenaxioms sei. Ich interpretiere es hoffentlich richtig, wenn das (umgangssprachlich) meint, dass $\begin{eqnarray*} \varphi \end{eqnarray*}$ ein Axiom ist, wenn es in eines der Axiomschemata einsetzbar ist.

Deiser fährt nun fort: „Ist ALSO $\begin{eqnarray*} \varphi \end{eqnarray*}$ ein logisches Axiom, so ist $\begin{eqnarray*} \forall x \varphi \end{eqnarray*}$ ein logisches Axiom für alle x. Das ist also offenbar doch ein Theorem, denn es folgt aus dem Hilbert-Kalkül. Wie kommt Deiser darauf? In seiner Darstellung des Hilbert-Kalküls folgt das nirgends und ein entsprechendes Axiomschema gibt es nicht. Wie kommt man denn nach Deiser von x = x zu $\begin{eqnarray*} \forall \end{eqnarray*}$ x: x = x? Das scheint mir unmöglich nur mit mp als Schlussregel und den drei Axiomschemata.

15.11.2024, 09:57

Finn_

Auf diesen Beitrag antworten »

Zitat:

Original von Pippen
Ich interpretiere es hoffentlich richtig, wenn das (umgangssprachlich) meint, dass $\begin{eqnarray*} \varphi \end{eqnarray*}$ ein Axiom ist, wenn es in eines der Axiomschemata einsetzbar ist.

Statt in eines der Schemata einsetzbar würde ich sagen von der Form eines der Schemata.

Zitat:

Original von Pippen
In seiner Darstellung des Hilbert-Kalküls folgt das nirgends und ein entsprechendes Axiomschema gibt es nicht. Wie kommt man denn nach Deiser von x = x zu $\begin{eqnarray*} \forall \end{eqnarray*}$ x: x = x?

Es ist schlicht Teil der induktiven Definition, was ein Axiom sei bzw. wie die Menge der Axiome beschaffen sei. So wie: 0 sei eine natürliche Zahl, und wenn n eine ist, dann auch succ(n). Hier: $\begin{eqnarray*} x = x \end{eqnarray*}$ sei ein Axiom usw. usf., und wenn $\begin{eqnarray*} \varphi \end{eqnarray*}$ eines ist, dann sei auch $\begin{eqnarray*} \forall x\,\varphi \end{eqnarray*}$ und usw. ein Axiom. Genau genommen ist $\begin{eqnarray*} x \end{eqnarray*}$ dabei natürlich eine metasprachliche Variable, die für jede beliebige Individuenvariable steht.

Die nächste induktive Definition betrifft die der Theoreme. Jedes Axiom sei ein Theorem. Und wenn man ein oder zwei Theoreme als Prämissen hat, dann sei auch jede Formel ein Theorem, die sich mit den Schlussregeln als Konklusion aus den Prämissen erhalten lässt.

Was eine Formel ist, wurde ebenfalls induktiv definiert. Jede Primformel sei eine Formel. Und wenn man Formeln $\begin{eqnarray*} \varphi,\psi \end{eqnarray*}$ hat, dann seien auch $\begin{eqnarray*} \lnot\varphi \end{eqnarray*}$ und $\begin{eqnarray*} \varphi\land\psi \end{eqnarray*}$ usw. Formeln.

Man hat immer Basisfälle (die Null, die Primformeln, die Axiome) und Funktionen zur schrittweisen Erweiterung (die Nachfolgerfunktion, die Produktionsregeln, die Schlussregeln).

Um zu verstehen, warum dieser Kalkül die Generalisierung von Axiomen beinhaltet, musst du dir Theoreme überlegen, die ohne sie nicht ableitbar wären. Am besten solche, wo die Generalisierung nicht ganz am Ende der Deduktion stattfindet.

16.11.2024, 11:49

Elvis

Auf diesen Beitrag antworten »

Meines Erachtens kommt man durch die Generalisierungsregel der Prädikatenlogik nicht von $\begin{eqnarray*} x=x \end{eqnarray*}$ auf $\begin{eqnarray*} \forall x\,x=x \end{eqnarray*}$ , weil in der Ausgangsformel die Objektvariable frei ist, was für die Generalisierungsregel ausgeschlossen ist.
Über die Gleichheit sagt Euklid "JEDES Ding ist sich selbst gleich", also formulieren wir das erste Identitätsaxiom $\begin{eqnarray*} (\forall x)\,x=x \end{eqnarray*}$ .
Über die Gleichheit sagt Leibniz "Zwei Dinge sind genau dann gleich, wenn man das eine durch das andere in jeder Aussage ersetzen kann - unter Erhaltung der Wahrheit", also formulieren wir für JEDES von Parametern $\begin{eqnarray*} Z=(z_1,...,z_n) \end{eqnarray*}$ abhängige Prädikat $\begin{eqnarray*} \varphi_Z \end{eqnarray*}$ das zweite Identitätsaxiom (genauer Axiomenschema) $\begin{eqnarray*} (\forall x,y,Z,\varphi_Z)\,x=y\rightarrow \varphi_Z(x)=\varphi_Z(y) \end{eqnarray*}$ .

16.11.2024, 14:51

Finn_

Auf diesen Beitrag antworten »

Die allgemeine Generalisierungsregel

$\begin{eqnarray*} \dfrac{\Sigma\vdash\varphi}{\Sigma\vdash\forall x\,\varphi}\,(x\notin\mathrm{FV}(\Sigma)) \end{eqnarray*}$

wird später gezeigt. Bezüglich $\begin{eqnarray*} \varphi:=(x=x) \end{eqnarray*}$ darf natürlich nicht $\begin{eqnarray*} \Sigma=\{\varphi\} \end{eqnarray*}$ sein, sondern wir haben $\begin{eqnarray*} \Sigma=\emptyset, \end{eqnarray*}$ insofern $\begin{eqnarray*} x=x \end{eqnarray*}$ voraussetzungslos gilt.

19.11.2024, 08:03

Elvis

Auf diesen Beitrag antworten »

Ich glaube, jetzt habe ich das entscheidende Missverständnis erkannt und kann auch eine Antwort zur letzten Frage im Eingangspost geben.
Ein Hilbertkalkül benutzt eine formalisierte mathematische Theorie L und die formalisierte Prädikatenlogik PL1. Axiome bzw. Axiomenschemata sind also alle Axiome bzw. Axiomenschemata von L und alle Axiome bzw. Axiomenschemata von PL1. Als logische Schlussregel wird ausschließlich der Modus Ponens benutzt. Theoreme werden durch korrektes Einsetzen von bereits bewiesenen Aussagen, also Axiomen und Theoremen in Axiomenschemata und MP abgeleitet.
Es gibt nicht den Hilbertkalkül sondern zu jeder formalisierten Theorie L einen Hilbertkalkül, und sein Sinn und Zweck ist die Untersuchung von mathematischen Beweisen. Theoretisch kann man mit einem Hilbertkalkül auch Beweise führen, aber das ist wahnsinnig kompliziert, und das macht auch niemand zum Zweck der Beweisführung. Hilbert wurde häufig missverstanden, er wollte nicht die Mathematik formalisieren sondern mathematische Theorien mit Hilfe der Beweistheorie untersuchen. Im richtigen Leben war auch Hilbert wie jeder andere Mathematiker einer, der ganz normale umgangssprachliche Beweise geführt hat, allerdings war er genial und hat mehr und wichtigere Beweise geführt als fast alle anderen.

21.11.2024, 11:01

Elvis

Auf diesen Beitrag antworten »

http://podnieks.id.lv/ "What is Mathematics" bietet eine gute Ergänzung zu Oliver Deiser "Einführung in die Mengenlehre". Aus einem Buch kann man nicht alles lernen, schon gar nicht, wenn es in manchen Teilen etwas oberflächlich wird.

Neue Frage »

Antworten »

Hilbert-Kalkül

Verwandte Themen