HOla.
Mi traducción es esta:
\(\bar\forall \psi \in PROP . ( \varphi \in Sub(\psi) \Rightarrow \bar\forall s \in Secf(\varphi). \psi \in s) \)
Supongo que esta puede servir...
Lo que estoy diciendo es que:
Para cualquier fórmula de PROP
Si tomo una subfórmula cualquier de esa
Y considero una secuencia cualquiera la primer fórmula,
entonces la subfórmula está en la secuencia.
Pero cuál es la lógica de hacer esto así?
Bien, si analizamos la letra original del ejercicio, nos encontramos que es la siguiente:
Primero identificamos los objetos que tenemos que se manejan en la tesis. En general están representados por metavariables, pero podría haber alguno implícito.
Metavariables:
- $$\varphi$$
- $$\psi$$
- Se habla de cualquier secuencia de formación para ψ. Esto indica que posiblemente necesitemos una metavariable s para representar una secuencia de formación genérica de $$\psi$$.
Ahora, necesitamos ver las condiciones sobre las metavariables y la dependencia o independencia entre ellas.
- $$\varphi$$ representa una subfórmula de $$\psi$$, por lo que es dependiente de $$\psi$$.
- s representa una secuencia de formación de $$\psi$$ por lo que también es dependiente de $$\psi$$.
- $$\psi$$ representa una subfórmula cualquiera de PROP, sin ninguna condición.
Conclusión:
Las metavariables que no tienen condiciones de ningún tipo, van más afuera que las condicionadas. En este caso, además, vemos que la que nos queda más afuera representa un elemento de un conjunto inductivo, lo que parece "sano".
Ahora bien, con un análisis de este tipo, se puede llegar a descubrir un poco la estructura de la tesis, lo que nos guía después, en la estructura de la demostración. Pero eso no significa que el análisis sea el adecuado.
Pero creo que en este caso es :-)
Saludos
FDO.
PD: Revisen el mensaje desde el EVA por si tengo que modificar algo.