Lógica geométrica

En lógica matemática, la lógica geométrica es una generalización infinitaria de la lógica coherente , una restricción de la lógica de primer orden debida a Skolem que es demostrable teóricamente . La lógica geométrica es capaz de expresar muchas teorías matemáticas y tiene estrechas conexiones con la teoría de topos .

Una teoría de la lógica de primer orden es geométrica si se puede axiomatizar utilizando sólo axiomas de la forma donde I y J son colecciones disjuntas de fórmulas índices de que cada una puede ser infinita y las fórmulas φ son átomos o negaciones de átomos. ^{[ cita requerida ]} Si todos los axiomas son finitos (es decir, para cada axioma, tanto I como J son finitos), la teoría es coherente. ${\displaystyle \bigwedge _{i\in I}\phi _{i,1}\vee \dots \vee \phi _{i,n_{i}}\implies \bigvee _{j\in J}\phi _{j,1}\vee \dots \vee \phi _{j,m_{j}}}$

Toda teoría de primer orden tiene una extensión conservadora coherente. ^{[ cita requerida ]}

Dyckhoff y Negri (2015) enumeran ocho consecuencias del teorema anterior que explican su importancia (omitiendo notas a pie de página y la mayoría de las referencias): ^[1]

1. En el contexto de un cálculo secuencial como G3c, las implicaciones coherentes especiales como axiomas pueden convertirse directamente en reglas de inferencia sin afectar la admisibilidad de las reglas estructurales (debilitamiento, contracción y corte);
2. En términos similares, las teorías coherentes son “las teorías expresables mediante reglas de deducción natural en una cierta forma simple en la que sólo las fórmulas atómicas juegan un papel crítico”;
3. Las implicaciones coherentes forman consecuentes que dan una clase de Glivenko. En este caso, el resultado, conocido como el teorema de Barr de primer orden, establece que si cada I i: 0≤i≤n es una implicación coherente y el consecuente I 1, . . . , I n ⇒ I 0 es demostrable clásicamente, entonces es demostrable intuicionistamente;
4. Hay muchos ejemplos de teorías coherentes/geométricas: todas las teorías algebraicas, como la teoría de grupos y la teoría de anillos, todas las teorías esencialmente algebraicas, como la teoría de categorías, la teoría de campos, la teoría de anillos locales, la teoría de redes, la geometría proyectiva, la teoría de anillos locales separados y cerrados (también conocidos como “anillos locales estrictamente henselianos”) y la teoría infinitaria de grupos abelianos de torsión;
5. Las teorías coherentes/geométricas se preservan mediante el retroceso a lo largo de morfismos geométricos entre topos (Maclane y Moerdijk 1992, capítulo X);
6. Los colimites filtrados en el conjunto de modelos de una teoría coherente T son también modelos de T;
7. Las implicaciones coherentes especiales ∀x. C ⊃ D generalizan las cláusulas de Horn de la programación lógica , donde se requiere que D sea un átomo; de hecho, generalizan las “cláusulas” de los programas lógicos disyuntivos, donde se permite que D sea una disyunción de átomos.
8. La demostración eficaz de teoremas para teorías coherentes se puede automatizar con relativa facilidad y claridad (en relación con la resolución). Como señalan Bezem et al... la ausencia de skolemización (introducción de nuevos símbolos de función) no supone una dificultad real, y la no conversión a la forma clausal permite conservar mejor la estructura de los argumentos matemáticos ordinarios.

• Dyckhoff, Roy; Negri, Sara (2015), "Geometrización de la lógica de primer orden", Bulletin of Symbolic Logic , 21 (2): 123–163, doi :10.1017/bsl.2015.7, hdl : 10023/6818
• Johnstone, Peter (2002), Bocetos de un elefante: un compendio de teoría topos , Oxford University Press, ISBN 978-0-19-852496-0, Zbl1071.18002 ​(Dos volúmenes, Oxford Logic Guides 43 y 44, tercer volumen en preparación)
• Maclane, Saunders Mac; Moerdijk, Ieke (1992), Haces en geometría y lógica , Springer: Berlín, doi :10.1007/978-1-4612-0927-0, ISBN 978-1-4612-0927-0

• "¿Por qué una teoría geométrica se llama "geométrica"?". Stack Exchange . 15 de noviembre de 2020.