Infinitär Logik

Innehållsförteckning:

Infinitär Logik
Infinitär Logik

Video: Infinitär Logik

Video: Infinitär Logik
Video: Независимые события (основы вероятности: независимость двух событий) 2024, Mars
Anonim

Inmatningsnavigering

  • Inmatningsinnehåll
  • Bibliografi
  • Akademiska verktyg
  • Vänner PDF-förhandsvisning
  • Författare och Citation Info
  • Tillbaka till toppen

Infinitär logik

Först publicerad Sun 23 januari 2000; substantiell revidering fredag 26 februari 2016

Traditionellt har uttryck i formella system betraktats som betydande begränsade inskriptioner som - åtminstone i princip - kan skrivas ut i primitiva notationer. Men det faktum att (första ordning) formler kan identifieras med naturliga nummer (via "Gödel-numrering") och därmed med ändliga uppsättningar gör det inte längre nödvändigt att betrakta formler som inskriptioner, och antyder möjligheten att skapa "språk" vissa av vars formler naturligtvis identifieras som oändliga uppsättningar. Ett "språk" av detta slag kallas ett infinitärt språk: i den här artikeln diskuterar jag de infinitära språk som kan erhållas på ett enkelt sätt från första ordningens språk genom att tillåta konjunktioner, disjunktioner och eventuellt kvantifieringssekvenser att vara av oändliga längd. Under diskussionen framgår att även om den uttrycksfulla kraften i sådana språk långt överskrider den hos deras finitiska (första ordning) motsvarigheter, har mycket få av dem de "attraktiva" egenskaperna (t.ex. kompakthet och fullständighet) hos den senare. Följaktligen förtjänar de infinitära språken som faktiskt har dessa funktioner speciell uppmärksamhet.

I §1 fastställs grundläggande syntax och semantik för infinitära språk; deras uttrycksfulla kraft visas sedan med hjälp av exempel. §2 ägnas åt de infinitära språk som endast tillåter begränsade kvantifieringssekvenser: dessa språk visar sig vara relativt väl uppförda. §3 ägnas åt en diskussion om kompakthetsproblemet för infinitära språk och dess koppling till rent set-teoretiska frågor om”stora” kardinalnummer. I §4 ritas ett argument som visar att de flesta "oändliga kvantifierare" -språk har en andra ordning och är, ipso facto, mycket ofullständiga. §5 ger en kort redogörelse för en viss speciell klass av underspråk på infinitära språk för vilka en tillfredsställande generalisering av kompakthetsteorem kan bevisas. Detta avsnitt innehåller ett underavsnitt om definitionen av tillåtna uppsättningar. Historiska och bibliografiska kommentarer återfinns i §6.

  • 1. Definition och grundläggande egenskaper för infinitära språk
  • 2. Finite-kvantifieringsspråk
  • 3. Egenskaperna för kompaktitet
  • 4. Ofullständighet i oändliga kvantifieringsspråk
  • 5. Underspråk för L (ω 1, ω) och Barwise Compactness Theorem

    5.1 Definition av begreppet tillåtet set

  • 6. Historiska och bibliografiska anmärkningar
  • Bibliografi
  • Akademiska verktyg
  • Andra internetresurser
  • Relaterade poster

1. Definition och grundläggande egenskaper för infinitära språk

Med tanke på ett par κ, λ av oändliga kardinaler så att λ ≤ κ, definierar vi en klass infinitära språk i vart och ett av vilka vi kan bilda konjunktioner och disjunktioner av uppsättningar av uppsättningar med kardinalitet <κ och kvantifieringar över sekvenser av variabler med längd < λ.

Låt L - det (finitära) basspråket - vara ett godtyckligt men fast första ordningsspråk med valfritt antal extralogiska symboler. Det infinitära språket L (κ, λ) har följande grundläggande symboler:

  • Alla symboler för L
  • En uppsättning Var av enskilda variabler, där kardinaliteten hos Var (skriven: | Var |) är κ
  • En logisk operatör ∧ (infinitär konjunktion)

Klassen för förformuleringar av L (κ, λ) definieras rekursivt enligt följande:

  • Varje formel av L är en förformel;
  • om φ och ψ är förformler, så är φ∧ψ och ¬φ;
  • om Φ är en uppsättning förformuler så att | Φ | <K, då är a en förformel;
  • om φ är en förformel och X ⊆ Var är sådan att | X | <λ, då är ∃ X a en förformel;
  • alla förformler definieras av ovanstående klausuler.

Om Φ är en uppsättning förformler som indexeras av en uppsättning I, säger Φ = {φ i: i ∈ I}, kommer vi överens om att skriva ∧Φ för:

i ∈ I  φ

eller, om jag är uppsättningen med naturliga siffror, skriver vi ∧Φ för:

φ 0 ∧ φ 1 ∧ …

Om X är en uppsättning individuella variabler som indexeras av en ordinal α, säger X = {x ξ: ξ <α}, håller vi med om att skriva (∃ x ξ) ξ <α φ för ∃ X φ.

De logiska operatörerna ∨, →, ↔ definieras på vanligt sätt. Vi introducerar också operatörerna ∨ (infinitär disjunktion) och ∀ (universal kvantifiering) av

∨Φ = df ¬∧ {¬φ: φ ∈ Φ}

∀Xφ = df ¬∃X¬φ,

och använder liknande konventioner som för ∧, ∃.

Således är L (κ, λ) det infinitära språket som erhållits från L genom att tillåta konjunktioner och disjunktioner av längd <κ och kvantifieringar [1] av längd <λ. Språk L (κ, ω) kallas finit-kvantifieringsspråk, resten oändliga kvantifieringsspråk. Observera att L (ω, ω) bara är L själv.

Lägg märke till följande avvikelse som kan uppstå på ett infinitärt språk men inte på ett finitalt språk. På språket L (ω 1, ω), som möjliggör oändligt många konjunktioner men endast begränsade kvantifieringar, finns det förformler med så många fria variabler att de inte kan "stängas" i meningar av L (ω 1, ω) genom att prefixa kvantifierare. Så är fallet till exempel för L (ω 1, ω) -preformeln

x 0 <x 1 ∧ x 1 <x 2 ∧ … ∧ x n <x n +1 …,

där L innehåller den binära relationssymbolen <. Av denna anledning gör vi följande

Definition. En formel för L (κ, λ) är en förformel som innehåller <λ fria variabler. Uppsättningen av alla formler för L (κ, λ) kommer att betecknas med form (L (κ, λ)) eller helt enkelt form (κ, λ) och uppsättningen av alla meningar med skickat (L (κ, λ)) eller helt enkelt skickat (κ, λ).

Observera i detta sammanhang att i allmänhet ingenting skulle erhållas genom att överväga "språk" L (κ, λ) med λ> κ. Till exempel, i "språket" L (ω, ω 1), kommer formler endast att ha ändligt många gratisvariabler, medan det finns en mängd "värdelösa" kvantifierare som kan binda oändligt många gratisvariabler. [2]

Efter att ha definierat syntaxen för L (κ, λ), skisserar vi nästa semantik. Eftersom de extralogiska symbolerna för L (κ, λ) bara är de för L, och det är dessa symboler som bestämmer formen för strukturerna där ett givet första ordningsspråk ska tolkas, är det naturligt att definiera en L (κ, λ) -struktur för att helt enkelt vara en L-struktur. Begreppet en formel av L (κ, λ) som uppfylls i en L-struktur A (av en sekvens av element från domänen till A) definieras på samma induktiva sätt som för formler av L förutom att vi måste lägga till två extra klausuler som motsvarar klausulerna för ∧Φ och ∃Xφ i definitionen av preformula. I dessa två fall definierar vi naturligtvis:

∧Φ är nöjd i A (av en given sekvens) ⇔ för alla φ ∈ Φ, φ är nöjd i A (av sekvensen);

∃ X φ är uppfyllt i A ⇔ finns det en sekvens av element från domänen av A i bijektiv korrespondens med X, som satisfierar O i A.

Dessa informella definitioner måste skärpas upp i en rigorös utveckling, men deras betydelse borde vara tydlig för läsaren. Nu blir de vanliga uppfattningarna om sanning, giltighet, tillfredsställelse och modell för formler och meningar av L (κ, λ) tillgängliga. I synnerhet, om A är en L-struktur och σ ∈ Skickat (κ, λ), ska vi skriva A σ σ för A är en modell av σ, och ⊨ σ för σ är giltig, det vill säga för alla A, A ⊨ σ. Om Δ ⊆ Skickat (κ, λ), ska vi skriva Δ ⊨ σ för σ är en logisk konsekvens av Δ, det vill säga varje modell av Δ är en modell av σ.

