¿Se puede geometrizar significativamente la lógica?

Question

Ya he hecho esta pregunta en philosophy.stackexchange, espero una respuesta diferente aquí:

Descartes ha sido elogiado por unir la geometría y el álgebra, y su logro permitió la invención del cálculo por Leibniz y Newton y permitió su desarrollo eficaz y explosivo por matemáticos y físicos posteriores en contraste con los pasos rudimentarios y primitivos dados por Arquímedes en la integración y la escuela Keralan en series de potencias.

Ahora, varias lógicas proposicionales pueden ser algebraizadas:

lógica proposicional clásica -> álgebras booleanas

lógica proposicional intuicionista -> álgebras Heyting

lógica modal -> álgebras modales

La pregunta: ¿existe una forma geométrica significativa de estas lógicas? Significativa, simplemente en no ser solo una traducción a forma geométrica, como en los Diagramas de Venn para álgebras booleanas (siendo representadas primero como algún sistema de conjuntos), sino que permita decir algo más profundo sobre la lógica en sí misma?

Por supuesto, existe la representación de Stone para una Álgebra Booleana, ¿pero qué dice significativamente sobre la lógica?

Answer 1

Una dirección que podrías explorar está trazada, por ejemplo, por Sheaves in Geometry and Logic: A First Introduction to Topos Theory (Springer, 1992) de Saunders Mac Lane e Ieke Moerdijk. Su Prólogo comienza

Un aspecto sorprendente de la teoría de tópos es que unifica dos temas matemáticos aparentemente completamente diferentes: por un lado, la topología y la geometría algebraica, y por el otro, la lógica y la teoría de conjuntos. De hecho, un tópos se puede considerar tanto como un "espacio generalizado" como como un "universo generalizado de conjuntos" ...

Otra dirección que podrías explorar es la Teoría de Tipos Homotópica: aquí tienes un artículo introductorio de Steve Awodey: http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf Sus palabras iniciales son

El propósito de este artículo de encuesta informal es introducir al lector a una conexión nueva y sorprendente entre Geometría, Álgebra y Lógica, que recientemente ha salido a la luz en forma de una interpretación de la teoría de tipos constructiva de Per Martin-Löf en la teoría de homotopía, ...

Entonces, esos son dos puntos iniciales hacia áreas donde realmente se hacen conexiones profundas entre geometría y lógica.

Pero - ¡y es realmente un gran "pero"! - estas son investigaciones matemáticas a un nivel de sofisticación y dificultad conceptuales que van mucho más allá de las lógica matemática introductoria. ¿Existen enlaces más elementales entre geometría y lógica, a un nivel de sofisticación/dificultad comparable al material en un texto estándar de lógica como el de Enderton o van Dalen, por ejemplo? Esa es una pregunta interesante, pero nada me viene inmediatamente a la mente ...