Lindström kvantifierare

Inom matematisk logik är en Lindströmkvantifierare en generaliserad polyadisk kvantifierare . Lindströms kvantifierare generaliserar första ordningens kvantifierare, såsom den existentiella kvantifieraren , den universella kvantifieraren och de räknande kvantifierarna . De introducerades av Per Lindström 1966. De studerades senare för sina tillämpningar i logik i datavetenskap och databasfrågespråk .

Generalisering av första ordningens kvantifierare

För att underlätta diskussionen behöver vissa notationskonventioner förklaras. Uttrycket

$\phi ^{A,x,{\bar {a}}}=\{x\in A\ kolon A\models \phi [x,{\bar {a}}]\}$

för A en L -struktur (eller L -modell) i ett språk L , φ en L -formel, och ${\bar {a}}$ en tupel av element i domänen dom( A ) av A . Med andra ord, $\phi ^{A,x,{\bar {a}}}$ betecknar en ( monadisk ) egenskap definierad på dom(A). I allmänhet, där x ersätts av en n -tuppel ${\bar {x}}$ av fria variabler, $\phi ^{A,{\bar { x}},{\bar {a}}}$ betecknar en n -är relation definierad på dom( A ). Varje kvantifierare $Q_{A}$ relativiseras till en struktur, eftersom varje kvantifierare ses som en familj av relationer (mellan relationer) på den strukturen. För ett konkret exempel, ta de universella och existentiella kvantifierarna ∀ respektive ∃. Deras sanningsvillkor kan specificeras som

$A\models \forall x\phi [x,{\bar {a}}]\iff \phi ^{ A,x,{\bar {a}}}\in \forall _{A}$

$A\models \exists x\phi [x,{\bar {a}}]\iff \phi ^{A,x,{\bar {a}}}\i \exists _{A},$

där $\forall _{A}$ är singeln vars enda medlem är dom( A ), och $\exists _{A}$ är mängden av alla icke-tomma delmängder av dom( A ) (dvs. effektmängden dom( A ) minus den tomma mängden). Med andra ord är varje kvantifierare en familj av egenskaper på dom( A ), så var och en kallas en monadisk kvantifierare. Varje kvantifierare definierad som en n > 0-är relation mellan egenskaper på dom( A ) kallas monadisk . Lindström introducerade polyadiska sådana som är n > 0-ära relationer mellan relationer på strukturdomäner.

Innan vi går vidare till Lindströms generalisering, lägg märke till att vilken familj av fastigheter som helst på dom( A ) kan betraktas som en monadisk generaliserad kvantifierare. Till exempel är kvantifieraren "det finns exakt n saker sådana att..." är en familj av delmängder av domänen för en struktur, som var och en har en kardinalitet av storleken n . Sedan, "det finns exakt 2 saker så att φ" är sant i A iff mängden saker som är sådan att φ är en medlem av mängden av alla delmängder av dom( A ) av storlek 2 .

En Lindström-kvantifierare är en polyadisk generaliserad kvantifierare, så istället för att vara en relation mellan delmängder av domänen är den en relation mellan relationer definierade på domänen. Till exempel, kvantifieraren $Q_{A }x_{1}x_{2}y_{1}z_{1}z_{2}z_{3}(\phi (x_{1}x_{2}),\psi (y_{1}),\theta (z_{1}z_{2}z_{3}))$ definieras semantiskt som

