Positive Instantial Neighbourhood logic

Este artículo introduce la Lógica de Vecindad Instancial Positiva (PINL), un sistema modal libre de negación con modalidades de caja y diamante independientes, y establece su completitud mediante semántica de vecindad persistente, semántica algebraica utilizando 2-DLIos y una representación bitopológica canónica.

Lo esencial

Imagina que eres un detective intentando comprender una ciudad misteriosa llamada Mundo. En esta ciudad, cada persona (o "mundo") tiene un Vecindario personal.

En la lógica tradicional, un detective podría preguntar: "¿Sigue las reglas todos en este vecindario?" o "¿Hay al menos una persona aquí que rompió las reglas?".

Este artículo introduce una forma nueva y más detallada de investigar estos vecindarios, llamada Lógica de Vecindarios Instantiales Positivos (PINL, por sus siglas en inglés). Así es como funciona, desglosada en conceptos simples:

1. La regla de "No Negación" (El giro positivo)

Normalmente, los detectives usan el "No" y el "No es el caso que" para resolver casos. Por ejemplo, "No es el caso que todos sean inocentes".
Sin embargo, este artículo decide prohibir la palabra "No". Los detectives solo pueden decir lo que es verdad, no lo que no es.

• La analogía: Imagina que estás describiendo una cesta de frutas. Puedes decir: "Hay una manzana" o "Hay un plátano". Pero no puedes decir: "No hay una naranja". Solo puedes describir lo que realmente está presente.
• El resultado: Debido a que no pueden usar el "No", las dos herramientas principales del detective —el Cuadro (que verifica si todos en un grupo hacen algo) y el Diamante (que verifica si alguien en un grupo hace algo)— se convierten en dos herramientas completamente separadas. Ya no pueden usarse para definirse el uno al otro.

2. Las dos herramientas especiales: El Cuadro y el Diamante

En esta nueva lógica, los detectives usan dos lentes especiales para observar un vecindario:

• La Lente del Cuadro (□): Esta lente pregunta: "¿Existe un grupo específico de personas en este vecindario donde todos siguen la regla principal, y individuos específicos también están presentes para probar que existen?"
  • Ejemplo: "¿Existe un grupo de personas donde todos llevan sombrero (la regla principal), y específicamente, hay una persona alta y una persona baja en ese grupo?"
• La Lente del Diamante (♢): Esta lente pregunta: "¿Es verdad que para cada grupo posible que pudiéramos elegir, o bien el grupo está compuesto enteramente por personas que rompen una regla específica, O el grupo contiene al menos a una persona que sigue la regla principal?"
  • Ejemplo: "No importa qué grupo de personas elijas, o bien son todos mentirosos, o al menos uno de ellos dice la verdad".

3. El problema con el mapa "Estándar"

Los autores intentaron construir un mapa perfecto (un "modelo canónico") de esta ciudad usando estas reglas. Pero se toparon con un obstáculo.

• El fallo (Glitch): En el mapa estándar, los vecindarios son simplemente listas sin etiquetar de personas. Si una lista de personas encaja con la descripción de la herramienta del "Cuadro", el mapa podría accidentalmente usar esa misma lista para satisfacer la herramienta del "Diamante", incluso si no debería. Es como usar una foto de una "Persona Alta" para probar que existe una "Persona Baja" solo porque están en la misma foto.
• La solución: Para resolver esto, los autores crearon un Mapa Tipado. En lugar de ser solo una lista de personas, cada vecindario en el mapa viene con una Etiqueta.
  • La analogía: Imagina que cada grupo de personas en la ciudad tiene una etiqueta con su nombre. Un grupo está etiquetado como "Grupo para la herramienta del Cuadro", y otro como "Grupo para la herramienta del Diamante". Esto evita que el detective se confunda y use el grupo equivocado para el trabajo equivocado.

4. El "Libro de Recetas" Algebraico

El artículo también traduce estas reglas lógicas en un "Libro de Recetas" matemático llamado 2-DLIO.

• Piensa en esto como un libro de cocina donde los ingredientes son enunciados lógicos.
• El libro tiene dos conjuntos de instrucciones (recetas): un conjunto para los ingredientes del Cuadro y un conjunto para los ingredientes del Diamante.
• Los autores demostraron que si sigues las reglas de su lógica (PINL), esencialmente estás siguiendo las reglas de este Libro de Recetas específico. Mostraron que el "Álgebra de Lindenbaum" (que es solo una forma elegante de decir "la colección de todas las posibles recetas lógicas") encaja perfectamente en este libro.

