Implikationspfeile, Drehkreuze etc

1. Ja.
2. Ja. Beachten Sie, dass, wenn der Vollständigkeitssatz gilt (dies ist der Fall in der Aussagenlogik oder Logik erster Ordnung), dann$\vdash$Und$\models$sind im Wesentlichen austauschbar, außer dass$\mathfrak{M} \vdash a$Und$\mathfrak{M} \vdash T$ergibt keinen Sinn.
3. Ja, genauer gesagt$a \equiv b$normalerweise bedeutet$\models (a \to b) \land (b \to a)$(was das gleiche ist wie$\vdash (a \to b) \land (b \to a)$wenn der Vollständigkeitssatz gilt). Manchmal findet man auch die Notationen$a \equiv_T b$(was bedeutet$T \models (a \to b) \land (b \to a)$), Und$a \dashv\vdash b$(was bedeutet$\vdash (a \to b) \land (b \to a)$, Und$a \dashv\vdash_T b$(was bedeutet$T \vdash (a \to b) \land (b \to a)$).
4. Oft$a \implies b$steht für$T \vdash a \to b$wo die Theorie$T$geht aus dem Zusammenhang hervor (und meist$T$ist eine Theorie in einer Logik, in der der Vollständigkeitssatz gilt). Aber diese Notation ist sehr informell (obwohl nützlich und gebräuchlich) und kann andere Bedeutungen haben. Also sei vorsichtig. Manchmal kann es zum Beispiel bedeuten, dass „seit$a$gilt (in einer Theorie$T$) Und$b$Folgt aus$a$, Dann$b$gilt" (d.h. auch ein modus ponens wird implizit belassen); formal steht es in diesem Fall für$T \vdash a \land (a \to b)$(und daher$T \vdash b$).

Ich möchte die obige Antwort mit ein paar Kommentaren ergänzen und anmerken, dass Q2 weiterer Diskussion bedarf.

1. Ja, dies ist eine gute Liste von "Standard"-Notationen, aber aufgrund von Äquivalenztheoremen (insbesondere der Korrektheits- und Vollständigkeitstheoreme) weichen einige Lehrbücher von diesen Definitionen ab. Zum Beispiel verwenden Boolos und Jeffrey$\vdash$bei der Einführung von "semantischer Inferenz" und nach dem Vollständigkeitssatz wiederverwenden, um auch Abziehbarkeit zu bedeuten. Auch "semantische Inferenz" wird manchmal als "logische Inferenz" bezeichnet. Diese Fragen werden wichtig, wenn man von der elementaren Logik zu der endlosen Vielfalt anderer Logiken übergeht: Modallogik, 3-wertige Logik usw., in denen der Vollständigkeitssatz möglicherweise nicht gilt.

2. Die Aussage, dass$a \vdash b$impliziert$\vdash a \rightarrow b$ist eigentlich der Abzugssatz . Wieder in erster Linie ein aussagenlogischer und logischer (Meta-)Satz erster Ordnung, aber er kann auch für andere Logiken bewiesen werden, aber auch hier muss die gegebene Logik dieses Ergebnis begründen. Ich sehe, dass eine Form der Quantenlogik als Beispiel angeführt wird, bei der dieses Meta-Theorem versagt.

3. Als andere Antwort.

4. In einem formalen Logiklehrbuch$\implies$wird wahrscheinlich früh eingeführt, wahrscheinlich im Kapitel über die Aussagenlogik. Allerdings in einer mathematischen Vorlesung oder Notizen$\implies$wird verwendet, um die Schritte in dem präsentierten mathematischen Beweis darzustellen. ZB in einer Algebra-Klasse könnten wir einige Schritte haben wie:$x > 1 \implies x^2 > 1$wobei der Bereich der Variablen implizit, aber durch die Algebra definiert ist, und so die vollständige logische Formulierung der algebraischen Beweise (in Bezug auf Modelle, Sprachen, Inferenzregeln usw.) implizit gelassen wird.