Hay varios problemas con lo que usted ha dicho. En primer lugar, no se han indicado las reglas claramente/correctamente. La primera regla sería algo así como: "Si, asumiendo $P$ podemos mostrar a $Q$, luego hemos probado a $P\Rightarrow Q$." Siguiente, no todas las sentencias son de la forma $P\Rightarrow Q$. Usted presumiblemente también quieren alguna manera de usar todas estas cosas que están asumiendo. En Hilbert estilo de los sistemas, este es normalmente el modus ponens, que establece que si sabemos $P\Rightarrow Q$ y sabemos $P$ entonces podemos concluir $Q$.
Para un típico Hilbert sistema de estilo para proposicional de la lógica, sólo hay una regla: modus ponens. La única manera de concluir nada en este tipo de sistema es 1) para que sea una instancia de un axioma, o 2) a través de modus ponens. No existe el concepto de "suponiendo" algo en una de Hilbert-sistema de estilo, así que ninguna de las reglas que mencionas son parte de un Hilbert sistema de estilo. Hilbert estilo de los sistemas son bastante inhumanas aunque (pero son muy minimalista que hace agradable para demostrar la meta-teoremas acerca de la prueba del sistema).
Un sistema a prueba de que mucho se asemeja más informal de las pruebas es la deducción natural. (Estrechamente relacionado es el secuente de cálculo que tiene un montón de buenas propiedades, pero cuyas reglas son generalmente menos intuitiva, aunque a menudo más fácil trabajar con.) En deducción natural, cada conectivo tiene sus propias reglas, cada una dividida en dos grupos: introducción de las reglas y la eliminación de las reglas. Introducción las reglas de mostrar cómo concluir una declaración que implican un conectivo, mientras que la eliminación de las reglas de mostrar cómo hacer uso de una declaración que implican un conectivo. Deducción Natural también tiene una noción de probar algo bajo supuestos: hipotético de las pruebas. Modus ponens es la eliminación de la regla de $\Rightarrow$ (y se llama simplemente $\Rightarrow$-eliminación de deducción natural), y la primera regla que mencionas es la introducción de la regla. En estos más estructural de los sistemas de prueba, cada uno de los conectivos se define por las reglas de forma independiente de las otras conectivas. A menudo en la deducción natural de los sistemas, $\neg P$ se define como $P\Rightarrow\bot$ donde $\bot$ es el nullary conectivo que se destaca por la siempre falsa fórmula. Se define mediante la eliminación de la regla de que si bajo algunos supuestos, podemos demostrar $\bot$, a continuación, bajo las mismas hipótesis que podemos demostrar nada. Esto es, el principio de explosión es la eliminación de la regla de $\bot$. No hay introducción de la regla.
Para apoyar la lógica clásica, tenemos que añadir un extra de regla o de un axioma. A diferencia de las otras reglas, esta regla se involucran múltiples conectivas que debilita algunas de las propiedades atractivas acerca de deducción natural. (El secuente cálculo no tiene este problema, que es uno de sus aspectos positivos.) Una opción común es esencialmente su tercera regla que voy a repetir: si, en virtud de algunos de los supuestos incluidos $\neg Q$ ( $Q\implies \bot$ ) podemos derivar $\bot$, entonces podemos probar $Q$ bajo los mismos supuestos excluyendo $\neg Q$. La segunda regla es entonces deriven de las normas para la eliminación de la introducción y reglas para $\Rightarrow$, la eliminación de la regla de $\bot$, y esta última regla.
Para clásica proposicional, lógica, podría reducir cada fórmula uno que involucran sólo a $\Rightarrow$ $\neg$ o $\Rightarrow$$\bot$. Así que las cuatro reglas anteriores suficiente para probar todo, para que de esta lógica. Para la lógica de primer orden, usted necesitará agregar reglas adicionales para los cuantificadores. Incluso Hilbert-estilo de sistemas suelen tomar generalización universal (es decir, $\forall$- introducción) como una regla adicional. Aún así, demostrando $P\lor Q$ asumiendo $\neg P$ y mostrando el $Q$ a menudo ser un poco tonto. En deducción natural, $\lor$ tiene dos introducción de las reglas, a saber: si podemos probar $P$ (en algunos supuestos), entonces podemos probar $P\lor Q$ (bajo los mismos supuestos), y si podemos probar $Q$, entonces podemos probar $P\lor Q$. Estas reglas se deriven de las cuatro reglas mencionadas arriba si definimos $P\lor Q$$(P\Rightarrow\bot)\Rightarrow Q$. Podemos derivar las reglas para todas las otras conectivas proposicionales en términos de las cuatro reglas que he mencionado dada adecuado definiciones de los conectivos en términos de$\Rightarrow$$\bot$. También podemos, por supuesto, se derivan de un ilimitado conjunto de reglas adicionales para capturar patrones comunes de razonamiento como el contrapositivo de la regla. También podemos hacer una elección diferente de lo que las conectivas y reglas que queremos tomar como primitivos.
Aunque yo diría que la primera regla que usted menciona ($\Rightarrow$-introducción) está íntimamente relacionado con el $\Rightarrow$, los otros dos no son particularmente relacionados con ella. Ellos están íntimamente relacionados con la lógica clásica, pero ambos no son necesarias y, dado otra regla/axiom para incorporar la lógica clásica, tanto potencialmente podría ser derivable. No hay ninguna razón para incluir tanto de las últimas dos reglas como que de alguna manera especial, mientras que excluyendo el infinito número de otros que se pueden derivar reglas que concluyen $P\Rightarrow Q$.