Vi ger nu några exempel avsedda att visa uttryckskraften hos de infinitära språken L (κ, λ) med κ ≥ ω 1. I båda fallen är det välkänt att begreppet i fråga inte kan uttryckas på något första ordningsspråk.

Karakterisering av standardmodellen för aritmetik i L (ω 1, ω). Här är standardmodellen för aritmetik strukturen N = ⟨N, +, ·, s, 0⟩, där N är uppsättningen av naturliga siffror, +, · och 0 har sina vanliga betydelser, och s är efterföljaren. Låt L vara den första ordningens språk lämpligt för N. Sedan sammanfaller klassen av L-strukturer som är isomorf till N med klassen av modeller i samband med följande L (ω 1, ω) meningar (där 0 är ett namn på 0):

m ∈ωn ∈ω s m 0 + s n 0 = s m + n 0

m ∈ωn ∈ω s m 0 · s n 0 = s m · n 0

m ∈ωn ∈ω− {m} s m 0 ≠ s n 0

∀ x ∨ m ∈ω x = s m 0

Termerna s n x definieras rekursivt av

s 0 x = x
s n +1 x = s (s n x)

Karaktärisering av klassen för alla ändliga uppsättningar i L (ω 1, ω). Här har basspråket inga extralogiska symboler. Klassen för alla ändliga uppsättningar sammanfaller sedan med klassen för modeller av L (ω 1, ω) -sensensen

n ∈ω ∃ v 0 … ∃ v n ∀ x (x = v 0 ∨ … ∨ x = v n).

Sanningsdefinition i L (ω 1, ω) för ett räknbart basspråk L. Låt L vara ett räknat första ordningsspråk (till exempel språket i aritmetik eller uppsättningsteori) som innehåller ett namn n för varje naturligt tal n, och låt σ 0, σ 1, … vara en uppräkning av dess meningar. Sedan L (ω 1, ω) -formeln

Tr (x) = dfn ∈ω (x = n ∧ σ n)

är en sanningspredikat för L i den meningen som meningen

Tr (n) ↔ σ n

är giltigt för varje n.

Karaktärisering av välbeställningar i L (ω 1, ω 1). Basspråket L inkluderar här en binär predikatsymbol ≤. Låt σ 1 vara den vanliga L-meningen som karakteriserar linjära ordningar. Sedan sammanfaller klassen av L-strukturer där tolkningen av ≤ är en välordnad sammansättning med klassen av modeller för L (ω 1, ω 1) meningen σ = σ 1 ∧ σ 2, där

σ 2 = df (∀ v n) n ∈ω ∃ x [∨ n ∈ω (x = v n) ∧ ∧ n ∈ω (x ≤ v n)].

Lägg märke till att meningen σ 2 innehåller en oändlig kvantifierare: den uttrycker den väsentligen andra ordningens påstående att varje räknbar delmängd har en minst medlem. Det kan faktiskt visas att förekomsten av denna oändliga kvantifierare är väsentlig: klassen av välordnade strukturer kan inte karakteriseras i något begränsat språk. Detta exempel indikerar att oändliga kvantifieringsspråk som L (ω 1, ω 1) uppför sig snarare som andra ordens språk; Vi kommer att se att de delar bristernas brister (ofullständighet) såväl som några av deras fördelar (stark uttrycksfull kraft).

Många tillägg av första ordens språk kan översättas till infinitära språk. Tänk till exempel det generaliserade kvantifieringsspråket L (Q 0) erhållet från L genom att lägga till en ny kvantifieringssymbol Q 0 och tolka Q 0 x φ (x) eftersom det finns oändligt många x så att φ (x). Man ser lätt att meningen Q 0 x φ (x) har samma modeller som L (ω 1, ω) -sensensen

¬∨ n ∈ω ∃ v 0 … ∃ v n ∀ x [φ (x) → (x = v 0 ∨ … ∨ x = v n)].

Således är L (Q 0), i naturlig mening, översättbara till L (ω 1, ω). Ett annat språk som kan översättas till L (ω 1, ω) i detta avseende är det svaga andra ordningsspråket som erhålls genom att lägga till en räknbar uppsättning av monadiska predikatvariabler till L som sedan tolkas som sträcker sig över alla ändliga uppsättningar av individer.

Språk med godtyckligt långa konjunktioner, disjunktioner och (eventuellt) kvantifieringar kan också införas. För en fast oändlig kardinal λ definieras språket L (∞, λ) genom att ange dess klass med formler, Form (∞, λ), som ska vara unionen, över alla κ ≥ λ, i uppsättningarna Form (κ, λ)). Således tillåter L (∞, λ) godtyckligt långa konjunktioner och disjunktioner, i den meningen att om Φ är en godtycklig delmängd av formen (∞, λ), så är både ∧Φ och ∨Φ medlemmar av formen (∞, λ). Men L (∞, λ) medger bara kvantifieringar av längden <λ: alla dess formler har <λ fria variabler. Språket L (∞, ∞) definieras i sin tur genom att ange dess klass av formler, Form (∞, ∞), för att vara unionen, över alla oändliga kardinaler λ, av klasserna Form (∞, λ). Så L (∞, ∞) tillåter godtyckligt långa kvantifieringar utöver godtyckligt långa konjunktioner och disjunktioner. Observera att Form (∞, λ) och Form (∞, ∞) är korrekta klasser i betydelsen av Gödel-Bernays uppsättningsteori. Tillfredsställelse med formlerna för L (∞, λ) och L (∞, ∞) i en struktur kan definieras av en uppenbar förlängning av motsvarande uppfattning för L (κ, λ).

2. Finite-kvantifieringsspråk

Vi har påpekat att oändliga kvantifieringsspråk som L (ω 1, ω 1) liknar andra ordningsspråk i den mån de tillåter kvantifiering över oändliga uppsättningar av individer. Det faktum att detta inte är tillåtet på finit-kvantifieringsspråk tyder på att dessa i vissa avseenden kan ligga närmare deras första ordnings motsvarigheter än vad som är uppenbart vid första anblicken. Vi ska se att detta verkligen är fallet, särskilt när det gäller L (ω 1, ω).

Språket L (ω 1, ω) upptar en speciell plats bland infinitära språk eftersom det, liksom första ordens språk, medger en effektiv deduktiv apparat. Låt oss faktiskt lägga till de vanliga första ordningens axiomer och inferdsregler till det nya axiomschemat

∧Φ → φ

för alla uppräknbara uppsättningar Φ ⊆ Form1, ω) och alla φ ∈ Φ, tillsammans med den nya inferensregeln

φ 0, φ 1, …, φ n, …
n ∈ω φ n

och låt avdrag vara avräknbar längd. Att skriva ⊢ * för avdragsgillighet i denna mening, då har vi

L (ω 1, ω) - Fullständighetsteorem. För alla σ ∈ skickade1, ω), ⊨ σ ⇔ ⊢ * σ

Som en omedelbar följd drar vi slutsatsen att denna deduktionsapparat är tillräcklig för avdrag från räknbara lokaler i L (ω 1, ω). Det vill säga, med den uppenbara utvidgningen av notationen har vi, för alla räknbara uppsättningar Δ ⊆ Skickat1, ω)

(2.1) Δ ⊨ σ ⇔ Δ⊢ * σ

Denna fullständighetsteorem kan bevisas genom att modifiera det vanliga Henkin-fullständighetsbeviset för första ordens logik, eller genom att använda booleska-algebraiska metoder. Liknande argument, tillämpade på lämpliga ytterligare förstärkningar av axiomerna och reglerna för inferens, ger analoga fullständighetssatser för många andra begränsade språk.

Om bara avdrag av räknbar längd tillåts, kan ingen deduktionsapparat för L (ω 1, ω) ställas in, vilket är tillräckligt för avdrag från godtyckliga uppsättningar av lokaler, det vill säga (2.1) skulle hålla för varje uppsättning Δ ⊆ Skickat1, ω), oavsett kardinalitet. Detta följer av den enkla iakttagelsen att det finns ett första ordningsspråk L och en oräknelig uppsättning Γ av L (ω 1, ω) -sensenser så att Γ inte har någon modell men varje räknbar delmängd av Γ gör. För att se detta, låt L vara språket i aritmetik förstärkt av ω 1 nya konstant symboler { c ξ: ξ <ω 1 } och låt Γ vara uppsättningen av L (ω 1, ω) -senser {σ} ∪ { cξc η: ξ ≠ η}, där σ är L (ω 1, ω) -sensensen som kännetecknar den aritmetiska standardmodellen. Detta exempel visar också att komprimeringssatsen misslyckas för L (ω 1, ω) och så även för alla L (κ, λ) med κ ≥ ω 1.

