Boolean-värderad modell

Inom matematisk logik är en boolesk-värderad modell en generalisering av den vanliga Tarskianska föreställningen om struktur från modellteorin . I en booleskt värderad modell sanningsvärdena för propositioner inte begränsade till "sant" och "falskt", utan tar istället värden i någon fast fullständig boolesk algebra .

Boolesk-värderade modeller introducerades av Dana Scott , Robert M. Solovay och Petr Vopěnka på 1960-talet för att hjälpa till att förstå Paul Cohens metod för att tvinga . De är också relaterade till Heyting algebra semantik i intuitionistisk logik .

Definition

Fixa en komplett boolesk algebra B och ett första ordningens språk L ; signaturen för L kommer att bestå av en samling konstantsymboler, funktionssymboler och relationssymboler .

0,...,an-1> of elements of 0 En booleskt värderad modell för språket L består av ett universum M , som är en uppsättning element (eller namn ), tillsammans med tolkningar för symbolerna. Specifikt måste modellen tilldela varje konstant symbol för L ett element av M , och till varje n -är funktionssymbol f för L och varje n -tuppel <a i=20><a i=21><a i=22><a i=23><a ,...,a n -1 > M , modellen måste tilldela ett element av M till termen f (a ,...,a n -1 ).

0,...,an-1> of elements of 0 Tolkningen av atomformlerna för L är mer komplicerad. Till varje par a och b av element av M måste modellen tilldela ett sanningsvärde || a = b || till uttrycket a = b ; detta sanningsvärde är hämtat från den booleska algebra B . På liknande sätt, för varje n -är relationssymbol R av L och varje n -tupel <a i=29><a i=30><a i=31><a i=32><a ,...,a n -1 > M , måste modellen tilldela ett element av B för att vara sanningsvärdet || R (a ,...,an - 1 )||.

Tolkning av andra formler och meningar

Atomformlernas sanningsvärden kan användas för att rekonstruera sanningsvärdena för mer komplicerade formler, med hjälp av den booleska algebras struktur. För propositionella bindemedel är detta enkelt; man tillämpar helt enkelt motsvarande booleska operatorer på underformlernas sanningsvärden. Till exempel, om φ( x ) och ψ( y , z ) är formler med en respektive två fria variabler och om a , b , c är element i modellens universum som ska ersätta x , y och z , då sanningsvärdet av

är helt enkelt

Fullständigheten hos den booleska algebra krävs för att definiera sanningsvärden för kvantifierade formler. Om φ( x ) är en formel med fri variabel x (och eventuellt andra fria variabler som är undertryckta), då

där den högra sidan ska förstås som det högsta i B av mängden av alla sanningsvärden ||φ( a )|| som ett intervall över M .

Sanningsvärdet för en formel är en del av den fullständiga booleska algebra B .

Boolesk-värderade modeller för mängdlära

Givet en komplett boolesk algebra B finns det en booleskt värderad modell betecknad med V B , som är den booleskvärderade analogen till von Neumann-universumet V . (Strängt taget V B en riktig klass , så vi måste omtolka vad det innebär att vara en modell på lämpligt sätt.) Informellt är elementen i V B "booleskt värderade uppsättningar". Med en vanlig uppsättning A är varje uppsättning antingen medlem eller inte; men givet en booleskt värderad uppsättning har varje uppsättning en viss, fast medlemskapsgrad i A .

Elementen i uppsättningen med booleskt värde är i sin tur också uppsättningar med booleskt värde, vars element också är uppsättningar med booleskt värde, och så vidare. För att få en icke-cirkulär definition av booleskt värdead mängd definieras de induktivt i en hierarki som liknar den kumulativa hierarkin . För varje ordinal a av enligt följande . V definieras mängden VBa

  • 0 V B är den tomma uppsättningen.
  • V B α+1 är mängden av alla funktioner från V B α till B . (En sådan funktion representerar en delmängd av V B α ; om f är en sådan funktion, då för varje x V B α , är värdet f ( x ) medlemskapsgraden för x i mängden.)
  • Om α är en gränsordinal är V B α föreningen av V B β för β < α.

Klassen VB . definieras som föreningen av alla mängder VBα

Det är också möjligt att relativisera hela denna konstruktion till någon transitiv modell M av ZF (eller ibland ett fragment därav). Den booleska modellen M B erhålls genom att tillämpa ovanstående konstruktion inuti M . Begränsningen till transitiva modeller är inte allvarlig, eftersom Mostowskis kollapssats antyder att varje "rimlig" (välgrundad, extensionell) modell är isomorf till en transitiv. (Om modellen M inte är transitiv blir saker stökigare, eftersom M: s tolkning av vad det innebär att vara en "funktion" eller en "ordinal" kan skilja sig från den "externa" tolkningen.)

När väl elementen i V B har definierats enligt ovan är det nödvändigt att definiera B -värderade relationer av jämlikhet och medlemskap på V B . VB Här VB är en B VB - värderad relation på en funktion från × till B. För att undvika förväxling med den vanliga jämlikheten och medlemskapet betecknas dessa med || x = y || och || x y || för x och y i V B . De definieras enligt följande:

