Positive Instantial Neighbourhood logic

Dit artikel introduceert de Positive Instantial Neighbourhood Logic (PINL), een negatievrije modale logica met onafhankelijke box- en diamond-modaliteiten, en vestigt de volledigheid ervan via persistente buurtsemantiek, algebraïsche semantiek met behulp van 2-DLIos, en een canonieke bitopologische representatie.

De kern

Stel je voor dat je een detective bent die probeert een mysterieuze stad genaamd World te begrijpen. In deze stad heeft elke persoon (of "wereld") een persoonlijke Buurt.

In de traditionele logica zou een detective vragen: "Volgt iedereen in deze buurt de regels?" of "Is er tenminste één persoon hier die de regels heeft overtreden?"

Dit artikel introduceert een nieuwe, meer gedetailleerde manier om deze buurten te onderzoeken, genaamd Positive Instantial Neighbourhood Logic (PINL). Zo werkt het, uiteengezet in eenvoudige concepten:

1. De "Geen Negatie" Regel (De Positieve Twist)

Normaal gesproken gebruiken detectives "Nee" en "Niet" om zaken op te lossen. Bijvoorbeeld: "Het is niet zo dat iedereen onschuldig is."
Echter, dit artikel besluit het woord "Nee" te verbieden. De detectives kunnen alleen zeggen wat wel waar is, niet wat niet zo is.

• De Analogie: Stel je voor dat je een fruitmand beschrijft. Je kunt zeggen: "Er is een appel," of "Er is een banaan." Maar je kunt niet zeggen: "Er is geen sinaasappel." Je kunt alleen beschrijven wat er daadwerkelijk aanwezig is.
• Het Resultaat: Omdat ze geen "Nee" kunnen gebruiken, worden de twee belangrijkste instrumenten van de detective — de Box (die controleert of iedereen in een groep iets doet) en de Diamond (die controleert of iemand in een groep iets doet) — twee volledig gescheiden instrumenten. Ze kunnen niet langer worden gebruikt om elkaar te definiëren.

2. De Twee Speciale Instrumenten: De Box en De Diamond

In deze nieuwe logica gebruiken de detectives twee speciale lenzen om naar een buurt te kijken:

• De Box Lens (□): Deze lens vraagt: "Is er een specifieke groep mensen in deze buurt waar iedereen de hoofdregel volgt, en zijn er ook specifieke individuen aanwezig om hun bestaan te bewijken?"
  • Voorbeeld: "Is er een groep mensen waar iedereen een hoed draagt (de hoofdregel), en zijn er specifiek een lange persoon en een korte persoon in die groep?"
• De Diamond Lens (♢): Deze lens vraagt: "Is het waar dat voor elke mogelijke groep die we zouden kunnen kiezen, ofwel de groep volledig bestaat uit mensen die een specifieke regel overtreden, ofwel de groep bevat tenminste één persoon die de hoofdregel volgt?"
  • Voorbeeld: "Noot welke groep mensen je ook kiest, of ze zijn allemaal leugenaars, of tenminste één van hen spreekt de waarheid."

3. Het Probleem met de "Standaard" Kaart

De auteurs probeerden een perfecte kaart (een "canonieke model") van deze stad te bouwen met behulp van deze regels. Maar ze liepen tegen een probleem aan.

• De Glitch: In de standaard kaart zijn buurten simpelweg ongelabelde lijsten van mensen. Als een lijst mensen voldoet aan de beschrijving voor de "Box"-tool, kan de kaart per ongeluk diezelfde lijst gebruiken om de "Diamond"-tool te bevredigen, zelfs als dat niet zou moeten. Het is alsof je een foto van een "Lang Persoon" gebruikt om te bewijzen dat een "Korte Persoon" bestaat, simpelweg omdat ze in dezelfde foto zitten.
• De Fix: Om dit op te lossen, hebben de auteurs een Typed Map (getypeerde kaart) gemaakt. In plaats van alleen een lijst met mensen, komt elke buurt op de kaart met een Label.
  • De Analogie: Stel je voor dat elke groep mensen in de stad een naamkaartje heeft. Eén groep is gelabeld als "Groep voor de Box Tool", en een andere groep is gelabeld als "Groep voor de Diamond Tool". Dit voorkomt dat de detective in de war raakt en de verkeerde groep voor de verkeerde taak gebruikt.

4. Het Algebraïsche "Receptenboek"

Het artikel vertaalt deze logische regels ook naar een wiskundig "Receptenboek" genaamd een 2-DLIO.

• Denk aan dit als een kookboek waarin de ingrediënten logische stellingen zijn.
• Het boek heeft twee sets instructies (recepten): één set voor de Box-ingrediënten en één set voor de Diamond-ingrediënten.
• De auteurs hebben bewezen dat als je de regels van hun logica (PINL) volgt, je in essentie de regels van dit specifieke Receptenboek volgt. Ze hebben aangetoond dat de "Lindenbaum Algebra" (wat gewoon een chique manier is om te zeggen: "de verzameling van alle mogelijke logische recepten") perfect in dit boek past.