Ett annat resultat som gäller i första ordningen men misslyckas för L (κ, ω) med κ ≥ ω 1 (och även för L (ω 1, ω 1), även om detta är svårare att bevisa) är den normala prenexformen teorem. En mening är en förkortning om alla dess kvantifierare visas framtill; vi ger ett exempel på en L (ω 1, ω) -sensens som inte motsvarar en sammansättning av prenexmeningar. Låt L vara det första ordningsspråket utan extralogiska symboler och låt σ vara L (ω 1, ω) -sensensen som kännetecknar klassen av ändliga uppsättningar. Anta att σ motsvarade en konjunktion

i ∈ I σ i

av prenex L (ω 1, ω) -senser σ i. Då är varje σ i formen

Q 1 x 1 … Q n x n φ i (x 1, …, x n),

där varje Q k är ∀ eller ∃ och φ jag är en (eventuellt infinitary) jämförd eller disjunktion av formler av formen x k = x l eller x k ≠ x l. Eftersom varje σ i är en mening, finns det bara ändligt många variabler i varje φ i, och det är lätt att se att varje φ i sedan är ekvivalent med en första ordningsformel. Följaktligen kan varje σ i anses vara en första ordnings mening. Eftersom σ antas vara ekvivalent med samband av σ jag följer att σ och uppsättningen Δ = {σ i: i ∈ Jag} har samma modeller. Men uppenbarligen har σ, och därmed också Δ, modeller av alla ändliga kardinaliteter; kompaktitetsteoremet för uppsättningar av första ordningsmeningar innebär nu att Δ, och därmed också σ, har en oändlig modell, vilket strider mot definitionen av σ.

När det gäller Löwenheim-Skolem-teoremet finner vi att den nedåtgående versionen har adekvata generaliseringar till L (ω 1, ω) (och faktiskt till alla infinitära språk). I själva verket kan man visa på ungefär samma sätt som för uppsättningar av första ordningsmeningar att om Δ ⊆ Skickat1, ω) har en oändlig modell av kardinalitet ≥ | Δ |, har den en modell av kardinalitet den större av ℵ 0, | Δ |. I synnerhet har varje L (ω 1, ω) -sensens med en oändlig modell en räknbar modell.

Å andra sidan misslyckas uppåt Löwenheim-Skolem-teoremet i sin vanliga form för alla infinitära språk. Till exempel har L (ω 1, ω) -stämningen som karakteriserar standardmodellen för aritmetik en modell av kardinalitet ℵ 0 men inga modeller av någon annan kardinalitet. Men allt går inte förlorat här, som vi kommer att se.

Vi definierar Hanf-talet h (L) för ett språk L för att vara det minsta kardinala K så att om en L- sans har en modell av kardinalitet κ, har den modeller av godtyckligt stor kardinalitet. Förekomsten av h (L) fastställs lätt. För varje L- sans σ som inte har modeller av godtyckligt stor kardinalitet låt κ (σ) vara det minsta kardinala κ så att σ inte har en modell av kardinalitet κ. Om λ är supremumet för alla κ (σ), om en mening av L har en modell av kardinalitet λ, har den modeller av godtyckligt stor kardinalitet.

Definiera kardinalerna μ (α) rekursivt med

μ (0) = 0
μ (α + 1) = 2 μ (α)
μ (λ) = α <λ μ (α), för gräns λ.

Då kan det visas det

h (L (ω 1, ω)) = μ (ω 1),

liknande resultat för andra ändliga kvantifieringsspråk. Värdena på Hanf-siffrorna för oändliga kvantifieringsspråk som L (ω 1, ω 1) är känsliga för närvaron eller på annat sätt av stora kardinaler, men måste i alla fall kraftigt överstiga värdet för L (ω 1, ω).

Ett resultat för L som generaliseras till L (ω 1, ω) men till inget annat infinitärt språk är

Craig Interpolation Teorem: Om σ, τ ∈ skickas1, ω) är sådana att ⊨ σ → τ, så finns det θ ∈ skickat1, ω) så att ⊨ σ → θ och ⊨ θ → τ, och vardera extralogisk symbol som förekommer i θ förekommer i både σ och τ.

Beviset är en ganska enkel utvidgning av första ordningen.

Slutligen nämner vi ytterligare ett resultat som generaliseras fint till L (ω 1, ω) men till inget annat infinitärt språk. Det är välkänt att, om A är någon begränsad L-struktur med endast ändligt många förhållanden, finns det en L-mening σ som kännetecknar A upp till isomorfism. För L (ω 1, ω) har vi följande generalisering känd som

Scott's isomorphism teorem. Om A är en uppräknelig L-struktur med endast uppräkneligt många förbindelser, då finns det en L (ω 1, ω) -sentence vars klass av räkningsbara modeller sammanfaller med den klass av L-strukturer isomorfa med A.

Begränsningen till räknbara strukturer är väsentlig eftersom räknbarheten i allmänhet inte kan uttryckas med en L (ω 1, ω) -sensens.

Språket L (∞, ω) kan också räknas som ett ändligt kvantifieringsspråk. Konceptet med ekvivalens mellan strukturer med avseende på detta språk är av särskild betydelse: vi kallar två (liknande) strukturer A och B (∞, ω) - ekvivalent, skriven A∞ω B, om samma meningar i L (∞, ω) fäste i både A och B. Denna relation kan först och främst kännetecknas av begreppet partiell isomorfism. En partiell isomorfism mellan A och B är en icke-befriande familj P av kartor så att:

  • För varje p ∈ P är dom (p) en underkonstruktion av A, språng (p) är en underkonstruktion av B, och p är en isomorfism för dess domän i dess område; och
  • Om p ∈ P, a ∈ A, b ∈ B, finns det r, s ∈ P båda sträcker sig p så att en ∈ dom (r), b ∈ sprang (s) ("fram och tillbaka" -egenskap).

Om en partiell isomorfism existerar mellan A och B, säger vi att A och B är delvis isomorfa och skriv Ap B. Vi har då

Karps teorem om delvis isomorfism.

För några liknande strukturer A, B, A∞ω BAp B.

Det finns också en version av Scotts isomorfisms teorem för L (∞, ω), nämligen,

(2.2) Med tanke på vilken som helst struktur A finns det en L (∞, ω) -sensens σ så att för alla strukturer B, Ap BB ⊨ σ.

Partiell isomorfism och (∞, ω) -ekvivalens är relaterade till uppfattningen om boolesk isomorfism. För att definiera detta måste vi introducera idén om en booleskt värderad modell för uppsättningsteori. Med tanke på en fullständig boolesisk algebra B erhålls universum V (B) av B-värderade uppsättningar, även känd som B-förlängning av universum V av uppsättningar, genom att först definiera, rekursivt på a,

V α (B) = {x: x är en funktion ∧ intervall (x) ⊆ B ∧ ∃ξ <α [domän (x) ⊆ V ξ (B)]}

och sedan inställning

V (B) = {x: ∃α (x ∈ V α (B))}.

Medlemmar av V (B) kallas B-värderade uppsättningar. Det är nu lätt att se att en B-värderad uppsättning exakt är en B-värderad funktion med domän en uppsättning B-värderade uppsättningar. Låt nu L vara det första ordningsspråket i setteorin och låt L (B) vara det språk som erhålls genom att lägga till L ett namn för varje element i V (B) (vi ska använda samma symbol för elementet och dess namn). Man kan nu konstruera en kartläggning [·] (B) av (meningarna i) språket L (B) till B: för varje mening σ för L (B) är elementet [σ] (B) i B " Booleska sanningsvärde”för σ i V (B). Denna kartläggning [·] (B) definieras så att den sänder alla teorierna om Zermelo-Fraenkel-setteorin till toppelementet 1 i B, det vill säga till "sanning"; följaktligen kan V (B) betraktas som en booleskt värderad modell för uppsättningsteori. I allmänhet, om [σ] (B) = 1, säger vi att σ är giltigt i V (B), och skriver V (B) ⊨ σ.

Nu har varje x ∈ V ett kanoniskt representativt x i V (B), tillfredsställande

x = y iff V (B) ⊨ x = y

x ∈ y iff V (B) ⊨ x ∈ y

