Cálculo proposicional y lógica intuicionista

Question

Como nunca he estado muy expuesto a la lógica matemática formal, he decidido embarcarme en una búsqueda para rectificar esto; desafortunadamente, habiendo estado expuesto a los conceptos de la Lógica Intuicionista a través de mis incursiones en la programación funcional, me encuentro con problemas para entender "cómo encaja todo".

Estoy familiarizado con la noción de rechazar la ley del medio excluido (LEM); por lo poco que sé de la lógica intuicionista, entiendo que esto se hace en el sentido de que la LEM no se trata como un axioma dentro de cualquier sistema deductivo que se utilice. Sin embargo, mirando los tratamientos del cálculo proposicional dentro de casi cualquier texto que pueda tener en mis manos, encuentro que después de una discusión de la sintaxis de una lógica de orden zerótico, el autor empieza a hablar de "semántica", en muchos casos ilustrando esto con tablas de verdad.

En este punto me encuentro con un problema, porque claramente la semántica presentada por ejemplo en Goldrei (Propositional and Predicate Calculus: A Model of Argument) significa que LEM es una tautología.

Al presentar "la semántica del cálculo proposicional", ¿el autor está presentando de hecho una "lógica" específica (es decir, la lógica clásica), o son estas semánticas una parte fundamental de cualquier cálculo proposicional? Me parece que esto último no puede ser cierto (ya que la lógica proposicional intuicionista existe definitivamente), pero no encuentro un texto introductorio en el que el autor aborde esta cuestión.

Es probable que esté cayendo en la trampa de que un poco de conocimiento es algo peligroso y es muy posible que todo lo que creo saber sobre esto esté equivocado, pero actualmente me encuentro incapaz de pasar de este punto sin tener serias dudas sobre a qué se refiere realmente lo que estoy leyendo.

Answer 1

La semántica de la tabla de verdad es particular para clásico lógica proposicional. Así que si el autor estuviera siendo específico, habría añadido este calificativo. (Sin embargo, es probablemente una buena regla general que si sólo ves "cálculo proposicional", en la mayoría de los contextos se están refiriendo a la clásica).

Mientras que "proposicional" es un descriptor que se refiere principalmente al lenguaje (en particular, a la ausencia de símbolos no lógicos distintos de las letras de la frase), en cuanto empezamos a hablar de sistemas de prueba o de semántica, tenemos en mente una lógica particular: clásica, intuicionista, mínima, modal, etc.

Answer 2

En la lógica proposicional clásica, una interpretación semántica puede ser proporcionada más generalmente por un álgebra booleana, que es un conjunto $X$ con las constantes $\top, \bot$ Operación unitaria $\lnot$ y operaciones binarias $\wedge, \vee$ que satisface ciertos axiomas. El prototipo de álgebra booleana es $\{ T, F \}$ con las interpretaciones obvias.

En la lógica proposicional intuicionista, la construcción correspondiente es un álgebra de Heyting, que es un conjunto $X$ con las constantes $\top, \bot$ y operaciones binarias $\wedge, \vee, \rightarrow$ que satisface ciertos axiomas. Dado un álgebra de Heyting, a menudo podemos definir $\lnot x := (x \rightarrow \bot)$ Sin embargo, en un álgebra de Heyting general, algunos de los axiomas del álgebra de Boole o las identidades derivadas, como $x \vee \lnot x = \top$ , $\lnot(\lnot x) = x$ y $\lnot(x \wedge y) = (\lnot x) \vee (\lnot y)$ ya no se sostiene.

Un ejemplo interesante de un álgebra de Heyting que no es un álgebra de Boole es si $X$ es el conjunto de subconjuntos abiertos de $\mathbb{R}$ con $\top := \mathbb{R}$ , $\bot := \emptyset$ , $U \wedge V := U \cap V$ , $U \vee V := U \cup V$ y $U \rightarrow V := \operatorname{int}((\mathbb{R} \setminus U) \cup V)$ . En esta álgebra de Heyting, por ejemplo, si ponemos $U := \mathbb{R} \setminus \{ 0 \}$ entonces $\lnot U = (U \rightarrow \emptyset) = \operatorname{int}(\{ 0 \}) = \emptyset$ Así que $U \vee \lnot U = \mathbb{R} \setminus \{ 0 \} \neq \top$ y $\lnot (\lnot U) = \mathbb{R} \ne U$ . (Por supuesto, no hay nada especial en $\mathbb{R}$ en este ejemplo: la misma construcción funcionará para los subconjuntos abiertos de cualquier espacio topológico).

En caso de que no te sientas cómodo con la topología o el análisis real, también hay un ejemplo finito que se utiliza a menudo: $X := \{ 0, \frac{1}{2}, 1 \}$ ; $\top := 1$ ; $\bot := 0$ ; $x \vee y := \max(x,y)$ ; $x \wedge y := \min(x,y)$ y $x \rightarrow y$ está dada por una tabla. En esta álgebra de Heyting, $\lnot(\frac{1}{2}) = (\frac{1}{2} \rightarrow 0) = 0$ Así que $\frac{1}{2} \vee \lnot(\frac{1}{2}) = \frac{1}{2} \ne \top$ .

Answer 3

¿Qué autor está leyendo? El autor puede estar refiriéndose a la semántica en el contexto de la teoría de las categorías y la teoría de los tipos, donde varias nociones de igualdad en la teoría de los tipos tienen la misma propiedad estructural en la teoría de las categorías que son varias nociones de semántica.