Los novatos en la inducción intentan encontrar pruebas de deducción natural con determinados axiomas

Question

Estoy tratando de probar la conjetura:

$∀x.∀y.∀z.(x+y)+z=x+(y+z)$

Tengo acceso a los siguientes axiomas más la inducción, y las otras reglas regulares de deducción natural.

$A1: nat(0)$

$A2: nat(T) ⊢ nat(s(T))$

$A3: nat(T), nat(U) ⊢ nat(T+U)$

$A4: nat(T), nat(U) ⊢ nat(T · U)$

$A5: 1=s(0)$

$A6: ∀x. 0+x=x$

$A7: ∀x.∀y.s(x)+y=s(x+y)$

$A8: ∀x.0·x = 0$

$A9: ∀x.∀y.s(x)·y = y + x · y$

Estoy muy cerca de completar esta prueba, sin embargo no estoy seguro de cómo completarla con los números entre paréntesis

Answer 1

El problema que tienes es que nunca usas tu hipótesis inductiva (línea 16). Esto es lo que necesitas para pasar:

$(s(a2) + a3) + a4 = ( \text {using} A7: s(a2) + a3 = s(a2 + a3))$

$s(a2 + a3) + a4 = ( \text {using } A7 \text { again})$

$s((a2 + a3) + a4) = ( \text {use inductive hypothesis! }(a2 + a3) + a4 = a2 + (a3 + a4))$

$s(a2 + (a3 + a4)) =( \text {using } A7)$

$s(a2) + (a3 + a4)$

A continuación hay una prueba formal usando el programa de computadora llamado Fitch (que viene con el libro Language Proof and Logic):

Por favor, noten cómo la prueba formal refleja de cerca la prueba algebraica matemática como se muestra al principio de este post: por cada paso matemático, hago dos pasos en la prueba formal, un $ \forall \: Elim$ seguido de un $= \: Elim$ . También empiezo con una frase "LHS=LHS" (LHS: lado izquierdo) al principio usando un $= \: Intro$ para iniciar la transformación gradual. Sé que usted hace todos estos pasos en algún momento también en su prueba, pero el orden en que los hace parece un poco menos organizado, así que le animo a seguir la transformación sistemática como yo lo hago en mi prueba, porque de lo contrario es muy fácil perderse en todas las cadenas de símbolos, ¡como estoy seguro de que ha notado!

OK, tengo la maldita cosa... ¡qué interfaz tan infernal!

Answer 2

No sigue. [¡O no lo hizo antes de "y la inducción!"]

Tome el modelo para la Aritmética de Robinson y por lo tanto su aritmética en la p. 69 de mi libro de Gödel - y verá que en ese modelo, con $a$ y $b$ como se define, $(a + b) + a \neq a + (b + a)$ .

El punto básico es que, como no tienes un axioma de inducción dentro de tu aritmética, no puedes probar casi ninguna de las verdades generales más simples de la aritmética.

Estoy siendo un poco conciso, ya que ya he respondido a una pregunta similar de la OP No estoy seguro de qué libro/juego de notas de la conferencia se está utilizando aquí, pero algo va mal.