Vi säger att två liknande strukturer A, B är booleska isomorfa, skrivna Ab B, om vi för V fullständig boolesisk algebra B har V (B)AB, det vill säga om det finns en boolesisk förlängning av universum av uppsättningar där de kanoniska representanterna för A och B är isomorfa med booleskt värde 1. Det kan då visas att:

(2,3) A∞ω BAb B.

Detta resultat kan stärkas genom formulering av teoretisk kategori. För detta kräver vi begreppet en (n) (elementär) topos. För att introducera detta koncept börjar vi med den familjära kategorin Uppsättning av uppsättningar och kartläggningar. Set har följande nyckelegenskaper:

  1. Det finns ett "terminal" -objekt 1 så att det för alla objekt X finns en unik karta X → 1 (för 1 kan vi ta alla en-elementuppsättningar, i synnerhet {0}).
  2. Alla par av objekt X, Y har en kartesisk produkt X × Y.
  3. för alla par av objekt kan man bilda det "exponentiella" objektet Y X för alla kartor från X → Y.
  4. Det finns ett "sanningsvärde" -objekt Ω så att för varje objekt X finns en naturlig korrespondens mellan underobjekt (underuppsättningar) av X och kartor X → Ω. (För Ω kan vi ta uppsättningen 2 = {0,1}; kartor X → Ω är då karakteristiska funktioner på X.)

Alla fyra av dessa villkor kan formuleras på kategoriteoretiskt språk - en kategori som uppfyller dem kallas en topos. Kategorin Set är en topos; så även är (i) kategorin Set (B) av Boolean-värderade uppsättningar och mappningar i någon boolesk förlängnings V (B) av universum av uppsättningar; (ii) kategorin skivor av uppsättningar i ett topologiskt utrymme; (iii) kategorin för alla diagram över kartor över uppsättningar

X 0 → X 1 → X 2 → …

Objekten i var och en av dessa kategorier kan betraktas som uppsättningar som varierar på något sätt: i fall (i) över en boolesk algebra; i fall (ii) över ett topologiskt utrymme; i fall (iii) över (diskret) tid. En topos kan då tänkas som ett universum av "variabla" uppsättningar. Den välkända kategorin Set är det speciella begränsande fallet för en topos där objektens "variation" har reducerats till noll.

Precis som i uppsättningsteorin kan "logiska operatörer" definieras på sanningsvärdesobjektet i alla topos. Dessa är kartor ¬: Ω → Ω; ∧, ∨, ⇒: Ω × Ω → Ω motsvarande de logiska operationerna för negation, konjunktion, disjunction och implikation. Med dessa operationer blir a en Heyting-algebra och därmed i allmänhet förkroppsligar lagarna inte av klassisk utan intutionistisk logik. På det sättet "internaliseras" den intuitionistiska logiken i en topos: intuitionistisk logik är variabeluppsättningens logik. (Naturligtvis är klassisk logik internaliserad i vissa toposer, till exempel Set och Set (B) för alla kompletta booleska algebra B.)

Alla topos kan tänkas som möjligt "diskursuniversum" där matematiska påståenden kan tolkas och matematiska konstruktioner kan utföras. Matematiska påståenden görs tolkbara i en topos E genom uttryck inom E: s interna språk - en typteoretisk version av det vanliga språket i setteorin. På ett sätt som är analogt med Booleskt värderat giltighet kan man införa en lämplig uppfattning av giltighet i E av en mening σ i dess interna språk. Återigen skriver vi E ⊨ σ för “σ är giltigt i E”.

En topos E sägs vara full om, för någon uppsättning I, I-fald copower [3]I 1 av dess terminalobjekt finns i E. ∐ I 1 kan betraktas som den kanoniska representanten i E i uppsättningen Jag; därför skriver vi det helt enkelt som jag. (I V (B) sammanfaller detta med I såsom tidigare definierats.) Alla ovan nämnda toposer är fulla.

Låt nu E vara en fullständig topos. Om A = (A, R, …) är en struktur, skriv A för (A, R, …). Två strukturer A och B sägs vara topos isomorf, skriven At B, om vi för vissa topos E definierade över kategorin set har E ⊨ A ≅ B. Med andra ord är två strukturer topos isomorfa om deras kanoniska representanter är isomorfa på det inre språket för vissa topos. Det kan då visas det

(2,4) A∞ω BAt B.

Följaktligen (∞, ω) -ekvivalens kan betraktas som isomorfism i det extremt allmänna sammanhanget för universum av "variabla" uppsättningar. I detta avseende (∞, ω) är ekvivalens en "invariant" uppfattning om isomorfism.

3. Egenskaperna för kompaktitet

Som vi har sett misslyckas kompaktheten i dess vanliga form för alla infinitära språk. Ändå är det av ett visst intresse att avgöra om infinitära språk uppfyller någon lämpligt modifierad version av teoremet. Detta så kallade kompakthetsproblem visar sig ha en naturlig koppling till rent setteoretiska frågor som involverar”stora” kardinalnummer.

Vi konstruerar följande definition. Låt κ vara en oändlig kardinal. Ett språk L sägs vara κ-kompakt (resp. Svagt κ-kompakt) om närhelst a är en uppsättning av L- sanser (resp. En uppsättning av L- sanser av kardinalitet ≤ κ) och varje delmängd av Δ av kardinalitet < κ har en modell, så gör Δ. Lägg märke till att den vanliga kompakthetsteoremet för L exakt är påståendet att L är ω-kompakt. Ett skäl till enligt betydelse för egenskapen κ-kompakthet är följande. Ring L κ- komplett (resp. Svagt κ- komplett) om det finns ett deduktivt system P för L med avdrag för längd <κ så att, om Δ är en P- konsistent [4] uppsättning av L- lutningar (resp. Så att | Δ | ≤ κ), sedan Δ har en modell. Observera att en sådan P kommer att vara tillräcklig för avdrag från godtyckliga uppsättningar av lokaler (av kardinalitet ≤ κ) i den mening som avses i §2. Det är lätt att se att om L är K-komplett eller svagt K-komplett, så är L K-kompakt eller svagt K-kompakt. Således, om vi kan visa att ett givet språk inte är (svagt) k-kompakt, kan det inte finnas något deduktivt system för det med avdrag för längd <κ som är tillräckligt för avdrag från godtyckliga uppsättningar av lokaler (av kardinalitet ≤ κ).

Det visar sig faktiskt att de flesta språk L (κ, λ) misslyckas med att vara till och med svagt κ-kompakta, och för de som är det måste κ vara en mycket stor kardinal. Vi kommer att behöva några definitioner.

En oändlig kardinal K sägs vara svagt otillgänglig om

(a) λ <κ → λ + <κ, (där λ + betecknar kardinalens efterföljare för λ), och

(b) | I | <κ och λ i <κ (för alla i ∈ I) ⇒ ∑ i ∈ I λ i <κ.

Om dessutom

(c) λ <κ ⇒ 2 λ <κ,

då sägs κ vara (starkt) otillgänglig. Eftersom ℵ 0 är otillgänglig är det normal praxis att begränsa uppmärksamhet till de otillgängliga, eller svagt otillgängliga, kardinaler som överstiger ℵ 0. Följaktligen kommer otillgängliga eller svagt otillgängliga kardinaler alltid att anses vara oräkneliga. Det är uppenbart att sådana kardinaler - om de finns - måste vara extremt stora; och faktiskt innebär att Gödel-ofullständighetsteoremet inte kan bevisas förekomsten av till och med svagt otillgängliga kardinaler med de vanliga axiomerna i setteorin.

Låt oss kalla en kardinal κ-kompakt (resp. Svagt kompakt) om språket L (κ, κ) är κ-kompakt (resp. Svagt κ-kompakt). Sedan har vi följande resultat:

(3.1) ℵ 0 är kompakt. Detta är naturligtvis bara ett kortfattat sätt att uttrycka kompakthetsteorem för första ordningens språk.

(3.2) κ är svagt kompakt ⇒ L (κ, ω) är svagt κ-kompakt ⇒ κ är svagt otillgänglig. Följaktligen är det konsekvent (med de vanliga axiomerna i uppsättningsteorin) att anta att inget språk L (κ, ω) med κ ≥ ω 1 är svagt k-kompakt, eller, fortiori, svagt k-komplett.

(3.3) Anta att κ är otillgänglig. Då är κ svagt kompakt ⇔ L (κ, ω) är svagt κ-kompakt. Dessutom är κ också svagt kompakt ⇒ det finns en uppsättning κ otillgängliga före κ. Således är en svagt kompakt otillgänglig kardinal mycket stor; i synnerhet inte kan vara den första, andra, …, n th … otillgängliga.

