Dependence Logic

2023 Auteur: Noah Black | [email protected]. Laatst gewijzigd: 2023-11-26 16:11

Toegang navigatie

• Inhoud van het item
• Bibliografie
• Academische hulpmiddelen
• Vrienden PDF-voorbeeld
• Info over auteur en citaat
• Terug naar boven

Dependence Logic

Voor het eerst gepubliceerd op 23 februari 2017

Afhankelijkheidslogica is een uitbreiding van eerste-orde logica die er afhankelijkheidsatomen aan toevoegt, dat wil zeggen uitdrukkingen van de vorm (eqord (x_1 / ldots x_n, y)) die beweren dat de waarde van (y) is functioneel afhankelijk van (met andere woorden, bepaald door) de waarden van (x_1 / ldots x_n). Deze atomen maken de specificatie mogelijk van niet-lineair geordende afhankelijkheidspatronen tussen variabelen, veel in dezelfde zin van IF-Logic-slashed kwantificatoren; maar, anders dan bij IF-logica, scheidt de afhankelijkheidslogica de kwantificering van de specificatie van dergelijke afhankelijkheids- / onafhankelijkheidsvoorwaarden. De belangrijkste semantiek van afhankelijkheidslogica, team semantiek genoemd, generaliseert Tarski's semantiek door uitdrukkingen al dan niet tevreden te stellen met betrekking tot sets van variabele opdrachten in plaats van met betrekking tot afzonderlijke opdrachten. Deze semantiek dateert van vóór de ontwikkeling van de eigen afhankelijkheidslogica en werd oorspronkelijk ontwikkeld door Wilfrid Hodges in de context van IF-logic (Hodges 1997). Er bestaat ook een speltheoretische semantiek voor afhankelijkheidslogica, gebaseerd op spellen met onvolmaakte informatie en ongeveer analoog aan de speltheoretische semantiek voor onafhankelijkheidsvriendelijke logica (Väänänen 2007a). Sensu stricto verwijst de term "afhankelijkheidslogica" uitsluitend naar de taal die wordt verkregen door de bovengenoemde functionele afhankelijkheidsatomen toe te voegen aan de taal van de eerste-orde logica; maar de term wordt in meer algemene zin ook gebruikt om te verwijzen naar het onderzoeksgebied dat de eigenschappen van logica bestudeert door verschillende noties van afhankelijkheid en onafhankelijkheid toe te voegen aan eerste-orde logica, zoals onafhankelijkheidslogica (Grädel & Väänänen 2013),intuïtionistische afhankelijkheidslogica (Yang 2013) of inclusielogica (Galliani 2012, Galliani & Hella 2013), of zelfs logica die andere logische kaders uitbreidt door vergelijkbare atomen, zoals in het geval van modale afhankelijkheidslogica (Väänänen 2008). In dit artikel zal de term "afhankelijkheidslogica" worden gebruikt om te verwijzen naar de eigenlijke afhankelijkheidslogica, en de term "logica van afhankelijkheid en onafhankelijkheid" zal in plaats daarvan worden gebruikt om te verwijzen naar de varianten en generalisaties ervan.en de term "logica van afhankelijkheid en onafhankelijkheid" zal in plaats daarvan worden gebruikt om te verwijzen naar de varianten en generalisaties ervan.en de term "logica van afhankelijkheid en onafhankelijkheid" zal in plaats daarvan worden gebruikt om te verwijzen naar de varianten en generalisaties ervan.

• 1. Afhankelijkheidspatronen in eerste-orde logica en de uitbreidingen ervan

• 2. Teamsemantiek

  2.1 Speltheoretische semantiek

• 3. Eigenschappen

  • 3.1 Expressiviteit
  • 3.2 Hiërarchieën in afhankelijkheidslogica
  • 3.3 Negatie in afhankelijkheidslogica
  • 3.4 Waarheids-, geldigheids- en bewijssystemen in afhankelijkheidslogica

• 4. Varianten van afhankelijkheidslogica

  • 4.1 Onafhankelijkheidslogica
  • 4.2 Inclusielogica
  • 4.3 Teamlogica
  • 4.4 Intuïtionistische logica van afhankelijkheid
  • 4.5 Propositionele afhankelijkheidslogica
  • 4.6 Modale afhankelijkheidslogica

• 5. Toepassingen van afhankelijkheidslogica

  • 5.1 Afhankelijkheidslogica en databasetheorie
  • 5.2 Afhankelijkheidslogica en geloofsrepresentatie
  • 5.3 Afhankelijkheidslogica en de stelling van Arrow
  • 5.4 Quantum teamlogica en Bell's ongelijkheden
• Bibliografie
• Academische hulpmiddelen
• Andere internetbronnen
• Gerelateerde vermeldingen

1. Afhankelijkheidspatronen in eerste-orde logica en de uitbreidingen ervan

Een kenmerk van logica van de eerste orde die een groot deel van zijn expressiviteit en toepasbaarheid verklaart, is het feit dat kwantificatoren kunnen worden genest, en daardoor de specificatie van afhankelijkheidspatronen tussen gekwantificeerde variabelen mogelijk maakt. Neem bijvoorbeeld de (hopelijk valse) stelling dat 'elke jongen van een meisje houdt dat van een andere jongen houdt'. Het kan eenvoudig worden vertaald in logica van de eerste orde als

(tag {1} label {eq: boygirl1} begin {align} & / forall x (boy (x) rightarrow / bestaat y (girl (y) land / loves (x, y) land {} & / quad / bestaat z (boy (z) land x / not = z / land / loves (y, z)))) end {align})

wiens waarheidstoestand, volgens Tarski's gebruikelijke semantiek, precies is wat men zou verwachten: de bovenstaande uitdrukking is waar als en alleen als voor elke jongen (b) het mogelijk is om een meisje (g) en een jongen te vinden (b ') zodat (b) loves (g) en (g) loves (b') en (b) en (b ') niet hetzelfde zijn. De identiteit van het meisje (g) kan natuurlijk afhangen van de identiteit van de eerste jongen (b) - om deze uitdrukking waar te maken, vereisen we immers niet dat alle jongens verliefd zijn op alle meisjes- en bovendien kan de identiteit van de tweede jongen (b ') afhangen van zowel de identiteit van de eerste jongen (b) (aangezien (b') anders moet zijn dan (b)) en van de identiteit van het meisje (g) waar (b) van houdt. Dus het afhankelijkheidspatroon tussen onze gekwantificeerde variabelen is als volgt: (y) hangt af van (x),terwijl (z) afhankelijk is van zowel (x) als (y). Vanuit syntactisch perspectief wordt dit weerspiegeld in het feit dat (bestaat y) binnen het bereik van (forall x) valt terwijl (bestaat z) onder het bereik van beide (forall x) en (bestaat y).

Verschillen in de afhankelijkheidspatronen tussen operators kunnen worden gebruikt om belangrijke verschillen te formaliseren, zoals bijvoorbeeld die tussen de continuïteit van een functie (f)

