Knowing-Value Logic with Successor Arithmetic

Technische Samenvatting: Knowing-Value Logica met Opvolger-Arithmetica

Probleemstelling
Dit artikel behandelt de beperkingen van bestaande "knowing-value" logica's, specifiek de conditionele knowing-value logica ($ELKvr$) en de public announcement uitbreiding ($PALKvr$) voorgesteld door Wang en Fan. Hoewel deze systemen uitspraken zoals "Agent $i$ kent de waarde van $c$ gegeven $\phi$" formaliseren, missen ze de syntactische machinerie om rekenkundige operaties en gelijkheid direct te verwerken. Bijgevolg kunnen ze de interne structuur van proposities die getallen bevatten, zoals de relatie tussen opeenvolgende gehele getallen, niet vatten. In natuurlijke taalscenario's en logische puzzels (bijv. de "Consecutive Numbers" puzzel) berust redeneren vaak op de interactie tussen epistemische operatoren, gelijkheid en rekenkundige functies (met name de opvolgerfunctie). De bestaande kaders behandelen numerieke condities als opake propositionele letters, waardoor ze niet in staat zijn om implicaties af te leiden die evident zijn in natuurlijke taal (bijv. dat het kennen van een getal dat 4-cijferig is, en het kennen van de implicatie "als 4-cijferig dan 1111", moet impliceren dat men de waarde 1111 kent). Bovendien zijn de standaardsemantiek voor deze logica's, gebaseerd op ongestructureerde verzamelingen objecten, ontoereikend voor het modelleren van specifieke wiskundige structuren zoals de natuurlijke getallen met een opvolgerfunctie.

Methodologie
De auteur introduceert een nieuwe logica, $ELKvSAr$ (het fragment zonder publieke aankondigingen van $PALKvSAr$), die de conditionele knowing-value logica uitbreidt met:

1. Termen: Inclusief een rigide constante $0$, niet-rigide constanten $C$, en de opvolgerfunctie $S$.
2. Atomische formules: Gelijkheid tussen termen ($t_1 \approx t_2$).
3. Semantiek: Het artikel definieert twee onderscheidende klassen van modellen:
   • Standaard Modellen: Gebaseerd op de standaard natuurlijke getallen $(\mathbb{N}, S)$.
   • Niet-standaard Modellen: Gebaseerd op een specifiek niet-standaard model van opvolger-arithmetica $(\mathbb{N}^\star, S^\star)$, waarbij $\mathbb{N}^\star$ de standaard natuurlijke getallen bevat plus oneindig veel "Z-chains" (kopieën van de gehele getallen). Deze uitbreiding is noodzakelijk omdat de logica niet compact is over de klasse van standaard modellen.

De technische aanpak omvat:

• Axiomatisering: Het voorstellen van het systeem $ELKVSAr$, dat axioma's bevat voor gelijkheid, opvolger-arithmetica (bijv. $\neg Sx \approx 0$, injectiviteit van $S$), en specifieke axioma's/regels die knowing-value en arithmetica overbruggen (bijv. $KvrS$, $KVE1$, $KVE2$). Een cruciaal kenmerk is de $Kvr$-Elim regel, die functioneert analoog aan existentiële eliminatie in eerste-orde logica, waardoor het verwijderen van gerelativeerde knowing-value operatoren tijdens afleiding mogelijk is.
• Volledigheidsproef: Het bewijzen van sterke volledigheid met betrekking tot niet-standaard modellen. De bewijsvoering maakt gebruik van een innovatieve constructie van een boom-achtige canonieke frame in plaats van een standaard canoniek model. Dit houdt het construeren van geschiedenissen van maximale consistente verzamelingen in en het definiëren van een waarderingsfunctie die constanten naar elementen in $\mathbb{N}^\star$ mapt terwijl de equivalentierelaties geïnduceerd door de knowing-value operator en de arithmetische structuur worden gerespecteerd.
• Eindige Model Eigenschap en Beslisbaarheid: Het aantonen dat elke vervulbare formule een eindig niet-standaard model heeft, dat vervolgens via een injectieve afbeelding naar een eindig standaard model kan worden gemapt die arithmetische afstanden behoudt en componenten scheidt. Dit vestigt de eindige model eigenschap en beslisbaarheid.
• Toepassing: Het formaliseren van de "Consecutive Numbers" puzzel met behulp van public announcement operatoren ($PALKvSAr$) om te laten zien hoe de kennis van agenten evolueert door arithmetische deducties.

Belangrijkste Bijdragen en Resultaten

1. Logica Uitbreiding: De introductie van $ELKvSAr$ en $PALKvSAr$, die gelijkheid en de opvolgerfunctie integreren in de conditionele knowing-value logica.
2. Axiomatisch Systeem: De definitie van $ELKVSAr$, die bewezen is:
   • Sterk volledig te zijn met betrekking tot de klasse van niet-standaard modellen.
   • Zwak volledig te zijn met betrekking tot de klasse van standaard modellen.
3. Meta-logische Eigenschappen:
   • Eindige Model Eigenschap (FMP): De logica bezit de FMP met betrekking tot zowel standaard als niet-standaard modellen.
   • Beslisbaarheid: Het verzadigbaarheidsprobleem voor $ELKvSAr$ is beslisbaar.
4. Niet-compactheid: Het artikel bewijst dat $ELKvSAr$ niet compact is met betrekking tot standaard modellen, wat de introductie van niet-standaard modellen voor de volledigheidsproef motiveert.
5. Puzzel Oplossing: De "Consecutive Numbers" puzzel wordt succesvol geformaliseerd en opgelost binnen het systeem, wat aantoont dat de logica de stapsgewijze eliminatie van mogelijkheden gebaseerd op arithmetische restricties en epistemische updates kan vatten.

Significantie
Het artikel claimt een nieuw kader te bieden voor het integreren van epistemische logica met arithmetica. Door de knowing-value logica te verrijken met de opvolgerfunctie, overwint het systeem de grofmazige aard van eerdere benaderingen, waardoor de formalisering van redeneringen die afhangen van de interne structuur van numerieke proposities mogelijk wordt. Het werk vestigt een balans tussen expressiviteit (het hanteren van arithmetica en epistemische interactie) en computationele complexiteit (het behouden van beslisbaarheid). De auteurs merken op dat dit kader de grondslag legt voor toekomstige uitbreidingen naar complexere arithmetische structuren (optelling en vermenigvuldiging), die nodig zouden zijn voor het oplossen van puzzels zoals "Sum and Product", hoewel dergelijke uitbreidingen aanzienlijke uitdagingen met zich meebrengen wat betreft volledigheid en beslisbaarheid.