Flechas de implicación, torniquetes, etc.

1. Sí.
2. Sí. Tenga en cuenta que si se cumple el teorema de completitud (este es el caso en la lógica proposicional o de primer orden), entonces$\vdash$y$\models$son esencialmente intercambiables, excepto que$\mathfrak{M} \vdash a$y$\mathfrak{M} \vdash T$no tiene sentido.
3. si, mas precisamente$a \equiv b$por lo general significa$\models (a \to b) \land (b \to a)$(que es lo mismo que$\vdash (a \to b) \land (b \to a)$si se cumple el teorema de completitud). A veces también puedes encontrar las notaciones$a \equiv_T b$(lo que significa$T \models (a \to b) \land (b \to a)$), y$a \dashv\vdash b$(lo que significa$\vdash (a \to b) \land (b \to a)$, y$a \dashv\vdash_T b$(lo que significa$T \vdash (a \to b) \land (b \to a)$).
4. A menudo$a \implies b$representa$T \vdash a \to b$donde la teoria$T$queda claro por el contexto (y por lo general$T$es una teoría en una lógica donde se cumple el teorema de completitud). Pero esta notación es muy informal (aunque útil y común), y puede tener otros significados. Así que ten cuidado. Por ejemplo, a veces puede significar que "Desde que$a$sostiene (en una teoría$T$) y$b$sigue desde$a$, entonces$b$sostiene" (es decir, también se deja implícito un modus ponens ); formalmente, en este caso significa$T \vdash a \land (a \to b)$(y por lo tanto$T \vdash b$).

Me gustaría complementar la respuesta anterior con un par de comentarios y señalar que el segundo trimestre necesita más discusión.

1. Sí, esta es una buena lista de notaciones "estándar", pero debido a los teoremas de equivalencia (especialmente los teoremas de solidez y completitud) algunos libros de texto se desviarán de estas definiciones. Por ejemplo, Boolos y Jeffrey usan$\vdash$al introducir "inferencia semántica" y después del teorema de completitud, reutilícelo para significar también deducibilidad. También la "inferencia semántica" a veces se denomina "inferencia lógica". Estos temas se vuelven importantes a medida que uno pasa de la lógica elemental a la infinita variedad de otras lógicas: lógica modal, lógica de 3 valores, etc., en las que el teorema de completitud podría no cumplirse.

2. La declaración de que$a \vdash b$implica$\vdash a \rightarrow b$es en realidad el teorema de deducción . Nuevamente, principalmente un (meta-) teorema de lógica proposicional y de primer orden, pero también se puede probar para otras lógicas, pero nuevamente la lógica dada deberá establecer este resultado. Veo que se da una forma de lógica cuántica como ejemplo en el que falla este metateorema.

3. Como otra respuesta.

4. En un libro de texto de lógica formal$\implies$probablemente se introducirá al principio, probablemente en el capítulo de lógica proposicional. Sin embargo, en una conferencia matemática o notas$\implies$se utiliza para representar los pasos en la prueba matemática que se presenta. Por ejemplo, en una clase de álgebra, podríamos tener algunos pasos como:$x > 1 \implies x^2 > 1$con el rango de las variables implícito, pero definido por el álgebra, por lo que la formulación lógica completa de las pruebas algebraicas (en términos de modelos, lenguajes, reglas de inferencia, etc.) quedó implícita.