(3.4) κ är kompakt ⇒ κ är otillgänglig. (Men med resultatet omedelbart ovan misslyckas konversationen.)

Låt Constr stå för Gödels axiom av konstruerbarhet; minns att Constr överensstämmer med vanliga axiomer i setteorin.

(3.5) Om Constr håller, finns det inga kompakta kardinaler.

(3.6) Anta Constr och låt κ vara otillgängliga. Då är κ svagt kompakt ⇔ L (ω 1, ω) är svagt κ-kompakt för alla L.

(3.7) Om Constr håller, finns det inga kardinaler κ för vilka L (ω 1, ω) är kompakt. Följaktligen överensstämmer det med de vanliga axiomerna i uppsättningsteorin att anta att det inte finns några kardinala K så att alla språk L (ω 1, ω) är K-kompletta. Detta resultat ska kontrasteras med det faktum att alla första ordningens språk är ω-kompletta.

Importen av dessa resultat är att kompakthetstormen misslyckas mycket dåligt för de flesta språk L (κ, λ) med κ ≥ ω 1.

Här finns några historiska anmärkningar. På 1930-talet undersökte matematiker olika versioner av det så kallade måttproblemet för uppsättningar, ett problem som uppstod i samband med teorin om Lebesgue-mått på kontinuummet. I synnerhet formulerades följande mycket enkla begrepp om åtgärd. Om X är en uppsättning, är ett (räknat additivt tvåvärderat icke-trivialt) mått på X en karta μ på effektuppsättningen P X till uppsättningen {0, 1} som uppfyller:

(a) μ (X) = 1, (b) μ ({x}) = μ (∅) = 0 för alla x ∈ X, och

(c) om A är någon räknbar familj med ömsesidigt osammanhängande undergrupper av X, då μ (∪ A) = ∑ {μ (Y): Y ∈ A }.

Det är uppenbart att huruvida en given uppsättning stöder en sådan åtgärd endast beror på dess kardinalitet, så det är naturligt att definiera en kardinal K för att vara mätbar om alla uppsättningar av kardinalitet κ stöder ett mått av denna typ. Man förstod snabbt att en mätbar kardinal måste vara otillgänglig, men falskheten i det konverserade fastställdes inte förrän på 1960-talet då Tarski visade att mätbara kardinaler är svagt kompakta och hans student Hanf visade att den första, andra osv. Otillgängliga är inte svagt kompakt (jfr (3.3)). Även om slutsatsen att mätbara kardinaler måste vara monströst stort nu nu bevisas utan omväg genom svag kompakthet och infinitära språk, kvarstår faktum att dessa idéer användes för att fastställa resultatet i första hand.

4. Ofullständighet i oändliga kvantifieringsspråk

Förmodligen det viktigaste resultatet om första ordningsspråk är Gödel fullständighetsteorem som naturligtvis säger att uppsättningen av alla giltiga formler för alla första ordningsspråk L kan genereras från en enkel uppsättning axiomer med hjälp av några enkla regler för slutledning. En viktig konsekvens av detta teorem är att om formlerna för L kodas som naturliga siffror på något konstruktivt sätt, så är uppsättningen (koder med) giltiga meningar rekursivt otaliga. Således innebär fullständigheten av ett första ordningsspråk att uppsättningen av dess giltiga meningar är definierbar på ett särskilt enkelt sätt. Det skulle således vara rimligt, med tanke på ett godtyckligt språk L, för att vända denna förstått runt och föreslå att om uppsättningen av giltiga L-Sensenser kan inte definieras på något enkelt sätt, då kan inget meningsfullt fullständighetsresultat fastställas för L, eller, som vi säger, att L är ofullständigt. I det här avsnittet kommer vi att använda detta förslag när vi skissar ett bevis på att "de flesta" oändliga kvantifieringsspråk är ofullständiga i den meningen.

Låt oss först införa det formella begreppet definierbarhet enligt följande. Om L är ett språk, A en L- struktur och X en delmängd av domänen A för A, säger vi att X kan definieras i A med en formel φ (x, y 1, …, y n) av L om där är en sekvens en 1, …, en n av element i A så att X är den undergrupp av alla element x ∈ A för vilka φ (x, a 1, …, en n) innehar i A.

Skriv nu Val (L) för uppsättningen av alla giltiga L- sanser, dvs de som finns i varje L- struktur. För att tilldela en betydelse till uttalandet "Val (L) är definierbart", måste vi ange

  1. en struktur C (L) - den kodande strukturen för L;
  2. en speciell en-en-karta-kodningskartan - av uppsättningen av formler för L till domänen till C (L).

Om vi sedan identifierar Val (L) med dess bild i C (L) under kodningskartan, ska vi tolka uttalandet "Val (L) är definierbart" som uttalandet "Val (L), betraktat som en delmängd av domän för C (L), kan definieras i C (L) med en formel av L.”

Till exempel, när L är det första ordningsspråket L för aritmetik, användes Gödel ursprungligen som kodningsstruktur standardmodellen för aritmetik ℕ och som kodningskarta den välkända funktionen som erhållits från primära faktoriseringsteoremet för naturliga nummer. Den rekursiva mängden Val (L) betyder då helt enkelt att uppsättningen koder (“Gödel-nummer”) för medlemmar av Val (L) kan definieras i ℕ med en L-formel med formen ∃ y φ (x, y), där φ (x, y) är en rekursiv formel.

En annan, ekvivalent, kodande struktur för det första ordningsspråket för aritmetik är strukturen [5] ⟨H (ω), ∈ ⨡ H (ω)⟩ för ärftliga finituppsättningar, där en uppsättning x är ärftligt finit om x, dess medlemmar, dess medlemmar av medlemmar, etc., är alla begränsade. Denna kodningsstruktur tar hänsyn till det faktum att första ordningens formler naturligtvis betraktas som ändliga uppsättningar.

Med tanke på fallet där L är ett infinitärt språk L (κ, λ), vad skulle vara en lämplig kodningsstruktur i detta fall? Vi påpekade i början att infinitära språk föreslogs av möjligheten att tänka på formler som setteoretiska objekt, så låt oss försöka få vår kodningsstruktur genom att tänka på vilken typ av setteoretiska objekt vi borde ta infinitära formler för att vara. Med tanke på det faktum att för varje φ∈- form (κ, λ), φ och dess subformler, sub-formler etc., är alla av längden <κ, [6]ett ögonblicks reflektion avslöjar att formler av L (κ, λ) “motsvarar” uppsättningar x som är herligt kardinalitet <κ i den meningen att x, dess medlemmar, dess medlemmars medlemmar, etc., alla är kardinalitet <κ. Samlingen av alla sådana uppsättningar är skrivna H (κ). H (ω) är samlingen av ärftliga ändliga uppsättningar som introducerats ovan, och H (ω 1) den för alla ärftligt räknbara uppsättningar.

För enkelhets skull låt oss anta att den enda extralogiska symbolen för basspråket L är den binära predikatsymbolen ∈ (diskussionen utvidgas lätt till det fall där L innehåller ytterligare extralogiska symboler). Med hjälp av kommentarerna ovan tar vi strukturen för L (κ, λ),

H (κ) = df ⟨H (κ), ∈ ⨡ H (κ)⟩.

Nu kan vi definiera kodningskartan för Form (κ, λ) till H (κ). Först tilldelar vi varje bassymbol för L (κ, λ) ett kodobjekt ⌈ s ∈ H (κ) enligt följande. Låt {v ξ: ξ <κ} vara en uppräkning av de individuella variablerna för L (κ, λ).

Symbol Kodobjekt Notation
¬ 1 ¬
2
3
4
5
= 6 =
v ξ ⟨0, ξ⟩ v ξ

Sedan tilldelar vi varje φ ∈- formulär (κ, λ) kodobjektet ⌈ φ rekursivt enligt följande:

v ξ = v r | = df v ξ , = , v r | ⟩, v £, ∈ v r | = df v £, , , v r | ⟩;

för φ, ψ ∈ Form (κ, λ),

cp ∧ v | = df cp , , v |

¬φ = df ¬ , cp

∃ X cp = df, { x : x ∈ X}, cp ⟩;

och slutligen om Φ ⊆ Form (κ, λ) med | Φ | <κ,

∧Φ = df, { cp : φ ∈ Φ}⟩.

Kartan φ ↦ φ från form (κ, λ) till H (κ) kan lätt ses som en och är den nödvändiga kodningskartan. Följaktligen är vi överens om att identifiera Val (L (κ, λ)) med dess bild i H (κ) under denna kodningskarta.

