¿Es el teorema de la deducción un metateta teorema o un metateorema?

Question

Estoy hablando de un estilo Hilbert del sistema para el Cálculo Proposicional. La única axiomas y reglas de inferencia que puedo usar son,

$\color{crimson}{\text{Axiom 1.}}\ P\to (Q\to P)$

$\color{crimson}{\text{Axiom 2.}}\ (S\to (P\to Q))\to((S\to P)\to (S\to Q))$

$\color{crimson}{\text{Axiom 3.}}\ (\neg Q\to\neg P)\to(P\to Q)$

$\color{crimson}{\text{Rule of Inference.}}$ Modus Ponens.

Mi principal pregunta es con respecto a la Deducción del Teorema para este sistema. Antes de declarar mi pregunta, permítanme en primer lugar el estado de la Deducción del Teorema de completitud de este post.

Deducción Del Teorema. Deje $\Delta$ ser un conjunto de fórmulas. Si $\Delta\cup\{S\}\vdash T$$\Delta\vdash S\to T$.

Aquí símbolos tienen un significado usual (si es necesaria una aclaración, por favor hágamelo saber a través de un comentario(s)).

La principal pregunta que tengo es,

Es el Teorema de la Deducción de una meta-teorema o un meta-meta teorema?

Debido a la ocurrencia de $\vdash$ en la declaración de la Deducción del Teorema y desde $\vdash$ no está en el alfabeto del Cálculo Proposicional (por ejemplo, ver aquí) la declaración del Teorema de la Deducción no puede ser una declaración de que el objeto del lenguaje. En la lógica de los libros de texto (al menos los que he visto) el teorema es caracterizado como un metatheorem.

Sin embargo, a partir de la declaración del teorema a mí me parece que el teorema es hablar de (aproximadamente) acerca de una propiedad de $\vdash$. Desde el teorema de conversaciones acerca de una propiedad de $\vdash$, pensé que el teorema de la Deducción es, probablemente, una metametatheorem. Mis preguntas son,

1. Es el Teorema de la Deducción de una metametatheorem?
2. En qué idioma está la prueba de la Deducción del Teorema de ser llevado a cabo (es decir, en el metalenguaje o en el metametalanguage)?
3. Es posible un estado demostrar el teorema de la deducción en un idioma que no es un Lenguaje Natural (como el inglés)?

---

Edit: Consulte este comentario para mayor aclaración de la motivación para hacer esta pregunta.

Answer 1

El símbolo $\vdash$ está siendo utilizado en su declaración de la deducción como una notación abreviada; $\Delta \vdash A$ significa que "la fórmula $A$ es derivable a partir del conjunto de fórmulas de $\Delta$". La declaración no hablar de $\vdash$, sólo la utiliza. Por lo que la deducción del teorema es una metatheorem en lugar de un metametathorem y su prueba es (en los típicos libros de texto) llevado a cabo en un metalenguaje que comprende una mezcla de lenguaje natural y símbolos como $\vdash$, $\cup$, $\{$ y $\}$ etc.

Sería posible afirmar y demostrar el teorema de la deducción en un lenguaje formal, como el lenguaje de la teoría de conjuntos o en el lenguaje de un típico automatizado de prueba asistente.

Answer 2

Su declaración de La Deducción del Teorema es un poco impreciso. Que en realidad no dicen, parenthesizing la implicación como sea necesario, que "Vamos a Δ ser un conjunto de fórmulas. Si Δ∪{S}⊢T entonces Δ⊢(S→T)." Si lo hizo, entonces para todos los usos de $\vdash$ tendríamos que. Pero, existen algunos sistemas lógicos donde no es, como Lukasiewicz de tres valores de la lógica. A veces ni siquiera se indica en la lógica clásica, como en Frege de trabajo o queda relegado a un apéndice como en Arthur Antes de el libro de la Lógica Formal. La Deducción del Teorema que dice:

"Vamos a Δ ser un conjunto de fórmulas. Si Δ∪{S} ⊢$_{(1, 2, 3)}$ T entonces Δ ⊢$_{(1, 2, 3)}$ (S→T)."

Así que, no creo que La Deducción del Teorema de conversaciones acerca de una propiedad de $\vdash$. Habla acerca de una propiedad del sistema deductivo en la mano. El "si-entonces" es la instrucción de la propiedad. Que implica El Teorema de la Deducción como una meta-teorema de que el sistema deductivo.