Demostración de deducción natural de $ a = b \rightarrow f (a) = f (b) $. ¿Dónde me equivoqué?

Question

Estoy tratando de demostrar una propiedad básica de las funciones usando los pasos de la deducción natural, dentro de la teoría de conjuntos. Específicamente, que si a = b, entonces f(a) = f(b) para cualquier función f. Sé que la prueba que he desarrollado tiene fallos (explicaré a continuación por qué), pero no estoy seguro en qué línea ocurre.

Primero, afirmo las siguientes definiciones:

[Def 1] $ \forall x(x \in D(f) \to \exists y((x,y) \in f \wedge \forall z((x,z)\in f \to y = z)))$ -- Define una función $f$ con dominio $D(f)$

[Def 2] $ \forall x \forall y(f(x) = y \leftrightarrow (x,y) \in f)$ -- Define la notación $f(x)$

y a partir de esto quiero probar:

$$ \forall x \forall y((x \in D(f) \wedge x = y) \to f(x) = f(y))$$

Aquí está la prueba que utilizo:

1. $a \in D(f)~~~~~\text{(Suposición)}$
2. $ a = b~~~~~\text{(Suposición)}$
3. $ a \in D(f) \to \exists y((a,y) \in f \wedge \forall z((a,z)\in f \to y = z))~~~(\forall \text{-elim, Def 1.})$
4. $ \exists y((a,y) \in f \wedge \forall z((a,z)\in f \to y = z))~~~(\to\text{elim; 1, 3})$
5. $ (a,c) \in f \wedge \forall z((a,z)\in f \to c = z)~~~~\text{(Suposición)}$
6. $ (a,c) \in f~~(\wedge\text{-elim, 5.})$
7. $ f(a) = c \leftrightarrow (a,c) \in f~~~~(\forall\text{-elim dos veces en Def 2.})$
8. $ (a,c) \in f \to f(a) = c ~~~(\leftrightarrow\text{elim; 7.})$
9. $ f(a) = c~(\to\text{elim; 6, 8})$
10. $ (a, f(a)) \in f~~\text{(=-elim; 6, 9. Además, la suposición en 5. se descarta mediante }\exists\text{-elim.)}$
11. $ (b, f(a)) \in f~~\text{(=-elim; 2, 10)}$
12. $ f(b) = f(a) \leftrightarrow (b,f(a)) \in f~~~~(\forall\text{-elim dos veces en Def 2.})$
13. $ (b,f(a)) \in f \to f(b) = f(a) ~~~(\leftrightarrow\text{elim; 12.})$
14. $ f(b) = f(a)~(\to\text{elim; 11,13})$
15. $ f(a) = f(b)~\text{(=-symm; 14)}$
16. $ (a \in D(f) \wedge a = b) \to f(a) = f(b)~~\text{(Descartar suposiciones 1 y 2)}$
17. $ \forall x \forall y((x \in D(f) \wedge x = y) \to f(x) = f(y))~~~~~(\forall\text{-intro usado dos veces)}$

(Nota: Utilizo las reglas de inferencia de la deducción natural definidas en Chiswell y Hodges: Lógica Matemática)

Esta prueba debe estar equivocada, porque no utiliza en absoluto la parte clave de la Definición 1, que garantiza la unicidad del valor de una función para cierta entrada. ¡Es decir, puedo simplemente eliminarla con $\wedge$ en el paso 6! ¿Alguien puede señalar en qué paso cometí un error?

PD. Disculpas por el pobre formato de las líneas de la prueba, pero no tengo suficiente conocimiento de LaTeX para formatearlo correctamente.

Answer 1

Considera la relación "$\text {Hijo_de}(x,y)$" e introduce la notación $\text {Hijo_de}(x)=y$.

Tenemos que:

si $ \ \text {Juan} = \text {Bobby} \ $, entonces $ \ \text {Hijo_de}(\text {Juan}) = \text {Hijo_de}(\text {Bobby}).$

Pero de:

$ \ \text {Hijo_de}(\text {Juan}) = \text {Ron} \ $ y $ \ \text {Hijo_de}(\text {Juan}) = \text {Tommy}$

no se sigue que :

$ \ \text {Ron} = \text {Tommy} \ $.

¿Qué ha salido mal? La definición de la notación $\text {Hijo_de}(x)=y$.

No podemos usarla con la relación "$\text {Hijo_de}(x,y)$" porque no es funcional.

Por lo tanto, en tu demostración, al aplicar [Def 2] has asumido implícitamente que también se cumple la cláusula de unicidad de [Def 1].

Answer 2

En la lógica de primer orden, los símbolos de función son tratados inherentemente como cosas que funcionan funcionalmente, por lo que a partir de $a=b$, lógicamente se seguirá que $f(a) = f(b):

1. $a=b \qquad\quad\qquad$ Suposición
2. $f(a)=f(a) \qquad$ = Intro
3. $f(a)=f(b) \qquad$ = Elim 1,2

Ahora, sé que intentaste evitar hacer esto creando una definición axiomática para una función, y tratando de derivar su funcionalidad a partir de eso. Sin embargo, acabaste usando símbolos funcionales, y de hecho en la línea 10 explotaste la funcionalidad inherente de los símbolos de función en la lógica después de todo, haciendo efectivamente lo que hace la prueba anterior, eliminando así la necesidad de Def. 1.

Para evitar tales explotaciones no deseadas de la naturaleza de los símbolos de función en la lógica, te recomendaría 1) evitar los símbolos de función por completo, 2) utilizar Def. 1 como tu única definición axiomática de una función, 3) deshacerte de Def. 2, y 4) reformular tu objetivo para no utilizar símbolos de función, y en su lugar usar algo como:

$ \forall x \forall y ((x \in D(f) \wedge y \in D(f) \wedge x = y) \to \forall v \forall w (((x,v) \in f \wedge (y,w) \in f) \to v = w))$

A continuación se muestra una prueba de Deducción Natural para el resultado deseado siguiendo ese enfoque.