När är Val (L (κ, λ)) en definierbar delmängd av H (κ)? För att besvara denna fråga kräver vi följande definitioner.

En L-formel kallas en Δ 0 - formel om den är ekvivalent med en formel där alla kvantifierare har formen ∀ x ∈ y eller ∃ x ∈ y (dvs. ∀ x (x ∈ y → …) eller ∃ x (x ∈ y ∧ …)). En L-formel är en Σ 1 - formel om den är ekvivalent med en som kan byggas upp från atomformler och deras negationer med bara de logiska operatörerna ∧, ∨, ∀ x ∈ y, ∃ x. En delmängd X i en uppsättning A sägs vara Δ 0 (resp. Σ 1) på A om den är definierbar i strukturen ⟨A, ∈ ⨡ A⟩ med en Δ 0 - (resp. Σ 1 -) formel av L.

Om vi till exempel identifierar uppsättningen med naturliga siffror med uppsättningen H (ω) för ärftliga ändliga uppsättningar på vanligt sätt, har vi för varje X ⊆ H (ω):

X är Δ 0 på H (ω) ⇔ X är rekursivt

X är Σ 1 på H (ω) ⇔ X är rekursivt uppräknbart.

Således kan föreställningarna om Δ 0 - och- 1- set betraktas som generaliseringar av begreppen rekursiv respektive rekursivt antal.

Fullständighetsteoremet för L antyder att Val (L) - betraktas som en delmängd av H (ω) - är rekursivt talrik, och därmed Σ 1 på H (ω). På motsvarande sätt innebär fullständighetsteoremet för L (ω 1, ω) (se §2) att Val (L (ω 1, ω)) - betraktas som en delmängd av H (ω 1) - är on 1 på H (ω 1). Emellertid kollapsar detta trevliga tillstånd helt så snart L (ω 1, is 1) har nåtts. För man kan bevisa

Scotts undefinerbarhetsteorem för L (ω 1, ω 1). Val (L (ω 1, ω 1)) kan inte definieras i H (ω 1) ens med en L (ω 1, ω 1) - formel; följaktligen är en fortiori Val (L (ω 1, ω 1)) inte Σ 1 på H (ω 1).

Denna sats bevisas på ungefär samma sätt som det välkända resultatet att uppsättningen (koder med) giltiga meningar för det andra ordningsspråket i aritematiska L 2 inte är andra ordningsdefinierbart i dess kodningsstruktur. För att få detta senare resultat, en första påpekat att ℕ kännetecknas av en enda L 2 -sentence, och sedan visar att, om resultatet var falska, sedan”sanning i ℕ” för L 2 -sentences skulle vara definierbart genom en L 2 -formulär, och därigenom kränker Tarskis teorem om sannings odefinierbarhet.

För att bevisa Scotts odefinieringssats enligt ovanstående linjer måste man fastställa:

(4.1) Karaktäriserbarhet för kodningsstrukturen H (ω 1) i L (ω 1, ω 1): det finns en L (ω 1, ω 1) -sensens τ 0 så att för alla L-strukturer A, A ⊨ τ 0A ≅ H (ω 1).

(4.2) Sannolikhet för L (ω 1, ω 1) - meningar i kodningsstrukturen: det finns ingen L (ω 1, ω 1) -formel φ (v 0) så att för alla L (ω 1, ω 1) -tenser σ, H (ω 1) ⊨ σ↔φ ( σ ).

(4.3) Det finns en term t (v 0, v 1) av L (ω 1, ω 1) så att för varje meningspar σ, τ av L (ω 1, ω 1), H (ω 1) ⊨ [t ( σ , τ ) = σ → τ ].

(4.1) bevisas genom att analysera den setteoretiska definitionen av H (ω 1) och visa att den kan "internt" formuleras i L (ω 1, ω 1). (4.2) är etablerat på ungefär samma sätt som Tarskis teorem om sannolikhetens odefinierbarhet för första- eller andra ordningens språk. (4.3) erhålls genom att formalisera definitionen av kodningskartan σ ↦ σ i L (ω 1, ω 1).

Beväpnad med dessa fakta kan vi få Scotts odefinieringssats på följande sätt. Anta att det var falskt; då skulle det finnas en L (ω 1, ω 1) -formel θ (v 0) så att, för alla L (ω 1, ω 1) -tenser σ,

(4.4) H (ω 1) ⊨ θ ( σ ) iff σ ∈ Val (L (ω 1, ω 1)).

Låt τ 0 vara meningen som ges i (4.1). Då har vi, för alla L (ω 1, ω 1) -tenser σ,

H (ω 1) ⊨ σ iff (τ 0 → σ) ∈ Val (L (ω 1, ω 1)),

så att med (4.4),

H (ω 1) ⊨ σ iff H (ω 1) ⊨ θ ( τ 0 → σ ).

Om t är termen som anges i (4.3), skulle det följa det

H (ω 1) ⊨ σ↔θ (t ( τ 0 , σ )).

Skriv nu φ (v 0) för L (ω 1, ω 1) -formeln θ (t ( τ 0 , σ )). Sedan

H (ω 1) ⊨ σ↔φ ( σ ),

motsägelse (4.2) och slutföra beviset.

Således är Val (L (ω 1, ω 1)) inte definierbar ens med en L (ω 1, ω 1) - formel, så en fortiori L (ω 1, ω 1) är ofullständig. Liknande argument visar att Scotts odefinieringssats fortsätter att hålla när ω 1 ersätts av någon efterföljande kardinal κ +; följaktligen är språken L (κ +, κ +) alla ofullständiga. [7]

5. Underspråk för L (ω 1, ω) och Barwise Compactness Theorem

Med tanke på vad vi nu vet om infinitära språk verkar det som att L (ω 1, ω) är den enda som är rimligt väl uppförd. Å andra sidan är bristen på kompaktitetsteoremet att generalisera till L (ω 1, ω) på något användbart sätt en allvarlig nackdel när det gäller tillämpningar. Låt oss försöka analysera detta fel mer detaljerat.

Kom ihåg från §4 att vi kan koda formlerna för ett första ordningsspråk L som ärftligt definierade uppsättningar, dvs som medlemmar av H (ω). I så fall är varje begränsad uppsättning (koder för) L-meningar också en medlem av H (ω), och det följer att kompaktitetsteoremet för L kan anges i formen:

(5.1) Om Δ ⊆ Skickat (L) är sådan att varje delmängd Δ 0 ⊆ Δ, Δ 0 ∈ H (ω) har en modell, så gör Δ också.

Nu är det välkänt att (5.1) är en omedelbar följd av den allmänna fullständighetsteoremet för L, som, anges i en form som liknar den i (5.1), blir påståendet:

(5.2) Om Δ ⊆ Skickat (L) och σ ∈ Skickat (L) uppfyller Δ ⊨ σ, finns det ett avdrag D för σ från Δ så att D ∈ H (ω). [8]

I §2 påpekade vi att kompaktheten för L (ω 1, ω) misslyckas mycket starkt; i själva verket konstruerade vi en uppsättning Γ ⊆ Skickad1, ω) så att

(5.3) Varje räknelig delmängd av Γ har en modell men Γ inte.

Minns också att vi introducerade begreppet avdrag i L (ω 1, ω); eftersom sådana avdrag är av räknbar längd följer det snabbt från (5.3) att

(5.4) Det finns en mening [9] σ ∈ Skickat1, ω) så att Γ ⊨ σ, men det finns inget avdrag för σ i L (ω 1, ω) från Γ.

Nu kan formlerna för L (ω 1, ω) kodas som medlemmar av H (ω 1), och det är uppenbart att H (ω 1) är stängd under bildningen av räknbara undergrupper och sekvenser. Följaktligen kan (5.3) och (5.4) skrivas:

(5.3 bis) Varje Γ 0 ⊆ Γ så att Γ 0 ∈ H (ω 1) har en modell, men Γ inte;

(5.4 bis) Det finns en mening σ ∈ Skickat1, ω) så att Γ ⊨ σ, men det finns inget avdrag D ∈ H (ω 1) för σ från Γ.

Av detta följer att (5.1) och (5.2) misslyckas när”L” ersätts av”L (ω 1, ω)” och”H (ω)” med”H (ω 1)”. Dessutom kan det visas att uppsättningen Γ ⊆ Skickat1, ω) i (5.3 bis) och (5.4 bis) kan anses vara Σ 1 på H (ω 1). Således misslyckas kompaktheten och generaliserade fullständighetsteorema även för Σ 1- uppsättningar av L (ω 1, ω) -senser.

