es la lógica última y, como tal, puede ser un modelo simplificado del cómputo, usado en la teoría de la computabilidad (el estudio de qué puede ser computado) y la teoría de la prueba (el estudio de qué se puede probar matemáticamente).
(Wikipedia).