Diferencia entre revisiones de «Deducción natural»

1037 bytes añadidos ,  hace 10 años
Agregué reglas para los cuantificadores. Sin embargo, están incompletas e incluso MAL. Por favor quien sepa más, amplíe y corrija.
(Página creada con «La '''deducción natural''' es una aproximación a la teoría de la demostración en la que se busca capturar mejor la manera los humanos efectivamente construyen [[Demost...»)
 
(Agregué reglas para los cuantificadores. Sin embargo, están incompletas e incluso MAL. Por favor quien sepa más, amplíe y corrija.)
 
=== Cuantificadores ===
 
Sea ''a'' una constante de individuo y ''t'' un término. Sea ''A(b/c)'' el resultado de reemplazar todas las apariciones de ''b'' en ''A'' por ''c''. Luego:
 
{|border="1" cellpadding="7" style="margin:1em; border:solid 1px LightGray; border-collapse:collapse;"
!Nombre de la regla
!Abreviación
!Formalización
!Cálculo de secuentes
|- align="center"
|align="left"|Introducción del [[cuantificador universal]]
|<math>I \forall \,</math>
|<math>\frac{\phi} {\forall x \phi}</math>
|<math>\phi \vdash \forall x \phi</math>
|- align="center"
|align="left"|Eliminación del [[cuantificador universal]]
|<math>E \forall \,</math>
|<math>\frac{\forall x \phi} {\phi(x/a)}</math>
|<math>\forall x \phi \vdash \phi(x/a)</math>
|- align="center"
|align="left"|Introducción del [[cuantificador existencial]]
|<math>I \exists \,</math>
|<math>\frac{\phi} {\exists x \phi(t/x)}</math>
|<math>\phi \vdash \exists x \phi(t/x)</math>
|- align="center"
|align="left"|Eliminación del [[cuantificador existencial]]
|<math>E \exists \,</math>
|
|
|}
 
== Demostraciones ==
20 693

ediciones