supongamos tengo P(x,y)/\(Ex)x='x y clausuro quedando paratodo x , paratodo y P(x,y)/\(Ex)x='x al aplicar 245 y sustituir que digo? que por alcance de cuantificadores sustituyo solo hasta antes del existe ? podrian dar un ejemplo claro ? gracias
Cuando aplicamos clausura a una cosa que está compuesta en parte por sentencias con cuantificadoress, que hacemos?
supongamos tengo P(x,y)/\(Ex)x='x y clausuro quedando paratodo x , paratodo y P(x,y)/\(Ex)x='x al aplicar 245 y sustituir que digo? que por alcance de cuantificadores sustituyo solo hasta antes del existe ? podrian dar un ejemplo claro ? gracias
supongamos tengo P(x,y)/\(Ex)x='x y clausuro quedando paratodo x , paratodo y P(x,y)/\(Ex)x='x al aplicar 245 y sustituir que digo? que por alcance de cuantificadores sustituyo solo hasta antes del existe ? podrian dar un ejemplo claro ? gracias
Lo que tenemos que hacer es aplicar las definiciones y lemas:
nuestra fórmula: (∀x)((∀y)(P(x,y) ^ (∃x)x='x))
el 2.4.5 dice
M |= (∀x)α sii para todo a ∈ |M| M|= α[a/x]
¿quién es α en este caso? (∀y)(P(x,y) ^ (∃x)x='x)
entonces hay que hacer
(∀y)(P(x,y) ^ (∃x)x='x)[a/x]
hay que aplicar la definición de sustitución
como la variable cuantificada (y) es distinta de la variable a sustituir (x), la def 2.3.10 dice
(∀y)(P(x,y) ^ (∃x)x='x)[a/x] = (∀y)((P(x,y) ^ (∃x)x='x)[a/x])
aplicando de vuelta la def 2.3.10
(P(x,y) ^ (∃x)x='x)[a/x] = P(x,y)[a/x] ^ ((∃x)x='x)[a/x]
por def 2.3.10: P(x,y)[a/x] = P(x[a/x],y[a/x]) = [def 2.3.9] P(a,y)
¿Cómo queda ((∃x)x='x)[a/x] según la definición de sustitución?
En respuesta a Romina Romero - InCo
Re: Clausura con cuantificadores
Entonces, resumiendo pasos, da:
M |= (∀x)((∀y)(P(x,y) ^ (∃x)x='x)) <=> (Por 2.4.5) Para todo a ∈ |M| :: M |= (∀y)(P(a,y) ^ (∃x)a='a)
No?
M |= (∀x)((∀y)(P(x,y) ^ (∃x)x='x)) <=> (Por 2.4.5) Para todo a ∈ |M| :: M |= (∀y)(P(a,y) ^ (∃x)a='a)
No?