5. De Finale Kaart: De Bitopologische Stad

Ten slotte hebben de auteurs een grandioze, finale versie van de stadskaart gebouwd: een Bitopologische Ruimte.

• Deze kaart heeft twee lagen geografie:
  1. Een Positieve Laag (die laat zien waar dingen zijn).
  2. Een Negatieve Laag (die laat zien waar dingen niet zijn, maar dat beschreven zonder het woord "Nee" te gebruiken — in plaats daarvan beschrijven ze de "tegentheorie" of de lijst van dingen die mislukten).
• De Grote Prestatie: Ze hebben bewezen dat het "Receptenboek" (de algebra) en deze "Twee-Lagen Stadkaart" (de topologie) eigenlijk hetzelfde zijn, slechts vanuit verschillende hoeken bekeken. Als je de recepten kent, kun je de stad bouwen, en als je naar de stad kijkt, kun je de recepten lezen.

Samenvatting

Dit artikel creëert een nieuwe, "Geen-Negatie" versie van een logisch systeem voor buurten. Het lost een lastig probleem op waarbij de twee belangrijkste instrumenten (Box en Diamond) in de war raken door een gelabelde, "getypeerde" kaart te bouwen. Het bewijst vervolgens dat dit logische systeem wiskundig solide is door aan te tonen dat het perfect overeenkomt met een specifiek type algebraïsch receptenboek en een twee-lagen stadskaart.

Wat het papier NIET doet:

• Het past dit niet toe op echte computersystemen, medische diagnoses of juridische zaken.
• Het beweert niet de "dualiteit"-problematiek volledig op te lossen (het noemt dit een "eerste stap" naar een toekomstige theorie).
• Het combineert de Box en Diamond instrumenten niet tot één enkel instrument; het houdt ze voor nu gescheiden.

Technische samenvatting

Technische Samenvatting: Positive Instantial Neighbourhood Logic (PINL)