Vi ser från (5.4 bis) att orsaken till att den allmänna fullständighetsstelsen misslyckas för Σ 1- uppsättningar i L (ω 1, ω) är att grovt sett H (ω 1) inte "stängs" under bildandet av avdrag från Σ 1- setningar av meningar i H (ω 1). Så för att avhjälpa detta verkar det vara naturligt att ersätta H (ω 1) med uppsättningar A som på något sätt är stängda under bildandet av sådana avdrag och sedan överväga bara de formler vars koder finns i A.

Vi ger nu en skiss över hur detta kan göras.

Först identifierar vi symbolerna och formlerna för L (ω 1, ω) med deras koder i H (ω 1), som i §4. För varje räknbar transitiv [10] uppsättning A, låt

L A = Form (L (ω 1, ω)) ∩ A.

Vi säger att L A är ett språk i L (ω 1, ω) om följande villkor är uppfyllda:

  1. L ⊆ L A
  2. om φ, ψ ∈ L A, då φ ∧ ψ ∈ L A och ¬φ ∈ L A
  3. om φ ∈ L A och x ∈ A, då ∃ x φ ∈ L A
  4. om φ (x) ∈ L A och y ∈ A, då φ (y) ∈ L A
  5. om φ ∈ L A, är varje underformel i in i L A
  6. om Φ ⊆ L A och Φ ∈ A, sedan ∧Φ ∈ L A.

Begreppet avdrag i L A definieras på sedvanligt sätt; om Δ är en uppsättning av meningarna i L A och cp ∈ L A, därefter ett avdrag av φ från Δ i L A är ett avdrag på φ från Δ i L (ω 1, ω) varje formel av vilket är i L A. Vi säger att φ kan dras från Δ i L A om det finns ett avdrag D för φ från Δ i L A; under dessa förhållanden skriver vi Δ ⊢ A φ. Generellt sett kommer D inte att vara medlem i A; för att säkerställa att ett sådant avdrag kan hittas i A kommer det att vara nödvändigt att införa ytterligare villkor för A.

Låt A vara en uppräknelig transitiv uppsättning så att L A är en underspråk av L (ω 1, ω) och låt Δ vara en uppsättning meningar av L A. Vi säger att A (eller genom missbruk av terminologi, L A) är closed- stängd om för någon formel φ av L A så att Δ ⊢ A φ finns ett avdrag D för φ från Δ så att D ∈ A. Det kan visas att det enda räknbara språket som är closed-stängt för godtyckligt Δ är första ordningsspråket L, dvs. när A = H (ω). Men J. Barwise upptäckte att det finns räknbara uppsättningar A ⊆ H (ω 1) vars motsvarande språk L A skiljer sig från L och ändå är Δ-stängda för alla Σ 1- uppsättningar av meningar Δ. Sådana uppsättningar A kallas tillåtna uppsättningar; grovt sett är de förlängningar av de ärftliga ändliga uppsättningarna där rekursionsteori - och därmed bevisteori - fortfarande är möjliga (för full definition, se avsnitt 5.1 nedan).

Från Barwises resultat erhåller man omedelbart

Barwise Compactness Theorem. Låt A vara en räknbar tillåtbar uppsättning och låt Δ vara en uppsättning meningar av L A som är Σ 1 på A. Om varje Δ '⊆ Δ så att Δ' ∈ A har en modell, så gör det också Δ.

Närvaron av”Σ 1” här indikerar att detta ställe är en generalisering av kompaktheten för rekursivt många uppsättningar av meningar.

En annan version av Barwise kompaktitetsteorem, användbart för att konstruera modeller av setteori, är följande. Låt ZFC vara den vanliga axiomuppsättningen för Zermelo-Fraenkel-setteorin, inklusive valet axiom. Då har vi:

5.5 Sats. Låt A vara en räknbar transitiv uppsättning så att A = ⟨A, ∈ ⨡ A⟩ är en modell av ZFC. Om Δ är en uppsättning meningar av L A som kan definieras i A med en formel för språket i uppsättningsteorin och om varje Δ '⊆ Δ så att Δ' ∈ A har en modell, så gör Δ.

Avslutningsvis ger vi en enkel tillämpning av detta teorem. Låt A = ⟨A, ∈ ⨡ A⟩ vara en modell av ZFC. En modell B = ⟨B, E⟩ av ZFC sägs vara en korrekt slutförlängning av A om (i) AB, (ii) AB, (iii) a ∈ A, b ∈ B, bEa ⇒ b ∈ A. En korrekt slutförlängning av en modell av ZFC är alltså en korrekt förlängning där inget "nytt" element kommer "före" något "gammalt" element. Som vår tillämpning av 5.5 bevisar vi

5.6 Sats. Varje kvantifierbart transitiv modell av ZFC har en riktig slut förlängning.

Bevis. Låt A = ⟨A, ∈ ⨡ A⟩ vara en transitiv modell av ZFC och låt L vara det första ordningsspråket i setteorin, förstärkt med ett namn a för varje a ∈ A, och en ytterligare konstant c. Låt Δ vara uppsättningen av L A- sanser innefattande:

  • alla axiomer av ZFC;
  • ca, för varje a ∈ A;
  • ∀ x (x ∈ a → ∨ b ∈ a x = b), för varje a ∈ A;
  • ab, för varje a ∈ b ∈ A.

Det visas lätt att Δ är en delmängd av A som kan definieras i A med en formel för språket i setteorin. Dessutom har varje delmängd Δ '⊆ Δ så att Δ' ∈ A har en modell. För uppsättningen C för alla a ∈ A för vilken a förekommer i Δ 'tillhör A - eftersom Δ' gör det - och så, om vi tolkar c som någon medlem av den (nödvändigtvis undantag) uppsättningen A - C, så är A en modell av Δ '. Följaktligen antyder (5.5) att Δ har en modell ⟨B, E⟩. Om vi tolkar varje konstant en som elementet a ∈ A, så är ⟨B, E⟩ en ordentlig ände-förlängning av A. Beviset är komplett.

Läsaren kommer snabbt att se att första ordningens kompaktitetsteorem inte ger detta resultat.

5.1 Definition av begreppet tillåtet set

En nonempty transitiv uppsättning A sägs vara tillåten när följande villkor är uppfyllda:

  1. om a, b ∈ A, då {a, b} ∈ A och ∪ A ∈ A;
  2. om a ∈ A och X ⊆ A är Δ 0 på A, då X ∩ a ∈ A;
  3. om a ∈ A, X ⊆ A är Δ 0 på A och ∀ x ∈ a ∃ y (<x, y> ∈ X), då för vissa b ∈ A, ∀ x ∈ a ∃ y ∈ b (<x, y> ∈ X).

Skick (ii) - Δ 0 - separationsschema - är en begränsad version av Zermelos separationsaxiom. Skick (iii) - en liknande försvagad version av ersättningsaxiom - kan kallas Δ 0 - ersättningsschema.

Det är ganska lätt att se att om A är en transitiv uppsättning så att <A, ∈ | A> är en modell av ZFC, då är A tillåtet. Mer generellt fortsätter resultatet att hålla när kraftinställningsaxiom utelämnas från ZFC, så att både H (ω) och H (ω 1) är tillåtna. Eftersom det sistnämnda är oöverskådligt, misslyckas Barwise-kompaktstormen emellertid inte på den.

6. Historiska och bibliografiska anmärkningar

§§ 1 och 2. Infinitära propositionerspråk och predikatspråk verkar ha gjort sitt första uttryckliga utseende med tryck från Scott och Tarski [1958] och Tarski [1958]. Fullständighetsteoremet för L (ω 1, ω) såväl som för andra infinitära språk bevisades av Karp [1964]. Hanf-talberäkningarna för L (ω 1, ω) utfördes först av Morley [1965]. Karp [1965] och Lopez-Escobar [1966] bevisades obestämbarheten för välbeställningar i finit-kvantifieringsspråk. Interpolationsteoremet för L (ω 1, ω) bevisades av Lopez-Escobar [1965] och Scott's isomorphism teorem för L (ω 1, ω) av Scott [1965].

Karps partiella isomorfisms teorem bevisades först i Karp [1965]; se även Barwise [1973]. Resultat (2.2) visas i Chang [1968], resultat (2.3) i Ellentuck [1976] och resultat (2.4) i Bell [1981].

