14 Sistemas formales de demostracion

Un sistema formal de demostracion consiste en los siguientes tres elementos:

•  
  ​

  Una sintaxis: un alfabeto y un lenguaje definido sobre ese alfabeto que establece cuales son las formulas bien construidas del sistema.

•  
  ​

  Un conjunto de axiomas: formulas que se admiten como validas en el sistema sin necesidad de demostracion.

•  
  ​

  Un conjunto de reglas de inferencia o reglas de deduccion: permiten demostrar la validez de una formula en el sistema tomando como punto de partida axiomas u otras formulas ya demostradas válidas.

Un teorema en un sistema de demostracion formal es una formula valida, en el sentido de que se obtiene de una de estas dos formas:

•  
  ​

  Es un axioma del sistema.

•  
  ​

  Se obtiene a partir de otros teoremas usando una regla de inferencia.

Notacion: $\displaystyle\vdash\varphi$ (“$\displaystyle\varphi$ es un teorema”).

Notacion: $\displaystyle\{\varphi_{1},\varphi_{2},\ldots,\varphi_{n}\}\vdash\varphi$

Una demostracion de un teorema $\displaystyle\varphi$ es una sucesion finita de formulas

donde cada formula de la sucesion cumple una de las siguientes afirmaciones:

1. 1.
   ​

   Es un axioma del sistema.

2. 2.
   ​

   Es un teorema ya demostrado en el sistema.

3. 3.
   ​

   Se obtiene a partir de las formulas anteriores de la sucesion usando una regla de inferencia.

Una demostracion de un razonamiento $\displaystyle\{\varphi_{1},\ldots,\varphi_{n}\}\vdash\varphi$ es una sucesion finita de formulas

donde cada formula de la sucesion cumple:

1. 1.
   ​

   Es una premisa (las $\displaystyle n$ primeras).

2. 2.
   ​

   Es un axioma del sistema.

3. 3.
   ​

   Es un teorema ya demostrado.

4. 4.
   ​

   Se obtiene a partir de las formulas anteriores de la sucesion usando una regla de inferencia.