Hola,
Complementando lo que dice Martín: el tema es que cuando en una demostración introduces una constante de predicado "fresca"
, en la prueba necesariamente no usaste nada especifico de esa constante. Entonces, tu prueba es --insistiendo en lo que creo que es la clave de todo esto-- uniforme en .
Complementando lo que dice Martín: el tema es que cuando en una demostración introduces una constante de predicado "fresca"
, en la prueba necesariamente no usaste nada especifico de esa constante. Entonces, tu prueba es --insistiendo en lo que creo que es la clave de todo esto-- uniforme en . Entonces, cuando cambies por cualquier fórmula 
en la prueba, todas las reglas se aplican. Comentaba yo que meter esa constante "fresca" es una manera de cuantificar en segundo orden sin meterlo formalmente en el lenguaje. En el fondo una expresión que depende de un "fresco" dice algo que vale 
, pero no lo puedes escribir porque no te autorizas el cuantificador.
por cualquier fórmula en la prueba, todas las reglas se aplican. Comentaba yo que meter esa constante "fresca" es una manera de cuantificar en segundo orden sin meterlo formalmente en el lenguaje. En el fondo una expresión que depende de un "fresco" dice algo que vale , pero no lo puedes escribir porque no te autorizas el cuantificador.Saludos,
Mauricio.