Un sistema axiomático cuenta con un lenguaje formal, un conjunto de axiomas y reglas de deducción. Primero definimos el lenguaje formal del cálculo de predicados (que básicamente nos dice que cosas se pueden escribir). En el mismo se deben involucrar: constantes, variables, símbolos de función, símbolos predicativos, y conectores lógicos. En definitiva en un lenguaje formal de primer orden necesitamos definir:
-
alfabeto
-
términos
-
fórmulas bien formadas
El alfabeto está formado por:
-
constantes: c1…………cn…. (tantas como se necesite)
-
variables: x1,x2……….xn…. (tantas como se necesite)
-
símbolos de función fin.
-
símbolos predicativos Pin y el símbolo de predicado constante ^(siempre falso).
-
conectores lógicos

-
cuantificadores

-
símbolos de puntuación: ),( y , .
No utilizamos el cuantificador existencial y los otros conectores lógicos porque se pueden expresar en función de los que definimos (aunque a veces informalmente los usemos para simplificar). El superíndice n sobre la P y la f indica la aridad de los predicados y funciones, mientras que el subíndice i de ambas distingue distintos predicados y distintas funciones.
Definimostérminocomo:
-
Toda constante es un término
-
Toda variable es un término
-
Si t1,………..tn son términos entonces fin(t1,………..tn) es un término (la aplicación de funciones a términos nos da un término).
-
Ninguna otra cosa es un término
Las fórmulas bien formadas (wff) son:
-
Pin(t1,………..tn) es una wff siendo ti términos.
-
Si A y B son wff entonces

-
Si A es una wff entonces

Dentro de las wff existen las que se denominan fórmulas atómicas: si P es un predicado y t1…tk términos, entonces P(t1…..tk) es una fórmula atómica.
Esquemas Axiomas de la Lógica de Primer Orden:

Reglas de deducción (tenemos dos) :

La noción de Teorema en la Lógica de Primer Orden
La noción de teorema es similar a la del cálculo proposicional. También se puede definir como la última fórmula de una deducción con un conjunto de hipótesis vacío. Una deducción es, dado un conjunto de hipótesis H, una secuencia de fórmulas F1…Fn tal que para cada i (1<= i <= n) se cumple alguna de las siguientes condiciones:

La deducción sintáctica la notamos (como en cálculo proposicional) como:

Teorema de la deducción de la LPO.

Corolario del teorema de la deducción
