lógica intuicionista

Question

La siguiente es una deducción clásicamente válida para cualquier propuesta$A,B,C$. $\def\imp{\rightarrow}$

$A \imp B \lor C \vdash ( A \imp B ) \lor ( A \imp C )$.

Pero estoy bastante seguro de que no es intuitivamente válido, aunque no sé cómo probarlo, que es mi primera pregunta.

Si mi conjetura es verdadera, mi siguiente pregunta es qué sucede si agregamos esta regla a la lógica intuicionista. No creo que obtengamos lógica clásica. Es mi suposición, ¿verdad?

Answer 1

Está usted familiarizado con la semántica de Kripke de intuitionistic lógica (ver aquí, la sección pertinente de la Semántica de intuitionistic lógica)?

Intuitivamente, una proposición no es interpretado como globalmente verdad o falso, sino más bien como el conjunto de " conocimientos de los estados en los que es 'conocido'. El conocimiento de los estados, pueden evolucionar, y la única restricción para la interpretación de las proposiciones es que el conocimiento no puede ser revocado.

Formalmente, tendrá que seleccionar un marco de Kripke, es decir, un conjunto $W$ equipada con un preorder $\leq$, e interpretar cualquier variable proposicional como un subconjunto de a $W$ que es cerrado bajo pasando a $\leq$-mayor de elementos. Con las interpretaciones de las variables proposicionales fijo, interpretar $\lor$ $\land$ como la unión y la intersección respectivamente. También, usted puede interpretar $\bot$ ya que ninguno de $W$ (el conjunto vacío) y $\top$ como todos los de $W$. La parte interesante es la interpretación de la implicación: Si $\psi$ $\phi$ son interpretados como $A,B\subset W$, $\psi\imp\phi$ se interpreta como el conjunto de los estados $w\in W$ tal que para cualquier $v\in W$$w\leq v$$v\in A$, también ha $v\in B$. Apelando a la intuición de nuevo, significa que sin embargo el conocimiento evoluciona, siempre que $\psi$ es conocido lo es $\phi$. Por ejemplo, $\neg\neg\phi \equiv ( \phi \imp \bot ) \imp \bot$ es conocido en $w$ precisamente si por cualquier $v\in W$ $w\leq v$ hay $z\in W$ $w\leq z$ tal que $\phi$ mantiene en $z$ - en otras palabras, nunca se puede refutar $\phi$. Esto es mucho más débil que la afirmación de que $\phi$ tiene para todos los de $W$, como se puede ver, por ejemplo, en el ejemplo al final del post, donde $W = \{0\to 1\}$.

De todos modos, la semántica de Kripke es el sonido para intuitionistic lógica, por lo que para demostrar que una fórmula es no un intuitionistic tautología, es suficiente para proporcionar algunos Kripke marco con una interpretación de las fórmulas " proposicional variables que la asociada a la interpretación no es cierto en todo el marco de Kripke.

Vamos a hacer esto para $(A\imp (B\lor C))\imp ((A\imp B)\lor (A\imp C))$: Considerar el marco de $1\leftarrow 0\rightarrow 2$ e interpretar $A$ como se conoce sólo en $1,2$, $B$ como es conocido sólo en $1$ $C$ como se conoce sólo en $2$. A continuación, $A\imp B$ $A\imp C$ son ambos no se conoce en la $0$, ya que hay una evolución que valida $A$ pero no validar $B$ (de manera similar $C$). Sin embargo, $A\imp (B\lor C)$ es válido en $0$, ya que para cualquier evolución de $0$ a $1$ o $2$, $B$ o $C$ es válido en el nuevo estado.

Respecto a su segunda pregunta: Un ejemplo como el anterior sólo puede existir si el marco de $W$ bajo consideración tiene ramas; si, por el contrario, la evolución es único significado formalmente que para cualquiera de los tres elementos de la $u,v,w$ en el marco de la satisfacción de $u\leq v$$u\leq w$, tendremos a $v\leq w$ o $w\leq v$ - la fórmula $(A\imp (B\lor C))\imp ((A\imp B)\lor (A\imp C))$ hecho se mantenga bajo cualquier interpretación.

Por lo tanto, si usted agregue $(A\imp (B\lor C))\imp ((A\imp B)\lor (A\imp C))$ como un axioma para intuitionistic lógica, usted todavía va a tener el sonido semántica de Kripke cuando la restricción para marcos con singular evolución. Por lo tanto, para comprobar que una fórmula no es una tautología con respecto a este más fuerte de cálculo, basta con encontrar una interpretación de tal forma exclusiva evolución de la trama que no da validez a la fórmula. Para $\neg \neg A$, se puede elegir el marco de $W = \{0\to 1\}$ e interpretar $A$ al $1$, pero se desconoce en $0$: a Continuación, $\neg\neg A$ es conocida a nivel mundial (véase más arriba), sino $A$ no lo es. Por lo tanto, $\neg \neg A \imp A$ no es una tautología en la mejora del cálculo, y por lo tanto la mayor cálculo es todavía estrictamente contenida en la clásica lógica proposicional.