(forall x / forall / epsilon / exist / delta / forall x '(| x - x' | <\ delta / rightarrow | f (x) - f (x ') | <\ epsilon))

en de uniforme continuïteit

(voorall / epsilon / bestaat / delta / voorall x / voorall x '(| x - x' | <\ delta / rightarrow | f (x) - f (x ') | <\ epsilon))

of, in intensieve uitbreidingen van logica van de eerste orde, om het verschil tussen de lezingen van De Dicto en De Re uit te drukken (bijv. "Het is voor iedereen mogelijk om gek te zijn" kan worden begrepen als ofwel te verklaren dat het voor elke persoon is), het is mogelijk dat (p) gek is, (forall x (person (x) rightarrow / Diamond / crazy (x))), of dat het mogelijk is dat iedereen gek is samen (Diamond / forall x (person (x) rightarrow / crazy (x)))).

Afhankelijkheidspatronen tussen gekwantificeerde variabelen in eerste-orde logica zijn noodzakelijkerwijs transitief, zoals blijkt uit hun verbindingen met de reikwijdte van de corresponderende subuitdrukkingen: als (bestaat y) valt binnen het bereik van (forall x) en (bestaat z) valt binnen het bereik van (bestaat y), dan zal noodzakelijkerwijs (bestaat z) vallen onder het bereik van (en daarom afhankelijk zijn van) (forall x). Verder is de verzameling van alle kwantoren waarin een of andere subformule (alpha) ligt lineair geordend: als (alpha) binnen de scope van (Q_1 x_1) en (Q_2 x_2) valt, dan (Q_1 x_1) valt binnen het bereik van (Q_2 x_2) of omgekeerd.

Dit beperkt de expressieve mogelijkheden van eerste-orde logica. Laten we bijvoorbeeld aannemen dat we onze eerdere bewering over jongens en meisjes als volgt willen wijzigen: elke jongen houdt van een meisje dat van een andere jongen houdt, en deze tweede jongen kan onafhankelijk worden gekozen op de eerste. Wat dit intuïtief betekent, is eenvoudig genoeg: voor elke jongen (b) kunnen we een meisje (g) vinden zodat (b) van (g) houdt, en voor elk van die meisjes kunnen we zoek een jongen (b ') zodat (g) van (b') en (b / not = b ') houdt, en bovendien kunnen we de identiteit van de tweede jongen (b' vinden)) zonder dat te weten van (b), op basis van de identiteit van het meisje (g) alleen. Dit kan nog steeds het geval zijn in sommige scenario's, zoals bijvoorbeeld als twee jongens (b_1) en (b_2) respectievelijk van twee meisjes (g_1) en (g_2) houden,die echter alleen van respectievelijk (b_2) en (b_1) houden. Het is echter gemakkelijk te zien dat het niet gelijk is aan onze vorige verklaring: als ons universum bijvoorbeeld bestaat (zoals in (b) hierboven) uit twee jongens (b) en (b ') en een meisje (g), en (b) en (b ') beiden houden van (g) die van beide houdt, dan is onze vorige bewering waar, maar de huidige is onwaar.

Twee scenario's waarin ((ref {eq: boygirl1})) waar is. In (a) kan (z) onafhankelijk worden gekozen uit (x); in (b) kan het niet.

Het is echter niet duidelijk hoe deze voorwaarde in de eerste-orde-logica kan worden geformaliseerd. In wezen zouden we ((ref {eq: boygirl1})) moeten aanpassen zodat (z) niet binnen de scope van (x) valt, en daarom niet afhankelijk is; we willen echter nog steeds dat (z) afhankelijk is van (y) en (y) op (x). Zoals zojuist besproken, is een dergelijk afhankelijkheidspatroon niet realiseerbaar in de eerste-orde logica. We kunnen het probleem omzeilen door onze toevlucht te nemen tot hogere orde kwantificering: inderdaad, men kan zien dat de uitdrukking

(tag {2} label {boygirl2} begin {align} & / bestaat F / forall x (boy (x) rightarrow / bestaat y (girl (y) land / loves (x, y) land / boy (F (y)) land {} & / quad x / not = F (y) land / loves (y, F (y)))) end {align})

legt onze beoogde interpretatie vast, maar alleen ten koste van expliciete existentiële kwantificering over functies.

Een mogelijk alternatief zou zijn om de syntaxis van de logica van de eerste orde uit te breiden om de beperkingen over afhankelijkheidspatronen tussen gekwantificeerde variabelen op te heffen. Dit is de route die wordt gevolgd door vertakkende kwantificatielogica (Henkin 1961), waarin de waarheidscondities van ((ref {boygirl2})) overeenkomen met die van

(tag {3} label {boygirl3} begin {align} & / left (begin {smallmatrix} forall x & / bestaat y \\ / forall z & / bestaat met / small {smallmatrix} right) (boy (x) rightarrow (girl (y) land / loves (x, y) land {} & / quad (y = z / rightarrow (boy (w) land x / not = w / land / loves (z, w))))), / end {align})

en aan onafhankelijkheidsvriendelijke logica, waarin ((ref {boygirl2})) gelijk is aan

(tag {4} label {boygirl4} begin {align} & / forall x / bestaat y (boy (x) rightarrow (girl (y) land / loves (x, y) land (bestaat z / x) (boy (z) land {} & / quad x / not = z / land / houdt van (y, z)))). / end {align})

We zullen hier geen gedetailleerde uitleg geven van de semantiek van deze twee formalismen; het volstaat om te zeggen dat in ((ref {boygirl3})) de waarde van (w) niet afhankelijk is van de waarden van (x) en (y) (hoewel het mogelijk afhankelijk is van de waarde van (z)), aangezien ze behoren tot verschillende "rijen" van de complexe kwantor (left (begin {smallmatrix} forall x & / bestaat y \\ / forall z & / bestaat w / end {smallmatrix } right)), terwijl in ((ref {boygirl4})) de waarde van (z) niet afhankelijk is van de waarde van (x), omdat deze afhankelijkheid expliciet wordt "weggehaald" door de kwantor ((bestaat z / x)).

Zoals we kunnen zien, is een kenmerk van vertakte kwantificatorlogica en onafhankelijkheidsvriendelijke logica dat ze de kwantificering van variabelen niet scheiden van de specificatie van niet-standaardpatronen van afhankelijkheid: zoals in het geval van eerste-orde logica, of een gekwantificeerde variabele (v_1) hangt wel of niet af van een andere gekwantificeerde variabele (v_2) wordt bepaald door de respectievelijke positie en vorm van hun kwantoren.

Dependence-logica benadert het probleem van het uitbreiden van de logica van de eerste orde op een andere manier om ((ref {boygirl2})) weer te geven. Vergeleken met ((ref {eq: boygirl1})), is de enige nieuwe voorwaarde die waarin staat dat de waarde van (z) wordt bepaald door (dat wil zeggen functioneel afhankelijk van) de waarde van (y); en dit komt overeen met een nieuwe atomaire conditie (eqord (y, z)), een afhankelijkheidsatoom genoemd, waarvan de bedoelde betekenis is dat (de waarde van) (z) een functie is van de waarde van (y). Anders dan bij vertakte kwantificatielogica of onafhankelijkheidsvriendelijke logica, is dit een voorwaarde over de waarden die (y) en (z) kunnen aannemen, geen voorwaarde over het gedrag van de kwantor (bestaat z): inderdaad, er is in het algemeen geen reden om te eisen dat (z) überhaupt een gekwantificeerde variabele is - het zou in plaats daarvan een vrije variabele kunnen zijn,of een complexe term met meerdere variabelen.

In afhankelijkheidslogica kan ((ref {boygirl2})) worden geformaliseerd als

(tag {5} label {boygirl5} begin {align} & / forall x / bestaat y / bestaat z (eqord (y, z) land (boy (x) rightarrow (girl (y) land / loves (x, y) rightarrow {} & / quad (boy (z) land x / not = z / land / loves (y, z))))) end {align})

De waarheidsvoorwaarden van ((ref {boygirl2})), ((ref {boygirl3})), ((ref {boygirl4})) en ((ref {boygirl5})) zijn precies hetzelfde: elk model dat voldoet aan een van deze uitdrukkingen (in de respectievelijke talen) voldoet aan alle vier. Meer in het algemeen zijn, zoals we zullen zien, de expressieve krachten van existentiële tweede-orde logica, onafhankelijkheidsvriendelijke logica en afhankelijkheidslogica met betrekking tot de definieerbaarheid van klassen van modellen precies hetzelfde. Dit is echter niet het geval voor formules met vrije variabelen; en bovendien kunnen deze logica's langs duidelijk verschillende lijnen worden uitgebreid en gewijzigd.

2. Teamsemantiek

Teamsemantiek, voor het eerst ontwikkeld door Wilfrid Hodges in de context van onafhankelijkheidsvriendelijke logica (Hodges 1997), is een veralgemening van Tarski's semantiek voor logica van de eerste orde in het geval van meerdere toewijzingen van elementen aan variabelen. Sets van dergelijke opdrachten, om historische redenen teams genoemd, vormen de fundamentele semantische notie van team semantiek, en formules zijn al dan niet tevreden met betrekking tot hen in plaats van met betrekking tot afzonderlijke opdrachten. Het verband tussen team-semantiek en Tarski-semantiek wordt aangetoond door het volgende resultaat, dat zowel in de afhankelijkheidslogica als in alle varianten van de eerste orde geldt:

Conservativiteit:

Een team-formule (in de zin van team-semantiek) voldoet aan een eerste-ordeformule als en alleen als alle opdrachten (in de zin van Tarski-semantiek) hieraan voldoen (in de zin van Tarski-semantiek).

Meer in het algemeen kunnen teams worden opgevat als geloofssets, die de verzameling vertegenwoordigen van alle staten van de wereld (= opdrachten) die sommige agenten mogelijk achten. Dan zal een team (X) voldoen aan een bepaalde formule (phi) als en alleen als (phi) geldt wanneer (X) de verzameling is van alle mogelijke toestanden; en in dit geval schrijven we (X / models / phi) (of (M, X / models / phi) als de keuze van het model (M) niet duidelijk is). In deze sectie zullen we de regels van team semantiek en hun interpretatie in termen van dit principe onderzoeken; vervolgens zullen we in de volgende sectie bespreken hoe het ook voortkomt uit de imperfecte-informatie speltheoretische semantiek voor afhankelijkheidslogica.

De voorwaarde voor de nieuwe afhankelijkheidsatomen (eqord (x_1 / ldots x_n, y)), die overeenkomen met de bewering dat de waarde van (y) een functie is van de waarden van (x_1 / ldots x_n), is gemakkelijk te begrijpen:

TS-dep:

(X / models ~ / eqord (x_1 / ldots x_n, y)) als en alleen als er twee opdrachten (s_1, s_2 / in X) zijn die het eens zijn over de waarden van (x_1 / ldots x_n) ben het ook eens over de waarde van (y).

Stel bijvoorbeeld dat (X) een set opdrachten is over de drie variabelen (x_1), (x_2) en (y), waarbij (x_1) de nationaliteit van een kandidaat vertegenwoordigt om een positie, (x_2) vertegenwoordigt hun score (volgens een geschikte evaluatiemethode) en (y) geeft aan of ze zijn geaccepteerd of afgewezen. Dan komt het atoom (eqord (x_2, y)) overeen met de stelling dat het aanbod alleen door de score wordt bepaald: als twee kandidaten dezelfde score behalen, ontvangen ze exact hetzelfde aanbod, ongeacht een andere factor. Een speciaal geval van afhankelijkheidsatoom wordt gegeven door de constantie-atomen (eqord (y)), die volgens bovenstaande semantiek door een team worden vervuld als en alleen als al zijn opdrachten overeenkomen over de waarde van (y).

(begin {array} {l | ccc} textbf {opdracht} & / mathbf {x_1} & / mathbf {x_2} & / mathbf {y} / \ hline s_0 & 0 & 0 & 0 \\ s_1 & 0 & 1 & 1 \\ s_2 & 1 & 0 & 1 \\ s_3 & 1 & 1 & 2 / einde {array})

Tabel 1: Een team (X) waarin (y = x_1 + x_2). Hier is (y) een functie van (x_1) en (x_2), en dus geldt (= \! \! (X_1 x_2, y)); (y) is echter niet alleen een functie van (x_1), dus (= \! \! (x_1, y)) is niet geldig.

Onder dezelfde interpretatie, de regels voor letterlijke en conjuncties van de eerste orde (voor de eenvoud gaan we ervan uit dat onze uitdrukkingen in de normale vorm van negatie zijn; en, zoals gebruikelijk, gaan we ervan uit dat de negaties van afhankelijkheidsatomen nooit vervuld zijn) gemakkelijk af te leiden:

TS-lit:

Voor alle eerste-orde literals (alpha), (X / models / alpha) als en alleen als voor alle opdrachten (s / in X), (s / models / alpha) in de gebruikelijke Tarski semantiek zin;

TS - (land):

(X / models / phi / land / psi) als en alleen als (X / models / phi) en (X / models / psi).

Het is de moeite waard erop te wijzen dat, zoals we al kunnen zien aan deze regels, de wet van het uitgesloten midden niet van toepassing is in de afhankelijkheidslogica (net zoals het niet geldt voor onafhankelijkheidsvriendelijke logica): bijvoorbeeld als een team (X) bevat zowel opdrachten (s) met (s (x) = s (y)) als opdrachten (s ') met (s' (x) not = s '(y)) dan (X / niet / modellen x = y) en (X / niet / modellen x / niet = y). In deze sectie zullen we in ieder geval de taal van de afhankelijkheidslogica presenteren zonder een expliciete negatie-operator; daarna bespreken we de gevolgen van het toevoegen aan de taal.

Hoe zit het met universele kwantificatie? In welke omstandigheden moet een universeel gekwantificeerde uitdrukking (forall v / psi) in een team staan? Nogmaals, we moeten de intuïtie herinneren waarbij een team een reeks mogelijke toestanden vertegenwoordigt. Als we (forall v / psi) willen evalueren, met betrekking tot welke mogelijke toestanden van dingen moeten we (psi) evalueren? Het natuurlijke antwoord is dat we alle toestanden van dingen die verschillen van die in (X) alleen moeten beschouwen met betrekking tot de waarde van (v). Dit rechtvaardigt de volgende regel:

TS - (forall):

(X / models / forall v / psi) als en alleen als (X [M / v] models / phi), waar (X [M / v]) is de set ({s ': / bestaat s / in X / mbox {st} s' / sim_v x })

waarbij (s '\ sim_v s) betekent dat de twee opdrachten (s) en (s') hoogstens van elkaar verschillen met betrekking tot de waarde van de variabele (v).

[X = / begin {array} {l | c} textbf {toewijzing} & x \\ / hline s_0 & 0 \\ s_1 & 1 / end {array} Rightarrow X [M / y] = / begin {array} {l | c | c} textbf {toewijzing} & x & y \\ / hline s'_0 & 0 & 0 \\ s'_1 & 0 & 1 \\ s'_2 & 1 & 0 \\ s'_3 & 1 & 1 / einde {array})

Tabel 2: (X) en (X [M / y]) in een model met twee elementen (0) en (1).

Laten we nu disjunctie beschouwen. Wanneer moet (phi / lor / psi) worden bewaard? Laten we om dit te beantwoorden nogmaals bedenken dat teams kunnen worden opgevat als verzamelingen van mogelijke toestanden en dat daarom de vereniging van twee teams (Y) en (Z) alle toestanden vertegenwoordigt die mogelijk optreden als (Y) of (Z) het geval is. Daarom, als aan de twee formules (phi) en (psi) wordt voldaan door de set teams ({Y_1 / ldots Y_n, / ldots }) en ({Z_1 / ldots Z_n, / ldots }), hun disjunctie (phi / lor / psi) moet worden vervuld door de set teams ({Y_i / cup Z_j: i, j / in 1, / ldots }), of, equivalent,

TS - (lor):

(X / models / phi / lor / psi) als en alleen als (X = Y / cup Z) voor twee teams (Y) en (Z) zodat (Y / models / phi) en (Z / models / psi).

Het is de moeite waard hier op te merken dat we in het algemeen niet vereisen dat (Y) en (Z) onsamenhangend zijn. Vanwege de neerwaartse sluitingseigenschap, die we binnenkort zullen bespreken, zou deze aanvullende voorwaarde voor de eigenlijke semantiek van de afhankelijkheidslogica geen verschil maken; maar in het geval van bepaalde uitbreidingen en varianten van afhankelijkheidslogica, zou die aanvullende vereiste in strijd zijn met het plaatsbepalingsprincipe volgens hetwelk de tevredenheidsvoorwaarden van een uitdrukking alleen afhangen van de waarden van de variabelen die er vrij in voorkomen (Galliani 2012).

Het is ook belangrijk op te merken dat disjunctie in afhankelijkheidslogica niet idempotent is: (eqord (x, y) lor / eqord (x, y)) is bijvoorbeeld niet equivalent aan (eqord (x, y)), en het is tevreden door een team (X), al dan niet voor elke drie opdrachten in (X) die het eens zijn over (x), ten minste twee zijn het eens over (y). Dit lijkt misschien enigszins contra-intuïtief; maar het is een duidelijk gevolg van het feit dat, volgens onze interpretatie, (eqord (x, y) lor / eqord (x, y)) gelezen moet worden als elke mogelijke toestand komt van een van twee sets van toestanden, en in beide is (y) een functie van (x)”. Aangezien de unie van functies over het algemeen geen functie is, is het geen verrassing dat disjunctie in de afhankelijkheidslogica niet onbelangrijk is.

Ten slotte bekijken we het geval van existentiële kwantificering. Wanneer wordt door een team voldaan aan de uitdrukking (bestaat v / psi)? Om dit te beantwoorden, kunnen we beginnen met de interpretatie van de restrictie-operator, die, gegeven elk team (X), resulteert in het team (X _ { backslash v}) verkregen door het verwijderen van de variabele (v) (indien aanwezig) van alle opdrachten (s / in X) (en dan, aangezien (X) een verzameling is, door identieke opdrachten samen te vouwen). Dit kan worden opgevat als een vergeetactie, waarbij we alle informatie over de waarde van (v) verwijderen, bijvoorbeeld omdat wat we dachten over deze waarde onbetrouwbaar was, of omdat deze waarde is gewijzigd. Stel nu dat (X _ { backslash v} = Y _ { backslash v}): dan, in onze interpretatie,dit betekent dat de sets van mogelijke toestanden van dingen weergegeven door (X) en (Y) hooguit oneens zijn met betrekking tot de waarde van (v). Dus als (Y) voldoet aan de voorwaarde (phi), kunnen we zeggen dat (X) zou voldoen aan (phi), zo niet voor de waarde van (y), of equivalent, dat (X) voldoet (bestaat v / psi). Dit rechtvaardigt de volgende regel:

TS - (bestaat):

(X / modellen / bestaat v / psi) als en alleen als er wat (Y) bestaat, over de variabelen van (X) en (v), zodanig dat (X _ { backslash v} = Y _ { backslash v}) en (Y / models / psi).

Het is eenvoudig om te verifiëren dat dit het geval is als en alleen als (Y) de vorm heeft (X [F / y] = {s [a / y]: s / in X, a / in F (s) }) voor een bepaalde functie (F) van opdrachten in (X) tot niet-lege sets elementen van ons model.

Het is vermeldenswaard dat het in het algemeen niet vereist is door de bovenstaande definitie dat (X) en (Y) hetzelfde aantal opdrachten bevatten: een enkele opdracht in (X) komt mogelijk overeen met meerdere opdrachten in (Y), en -als (v) is al een variabele die voorkomt in de opdrachten van (X) - een enkele opdracht in (Y) kan ook overeenkomen met meerdere opdrachten in (X).

[X = / begin {array} {l | c} textbf {toewijzing} & x \\ / hline s_0 & 0 \\ s_1 & 1 / end {array} Rightarrow X [F / y] = / begin {array} {l | c | c} textbf {toewijzing} & x & y \\ / hline s'_0 & 0 & 0 \\ s'_1 & 0 & 1 \\ s'_2 & 1 & 0 / end {array})

Tabel 3: (X) en (X [F / y]) voor (F (s_0) = {0,1 }), (F (s_1) = {0 })

We zullen een diepgaande bespreking van de eigenschappen van afhankelijkheidslogica uitstellen tot na de specificatie van de speltheoretische semantiek. We sluiten dit gedeelte echter af met de volgende drie belangrijke gevolgen van de hierboven gegeven regels:

Plaats:

Als de beperkingen van (X) en (Y) tot de variabelen die vrij voorkomen in (phi) hetzelfde zijn, dan zijn (X / models / phi) al dan niet als (Y / modellen / phi).

Neerwaartse sluiting:

Als (X / models / phi) en (Y / subseteq X) then (Y / models / phi).

Lege set-eigenschap:

Als (emptyset) het team is dat geen opdrachten heeft, dan is (emptyset / models / phi) voor alle afhankelijkheidslogica-formules (phi).

Het plaatsprincipe vormt, samen met het conservativiteitsprincipe dat aan het begin van deze paragraaf wordt genoemd, een belangrijke 'gezondheidsvoorwaarde' waaraan elke variant en uitbreiding van de afhankelijkheidslogica moet voldoen. Hetzelfde kan niet worden gezegd over de neerwaartse sluiting en de lege set-eigenschap, die, zoals we zullen zien, worden geschonden door varianten van afhankelijkheidslogica.

Ten slotte moeten we de waarheid van een afhankelijkheidslogica-zin definiëren met betrekking tot een model. Aangezien een zin geen vrije variabelen heeft, hebben we volgens het plaatsbepalingsprincipe meteen dat ofwel alle niet-lege teams eraan voldoen of geen niet-leeg team eraan voldoet. Dit is analoog aan het geval van Tarski's semantiek, waarin aan een zin wordt voldaan door alle variabele opdrachten of door geen van hen. We kunnen de waarheid dus op de gebruikelijke manier definiëren:

Waarheid in team semantiek:

een zin (phi) is waar in een model (M) als en alleen als (M, { emptyset } models / phi), waar ({ emptyset }) is het team dat alleen de lege opdracht bevat. In dit geval schrijven we dat (M / models / phi).

2.1 Speltheoretische semantiek

Zoals gezegd is de speltheoretische semantiek voor afhankelijkheidslogica een variant van de imperfecte-informatiesemantiek voor onafhankelijkheidsvriendelijke logica, die zelf een aanpassing is van de speltheoretische semantiek van de eerste-orde logica. We verwijzen de lezer naar Väänänen 2007a voor een formele, gedetailleerde definitie van deze semantiek.

In speltheoretische semantiek worden een zin (phi) en een model (M) gemaakt om te corresponderen met een spel (meestal twee spelers) (G_M (phi)). Dan wordt de waarheid gedefinieerd in termen van het bestaan van winnende strategieën voor een van de spelers (die in dit werk simpelweg "Player (0)" zal worden genoemd): met andere woorden, als (sigma_0) een (mogelijk niet-deterministische) strategie voor Player (0) en (Pi (G_M (phi), / sigma_0)) is de set van alle plays die compatibel zijn met (sigma_0) then (phi) is waar als en alleen als elk spel in (Pi (G_M (phi), / sigma_0)) wint voor Player (0). Het is mogelijk om het spel (G_M (phi)) te zien als een debat tussen twee spelers, van wie één (speler (0)) wil aantonen dat het zo is dat (phi) terwijl de ander (Player (1)) wil aantonen dat het niet zo is dat (phi).

Zoals in het geval van eerste-orde logica en onafhankelijkheidsvriendelijke logica, zijn in het imperfect-informatiespel voor afhankelijkheidslogica de posities van het spel paren ((theta, s)), waar (theta) is een instantie van een subformule van (phi) (dat wil zeggen dat meerdere exemplaren van dezelfde uitdrukking als een subformule van (phi) afzonderlijk moeten worden beschouwd) en (s) is een variabele toewijzing over de model (M). ^[1] De beginpositie is ((phi, / emptyset)), waarbij (emptyset) de lege toewijzing is; en een niet-deterministische strategie (sigma_0) voor Player (0) selecteert voor elke disjunctie en existentiële kwantificatie een of meer opvolgers van de huidige positie volgens de volgende regels:

• Als de huidige positie de vorm ((psi / lor / theta, s)) heeft, zijn de opvolgers ((psi, s)) en ((theta, s));
• Als de huidige positie de vorm ((bestaat v / psi, s)) heeft, zijn de opvolgers alle posities ((psi, s ')) met (s' / sim_v s).

Evenzo zijn de opvolgers van ((psi / land / theta, s)) ((psi, s)) en ((theta, s)) en de opvolgers van ((forall v / psi, s)) zijn alle posities van de vorm ((psi, s ')) voor (s' / sim_v s); maar een strategie voor Player (0) kan geen opvolger voor deze posities specificeren, aangezien wordt aangenomen dat Player (1) kiest welke positie ze volgt.

Een reeks posities (overline / rho = / rho_0 / rho_1 / ldots / rho_n) is een spel van (G_M (phi)) als en alleen als

1. (rho_0 = (phi, / emptyset));
2. Voor alle (i = 1 / ldots n) is (rho_ {i}) een opvolger van (rho_ {i-1}).

Als bovendien (rho_ {i + 1} in / sigma_0 (rho_i)) telkens wanneer (rho_i) overeenkomt met een disjunctie of een existentiële kwantor, dan zeggen we dat (overline / rho) de strategie (sigma_0); en zoals gezegd schrijven we (Pi (G_M (phi), / sigma_0)) voor de set van alle plays over (G_M (phi)) die respecteren (sigma_0).

We zeggen dat een strategie (sigma_0) wint als elk spel (overline / rho) eindigt op een positie ((alpha, s)) waar (alpha) een eerste is De letterlijke volgorde is zodanig dat de opdracht (s) voldoet aan (alpha) in de gebruikelijke zin van Tarski's semantiek. Afhankelijkheidsatomen - en de spelen die eindigen in afhankelijkheidsatomen - zijn niet relevant om te beslissen of een bepaalde strategie wint. Ze worden echter gebruikt om aan te geven of een bepaalde strategie uniform is:

Uniformiteitsvoorwaarde

Een strategie (sigma_0) voor (G_M (phi)) is uniform als er twee spelen (overline / rho, / overline / gamma / in / Pi (G_M (phi), / sigma_0)) die eindigen op twee posities ((eqord (x_1 / ldots x_n, y), s)), ((eqord (x_1 / ldots x_n, y), s ')) voor dezelfde instantie van het afhankelijkheidsatoom (eqord (x_1 / ldots x_n, y)) dat hebben we

(textrm {If} s (x_1) ldots s (x_n) = s '(x_1) ldots s' (x_n) textrm {then} s (y) = s '(y).)

Vervolgens kunnen we de waarheid in de speltheoretische semantiek als volgt definiëren:

Waarheid in speltheoretische semantiek:

Een zin (phi) is waar in een model (M) (met betrekking tot speltheoretische semantiek) als en alleen als Player (0) een uniforme winnende strategie heeft in (G_M (phi)).

Aangetoond kan worden dat dit begrip gelijk is aan het begrip waarheid in team semantiek. We kunnen zelfs meer laten zien. Als voor een team (X) en formule (phi), het spel (G_ {M, X} (phi)) wordt gespeeld als (G_M (phi)) maar met de beginpositie willekeurig gekozen voor elk spel van ({(phi, s): s / in X }), dan geldt het volgende:

Gelijkwaardigheid van GTS en teamsemantiek:

een formule (phi) wordt vervuld door een team (X) (met betrekking tot een model (M)), al dan niet als Player (0) een uniform heeft winnende strategie in (G_ {M, X} (phi)).

Dit resultaat maakt terzijde duidelijk waarom de teamsemantiek van de afhankelijkheidslogica voldoet aan de lege set-eigenschap en de eigenschap voor neerwaartse sluiting. Inderdaad, als (X = / emptyset) dan is elke strategie voor Player (0) in (G_ {M, X} (phi)) triviaal winnend en uniform; en als (X / subseteq Y) dan is elke uniforme winnende strategie voor Player (0) in (G_ {M, X} (phi)) ook een uniforme winnende strategie voor Player (0) in (G_ {M, Y} (phi)).

3. Eigenschappen

3.1 Expressiviteit

Zinsgewijs is afhankelijkheidslogica equivalent aan het existentiële fragment (Sigma_1 ^ 1) van tweede-orde logica. Meer precies kan worden bewezen (Väänänen 2007a) dat

Zinsgewijze gelijkwaardigheid van afhankelijkheidslogica en (Sigma_1 ^ 1):

Voor elke afhankelijkheidslogische zin (phi) bestaat er een (Sigma_1 ^ 1) zin (phi ^ *) zodat

(tag {6} label {eq: DLESO} M / models / phi / Leftrightarrow M / models / phi ^ * / textrm {voor alle modellen} M.)

Evenzo bestaat er voor elke (Sigma_1 ^ 1) zin (phi ^ *) een afhankelijkheidslogica-zin (phi) zodat ((ref {eq: DLESO})) geldt.

Aangezien de stelling van Fagin (Fagin 1974) aantoont dat een eigenschap van eindige modellen definieerbaar is in (Sigma_1 ^ 1) als en alleen als het in polynoomtijd herkenbaar is aan een niet-deterministische Turing-machine (dat wil zeggen, als en alleen als het is in NPTIME) volgt daar meteen op

Afhankelijkheidslogica en NPTIME:

voor elke afhankelijkheidslogica-zin (phi) is de klasse van alle eindige modellen die eraan voldoen in NPTIME. Bovendien bestaat er voor elke NPTIME-klasse (mathcal K) van eindige modellen een logische afhankelijkheidszin (phi) zodat (M / models / phi) alleen en alleen als (M / in / mathcal K).

Een ander direct gevolg van de gelijkwaardigheid tussen afhankelijkheidslogica en (Sigma_1 ^ 1) op het niveau van zinnen is dat de compactheidsstelling en de stelling van Löwenheim-Skolem beide ook gelden voor afhankelijkheidslogica (Väänänen 2007a):

Compactheid:

Als een set (Phi) van logische zinnen met eindige afhankelijkheid in geen enkel model bevredigend is, dan is een bepaalde eindige subset (Phi_0 / subseteq_f / Phi) al niet bevredigend.

Stelling van Löwenheim-Skolem:

Als een logische zin voor afhankelijkheid een oneindig model heeft, dan heeft deze modellen van alle oneindige kardinaliteiten.

Bij formules met vrije variabelen zijn de zaken echter delicater. Dan is het mogelijk (Kontinen & Väänänen 2009) te laten zien dat afhankelijkheidslogica overeenkomt met het naar beneden gesloten fragment van existentiële tweede orde logica:

Teamdefinitie in afhankelijkheidslogica

Een set (mathcal X) teams over een model (M) en een set (V) variabelen heeft de vorm ({X: M, X / modellen / phi }) voor een of andere formule voor afhankelijkheidslogica (phi), met vrije variabelen in (V), al dan niet als

1. (mathcal X) is niet leeg;
2. (mathcal X) is naar beneden gesloten, dat wil zeggen (Y / subseteq X / in / mathcal X / Rightarrow Y / in / mathcal X);

3. (mathcal X) is (Sigma_1 ^ 1) - definieerbaar in (M), dat wil zeggen er bestaat een (Sigma_1 ^ 1) zin (Psi (R)), over de woordenschat van (M) plus het nieuwe (| V |) - ary relatiesymbool (R), zodat

   [X / in / mathcal X / textrm {als en alleen als} M, / textrm {Rel} (X) models / Psi (R))

   waarbij (textrm {Rel} (X)) de (| V |) - ary relatie ({s (V): s / in X }) is die overeenkomt met het team (X).

3.2 Hiërarchieën in afhankelijkheidslogica

In Durand & Kontinen 2012 werd het effect onderzocht van het beperken van het aantal afhankelijke variabelen van afhankelijkheidsatomen of het aantal universele kwantoren. Er werd aangetoond dat beide manieren om fragmenten van afhankelijkheidslogica te definiëren aanleiding geven tot hiërarchieën:

• Voor alle (k), laat (mathcal D (k- / forall)) afhankelijkheidslogica beperken tot maximaal (k) universele kwantoren en laat (mathcal D (k-dep)) be afhankelijkheidslogica beperkt tot afhankelijkheidsatomen in de vorm (eqord (vec x, y)) voor (| / vec x | / leq k). Vervolgens

  (begin {align *} mathcal D (k- / forall) & <\ mathcal D (k + 1-dep), \\ / mathcal D (k- / forall) & / leq / mathcal D (k- dep) leq / mathcal D (k + 1 - dep) end {align *})

  en

  (mathcal D (k- / forall) <\ mathcal D (2k + 2 - / forall))

  met betrekking tot de expressieve kracht van zinnen.

3.3 Negatie in afhankelijkheidslogica

Tot dusverre gingen we ervan uit dat alle logica-uitdrukkingen van de negatie in de normale vorm van negatie zijn en dat atomen van afhankelijkheid nooit worden genegeerd. Het toevoegen van een expliciete ontkenningsoperator aan de taal van de afhankelijkheidslogica is daarentegen enigszins problematisch, omdat de existentiële logica van de tweede orde niet wordt gesloten onder ontkenning. Inderdaad, de "voor de hand liggende" negatieregel

[X / models / sim / phi / textrm {als en alleen als} X / not / models / phi)

vergroot de expressieve kracht van afhankelijkheidslogica aanzienlijk en breidt deze uit tot teamlogica (Väänänen 2007a, b), wat in zeer sterke zin equivalent is aan volledige tweede-orde logica (Kontinen & Nurmi 2009).

Een minder sterke, 'dubbele' ontkenning (lnot) kan worden gedefinieerd in termen van de Morgan-regels, (lnot (phi / lor (land] psi) equiv (lnot / phi) land (lor] (lnot / psi)) en (lnot (bestaat v (alleen v] phi) equiv / forall v (bestaat v] (lnot / phi)), plus de wet van dubbele negatie (lnot / lnot / phi / equiv / psi) en de regel

[X / models { lnot / eqord} (vec x, y) textrm {als en alleen als} X = / emptyset)

voor negaties van afhankelijkheidsatomen (Väänänen 2007a, b). De resulterende taal is expressief equivalent aan ontkenningsvrije afhankelijkheidslogica, en in feite beschouwt de beschrijving van afhankelijkheidslogica van Väänänen 2007a deze ontkenning als onderdeel van haar taal; Zoals aangetoond in Kontinen & Väänänen 2011, hebben de tevredenheidsvoorwaarden van een formule voor afhankelijkheidslogica en die van de ontkenning ervan weinig met elkaar te maken. Preciezer:

Dubbele negatie- en afhankelijkheidslogica:

Voor elke twee afhankelijkheidslogica-formules (phi) en (psi) zodat (phi / land / psi) niet bevredigend is, bestaat er een afhankelijkheidslogica-formule (theta) zodat

[M, X / models / theta / textrm {als en alleen als} M, X / models / phi)

en

[M, X / models / lnot / theta / textrm {als en alleen als} M, X / models / psi)

voor alle modellen (M) en teams (X).

Er kan dus in het algemeen niets worden gezegd over de dubbele ontkenning van (phi), behalve dat het equivalent is aan een of andere logica van afhankelijkheid waaraan niet wordt voldaan door een team dat voldoet aan (phi). Aangezien, zoals reeds vermeld, de wet van het uitgesloten midden faalt in de afhankelijkheidslogica, is dit geen erg informatieve eigenschap; in het bijzonder is het mogelijk om in afhankelijkheidslogica (met dubbele negatie) equivalente uitdrukkingen te vinden met niet-equivalente negaties, zoals bijvoorbeeld (x / not = x / land y / not = y) en (lnot / eqord (x, y)).

3.4 Waarheids-, geldigheids- en bewijssystemen in afhankelijkheidslogica

Net als onafhankelijkheidsvriendelijke logica, kan afhankelijkheidslogica haar eigen waarheidsoperator definiëren (Väänänen 2007a), dat wil zeggen, als we voor alle formules (phi) hebben dat (lceil / phi / rceil) het Gödel-nummer is van (phi) dan kunnen we een formule (tau (x)) vinden, met (x) als enige vrije variabele, zodat

[M / models / phi / textrm {als en alleen als} M / models / tau (lceil / phi / rceil))

voor alle modellen (M) die voldoen aan de axioma's van Peano voor natuurlijke getallen. Dit is niet in tegenspraak met Tarski's stelling van ondefinieerbaarheid, omdat de afhankelijkheidslogica niet wordt gesloten onder tegenstrijdige ontkenning.

Het probleem om te beslissen of een logische zin voor afhankelijkheid geldig is (dat wil zeggen, geldt voor alle modellen) is niet-rekenkundig en in feite compleet met betrekking tot de klasse (Pi_2) van de Levy-hiërarchie. Desalniettemin is de bewijstheorie van afhankelijkheidslogica bestudeerd. Met name in Kontinen & Väänänen 2013 is een degelijk en volledig bewijssysteem ontwikkeld voor het probleem van het vinden van de eerste-orde-gevolgen van een afhankelijkheidslogica-theorie.

4. Varianten van afhankelijkheidslogica

In deze sectie zullen we de eigenschappen van de meest bestudeerde varianten van afhankelijkheidslogica kort samenvatten. Er bestaan veel van dergelijke varianten en er is veel werk verricht aan hun classificatie en vergelijking. In dit werk noemen we alleen die varianten die van bijzondere betekenis zijn vanwege hun relatie met de eigen afhankelijkheidslogica.

4.1 Onafhankelijkheidslogica

In plaats van de eerste-orde logica uit te breiden met afhankelijkheidsatomen (eqord (vec x, y)), breidt onafhankelijkheidslogica (Grädel & Väänänen 2013) het uit met onafhankelijkheidsatomen (vec x / mathop { bot _ { vec z }} vec y), waarvan de beoogde interpretatie is "voor elke mogelijke keuze van (vec z), zijn de mogelijke waarden van (vec x) en (vec y) onafhankelijk" -in met andere woorden, gegeven een vaste keuze van (vec z), zou het kennen van de waarde die wordt ingenomen door (vec x) geen informatie opleveren over de waarde die wordt ingenomen door (vec y). Dit is een concept van aanzienlijk conceptueel belang: men zou bijvoorbeeld willen uitdrukken dat - als men de encryptiesleutel niet kent - het zien van de gecodeerde versie van een bericht geen informatie bevat over de corresponderende duidelijke-tekstversie. Als (x) het gecodeerde bericht vertegenwoordigt en (y) het platte-tekstbericht,dan komt dit overeen met de voorwaarde (x / mathop { bot} y), waar (vec z) in dit geval leeg is. Evenzo, als (k) de sleutel vertegenwoordigt, dan vertegenwoordigt (x / mathop { bot} k) de bewering dat de sleutel niet kan worden afgeleid uit het gecodeerde bericht; en het conjunctie-afhankelijkheidsatoom (eqord (k, x, y)) (wat, zoals we binnenkort zullen zien, kan worden weergegeven in onafhankelijkheidslogica) vertegenwoordigt de bewering dat het platte-tekstbericht kan worden gedecodeerd gezien het gecodeerde bericht en de sleutel.kan worden weergegeven in onafhankelijkheidslogica) vertegenwoordigt de bewering dat het bericht in platte tekst kan worden gedecodeerd, gezien het gecodeerde bericht en de sleutel.kan worden weergegeven in onafhankelijkheidslogica) vertegenwoordigt de bewering dat het bericht in platte tekst kan worden gedecodeerd, gezien het gecodeerde bericht en de sleutel.

Formeel kan de tevredenheidsregel voor onafhankelijkheidsatomen als volgt worden gegeven:

TS-indep:

(M / models_X / vec x / mathop { bot _ { vec z}} vec y) als en alleen als voor alle (s, s '\ in X) met (s (vec z) = s '(vec z)) er bestaat een (s' '\ in X) met (s' '(vec z \, / vec x) = s (vec {x }, / vec {z})) en (s '' (vec y) = s '(vec y)).

(begin {array} {l | ccc} textbf {opdracht} & / mathbf {x_1} & / mathbf {x_2} & / mathbf {x_3} / \ hline s_0 & 0 & 0 & 0 \\ s_1 & 0 & 1 & 1 \\ s_2 & 1 & 0 & 1 \\ s_3 & 1 & 1 & 0 / einde {array})

Onafhankelijkheidslogica is strikt expressiever dan afhankelijkheidslogica: het mist inderdaad de neerwaartse sluitingseigenschap en het afhankelijkheidsatoom (eqord (vec x, y)) is equivalent aan het onafhankelijkheidsatoom (y / mathop { bot_ { vec x}} y). Verder kan ook worden aangetoond (Galliani & Väänänen 2014) dat geconditioneerde onafhankelijkheidsatomen (vec x / mathop { bot _ { vec y}} vec z) kunnen worden gedefinieerd in termen van onvoorwaardelijke onafhankelijkheidsatomen (vec x / mathop { bot} vec y).

Zinsgewijs is onafhankelijkheidslogica ook gelijk aan existentiële tweede-orde logica (Sigma_1 ^ 1); maar qua formule is het expressiever, en in Galliani 2012 werd aangetoond dat het alle niet-lege (Sigma_1 ^ 1) - definieerbare teameigenschappen kan vastleggen.

4.2 Inclusielogica

Inclusielogica (Galliani 2012, Galliani & Hella 2013) breidt de logica van de eerste orde uit met inclusie-atomen (vec x / subseteq / vec y), die doet denken aan de inclusie-afhankelijkheden van de databasetheorie. De semantiek is:

TS-inc:

(M / models_X / vec x / subseteq / vec y) als en alleen als voor alle (s / in X) er een (s '\ in X) bestaat zodat (s (vec x) = s '(vec y)).

(begin {array} {l | cc} textbf {toewijzing} & / mathbf {x_1} & / mathbf {x_2} / \ hline s_0 & 0 & 0 \\ s_1 & 0 & 1 \\ s_2 & 1 & 2 \\ s_3 & 2 & 3 / einde {array})

Anders dan afhankelijkheids- en onafhankelijkheidslogica, is inclusielogica (zinvol) strikt zwakker dan existentiële logica van de tweede orde. In feite kan worden aangetoond (Galliani & Hella 2013) dat het equivalent is van het positieve fragment van de grootste vaste-puntlogica, en daarom PTIME-eigenschappen van modellen vastlegt boven eindig geordende modellen. Formulegewijs is inclusielogica strikt zwakker dan onafhankelijkheidslogica, maar onvergelijkbaar met afhankelijkheidslogica: inderdaad, de voorwaarden voor bevrediging van de formules zijn niet neerwaarts gesloten, maar ze worden gesloten door vakbonden in de zin dat

[M, X_i / models / phi / forall i / in I / Rightarrow M, / bigcup_i X_i / models / phi.)

4.3 Teamlogica

Teamlogica (Väänänen 2007a, b; Kontinen & Nurmi 2009) breidt de afhankelijkheidslogica uit door er een tegenstrijdige ontkenning aan toe te voegen (lnot). Het is equi-expressief met volledige tweede orde logica, zowel wat betreft de definieerbaarheid van klassen van modellen (Väänänen 2007b) als met betrekking tot de klassen van teams die teamlogische uitdrukkingen kunnen definiëren met betrekking tot een bepaald model (Kontinen & Nurmi 2009).

4.4 Intuïtionistische logica van afhankelijkheid

Intuitionistische afhankelijkheidslogica (Abramsky & Väänänen 2009; Yang 2013) breidt de afhankelijkheidslogica uit door een impliciete connectieve (phi / rightarrow / psi) toe te voegen, waarvan de tevredenheidsregels in team semantiek worden gegeven door

TS - (rightarrow):

(X / models / phi / rightarrow / psi) als en alleen als voor alle subsets (Y) van (X), als (Y / models / phi) dan (Y / modellen / psi).

Deze operator wordt de 'intuïtionistische implicatie' genoemd, vanwege de overeenkomst tussen de semantiek ervan en die van de implicatie-operator in Kripke's semantiek voor intuïtionistische logica (Kripke 1965). De interpretatie ervan in termen van overtuiging is vrij eenvoudig: als de opdrachten in (X) de toestanden vertegenwoordigen die sommige agenten mogelijk achten, dan kan een subset (Y) van (X) het resultaat vertegenwoordigen van een geloofsupdate waarin de agent een aantal eerder veronderstelde mogelijke toestanden van zaken afwijst, en (phi / rightarrow / psi) stelt dat een dergelijke update die ervoor zou zorgen dat (phi) vasthoudt, ook (psi) vasthouden. Vanuit dit oogpunt is dit een heel natuurlijk concept dat ons in staat stelt voorspellingen te beschrijven over hoe de algemene geloofsstatus van een dergelijke agent zou reageren op geloofsupdates.

Echter, vanwege de universele kwantificatie van de tweede orde die impliciet is in de semantiek ervan, is dit bindmiddel voldoende om de expressieve complexiteit van de logica sterk te vergroten: met name, zoals aangetoond in Yang 2013, is elke zin van logica van de tweede orde equivalent aan een zin van intuïtionistische afhankelijkheid logica. Intuitionistische afhankelijkheidslogica behoudt de eigenschap van neerwaartse sluiting: als een team voldoet aan een intuïtionistische formule voor afhankelijkheidslogica, dan doen alle subsets dat ook.

4.5 Propositionele afhankelijkheidslogica

De tot dusver beschouwde afhankelijkheids- en onafhankelijkheidsatomen drukken relaties uit tussen de mogelijke waarden van variabelen in een reeks opdrachten. Dezelfde noties van afhankelijkheid en onafhankelijkheid kunnen echter even vanzelfsprekend worden toegepast op de propositie zelf, zoals het gebeurt in natuurlijke taaluitdrukking zoals bijvoorbeeld "Of hij wel of niet slaagt voor de cursus hangt alleen af van de inhoud van zijn eindexamen".

Propositionele afhankelijkheid Logica beschouwt dergelijke atomen binnen de context van propositionele logica. Propositionele logica-afhankelijkheidsteams zijn sets van waarderingen (v) van propositionele atomen (p_1 / ldots p_n) tot ({T, F }). De semantische regels - en hun rechtvaardigingen - weerspiegelen zeer nauw die van de eerste-orde team semantiek, en de regel voor afhankelijkheidsatomen is

PTS-dep:

(X / models / eqord (p_1 / ldots p_n, q)) als en alleen als er twee taxaties (v_1, v_2 / in X) zijn die het eens zijn over de waarden van (p_1 / ldots p_n) ook overeenstemming over de waarde van (q).

Veel van de varianten en generalisaties van eerste-orde afhankelijkheidslogica kunnen zonder problemen worden verlaagd naar het propositionele niveau: zo is het bijvoorbeeld mogelijk om de eigenschappen van propositionele inclusielogica, propositionele teamlogica, propositionele intuïtionistische afhankelijkheidslogica enzovoort te bestuderen..

Terwijl (eerste-orde) afhankelijkheidslogica strikt expressiever is dan eerste-orde-logica, is propositionele-afhankelijkheidslogica niet expressiever dan propositionele logica, aangezien direct volgt uit het feit dat alle propositionele functies in propositionele logica uit te drukken zijn. Er bestaat echter een nauwe relatie tussen de teams van propositionele afhankelijkheidslogica en de informatietoestanden van inquisitieve logica (Groenendijk 2009; Ciardelli & Roelofsen 2011), een semantisch raamwerk voor de studie van het begrip betekenis en informatie-uitwisseling: in het bijzonder de implicatie van onderzoekende logica is precies hetzelfde als die van propositionele intuïtionistische afhankelijkheidslogica.

Axiomatisaties voor propositionele afhankelijkheidslogica en veel van de uitbreidingen ervan zijn te vinden in Yang & Väänänen 2016.

4.6 Modale afhankelijkheidslogica

Modale afhankelijkheidslogica (Väänänen 2008) en zijn varianten breiden de modale logica uit door er dezelfde afhankelijkheidsatomen (eqord (p_1 / ldots p_n, q)) aan toe te voegen die al werden overwogen in het geval van propositionele afhankelijkheidslogica.

De tevredenheidsvoorwaarden kunnen worden gedefinieerd door een variant van teamsemantiek waarin teams worden vervangen door sets van mogelijke werelden.

Veel onderzoek heeft de complexiteitstheoretische eigenschappen van deze logica, van de fragmenten en de uitbreidingen ervan onderzocht (Ebbing, Lohmann, & Yang 2011; Ebbing & Lohmann 2012; Lohmann & Vollmer 2013).

5. Toepassingen van afhankelijkheidslogica

5.1 Afhankelijkheidslogica en databasetheorie

Er is een duidelijke connectie tussen de teams van team semantiek en de relaties bestudeerd in relationele database theorie: gegeven een team (X) en een tupel variabelen (vec v = v_1 / ldots v_k) die voorkomen in haar opdrachten, het is mogelijk om de relatie (X (vec v) = { langle s (v_1), / ldots, s (v_n) rangle: s / in X }) te definiëren. Bovendien zijn de afhankelijkheidsatomen die worden bestudeerd in de afhankelijkheidslogica en de varianten daarvan analoog aan - en in veel gevallen afgeleid van - afhankelijkheden die in de databasetheorie worden overwogen, zoals functionele afhankelijkheden (Väänänen 2007a), meerwaardige afhankelijkheden (Engström 2012), en inclusie- en uitsluitingsafhankelijkheden (Galliani 2012). De relatie tussen afhankelijkheidslogica en databasetheorie heeft niet alleen bijgedragen aan de verdere ontwikkeling van de afhankelijkheidslogica, maar ook aan die van de databasetheorie: bijvoorbeeldin Hannula & Kontinen 2016 werd een eindige axiomatisatie van het onbeperkte implicatieprobleem voor inclusie, functionele en ingebedde database-theoretische afhankelijkheden met meerdere waarden gevonden door de studie van een soortgelijk probleem binnen de context van team semantiek.

5.2 Afhankelijkheidslogica en geloofsrepresentatie

Zoals besproken in Yang 2014 en Yang & Väänänen 2016, bestaat er een nauw verband tussen (propositionele) intuïtionistische afhankelijkheidslogica en onderzoekende logica (Ciardelli & Roelofsen, 2011), een raamwerk voor de studie van betekenis en informatie-uitwisseling tussen agenten. Meer in het algemeen laten de afhankelijkheidsatomen en connectieven die in team semantiek zijn bestudeerd natuurlijke interpretaties toe in termen van geloofstoestanden en geloofsupdates, zoals besproken in Galliani 2015. Op dit moment, de exacte aard van de relatie tussen dergelijke logica en dynamisch-epistemische logica en zijn varianten (Van Ditmarsch, van Der Hoek, & Kooi 2007) zijn grotendeels onontgonnen, maar er is voldoende reden om verdere verbanden te vermoeden tussen deze twee gebieden van wiskundige en filosofische logica.

5.3 Afhankelijkheidslogica en de stelling van Arrow

De stelling van Arrow (Arrow 1950) is een zeer invloedrijk resultaat van de sociale-keuzetheorie die, kort gezegd, laat zien dat er geen stemsysteem bestaat (dat wil zeggen, geen systeem voor het omzetten van rangschikkingen van individuele voorkeuren tussen alternatieven in een globale ranglijst van voorkeuren op maatschappelijk niveau) dat kan voldoen aan drie redelijk klinkende voorwaarden, namelijk

• Als elke kiezer (A) verkiest boven (B), geeft de groep als geheel de voorkeur aan (A) en (B);
• Of de groep als geheel de voorkeur geeft aan (A) boven (B) of omgekeerd, hangt uitsluitend af van de voorkeuren van elke kiezer met betrekking tot (A) en (B), en niet van hun voorkeuren met betrekking tot andere mogelijke alternatieven;
• Geen enkele kiezer is een dictator, dat wil zeggen dat de voorkeuren van de groep niet worden bepaald door de voorkeuren van een enkele kiezer.

Zoals de formulering zelf suggereert, laten de tweede en derde voorwaarde een natuurlijke lezing toe in termen van afhankelijkheid en onafhankelijkheid: in feite, zoals aangetoond in Pacuit & Yang 2016, kan de stelling van Arrow worden geformaliseerd in onafhankelijkheidslogica en worden bewezen in een geschikt natuurlijk aftreksysteem.

5.4 Quantum teamlogica en Bell's ongelijkheden

In Hyttinen, Paolini & Väänänen 2015 wordt een variant van propositionele teamlogica geïntroduceerd, genaamd quantumteamlogica. In dit formalisme worden teams vervangen door kwantumteams, die verschillen van de gewone teams van propositionele teamlogica doordat ze het mogelijk maken dat de waarden van bepaalde variabelen onbepaald zijn met betrekking tot bepaalde taxaties en doordat ze meerdere instanties van hetzelfde toestaan waardering (dus een kwantitatief aspect toevoegen aan team semantiek). Vervolgens wordt over kwantumteams een semantiek gedefinieerd voor een taal die ongelijkheden met betrekking tot de waarschijnlijkheid van gebeurtenissen mogelijk maakt, en daarvoor wordt een degelijk en volledig bewijssysteem ontwikkeld; en tot slot wordt aangetoond dat de ongelijkheden van Bell tegenvoorbeelden in deze systemen toelaten,zoals ze doen volgens de voorspellingen van de kwantummechanica en volgens experimenteel bewijs (Einstein, Podolsky, & Rosen 1935; Bell 1964; Aspect, Grangier, & Roger 1981), terwijl ze dat niet doen in de klassieke versie van dit raamwerk.

Bibliografie

• Abramsky, Samson en Jouko Väänänen, 2009, "From IF to BI: A Tale of Dependence and Separation", Synthese, 167 (2): 207–230. doi: 10.1007 / s11229-008-9415-6
• Arrow, Kenneth J., 1950, "A Difflict in the Concept of Social Welfare", The Journal of Political Economy, pp.328–346. doi: 10.1086 / 256963
• Aspect, Alain, Philippe Grangier en Gérard Roger, 1981, "Experimental Tests of Realistic Local Theories via Bell's Theorem", Physical Review Letters, 47 (7): 460–463. doi: 10.1103 / PhysRevLett.47.460
• Bell, JS, 1964, "On the Einstein-Podolsky-Rosen Paradox", Physics, 1 (3): 195-200.
• Ciardelli, Ivano en Floris Roelofsen, 2011, "Inquisitive Logic", Journal of Philosophical Logic, 40 (1): 55-94. doi: 10.1007 / s10992-010-9142-6
• van Ditmarsch, Hans, Wiebe van der Hoek, en Barteld Kooi, 2007, Dynamic Epistemic Logic, (Synthese Library 337), Dordrecht: Springer. doi: 10.1007 / 978-1-4020-5839-4
• Durand, Arnaud en Juha Kontinen, 2012, "Hierarchies in Dependence Logic", ACM Transactions on Computational Logic (TOCL), 13 (4): 1-21. doi: 10.1145 / 2362355.2362359
• Ebbing, Johannes en Peter Lohmann, 2012, "Complexity of Model Checking for Modal Dependence Logic", SOFSEM 2012: International Conference on Current Trends in Theory and Practice of Computer Science (Lecture Notes in Computer Science, 7147), Berlin, Heidelberg: Springer, pp. 226–237. doi: 10.1007 / 978-3-642-27660-6_19
• Ebbing, Johannes, Peter Lohmann en Fan Yang, 2013, "Model Checking for Modal Intuitionistic Dependence Logic", International Tbilisi Symposium on Logic, Language, and Computation 2011 (Lecture Notes in Computer Science, 7758), Berlin, Heidelberg: Springer, blz. 231–256. doi: 10.1007 / 978-3-642-36976-6_15
• Einstein, A., B. Podolsky en N. Rosen, 1935, "Kan de kwantummechanische beschrijving van de fysieke werkelijkheid als volledig worden beschouwd?" Physical Review, 47 (10): 777–780. doi: 10.1103 / PhysRev.47.777
• Engström, Fredrik, 2012, "Generalized Quantifiers in Dependence Logic", Journal of Logic, Language and Information, 21 (3): 299–324. doi: 10.1007 / s10849-012-9162-4
• Fagin, Ronald, 1974, 'Generalized First-Order Spectra and Polynomial-Time Recognizable Sets', Complexity of Computation (SIAM-AMS Proceedings 7), Richard M. Karp (red.), Providence, RI: American Mathematical Society, pp. 27–41.
• Galliani, Pietro, 2012, "Inclusie- en uitsluitingsafhankelijkheden in teamsemantiek - sommige logica's van onvolmaakte informatie", Annals of Pure and Applied Logic, 163 (1): 68–84. doi: 10.1016 / j.apal.2011.08.005
• –––, 2015, "The Doxastic Interpretation of Team Semantics", Logic Without Borders: Essays on Set Theory, Model Theory, Philosophical Logic and Philosophy of Mathematics (Ontos Mathematical Logic, 5), Åsa Hirvonen, Juha Kontinen, Roman Kossak, en Andrés Villaveces (eds), Berlijn, Boston: De Gruyter, pp. 167–192. doi: 10.1515 / 9781614516873.167
• Galliani, Pietro en Lauri Hella, 2013, "Inclusion Logic and Fixed Point Logic", Computer Science Logic 2013 (Leibniz International Proceedings in Informatics (LIPIcs), 23), Dagstuhl, Duitsland: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, pp. 281–295. doi: 10.4230 / LIPIcs. CSL.2013.281
• Galliani, Pietro en Jouko Väänänen, 2014, “On Dependence Logic”, in Johan van Benthem on Logic and Information Dynamics (Outstanding contributions to logic, 5), Alexandru Baltag en Sonja Smets (eds), Cham: Springer, pp. 101– 119. doi: 10.1007 / 978-3-319-06025-5_4
• Grädel, Erich en Jouko Väänänen, 2013, "Dependence and Independence", Studia Logica, 101 (2): 399–410. doi: 10.1007 / s11225-013-9479-2
• Groenendijk, Jeroen, 2009, "Inquisitive Semantics: Two Possibility for Disjunction", in Peter Bosch, David Gabelaia, & Jérôme Lang (eds), Zevende internationaal Tbilisi Symposium on Language, Logic, and Computation (Lecture Notes in Computer Science: Volume 5422), Springer-Verlag, blz. 80-94. doi: 10.1007 / 978-3-642-00665-4_8
• Hannula, Miika en Juha Kontinen, 2016, "A Finite Axiomatization of Conditional Independence and Inclusion Dependencies". Informatie en berekening, 249: 121–137. doi: 10.1016 / j.ic.2016.04.001
• Henkin, Leon, 1961, "Some Remarks on Infinitely Long Formulas", in Infinitistic Methods (Proceedings of the Symposium on the Foundations of Mathematics, Warsaw, 1959), Oxford: Pergamon Press, pp. 167–183.
• Hodges, Wilfrid, 1997, "Compositionele semantiek voor een taal met onvolmaakte informatie", Logic Journal of the IGPL, 5 (4): 539–563. doi: 10.1093 / jigpal / 5.4.539
• Hyttinen, Tapani, Gianluca Paolini en Jouko Väänänen, 2015, "Quantum Team Logic and Bell's Inequalities", The Review of Symbolic Logic, 8 (4): 722–742. doi: 10.1017 / S1755020315000192
• Kontinen, Juha en Ville Nurmi, 2009, "Team Logic and Second-Order Logic", in Proceedings of the 16th International Workshop on Logic, Language, Information, and Computation (Lezing Notes in Computer Science, 5514), Berlijn, Heidelberg: Springer, blz. 230–241. doi: 10.1007 / 978-3-642-02261-6_19
• Kontinen, Juha en Jouko Väänänen, 2009, "On Definability in Dependence Logic", Journal of Logic, Language and Information, 18 (3): 317–332.doi: 10.1007 / s10849-009-9082-0
• –––, 2011, “A Remark on Negation in Dependence Logic”, Notre Dame Journal of Formal Logic, 52 (1): 55–65. doi: 10.1215 / 00294527-2010-036
• –––, 2013, “Axiomatizing First-Order Consequences in Dependence Logic”, Annals of Pure and Applied Logic, 164 (11): 1101–1117. doi: 10.1016 / j.apal.2013.05.006
• Kripke, Saul A., 1965, 'Semantical Analysis of Intuitionistic Logic I', in Formal Systems and Recursive Functions: Proceedings of the Eighth Logic Colloquium, Oxford, juli 1963 (Studies in Logic and the Foundations of Mathematics, 40), John N. Crossley en Michael AE Dummett (red.), Noord-Holland, pp. 92–130. doi: 10.1016 / S0049-237X (08) 71685-9
• Lohmann, Peter en Heribert Vollmer, 2013, "Complexity Results for Modal Dependence Logic", Studia Logica, 101 (2): 343–366. doi: 10.1007 / s11225-013-9483-6
• Pacuit, Eric en Fan Yang, 2016, "Dependence and Independence in Social Choice: Arrow'S Theorem", in Dependence Logic, Samson Abramsky, Juha Kontinen, Jouko Väänänen en Heribert Vollmer (eds), Dordrecht: Springer, pp. 235–260. doi: 10.1007 / 978-3-319-31803-5_11
• Väänänen, Jouko, 2007a, Dependence Logic: A New Approach to Independence Friendly Logic, (studententeksten London Mathematical Society, 70), Cambridge: Cambridge University Press. doi: 10.1017 / CBO9780511611193
• –––, 2007b, "Team Logic", in Interactive Logic: Selected Papers from the 7th Augustus de Morgan Workshop, (Texts in Logic and Games, 1), Johan van Benthem, Dov Gabbay en Benedikt Löwe (red.), Amsterdam: Amsterdam University Press, pp. 281–302.
• –––, 2008, "Modal Dependence Logic", New Perspectives on Games and Interaction (Texts in Logic and Games, 4), Krzysztof R. Apt en Robert van Rooij (eds), Amsterdam: Amsterdam University Press, pp.237– 254.
• Yang, Fan, 2013, "Zinnen van de tweede orde uitdrukken in intuïtionistische afhankelijkheidslogica", Studia Logica, 101 (2): 323–342. doi: 10.1007 / s11225-013-9476-5
• –––, 2014, “Over uitbreidingen en varianten van afhankelijkheidslogica: een studie van intuïtionistische connectieven in de Team Semantics-setting”. Proefschrift, Universiteit van Helsinki.
• Yang, Fan en Jouko Väänänen, 2016, 'Propositionele logica van afhankelijkheid', Annalen van pure en toegepaste logica, 167 (7): 557–589. doi: 10.1016 / j.apal.2016.03.003

Academische hulpmiddelen

	Hoe deze vermelding te citeren.
	Bekijk een voorbeeld van de PDF-versie van dit item bij de Vrienden van de SEP Society.
	Zoek dit itemonderwerp op bij het Internet Philosophy Ontology Project (InPhO).
	Verbeterde bibliografie voor dit item op PhilPapers, met links naar de database.

Andere internetbronnen

• Dependence Logic op Wikipedia
• Presentaties in Academy Colloquium Dependence Logic, Amsterdam, 2014