Probleemstelling
Instantial Neighbourhood Logic (INL) is een modale taal ontworpen voor buurtframes (neighbourhood frames), die het mogelijk maakt om formules niet alleen universele reikwijdtevoorwaarden uit te drukken, maar ook existentiële informatie over specifieke "soorten werelden" (instanties) die binnen een buurt voorkomen. Hoewel klassieke INL en de bijbehorende coalgebraische dualiteit (betrokken bij Boolean Algebras met Instantial Operators, of BAIO's) goed ontwikkeld zijn, bestaat er in de literatuur een gat wat betreft een systematische, positieve (negatievrije) versie van deze logica.

De afwezigheid van klassieke negatie in positieve logica verhindert de interdefinieerbaarheid van de box ($\Box$) en diamond ($\Diamond$) operatoren. Bijgevolg kan een positieve versie van INL niet louter worden behandeld als een fragment van klassieke INL; het vereist een afzonderlijk bewijssysteem, een geschikte positieve buurtsemantiek, een algebraïsche semantiek gebaseerd op distributieve lettertypen, en een canonieke representatie. Dit artikel adresseert het gebrek aan deze fundamentele componenten voor een positieve, tweezijdige instantial neighbourhood logic.

Methodologie
De auteurs ontwikkelen de logica, aangeduid als Positive Instantial Neighbourhood Logic (PINL), via een veelzijdige aanpak die bewijsleer, modeltheorie, algebra en topologie combineert:

1. Syntaxis en Bewijssysteem: De taal van PINL wordt geconstrueerd over een propositionele basis van begrensde distributieve lettertypen (met behulp van $\top, \bot, \land, \lor$) in plaats van klassieke propositionele logica. Het introduceert twee primitieve, onafhankelijke instantiale modaliteiten: een box-type $\Box(\phi_1, \dots, \phi_n; \psi)$ en een diamond-type $\Diamond(\phi_1, \dots, \phi_n; \psi)$. Een sequentieel bewijssysteem wordt geformuleerd met axioma's voor begrensde distributieve lettertypen en specifieke modale axioma's voor $\Box$ en $\Diamond$ die hun onafhankelijke aard reflecteren.
2. Semantiek (Persistente Tweezijdige Modellen): De logica wordt geïnterpreteerd over persistente tweezijdige buurtmodellen. Deze structuren bestaan uit een gedeeltelijk geordende verzameling $(W, \leq)$ en twee buurtfuncties, $N_\Box$ en $N_\Diamond$, die werelden mappen naar verzamelingen van upsets. Cruciaal is dat $N_\Box$ monotoon opwaarts is (behoudt de orde), terwijl $N_\Diamond$ monotoon neerwaarts is. Waarheid wordt gedefinieerd via getuigen-voorwaarden (witness conditions) voor $\Box$ (het bestaan van een buurt die de scope- en instantieformules bevredigt) en co-getuigen-voorwaarden (co-witness conditions) voor $\Diamond$ (universele voldoening van een disjunctie van voorwaarden).
3. Canonieke Constructie en Getypeerde Semantiek: Een directe canonieke volledigheidsbewijsvorm voor de standaard persistente semantiek wordt belemmerd door het extensionele karakter van buurten (ongelabelde upsets kunnen per ongeluk meerdere formules getuigen). Om dit te overwinnen, introduceren de auteurs een hulpstuk: een getypeerde persistente buurtsemantiek. In deze setting worden buurten gelabeld door de specifieke modale formules die zij bedoeld zijn te getuigen of te weerleggen. Een waarheidlemma wordt vastgesteld voor dit getypeerde model, waarbij bewezen wordt dat semantische waarheid samenvalt met lidmaatschap van de positieve component van de priem-theorie-paren.
4. Algebraïsche Semantiek (2-DLIO's): Het artikel introduceert 2-DLIO's (begrensde distributieve lettertypen uitgerust met twee families van instantiale operaties, $(f_n)$ voor $\Box$ en $(g_n)$ voor $\Diamond$) als het algebraïsche tegenovergestelde. De Lindenbaum-algebra van PINL wordt getoond een 2-DLIO te zijn.
5. Bitopologische Representatie: De auteurs construeren een canonieke bitopologische PINL-ruimte afgeleid van de priem-theorie-paren. Deze ruimte is uitgerust met twee topologieën ($\tau_+$ gegenereerd door positieve lidmaatschapsverzamelingen $U_\phi$ en $\tau_-$ gegenereerd door negatieve lidmaatschapsverzamelingen $V_\phi$). De algebra van de admissible positieve open verzamelingen in deze ruimte is aangetoond isomorf te zijn aan de Lindenbaum 2-DLIO.

Belangrijkste Bijdragen en Resultaten

• Formeel Systeem: Definitie van de taal en een volledig bewijssysteem voor PINL, waarbij $\Box$ en $\Diamond$ als onafhankelijke primitieven worden behandeld met afzonderlijke axioma-schema's.
• Volledigheid: Bewijs van de klank en volledigheid van PINL met betrekking tot persistente tweezijdige buurtmodellen. Dit wordt bereikt via de hulpstuk getypeerde semantiek, die de technische moeilijkheden van de canonieke constructie in de afwezigheid van negatie oplost.
• Algebraïsche Karakterisering: Introductie van 2-DLIO's als de algebraïsche semantiek voor PINL. Het artikel bewijst de algebraïsche klank en volledigheid, en toont aan dat de Lindenbaum-algebra van PINL een 2-DLIO is.
• Canonieke Representatie: Constructie van de canonieke bitopologische PINL-ruimte. Het artikel bewijst dat de algebra van de admissible positieve open verzamelingen van deze ruimte isomorf is aan de Lindenbaum 2-DLIO. Dit biedt een canonieke admissible-open representatie van de logica.
• Scheiding van Zaken: Het werk isoleert expliciet het positieve, onafhankelijke-operator fragment van INL, en onderscheidt dit van het klassieke Booleaanse kader en het volledige DLIO-kader waar interactie-axioma's kunnen bestaan.

Betekenis en Reikwijdte
Het artikel claimt de eerste systematische ontwikkeling te bieden van een positieve, negatievrije versie van de instantial neighbourhood logic. Het vult een specifiek gat in de literatuur door het bewijssysteem, de semantiek en de algebraïsche fundamenten voor deze logica vast te stellen.

De auteurs verklaren expliciet dat de reikwijdte beperkt is tot een canonieke representatietheorema, en niet tot een volledige categorische dualiteitstheorema. Hoewel het werk de grondslag legt voor een toekomstige dualiteitstheorie (specifiek een Priestley-stijl of bitopologische dualiteit voor 2-DLIO's), definieert dit huidige artikel niet de noodzakelijke categorie van descriptieve PINL-ruimten, morfismen of functoriële behandelingen. Eveneens merkt het artikel op dat een "geometrische" versie van INL (betrokken bij Scott-continuïteit) door de literatuur wordt gesuggereerd, maar aan toekomstig onderzoek wordt overgelaten.

De betekenis ligt in het overbruggen van positieve modale logica, buurtsemantiek en distributieve lettertypen, waarbij een rigoureus kader wordt geboden voor het redeneren over instantiale eigenschappen zonder klassieke negatie, en door de noodzakelijke algebraïsche en topologische instrumenten te bieden voor toekomstig dualiteitsonderzoek.