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: $\vdash\varphi$ (“$\varphi$ es un teorema”).

Un razonamiento valido en un sistema de demostracion formal es una coleccion de formulas formada por un conjunto de premisas y una conclusion $\varphi$ de manera que la conclusion se puede demostrar a partir de las premisas (como describiremos a continuacion).

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

Una demostracion de un teorema $\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 $\left\{\varphi_{1},\ldots,\varphi_{n}\right\}\vdash\varphi$ es una sucesion finita de formulas

donde cada formula de la sucesion cumple:

1. 1.
   ​

   Es una premisa (las $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.