${\displaystyle A\models Q_{A}x_{1}x_{2}y_{1}z_{1}z_{2}z_{3}(\ phi ,\psi ,\theta )[a]\iff (\phi ^{A,x_{1}x_{2},{\bar {a}}},\psi ^{A,y_{1},{ \bar {a}}},\theta ^{A,z_{1}z_{2}z_{3},{\bar {a}}})\i Q_{A}} [$

var

$\phi ^{A,{\bar {x}} ,{\bar {a}}}=\{(x_{1},\dots ,x_{n})\in A^{n}\colon A\models \phi [{\bar {x}},{ \bar {a}}]\}$

för en n -tuppel ${\bar {x}}$ av variabler.

Lindströms kvantifierare klassificeras enligt nummerstrukturen för deras parametrar. Till exempel $Qxy\phi (x)\psi (y)$ är en typ (1,1) kvantifierare, medan ${\ displaystyle Qxy\phi (x,y)}$ är en typ (2) kvantifierare. Ett exempel på typ (1,1) kvantifierare är Hartigs kvantifierare som testar ekvikardinalitet, dvs förlängningen av {A, B ⊆ M: |A| = |B|}. Ett exempel på en kvantifierare av typ (4) är Henkin-kvantifieraren .

Expressivitetshierarki

Det första resultatet i denna riktning erhölls av Lindström (1966) som visade att en typ (1,1) kvantifierare inte var definierbar i termer av en typ (1) kvantifierare. Efter att Lauri Hella (1989) utvecklat en allmän teknik för att bevisa kvantifierarnas relativa uttrycksförmåga, visade sig den resulterande hierarkin vara lexikografiskt ordnad efter kvantifierartyp:

(1) < (1, 1) < . . . < (2) < (2, 1) < (2, 1, 1) < . . . < (2, 2) < . . . (3) < . . .

För varje typ t finns det en kvantifierare av den typen som inte är definierbar i första ordningens logik utökad med kvantifierare som är av typer mindre än t .

Som föregångare till Lindströms sats

Även om Lindström endast delvis hade utvecklat den hierarki av kvantifierare som nu bär hans namn, räckte det för honom att observera att några fina egenskaper hos första ordningens logik går förlorade när den utökas med vissa generaliserade kvantifierare. Till exempel, att lägga till en "det finns ändligt många" kvantifierare resulterar i en förlust av kompakthet , medan att lägga till en "det finns oräkneligt många" kvantifierare till första ordningens logik resulterar i en logik som inte längre uppfyller Löwenheim– Skolem-satsen . År 1969 visade Lindström ett mycket starkare resultat som nu kallas Lindströms teorem , som intuitivt säger att första ordningens logik är den "starkaste" logiken som har båda egenskaperna.

Algoritmisk karakterisering

• Lindström, P. (1966). "Första ordningens predikatlogik med generaliserade kvantifierare". Teori . 32 (3): 186–195. doi : 10.1111/j.1755-2567.1966.tb00600.x .
• L. Hella. "Definability hierarchies of generalized quantifiers", Annals of Pure and Applied Logic , 43(3):235–271, 1989, doi : 10.1016/0168-0072(89)90070-5 .
• L. Hella. "Logiska hierarkier i PTIME". I Proceedings of the 7th IEEE Symposium on Logic in Computer Science , 1992.
• L. Hella, K. Luosto och J. Vaananen. "Hierarkisatsen för generaliserade kvantifierare". Journal of Symbolic Logic , 61(3):802–817, 1996.
•   Burtschick, Hans-Jörg; Vollmer, Heribert (1999), Lindström Quantifiers and Leaf Language Definability , ECCC TR96-005
• Westerståhl, Dag (2001), "Quantifiers", i Goble, Lou (red.), The Blackwell Guide to Philosophical Logic , Blackwell Publishing, s. 437–460 .
•   Antonio Badia (2009). Kvantifierare i aktion: Generaliserad kvantifiering i fråga, logiska och naturliga språk . Springer. ISBN 978-0-387-09563-9 .

Vidare läsning

•   Jouko Väänanen (red.), Generaliserade kvantifierare och beräkningar. 9:e Europeiska sommarskolan i logik, språk och information. ESSLLI'97 Workshop. Aix-en-Provence, Frankrike, 11–22 augusti 1997. Reviderade föreläsningar , Springer Lecture Notes in Computer Science 1754, ISBN 3-540-66993-0

externa länkar

• Dag Westerståhl, 2011. ' Generalized Quantifiers '. Stanford Encyclopedia of Philosophy .