Se verá a la lógica proposicional (o cálculo proposicional) como un sistema formal. Para esto es necesario realizar algunas definiciones previas.
Un sistema formal consiste de un lenguaje formal, un conjunto de axiomas y un conjunto de reglas de transformación o inferencia.
Lenguaje Formal:
-
Alfabeto de símbolos: ∑, utilizado para armar las oraciones válidas en el lenguaje.
-
Un conjunto de fórmulas bien formadas (fbf o wff), que es un subconjunto de cadenas de símbolos que pueden ser formados usando ∑.
Los axiomas son un subconjunto de las fórmulas bien formadas. Las reglas de inferencia permiten deducir oraciones a partir de otras oraciones
Inferencia
La regla anterior dice que a partir de las premisas p1……pn se puede deducir conclusión
Dadas las definiciones anteriores se puede entonces definir un sistema axiomático para la Lógica Proposicional.
Sistema axiomático de la lógica proposicional
1) Se define un alfabeto:
2)Un conjunto de fórmulas bien formadas o una manera de definir a éstas.
Una wff(fórmula bien formada) se define como aquellas xque:
La definición anterior es una definición inductiva ya que las wff son definidas a partir de formas más simples de sí misma, es decir de wff más sencillas.
Otra forma de definir una fórmula bien formada es a través de una gramática en forma normal de Bakus. Si bien el tema de gramáticas excede el contenido de este trabajo, basta con saber que es equivalente a la definición anterior. A modo ilustrativo mostramos como sería gramática de una wff del sistema proposicional.
Si bien según la definición que hemos dado una wff debe en general estar rodeada de paréntesis pero se puede tomar la decisión de eliminar los paréntesis si éstos no hacen una diferencia esencial. Por ejemplo 
puede escribirse 
.
Utilizaremos además letras mayúsculas A, B, C, etc., para indicar wff en general sin necesidad de referirnos a una en particular. Estas letras son llamadas variables proposicionales.
3) Como regla de inferencia elegimos el modus ponens:
De A y A->B puede derivarse B. Donde A y B son variables proposicionales. Mas formalmente:
4) Por último queda definir el conjunto de axiomas. En vez de definir axiomas definieremos esquemas axiomas, utilizando para ello las variables proposicionales. Decimos esquemas axiomas porque de ellos se pueden derivar los axiomas instanciando las variables proposicionales en wffconcretas. Los esquemas axiomas son tres:
Teoremas y Deducción
Se define como teorema a una wff tal que existe una secuencia de fórmulas, de la cual el teorema es la última y cada uno de los elementos de la secuencia es un axioma o bien se deduce de los anteriores por inferencia (en este caso modus ponens).
Otra forma de definirlo es como la última fórmula de una deducción que tiene el conjunto de hipótesis vacío. Una deducción de un conjunto de wff dado (llamado conjunto de hipótesis) es una secuencia de wff F1….Fn tal que cada Fi es un axioma, es un elemento del conjunto de hipótesis o es derivada por modus ponens de algunas Fj, Fk donde j, k < i.
Sea H el conjunto de hipótesis entonces decimos que Fn es consecuencia deductiva o es derivablede H. Esto de denota como 
.
Antes de definir la semántica de la lógica proposicional vamos a utilizar los conceptos previos para definir algunos Meta-Teoremas. Se trata de establecer teoremas de aplicación general para cualquier wff. En vez de probar p1 ->p1 (lo cual es un teorema) se tratará de probar que A->A para toda wff A. En ese sentido decimos que A->A es un meta-teorema.
Demostremos entonces el siguiente meta-teorema:
Puede verse que algunos de los axiomas no tienen la forma que se ve en la lista de esquemas axiomas. Pero tomando en cuenta que son presisamente esquemas axiomas entonces se pueden reescribir de una forma que sea útil para el propósito de demostrar el teorema
El paso 1 utiliza el axioma 2 :
,
Dado que A,B,C son variables proposicionales pueden ser reemplazadas por cualquier wff y también por otros esquemas que en el fondo representen formulas bien formadas..
En este caso en el lugar del axioma que dice B lo reemplazamos por (B->A) y C por A, dando lugar a:
En el paso 4 escribimos el axioma 1 tal cual figura en la lista de esquemas axiomas.
Semántica de la Lógica Proposicional
Hasta aquí hemos hablado de manera formal, definimos fórmulas bien formadas y la manera de deducir nuevas wff a partir de otras. Es el momento de pasar al mundo real y establecer el significado de las wff. La semántica se encarga de definir a que hechos del mundo hacen referencia las wff.
Para definir la semántica, es necesario especifícar como se interpretan los signos de proposición y los conectores. A los símbolos de proposición se les puede dar el significado que se desea. Por ejemplo podemos decir que p1 significa que “Sócrates es Humano”, o que “mañana llueve”. Además, para operar, es necesario asignar un valor de verdad a las wff. El valor de verdad de una wff compleja depende de los valores de verdad de sus componentes y de los conectores que utilice. Para establecer una valuación de verdad definimos una función v:
El conjunto {F,V} permite establecer dos valores de verdad: F para falso y V para verdadero. Para establecer el valor de verdad de una wff se puede armar una tabla de verdad, donde se asignan valores a cada proposición (o a cada variable proposicional) los cuales son dos (F o V) y se ve el resultado de aplicar la función de valuación definida. Ejemplo de tabla de verdad:
A
|
B
|
-A
|
A->B
|
|
F
|
F
|
V
|
V
|
|
F
|
V
|
V
|
V
|
|
V
|
F
|
F
|
F
|
|
V
|
V
|
F
|
V
|
La tabla se lee fila a fila, en la primera fila por ejemplo se indica que si A vale F (es falso) y B vale F (es falso) entonces ØA es verdadero y A®B es verdadero.
Los conectores lógicos que definimos son suficientes para la lógica proposicional, expresan la negación y la implicación. Podríamos haber usado otros dos conectores lógicos la conjunción (ylógico) y la disyunción(ológico) que se notan: Ù(conjunción) y Ú(disyunción). La razón de no haberlos incluído en el alfabeto es que la negación y la implicación pueden expresar lo mismo. Es decir la elección de los conectores podría ser cualquiera de los dos pares:
porque que son equivalentes.
La equivalencia es la siguiente
Aunque presentamos primero la sintaxis y el sistema axiomático, históricamente surgue primero la semántica (la intención de modelar algo) y luego el mecanismo de representar y de demostrar teoremas. Pero, ¿qué es un teorema desde el punto de vista de la semántica? Para determinar esto, es necesario enunciar un meta-teorema: el teorema de coherencia (soundness) de la lógica proposicional . Definamos primero el concepto de tautología:
Una wff A tal que para toda valuación v, v(A) = T es llamada tautología. La notamos |=A. Lo que significa que A es siempre verdadero.
Una fórmula que es tautología es verdadera en cualquier contexto e independientemente de los valores de verdad asignados a sus proposiciones componentes. Por ejemplo, la wff (A v -A) es una tautología (verlo realizando la tabla de verdad).
Meta-Teorema de la Soundness de la Lógica Proposicional
Es decir: Todo teorema es una tautología.
La demostración de este teorema se realiza por inducción en los pasos para demostrar un teorema. Sin entrar en detalles daremos una idea general de cómo se demuestra. En primer lugar hay que demostrar que los axiomas son tautologías (ya que además de ser axiomas son teoremas), lo cual se puede hacer por extensión realizando la tabla de verdad de cada uno. Decir que los axiomas son tautologías es decir que todo teorema con sólo un paso de demostración es una tautología. Queda entonces realizar el paso inductivo. La hipótesis inductiva dice que hasta n pasos cualquier wff de la demostración es una tautología.
Supongamos que A es un teorema en n + 1 pasos. Si A es un axioma entonces es un teorema (por caso base), sino es un axioma debe ser deducido por modus ponens de algunos de los pasos anteriores, debiendo haber en algún paso un B y un B->A. Pero por hipótesis inductiva, cualquier wff deducida en hasta n pasos es una tautología entonces B y B->A son tautologías. Si A es falso entonces B->A es falso (v(B) = T ), lo cual se contradice con la hipótesis inductiva, por lo tanto v(A) sólo puede ser T. A es una tautología.
Consistencia de Lógica Proposicional
La consistencia es una propiedad interesante de cualquier sistema lógico. Si a la lógica proposicional le agregamos axiomas propios tenemos un nuevo sistema.
Definimos que un sistema es consistente si para toda wff A no es posible que pase que 
Se puede probar que la lógica proposicional es consistente. Es bastante sencillo hacerlo. Si pasa que , es decir que A y -A son teoremas, entonces son tautologías, o sea que para toda valuación v : v(A) = T y v(-A) = T lo que es absurdo por definición de v. No puede pasar entonces , de lo que se deduce que la lógica proposicional es consistente.
Para denotar que una wff A es teorema de un sistema (que incluye además los axiomas de la lógica proposicional y otros propios) escribimos |-SA. Cuando demostramos la transitividad de la implicación, partimos de dos wff que considerábamos al mismo nivel que los axiomas (A->B y B->C). Estábamos de alguna forma definiendo un sistema formal del cual A->B y B->C serían los axiomas propios.
Se puede demostrar que si un sistema S es inconsistente ( es decir ├SA y ├S-A ) entonces para toda wff A pasa |-SA. La demostración de esto se realiza en pocos pasos:
S es inconsistente
Sea entonces B (una wff cualquiera) tal que |-SB y |-S-B
Pero -B->(B->A) (es un teorema, demuéstrelo cómo ejercicio)
Entonces por modus ponens B->A y también por modus ponens tenemos A. Demostramos A que es cualquier wff.
Completitud (Completeness )
Un sistema es completo si toda tautología es un teorema, es decir la vuelta en la implicación del teorema de soundness: S es completo si |=SA Þ|-SA
Teorema: La lógica proposicional es completa: 
La demostración de este teorema (o meta-teorema) escapa al alcance de este trabajo dado que es bastante más complejo que la soundness. En definitiva vemos una equivalencia entre aquellas cosas que son tautologías, es decir verdaderas siempre, y aquellas que se pueden demostrar (teoremas). Podemos concluir que la lógica proposicional es un sistema formal consistente, completo y coherente (soundness).