5. El Mapa Final: La Ciudad Bitopológica

Finalmente, los autores construyeron una versión grandiosa y final del mapa de la ciudad llamada Espacio Bitopológico.

• Este mapa tiene dos capas de geografía:
  1. Una Capa Positiva (que muestra dónde están las cosas).
  2. Una Capa Negativa (que muestra dónde no están las cosas, pero descritas sin usar la palabra "No"; en su lugar, describe la "contra-teoría" o la lista de cosas que fallaron).
• El gran logro: Demostraron que el "Libro de Recetas" (el álgebra) y este "Mapa de la Ciudad de dos capas" (la topología) son en realidad lo mismo, vistos desde ángulos diferentes. Si conoces las recetas, puedes construir la ciudad, y si miras la ciudad, puedes leer las recetas.

Resumen

Este artículo crea una nueva versión de la lógica de sistemas de vecindarios que no utiliza la negación ("No-Negation"). Resuelve un problema complicado donde las dos herramientas principales (Cuadro y Diamante) se confunden mediante la construcción de un mapa "tipado" y etiquetado. Luego demuestra que este sistema lógico es matemáticamente sólido al mostrar que coincide perfectamente con un tipo específico de libro de recetas algebraicas y un mapa de ciudad de dos capas.

Lo que este artículo NO hace:

• No aplica esto a sistemas informáticos del mundo real, diagnósticos médicos o casos legales.
• No afirma resolver el problema de la "dualidad" por completo (lo llama un "primer paso" hacia una teoría futura).
• No combina las herramientas del Cuadro y del Diamante en una sola herramienta; las mantiene separadas por ahora.

Resumen técnico

Resumen Técnico: Lógica de Vecindad Instancial Positiva (PINL)

Planteamiento del Problema
La Lógica de Vecindad Instancial (INL) es un lenguaje modal diseñado para marcos de vecindad, que permite que las fórmulas expresen no solo condiciones de alcance universal, sino también información existencial sobre "tipos de mundos" (instancias) que ocurren dentro de una vecindad. Si bien la INL clásica y su dualidad coalgebraica (que involucra Álgebras Booleanas con Operadores Instanciales, o BAIOs) están bien desarrolladas, existe una laguna en la literatura respecto a una versión sistemática y positiva (libre de negación) de esta lógica.

La ausencia de la negación clásica en la lógica positiva impide la interdefinibilidad de los operadores caja ($\Box$) y diamante ($\Diamond$). Por consiguiente, una versión positiva de la INL no puede tratarse meramente como un fragmento de la INL clásica; requiere un sistema de prueba distinto, una semántica de vecindad positiva adecuada, una semántica algebraica basada en retículos distributivos y una representación canónica. El artículo aborda la falta de estos componentes fundacionales para una lógica de vecindad instancial positiva y de dos lados.

Metodología
Los autores desarrollan la lógica, denominada Lógica de Vecindad Instancial Positiva (PINL), a través de un enfoque multifacético que combina teoría de la prueba, teoría de modelos, álgebra y topología:

