Parciales

Hola.

Observaciones:

Tenés que usar los nombres de las estructuras a las que realmente te estás refiriendo, es decir, si se llama M₁, hay que poner $M_1 \vDash \varphi_1$ y no $M \vDash \varphi$ (lo mismo con M₂).

Cuando usamos el 2.4.5 y sacamos un cuantificador para afuera, el nombre de la variable tiene que cambiar, porque ya no es la "x" que es una variable del lenguaje de primer orden (LPO), sino que es un elemento de nuestro universo, y por tanto no se puede llamar igual, porque son cosas distintas y porque sino no queda clara esa distinción. Por convención, usamos las últimas letras del alfabeto (w,x,y.z) para las variables del LPO y las primeras (a,b,c) para los elementos del universo (no es estricta, capaz que si el universo es $\Sigma^*$ resulta más natural usar $\omega$ en vez de a).

Además, los elementos pertenecen al universo de la estructura, lo que se representa poniendo barras a los lados de la estructura: |M₁| (o usando el nombre del universo, si es que tiene).

Entonces sería, por ejemplo, $\bar{\exists} a \in |M_1| : M_1 \vDash P_1(\bar{a})$ o también $\bar{\exists} a \in \mathbb{N} : M_1 \vDash P_1(\bar{a})$.

Antes de poder justificar que una sentencia se cumple (o no) para una estructura dada, hay que terminar la "traducción" desde el LPO al metalenguaje, debemos interpretar las fórmulas y los términos, hacer desaparecer el "$\vDash$" y la $M$.

Por ejemplo, en la primera parte falta este paso:

$\bar{\exists} a \in \mathbb{N} : M_1 \vDash P_1(\bar{a})$

sii [def $\vDash$, $v^{M_1}$ y $\_^{M_1}$ (def modelar fórmulas, interpretación de fórmulas e interpretación de términos)] *

$\bar{\exists} a \in \mathbb{N} : a \in \mathbb{N}$

Ahora sí tenemos algo completamente expresado en metalenguaje, y podemos decir "tomando x = 0 se cumple".

La justificación de $M_1 \vDash \varphi_3$ está mal, porque tenemos que probar un para todo, por lo que no alcanza mostrar que funciona para un ejemplo (x = y = 0). Hay que mostrar que para cualquier x va a existir un y que sea mayor o igual (podríamos decir que alcanza con tomar y = x, pero sin igualar a 0).

En la parte de $M_2 \vDash \varphi_1$, no es que el elemento sea vacío, sino que pertenezca al conjunto vacío.

Los $\lnot \exists$ es mejor sacarlos como $\forall \lnot$:

$M_2 \vDash \lnot (\exists x) (\exists y) \lnot P_2(x,y)$ sii $\bar{\forall} a \in |M_2| : M_2 \vDash \lnot (\exists y) \lnot P_2(\bar{a},y)$ sii $\bar{\forall} a, b \in |M_2| : M_2 \vDash \lnot \lnot P_2(\bar{a},\bar{b})$ sii $\bar{\forall} a, b \in |M_2| : M_2 \vDash P_2(\bar{a},\bar{b})$.

Si los sacás como $\not\bar{\exists}$, que es más bien un abuso de notación, no tiene que quedar:

$\not\bar{\exists} a,b \in |M_2| : M_2 \vDash \lnot P_2(\bar{a}, \bar{b})$, que es una abreviación de $(\not\bar{\exists} a \in |M_2|) (\not\bar{\exists} b \in |M_2|) : M_2 \vDash \lnot P_2(\bar{a}, \bar{b})$

sino

$(\not\bar{\exists} a \in |M_2|) (\bar{\exists} b \in |M_2|) : M_2 \vDash \lnot P_2(\bar{a}, \bar{b})$.

Porque:

$(\not\bar{\exists} a \in |M_2|) (\not\bar{\exists} b \in |M_2|) : M_2 \vDash \lnot P_2(\bar{a}, \bar{b})$

sii [notación]

$(NO \bar{\exists} a \in |M_2|) (NO \bar{\exists} b \in |M_2|) : M_2 \vDash \lnot P_2(\bar{a}, \bar{b})$

sii [equivalencia]

$(\bar{\forall} a \in |M_2|) NO (NO \bar{\exists} b \in |M_2|) : M_2 \vDash \lnot P_2(\bar{a}, \bar{b})$

sii [equivalencia]

$(\bar{\forall} a \in |M_2|) (\bar{\exists} b \in |M_2|) : M_2 \vDash \lnot P_2(\bar{a}, \bar{b})$

Manejar $\not \bar{\exists}$ es mucho más confuso y propenso a errores.

Lo demás se ve bien.

Saludos

* En realidad son varios pasos comprimidos, que se pueden comprimir siempre que en la justificación se incluya todo lo que se está haciendo):

$\bar{\exists} a \in \mathbb{N} : M_1 \vDash P_1(\bar{a})$

sii [def $\vDash$]

$\bar{\exists} a \in \mathbb{N} : v^{M_1} (P_1(\bar{a})) = 1$

sii [def $v^{M_1}$]

$\bar{\exists} a \in \mathbb{N} : \bar{a}^{M_1} \in \mathbb{N}$ (obs.: $P_1^{M_1} = \mathbb{N}$ )

sii [def interpretación términos]

$\bar{\exists} a \in \mathbb{N} : a \in \mathbb{N}$