Prueba de la propiedad de disyunción

Question

Estoy tratando de demostrar la propiedad de disyunción "si $\,\vdash\phi\lor\psi$ entonces $\,\vdash\phi$ o $\,\vdash\psi$ " para la lógica proposicional intuicionista.

Hasta ahora he pensado en elegir dos no-tautologías $\phi$ y $\psi$ con dos contramodelos de Kripke: $$(W, R_W, f_W)\mbox{such that}\exists (w\in W)(w\not\Vdash\phi)$$ $$(V, R_V, f_V)\mbox{such that}\exists (v\in V)(v\not\Vdash\psi)$$ Entonces crea un nuevo modelo de Kripke $(W\cup V\cup\{u\}, R, f)$ avec $R(u,w)$ y $R(u,v)$ .

Mi razonamiento es que $w\not\Vdash\phi\implies u\not\Vdash\phi$ y $v\not\Vdash\psi\implies u\not\Vdash\psi$ y por lo tanto $u\not\Vdash\phi\lor\psi$ que proporciona un contramodelo para $\phi\lor\psi$ siendo una tautología y $\phi$ y $\psi$ no siendo tautologías.

¿Es esto suficiente para ser una prueba? Para mí no está claro si añadir un mundo $u$ cambia qué frases $w$ fuerzas. Así que si añado un mundo $u$ ¿podría estar seguro de que todavía $w\not\Vdash\phi$ ?

Answer 1

Creo que tu idea de la prueba es buena.

Para añadir el mundo u, creo que si establecemos f(u) = \emptyset entonces no cambiará el hecho de que w \nVdash \phi , ya que f tiene que ser monótona, pero como ninguna variable proposicional se mantiene en u, todo puede ocurrir en su sucesor.

Creo que también hay que añadir una relación desde u a todos los sucesores de w y v, ya que debe ser transitiva ¿no?

Ahora lo estoy probando por mi cuenta, algunos otros problemas que me encontré: - ¿Qué pasa si los dominios W,V son (parcialmente) iguales? (pero las valoraciones podrían ser diferentes) ¿Cómo establecemos las valoraciones en el modelo fusionado? ¿Es una idea para fusionar copias isomórficas disjuntas para no tener este problema?

Answer 2

Sí, tu prueba funciona; sólo tienes que especificar que los dos contramodelos deben tener marcos disjuntos $\langle W_1, R_1 \rangle$ y $\langle W_2, R_2 \rangle$ .

El nuevo modelo tendrá $W = \{ w_0 \} ∪ W_1 ∪ W_2$ y la relación de accesibilidad "ampliada" será :

$xRy$ si $x=w_0$ o $xR_1y$ o $xR_2y$ .

Answer 3

\N - Sin guión \N - Textobf{Reclamación:} si $\varphi \vee \psi$ es una tautología intuicionista, entonces también lo es al menos una de $\varphi$ y $\psi$ .

\begin{proof} Suppose, for contradiction, that $\varphi \vee \psi$ is an intuitionistic tautology, but neither $\varphi$ nor $\psi$ is. Then, by definition, there exist Kripke models $(W_1,R_1,f_1)$, $(W_2,R_2,f_2)$ and states $w_1 \in W, w_2 \in W_2$ such that $(W_1,R_1,f_1),w_1 \nVdash \varphi$ and $(W_2,R_2,f_2),w_2 \nVdash \psi$. Now take the disjoint union of their isomorphic labeled copies. That is, consider $(W,R,f)$ with \begin{itemize} \item $W = W_1 \times {1} \cup W_2 \times {2}$, \item $R = {\langle (w,1),(v,1) \rangle | (w,v) \in R_1 } \cup {\langle (w,2),(v,2) \rangle | (w,v) \in R_2 }$, \item $f((w,i)) = f_i(w)$ for all $i \in {1,2}$ and $w \in W_i$. \end{itemize}

\Además, añadimos una raíz común $u$ de $(w_1,1),(w_2,2)$ al modelo, por lo que obtenemos $(W' = W \cup \{u\},R' = R \cup \{(u,u)\} \cup \{\langle u,(v_1,1) \rangle | R(w_1,1)(v_1,1)\} \cup \\ \{\langle u,(v_2,2) \rangle | R(w_2,2)(v_2,2)\}, f')$ avec $f'(w) = f(w)$ para $w \neq u$ y $f'(u)= \emptyset$ . \ para terminar con la prueba

\noindent Es sencillo comprobar que $(W',R',f')$ sigue siendo un modelo intuicionista de Kripke. $R$ sigue siendo claramente reflexivo y transitivo, y añadiendo $u$ también añadimos una flecha reflexiva y todas las flechas transitivas a los sucesores de $(w_1,1)$ y $(w_2,2)$ . Además, la monotonicidad de $f$ sigue siendo válida ya que $f(u) = \emptyset$ . Por lo tanto, si $u R' (v,i)$ , entonces debemos tener que $f(u) \subseteq f((v,i))$ . Por último, dado que los sucesores de $w_1$ , $w_2$ no se modifican, tenemos $(w,1) \nVdash \varphi$ y $(w,2) \nVdash \psi$ .

\vspace{0,3cm} \noindent Entonces se deduce que $u \nVdash \varphi$ desde $Ru(w_1,1)$ y $(w_1,1) \nVdash \varphi$ y $u \nVdash \psi$ desde $Ru(w_2,2)$ y $(w_2,2) \nVdash \psi$ . Pero entonces tenemos $u \nVdash \varphi \vee \psi$ lo que contradice nuestra suposición de que $\varphi \vee \psi$ es una tautología intuicionista.