¿Las reglas de inferencia significan lo mismo en un sistema de Hilbert y en un sistema deductivo natural?

¿Es correcto que A Mathematical Introduction to Logic de Enderton usa un sistema de estilo Hilbert para la lógica de primer orden?

En la página 110 de la SECCIÓN 2.4 Un cálculo deductivo en el Capítulo 2: Lógica de primer orden

Nuestra única regla de inferencia se conoce tradicionalmente como modus ponens. Se suele afirmar: A partir de las fórmulas$α$y$α → β$podemos inferir$β$:

$$\frac{α, α → β}{β}.$$

Que significa la regla:

1. Un ejemplo de relación$\vdash$:$\{α, α → β\} \vdash β$.

2. Una instancia de una relación entre las instancias de$\vdash$: si$\vdash α$y$\vdash α → β$, entonces$\vdash β$.

3. para un conjunto$\Gamma$de fórmulas, si$\Gamma \vdash α$y$\Gamma \vdash α → β$, entonces$\Gamma \vdash β$. Así que la cita significa tener$\Gamma$pero lo omite, pensando que sus lectores lo llenarán automáticamente. (Ver también más abajo)

4. ¿Algo más?

Algunas reflexiones, observaciones y preguntas:

• 2 y 3 son equivalentes, porque 2 implica 3 por el teorema deductivo (¿o me equivoco porque el teorema deductivo se deriva de las reglas de inferencia y los axiomas, entonces no existe antes que las reglas de inferencia y los axiomas?).

• Lo que me hace apoyar 3 sobre 2 es que vi en Wikipedia que el teorema deductivo se considera como una regla de inferencia extendida,

  Debido a que los sistemas de estilo Hilbert tienen muy pocas reglas de deducción, es común probar metateoremas que muestran que las reglas de deducción adicionales no agregan poder deductivo, en el sentido de que una deducción que usa las nuevas reglas de deducción se puede convertir en una deducción que usa solo la deducción original. normas.

  Algunos metateoremas comunes de esta forma son: El teorema de deducción, ...

  y en el libro de Enderton en p118

  TEOREMA DE DEDUCCIÓN Si$\Gamma; \gamma \vdash ϕ$, entonces$\Gamma \vdash ( γ → ϕ )$.

• ¿Las reglas de inferencia significan lo mismo en un sistema de Hilbert y en un sistema deductivo natural? El n. ° 3 anterior es similar al 3.5 "Modus ponens" en la página 65 en IV Sequent Calculus (en realidad, un sistema de deducción natural) en la Lógica matemática de Ebbinghuas . ¿Las líneas horizontales que aparecen en ambos significan "si... entonces..." en el nivel del metalenguaje?

  

• La respuesta a una pregunta relacionada dice que las reglas de inferencia pueden operar sobre fórmulas, si no están escritas explícitamente como operando sobre secuentes (es decir, instancias de$\vdash$). ¿Es eso incorrecto? Las reglas de inferencia siempre operan en instancias de$\vdash$, incluso si están escritos en una forma que parece que operan en fórmulas directamente?

Gracias.