|| x y || definieras som Σ t ∈Dom( y ) || x = t || ∧ y ( t ) (" x är i y om det är lika med något i y ").
|| x = y || definieras som || x y || ∧ || y⊆ x || (" x är lika med y om x och y båda är delmängder av varandra"), där
|| x y || definieras som Π t ∈Dom( x ) x ( t ) ⇒ || t y || (" x är en delmängd av y om alla element i x är i y ")

Symbolerna Σ och Π betecknar operationerna med minst övre gräns respektive största nedre gräns i den fullständiga booleska algebra B . Vid första anblicken verkar definitionerna ovan vara cirkulära: || ∈ || beror på || = ||, vilket beror på || ⊆ ||, vilket beror på || ∈ ||. En närmare granskning visar dock att definitionen av || ∈ || beror bara på || ∈ || för element av mindre rang, så || ∈ || och || = || är väldefinierade funktioner från V B × V B till B .

Det kan visas att B -värderade relationer || ∈ || och || = || på V B gör V B till en boolesk-värderad modell för mängdteori. Varje mening i första ordningens mängdteori utan fria variabler har ett sanningsvärde i B ; det måste visas att axiomen för likhet och alla axiomen i ZF mängdlära (skrivna utan fria variabler) har sanningsvärdet 1 (det största elementet i B ). Detta bevis är enkelt, men det är långt eftersom det finns många olika axiom som måste kontrolleras.

Förhållande till tvång

Mängdteoretiker använder en teknik som kallas forcering för att erhålla oberoende resultat och för att konstruera modeller för mängdteori för andra syften. Metoden utvecklades ursprungligen av Paul Cohen men har utökats kraftigt sedan dess. I en form, tvingande "lägger till i universum" en generisk delmängd av en poset , är poset designad för att påtvinga intressanta egenskaper på det nyligen tillagda objektet. Rynkan är att (för intressanta posetter) kan det bevisas att det helt enkelt finns någon sådan generisk delmängd av poset. Det finns tre vanliga sätt att hantera detta:

  • syntaktisk forcering En forceringsrelation definieras mellan elementen p i poseten och formlerna φ i det tvingande språket . Denna relation definieras syntaktisk och har ingen semantik; det vill säga, ingen modell tillverkas någonsin. Snarare, utgående från antagandet att ZFC (eller någon annan axiomatisering av mängdteorin) bevisar det oberoende påståendet, visar man att ZFC också måste kunna bevisa en motsägelse. Forceringen är dock "över V "; det vill säga det är inte nödvändigt att börja med en räknebar transitiv modell. Se Kunen (1980) för en beskrivning av denna metod.
  • countable transitive models Man börjar med en räknebar transitiv modell M av så mycket av mängdteorin som behövs för det önskade syftet, och som innehåller poset. Sedan finns det filter på poset som är generiska över M ; det vill säga som möter alla täta öppna delmängder av poset som också råkar vara element i M .
  • fiktiva generiska objekt Vanligtvis kommer mängdteoretiker helt enkelt att låtsas att posen har en delmängd som är generisk över hela V . Detta generiska objekt, i icke-triviala fall, kan inte vara en del av V och därför "finns inte riktigt". (Naturligtvis är det en filosofisk tvist om några uppsättningar "verkligen existerar", men det ligger utanför ramen för den aktuella diskussionen.) Kanske överraskande, med lite övning är denna metod användbar och tillförlitlig, men den kan vara filosofiskt sett. otillfredsställande.

Boolean-värderade modeller och syntaktisk forcering

Boolean-värderade modeller kan användas för att ge semantik till syntaktisk forcering; priset som betalas är att semantiken inte är 2-värdig ("true or false"), utan tilldelar sanningsvärden från någon komplett boolesk algebra. Givet en tvingande poset P , finns det en motsvarande komplett boolesk algebra B , ofta erhållen som samlingen av vanliga öppna delmängder av P , där topologin P definieras genom att förklara alla nedre mängder öppna (och alla övre mängder stängda). (Andra tillvägagångssätt för att konstruera B diskuteras nedan.)

Nu kan ordningen på B (efter att ha tagit bort nollelementet) ersätta P i forceringssyfte, och forceringsrelationen kan tolkas semantiskt genom att säga att för p ett element av B och φ en formel för det tvingande språket,

där ||φ|| är sanningsvärdet för φ i V B .

Detta tillvägagångssätt lyckas tilldela en semantik att tvinga över V utan att tillgripa fiktiva generiska objekt. Nackdelarna är att semantiken inte är 2-värderad, och att kombinatoriken för B ofta är mer komplicerad än den för den underliggande poset P .

Booleskt värderade modeller och generiska objekt över räkningsbara transitiva modeller

