Cálculo proposicional y lógica intuicionista

La semántica de la tabla de verdad es particular de la lógica proposicional clásica . Entonces, si el autor fuera específico, habría agregado este calificador. (Sin embargo, probablemente sea una buena regla general que si solo ve "cálculo proposicional", en la mayoría de los contextos se refieren a clásico).

Si bien “proposicional” es un descriptor que se refiere principalmente al lenguaje (en particular, la ausencia de símbolos no lógicos distintos de las letras de las oraciones), tan pronto como empezamos a hablar de sistemas de prueba o semántica, tenemos una lógica particular en mente: clásica , intuicionista, minimal, modal, etc.

En la lógica proposicional clásica, una interpretación semántica puede proporcionarse de manera más general mediante un álgebra booleana, que es un conjunto$X$con constantes$\top, \bot$, operación unaria$\lnot$y operaciones binarias$\wedge, \vee$satisfacer ciertos axiomas. El álgebra booleana prototípica 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 constantes$\top, \bot$y operaciones binarias$\wedge, \vee, \rightarrow$satisfacer ciertos axiomas. Dada un álgebra de Heyting, a menudo podemos definir$\lnot x := (x \rightarrow \bot)$; sin embargo, en un álgebra general de Heyting, algunos de los axiomas del álgebra booleana o identidades derivadas como$x \vee \lnot x = \top$,$\lnot(\lnot x) = x$, y$\lnot(x \wedge y) = (\lnot x) \vee (\lnot y)$ya no aguanta.

Un ejemplo interesante de un álgebra de Heyting que no es un álgebra booleana 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 este álgebra de Heyting, por ejemplo, si establecemos$U := \mathbb{R} \setminus \{ 0 \}$, entonces$\lnot U = (U \rightarrow \emptyset) = \operatorname{int}(\{ 0 \}) = \emptyset$, entonces$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 particular sobre$\mathbb{R}$en este ejemplo: la misma construcción funcionará para los subconjuntos abiertos de cualquier espacio topológico).

En caso de que no se sienta cómodo con la topología o el análisis real, también hay un ejemplo finito que se usa 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$viene dada por una tabla. En este álgebra de Heyting,$\lnot(\frac{1}{2}) = (\frac{1}{2} \rightarrow 0) = 0$, entonces$\frac{1}{2} \vee \lnot(\frac{1}{2}) = \frac{1}{2} \ne \top$.

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