Aunque en principio, ya está definida la semántica de la lógica proposicional, necesitamos de todos modos de algunos conceptos auxiliares, como el de consecuencia lógica. La consecuencia lógica se refiere a cuándo una fórmula sigue lógicamente de otras. Vamos a agrupar a todos los modelos que hacen cierta a una fórmula en un conjunto que vamos a describir asÃ: para consecuencia lógica se usa el mismo sÃmbolo que para satisfacción, pero ahora el lado izquierdo es un conjunto de fórmulas y omitimos las llaves de conjunto. Un conjunto de fórmulas "alfa1", "alfa2", hasta "alfa n", lógicamente implican a una fórmula "beta", si el conjunto de todos los modelos que hacen ciertas a todas las fórmulas del lado izquierdo está contenido en el conjunto de modelos que hacen cierto al lado derecho. El lado derecho, entonces, debe preservar la verdad del lado izquierdo, aunque es posible que el lado derecho sea verdadero en más situaciones que el lado izquierdo. Hay un caso especial. Si todo modelo hace cierto al lado izquierdo, o sea, que el lado izquierdo es el conjunto vacÃo, entonces, todo modelo también debe hacer cierto al lado derecho, y decimos que el lado derecho es una tautologÃa. Recordar que ya tenÃamos otro uso del torniquete: cuando el lado izquierdo es un modelo, y en ese caso significa satisfacción. El torniquete, entonces, está sobrecargado. Veamos un ejemplo de consecuencia lógica. Del lado izquierdo del torniquete, hay dos fórmulas, "a y b" implican "c y a". Del lado derecho tenemos "b" implica "c". En el lado izquierdo de esta tabla están todos los modelos para las variables "a, b y c", uno en cada renglón. Podemos ver que todos los modelos que hacen cierta a la conjunción de estas dos fórmulas hacen también cierto al lado derecho, que en este caso tiene más modelos que lo hacen cierto. Este ejemplo representa el razonamiento con el que empezamos. La conclusión de que "si el Señor A tiene un arma, entonces el Señor A cometió el homicidio" es correcta con respecto a la semántica que dimos. Otro concepto importante es el de equivalencia lógica. Vamos a decir que dos fórmulas son lógicamente equivalentes y vamos a usar este sÃmbolo si tienen exactamente los mismos modelos que las hacen ciertas. Este es un ejemplo en el que "beta" es lógicamente equivalente a la fórmula que tenÃamos antes. La equivalencia lógica nos hace darnos cuenta de que algunos conectivos lógicos se pueden expresar en términos de otros. Por ejemplo, la disyunción se puede expresar en términos de negación y conjunción, similarmente, con la implicación. Vamos ahora a distinguir fórmulas que tengan determinadas formas que nos van a ser útiles. Para eso necesitamos definir el concepto de literal. Una literal va a ser una variable proposicional o su negación y la vamos a representar con la letra "l". Una fórmula en forma normal disyuntiva tiene esta forma, es una disyunción de conjunciones de literales. Cada conjunción de literales se llama término. Esta forma se llama "normal" porque toda fórmula arbitraria es lógicamente equivalente a una fórmula en forma normal disyuntiva. En otras palabras, semánticamente hablando, podrÃamos tirar todas las fórmulas a la basura, excepto las que tienen forma normal disyuntiva y no perderÃamos expresividad. La otra forma normal que nos va a interesar es la forma normal conjuntiva. En este caso, tenemos una conjunción de disyunciones de literales. Cada disyunción de literales se llama "cláusula". Similarmente, limitándonos a las fórmulas en forma normal conjuntiva, tenemos la misma expresividad que con fórmulas arbitrarias. Una fórmula es satisfactible si existe un modelo que la hace cierta, y pueden existir más modelos que la hagan cierta. Por otro lado, ya vimos que una fórmula es una tautologÃa o fórmula válida si todo modelo la hace cierta. Estos dos conceptos están relacionados. Es posible demostrar que una fórmula arbitraria "alfa" es satisfactible, si y sólo si, "no alfa" no es tautologÃa. La importancia de este resultado es que, si tenemos una máquina que nos dice si una fórmula es satisfactible o no, podemos usar esa misma máquina para saber si una fórmula es tautologÃa o no.