En tolkning av forcering börjar med en räknebar transitiv modell M av ZF-mängdteori, en partiellt ordnad mängd P och en "generisk" delmängd G av P , och konstruerar en ny modell av ZF-mängdteori från dessa objekt. (Villkoren att modellen ska vara räknbar och transitiv förenklar vissa tekniska problem, men är inte väsentliga.) Cohens konstruktion kan utföras med hjälp av booleskt värderade modeller enligt följande.

  • Konstruera en komplett boolesk algebra B som den kompletta booleska algebra "genererad av" poseten P .
  • Konstruera ett ultrafilter U B (eller motsvarande en homomorfism från B till den booleska algebra {sant, falskt}) från den generiska delmängden G av P .
  • Använd homomorfismen från B till {true, false} för att förvandla den booleska modellen M B i avsnittet ovan till en vanlig modell av ZF.

Vi förklarar nu dessa steg mer i detalj.

För varje poset P finns det en komplett boolesk algebra B och en karta e från P till B + (de icke-nollelement i B ) så att bilden är tät, e ( p ) ≤ e ( q ) när p q , och e ( p ) e ( q )=0 närhelst p och q är inkompatibla. Denna booleska algebra är unik upp till isomorfism. Den kan konstrueras som algebra för vanliga öppna mängder i det topologiska rummet av P ( med underliggande mängd P , och en bas som ges av mängderna Up av element q med q p ).

Kartan från poset P till den fullständiga booleska algebra B är inte injektiv i allmänhet. Kartan är injektiv om och endast om P har följande egenskap: om varje r p är kompatibel med q , då p q .

Ultrafiltret U B definieras som uppsättningen av element b av B som är större än något element av (bilden av) G . Givet ett ultrafilter U på en boolesk algebra får vi en homomorfism till {true, false} genom att mappa U till sant och dess komplement till falskt. Omvänt, givet en sådan homomorfism, är den omvända bilden av sant ett ultrafilter, så ultrafilter är i huvudsak samma som homomorfismer till {true, false}. (Algebraister kanske föredrar att använda maximala ideal istället för ultrafilter: komplementet till ett ultrafilter är ett maximalt ideal, och omvänt är komplementet till ett maximalt ideal ett ultrafilter.)

Om g är en homomorfism från en boolesk algebra B till en boolesk algebra C och MB M är vilken som helst B -värderad modell av ZF (eller av någon annan teori för den delen) kan vi förvandla B till en C -värderad modell genom att tillämpa homomorfism g till värdet av alla formler. I synnerhet om C är {true, false} får vi en {true, false}-värderad modell. Detta är nästan detsamma som en vanlig modell: i själva verket får vi en vanlig modell på uppsättningen av ekvivalensklasser under || = || av en {sant, falsk}-värderad modell. Så vi får en vanlig modell av ZF-mängdlära genom att utgå från M , en boolesk algebra B och ett ultrafilter U B . (ZF-modellen konstruerad så här är inte transitiv. I praktiken tillämpar man Mostowskis kollapssats för att göra detta till en transitiv modell.)

Vi har sett att forcering kan göras med booleskt värderade modeller, genom att konstruera en boolesk algebra med ultrafilter från en poset med en generisk delmängd. Det är också möjligt att gå tillbaka åt andra hållet: givet en boolesk algebra B , kan vi bilda en poset P av alla element som inte är noll i B , och ett generiskt ultrafilter på B begränsar till en generisk uppsättning på P . Så teknikerna för forcering och booleskt värderade modeller är i huvudsak likvärdiga.

Anteckningar

  1. ^ a b B här ​​antas vara icke degenererad ; det vill säga 0 och 1 måste vara distinkta element av B . Författare som skriver på booleska modeller ser vanligtvis att detta krav är en del av definitionen av "boolesk algebra", men författare som skriver på booleska algebror i allmänhet gör det ofta inte.
  •   Bell, JL (1985) Boolean-Valued Models and Independence Proofs in Set Theory, Oxford. ISBN 0-19-853241-5
  • Grishin, VN (2001) [1994], "Boolean-valued model" , Encyclopedia of Mathematics , EMS Press
  •    Jech, Thomas (2002). Mängdlära, tredje millennieupplagan (reviderad och utökad) . Springer. ISBN 3-540-44085-2 . OCLC 174929965 .
  •    Kunen, Kenneth (1980). Mängdlära: En introduktion till oberoende bevis . Nord-Holland. ISBN 0-444-85401-0 . OCLC 12808956 .
  •    Kusraev, AG och SS Kutateladze (1999). Boolean värderad analys . Kluwer Academic Publishers. ISBN 0-7923-5921-6 . OCLC 41967176 . Innehåller en redogörelse för booleskt värderade modeller och tillämpningar på Riesz-rum, Banach-rum och algebror.
  •    Manin, Yu. I. (1977). En kurs i matematisk logik . Springer. ISBN 0-387-90243-0 . OCLC 2797938 . Innehåller en redogörelse för forcering och booleskt värderade modeller skrivna för matematiker som inte är mängdteoretiker.
  • Rosser, J. Barkley (1969). Förenklade oberoende bevis, booleska värderade modeller för mängdteori . Akademisk press.