1. Sintaxis y Sistema de Prueba: El lenguaje de la PINL se construye sobre una base proposicional de retículos distributivos acotados (usando $\top, \bot, \land, \lor$) en lugar de la lógica proposicional clásica. Introduce dos modalidades instanciales primitivas e independientes: una de tipo caja $\Box(\phi_1, \dots, \phi_n; \psi)$ y una de tipo diamante $\Diamond(\phi_1, \dots, \phi_n; \psi)$. Se formula un sistema de prueba basado en secuentes con axiomas para retículos distributivos acotados y axiomas modales específicos para $\Box$ y $\Diamond$ que reflejan su naturaleza independiente.
2. Semántica (Modelos de Dos Lados Persistentes): La lógica se interpreta sobre modelos de vecindad de dos lados persistentes. Estas estructuras consisten en un conjunto parcialmente ordenado $(W, \leq)$ y dos funciones de vecindad, $N_\Box$ y $N_\Diamond$, que mapean mundos a conjuntos de aumentos (upsets). Crucialmente, $N_\Box$ es monótona ascendente (preserva el orden), mientras que $N_\Diamond$ es monótona descendente. La verdad se define mediante condiciones de testigo para $\Box$ (existencia de una vecindad que satisfaga las fórmulas de alcance e instancia) y condiciones de co-testigo para $\Diamond$ (satisfacción universal de una disyunción de condiciones).
3. Construcción Canónica y Semántica Tipada: Una prueba de completitud canónica directa para la semántica persistente estándar se ve obstruida por la naturaleza extensional de las vecindades (los aumentos sin etiquetar pueden accidentalmente dar testimonio de múltiples fórmulas). Para superar esto, los autores introducen una semántica de vecindad persistente tipada auxiliar. En este entorno, las vecindades están etiquetadas por la fórmula modal específica que pretenden testimoniar o refutar. Se establece un Lema de Verdad para este modelo tipado, demostrando que la verdad semántica coincide con la membresía en el componente positivo del par primo.
4. Semántica Algebraica (2-DLIOs): El artículo introduce los 2-DLIOs (retículos distributivos acotados equipados con dos familias de operaciones instanciales, $(f_n)$ para $\Box$ y $(g_n)$ para $\Diamond$) como el contraparte algebraica. Se demuestra que el álgebra de Lindenbaum de la PINL es un 2-DLIO.
5. Representación Bitopológica: Los autores construyen un espacio PINL bitopológico canónico derivado de los pares de teorías primas. Este espacio está equipado con dos topologías ($\tau_+$ generada por conjuntos de membresía positivos $U_\phi$ y $\tau_-$ generada por conjuntos de membresía negativos $V_\phi$). Se demuestra que el álgebra de los abiertos positivos admisibles en este espacio es isomórfica al 2-DLIO de Lindenbaum.

Contribuciones Clave y Resultados

• Sistema Formal: Definición del lenguaje y un sistema de prueba completo para la PINL, tratando a $\Box$ y $\Diamond$ como primitivas independientes con esquemas de axiomas distintos.
• Completitud: Prueba de corrección y completitud de la PINL con respecto a modelos de vecindad de dos lados persistentes. Esto se logra mediante la semántica tipada auxiliar, que resuelve las dificultades técnicas de la construcción canónica en ausencia de negación.
• Caracterización Algebraica: Introducción de los 2-DLIOs como la semántica algebraica para la PINL. El artículo prueba la corrección y completitud algebraica, demostrando que el álgebra de Lindenbaum de la PINL es un 2-DLIO.
• Representación Canónica: Construcción del espacio bitopológico canónico de la PINL. El artículo demuestra que el álgebra de los abiertos positivos admisibles de este espacio es isomórfica al 2-DLIO de Lindenbaum. Esto proporciona una representación canónica de abiertos admisibles de la lógica.
• Separación de Preocupaciones: El trabajo aísla explícitamente el fragmento de lógica positiva e de operadores independientes de la INL, distinguiéndolo del marco booleano clásico y del marco completo de DLIO donde podrían existir axiomas de interacción.

Significado y Alcance
El artículo afirma proporcionar el primer desarrollo sistemático de una versión positiva y libre de negación de la lógica de vecindad instancial. Llena una laguna específica en la literatura al establecer el sistema de prueba, la semántica y los fundamentos algebraicos para esta lógica.

Los autores declaran explícitamente que el alcance se limita a un teorema de representación canónica, no a un teorema de dualidad categórica completo. Si bien el trabajo sienta las bases para una futura teoría de dualidad (específicamente una dualidad de tipo Priestley o bitopológica para los 2-DLIOs), el presente artículo no define la categoría necesaria de espacios PINL descriptivos, morfismos o tratamientos funcionales. Del mismo modo, el artículo señala que una versión "geométrica" de la INL (que involucra la continuidad de Scott) es sugerida por la literatura pero se deja para trabajos futuros.

La importancia radica en el puente entre la lógica modal positiva, la semántica de vecindad y la teoría de retículos distributivos, ofreciendo un marco riguroso para razonar sobre propiedades instanciales sin la negación clásica, y proporcionando las herramientas algebraicas y topológicas necesarias para futuras investigaciones de dualidad.