§ 3. Resultaten (3.2) och (3.3) beror på Hanf [1964], med några förbättringar av Lopez-Escobar [1966] och Dickmann [1975], medan (3.4) bevisades av Tarski. Resultat (3.5) beror på Scott [1961], (3.6) till Bell [1970] och [1972]; och (3.7) till Bell [1974]. Mätbara kardinaler övervägs först av Ulam [1930] och Tarski [1939]. Det faktum att mätbara kardinaler är svagt kompakta noterades i Tarski [1962].

§ 4. Beträffande odefinieringssatsen för L (ω 1, ω 1). Carol Karp kommenterar (1964, 166),”Vid den internationella kongressen för logik, metodik och vetenskapsfilosofi vid Stanford University 1960, cirkulerade Dana Scott en översikt av ett bevis på omöjligheten av ett komplett definierbart formellt system för (γ +, γ +) språk med en enda två-plats predikatsymbol utöver jämställdhetssymbolen.” Scott publicerade aldrig sitt resultat, och ett fullständigt detaljerat bevis dök först upp i Karp [1964]. Den strategi som man använde här bygger på berättelsen i Dickmann [1975].

§ 5. Den ursprungliga motivationen för resultaten som presenterades i detta avsnitt kom från Kreisel; i hans [1965] påpekade han att det inte fanns några tvingande skäl för att välja infinitära formler endast på grund av”längd”, och föreslog istället att kriterier för definibilitet eller”stängning” skulle användas. Kreisels förslag togs upp med stor framgång av Barwise [1967], där hans kompakthetsteorem bevisades. Uppfattningen om tillåtna uppsättningar beror på Platek [1966]. Sats (5.6) är hämtat från Keisler [1974].

För ytterligare läsning om ämnet infinitära språk, se Aczel [1973], Dickmann [1975], Karp [1964], Keisler [1974] och Makkai [1977]. En användbar redogörelse för kopplingen mellan infinitära språk och stora kardinaler finns i kapitel 10 i Drake [1974].

Bibliografi

  • Aczel, P., 1973, "Infinitary Logic and the Barwise Compactness Theorem", Proceedings of the Bertrand Russell Memorial Logic Conference (Uldum, Denmark), J. Bell, J. Cole, G. Priest och A. Slomson (eds).), Leeds: Bertrand Russell Memorial Logic Conference, 234–277.
  • Barwise, J., 1967, Infinitary Logic and Admissible Sets. Ph. D. Examensarbete, Stanford University.
  • –––, 1973,”Tillbaka och framåt genom infinitärlogik. Studies in Model Theory”, i Studies in Mathematics (Volym 8), Buffalo: Mathematical Association of American, s. 5–34.
  • ––– 1975, Tillåtna uppsättningar och strukturer, Berlin: Springer-Verlag.
  • Barwise, J. och S. Feferman (red.), 1985, Handbook of Model-Theoretic Logics, New York: Springer-Verlag.
  • Baumgartner, J., 1974,”Hanf-numret för kompletta L ω 1, ω- meningar (utan GCH)”, Journal of Symbolic Logic, 39: 575–578.
  • Bell, JL, 1970, "Svag kompaktitet i begränsade andra ordens språk", Bulletin of the Polish Academy of Sciences, 18: 111–114.
  • ––– 1972,”Om förhållandet mellan svag kompaktitet i L ω 1, ω, L ω 1, ω 1 och begränsade andra ordens språk”, Arkiv för matematisk logik, 15: 74–78.
  • –––, 1974, “On Compact Cardinals”, Zeitschrift für Mathematical Logik und Grundlagen der Mathematik, 20: 389–393.
  • ––– 1981, “Isomorphism of Structures in S-toposes”, Journal of Symbolic Logic, 43 (3): 449–459.
  • Chang, CC, 1968, "Några kommentarer om modellteorin för infinitära språk". i Syntax and Semantics of Infinitary Language (Lecture Notes in Mathematics: Volume 72), J. Barwise (red.), Springer-Verlag, Berlin, 36-63.
  • Dickmann, MA, 1975, Stora infinitära språk, Amsterdam: Nord-Holland.
  • Drake, FR, 1974, Set Theory: An Introduction to Large Cardinals, Amsterdam: North-Holland Publishing Company.
  • Ellentuck, E., 1976, "Categoricity Regained", Journal of Symbolic Logic, 41 (3): 639–643.
  • Hanf, WP, 1964, Inkompaktitet i språk med oändligt långa uttryck, Amsterdam: Nord-Holland.
  • Karp, C., 1964, Språk med uttryck för oändlig längd, Amsterdam: Nord-Holland.
  • –––, 1965,”Finite-Quantifier Equivalence” i Theory of Models, J. Addison, L. Henkin och A. Tarski (red.), Amsterdam: Nord-Holland, 407–412.
  • Keisler, HJ, 1974, Model Theory for Infinitary Logic, Amsterdam: North-Holland.
  • Keisler, HJ och Julia F. Knight, 2004, "Barwise: Infinitary Logic And Admissible Sets", Journal of Symbolic Logic, 10 (1): 4–36
  • Kolaitis, P. och M. Vardi, 1992, "Fixpoint Logic vs. Infinitary Logic in Finite-Model Theory," Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS '92), IEEE, s. 46-57; tillgängligt online, doi: 10.1109 / LICS.1992.185518
  • Kreisel, G., 1965, "Model-Theoretic Invariants, Applications to Recursive and Hyperarithmetic Operations", i The Theory of Models, J. Addison, L. Henkin, och A. Tarski (red.), Amsterdam: North-Holland, 190-205.
  • Kueker, D., 1975, "Fram och tillbaka argument på infinitära språk", i Infinitär logik: I Memoriam Carol Karp (Föreläsningsanteckningar i matematik: volym 492), D. Kueker (red.), Berlin: Springer-Verlag.
  • Lopez-Escobar, EGK, 1965,”En interpolationsteorem för oändligt långa meningar”, Fundamenta Mathematicae, 57: 253–272.
  • ––– 1966,”Om att definiera välbeställningar”, Fundamenta Mathematicae, 59: 13–21.
  • Makkai, M., 1977, "Admissible Sets and Infinitary Logic", Handbook of Mathematical Logic, J. Barwise (red.), Amsterdam: North-Holland, 233-282.
  • Morley, M., 1965, "Omitting Classes of Elements", The Theory of Models, J. Addison, L. Henkin och A. Tarski (eds.), Amsterdam: North-Holland, 265-273.
  • Nadel, M. 1985, “L ω 1, ω and Admissible Fragments”, i J. Barwise och S. Feferman (red.) 1985, 271–287.
  • Platek, R., 1966, Foundations of Recursion Theory, Ph. D. Examensarbete, Stanford University.
  • Scott, D., 1961, "Mätbara kardinaler och konstruerbara uppsättningar", Bulletin of the Academy of Polish Sciences, 9: 521–524.
  • –––, 1965, “Logik med mängder med oändligt långa formler och ändliga strängar”, Theory of Models, J. Addison, L. Henkin och A. Tarski (red.), Amsterdam: Nord-Holland, 329-341.
  • Scott, D. och A. Tarski, 1958, "Den känslomässiga beräkningen med oändligt långa uttryck", Colloquium Mathematicum, 16: 166-170.
  • Shelah, Saharon, 2012, “Nice infinitary logics”, Journal of the American Mathematical Society, 25: 395-427, tillgängligt online, doi: 10.1090 / S0894-0347-2011-00712-1
  • Tarski, A., 1939, "Ideale in völlständingen Mengenkörpern I", Fundamenta Mathematicae, 32: 140–150.
  • –––, 1958, "Anmärkningar om predikatlogik med oändligt långa uttryck", Colloquium Mathematicum, 16: 171–176.
  • –––, 1962, "Vissa problem och resultat som är relevanta för grunden för uppsättningsteori", i E, Nagel, P. Suppes och A. Tarski (red.), Logic, Methodology and Philosophy of Science, Stanford: Stanford University Press 123-135.
  • Ulam, S., 1930, “Zur Masstheorie in der algemeinen Mengenlehre”, Fundamenta Mathematicae, 16: 140–150.

Akademiska verktyg

sep man ikon
sep man ikon
Hur man citerar det här inlägget.
sep man ikon
sep man ikon
Förhandsgranska PDF-versionen av det här inlägget på SEP-samhällets vänner.
ino-ikon
ino-ikon
Slå upp det här ämnet vid Internet Philosophy Ontology Project (InPhO).
phil papper ikon
phil papper ikon
Förbättrad bibliografi för detta inlägg på PhilPapers, med länkar till dess databas.

Andra internetresurser

Rekommenderas: