Löbs sats

I matematisk logik säger Löbs sats att i Peano-aritmetik (PA) (eller vilket formellt system som helst inklusive PA), för vilken formel P som helst , om det är bevisbart i PA att "om P är bevisbart i PA så är P sant", så är P är bevisbart i PA. Om Prov( P ) betyder att formeln P är bevisbar, kan vi uttrycka detta mer formellt som

Om

${\displaystyle PA\,\vdash \,{{\rm {Prov}}(P)\rightarrow P}} så$

P

$\displaystyle PA\, \vdash \,P}$

En omedelbar följd ( kontrapositiva ) av Löbs sats är att om P inte är bevisbart i PA, så är "om P är bevisbart i PA, så är P sant" inte bevisbart i PA. Till exempel, "Om $1+1=3$ är bevisbart i PA, så är $1+1=3$ inte bevisbart i PA.

Löbs sats är uppkallad efter Martin Hugo Löb , som formulerade den 1955. Den är relaterad till Currys paradox .

Löbs sats i bevisbarhetslogik

Bevisbarhetslogik abstraherar bort från detaljerna i kodningar som används i Gödels ofullständighetsteorem genom att uttrycka bevisbarheten för $\phi$ i det givna systemet i modallogikens språk , med hjälp av modaliteten $\Box \ phi$ .

Då kan vi formalisera Löbs sats med axiomet

$\Box (\Box P\rightarrow P)\rightarrow \Box P,$

känt som axiom GL, för Gödel–Löb. Detta formaliseras ibland med hjälp av en slutledningsregel som infererar

$P$

från

$\Box P\rightarrow P.$

Den bevisbarhetslogik GL som blir resultatet av att ta den modala logiken K4 (eller K , eftersom axiomschemat 4 , ${\displaystyle \Box A\rightarrow \Box \Box A},$ sedan blir överflödig) och lägga till ovanstående axiom GL är det mest intensivt undersökta systemet inom bevisbarhetslogik.

Modalt bevis på Löbs sats

Löbs teorem kan bevisas inom modal logik med endast några grundläggande regler om bevisbarhetsoperatorn (K4-systemet) plus förekomsten av modala fixpunkter.

Modala formler

Vi kommer att anta följande grammatik för formler:

1. Om $X$ är en propositionsvariabel så är $X$ en formel.
2. Om $K$ är en propositionskonstant, så är $K$ en formel.
3. Om $A$ är en formel, då $\Box A$ är en formel.
4. Om $A$ och $B$ är formler, så är det också $\neg A$ , $A\rightarrow B$ , $A\ kil B$ , $A\vee B$ och $A\leftrightarrow B$

En modal mening är en modal formel som inte innehåller några propositionella variabler. Vi använder $\vdash A$ för att betyda $A$ är ett teorem.

Modala fixpunkter

Om $F(X)$ är en modal formel med endast en propositionsvariabel ${\displaystyle X} ,$ då är en modal fixpunkt för $F(X)$ en mening $\Psi$ så att

$\vdash \Psi \leftrightarrow F(\Box \Psi )$

Vi kommer att anta att det finns sådana fixpunkter för varje modal formel med en fri variabel. Detta är naturligtvis inte en självklar sak att anta, men om vi tolkar $\Box$ som bevisbarhet i Peano Arithmetic, så följer förekomsten av modala fixpunkter av diagonallemmat .

Modala regler för slutledning

Förutom förekomsten av modala fixpunkter, antar vi följande slutledningsregler för bevisbarhetsoperatorn ${\displaystyle \Box } ,$ känd som Hilbert–Bernays bevisbarhetsvillkor :

1. (nödvändighet) Av $\vdash A$ dra slutsatsen $\vdash \Box A$ : Informellt säger detta att om A är ett teorem så är det bevisbart.
2. (intern nödvändighet) $\vdash \Box A\rightarrow \Box \Box A$ : Om A är bevisbart så är det bevisbart att det är bevisbart.
3. (rutafördelning) ${\displaystyle \vdash \Box (A\högerpil B)\högerpil (\Box A\högerpil \Ruta B)} :$ Denna regel låter dig att göra modus ponens inuti bevisbarhetsoperatören. Om det är bevisbart att A antyder B, och A är bevisbart, så är B bevisbart.

Bevis för Löbs sats

Mycket av bevisen använder sig inte av antagandet ${\displaystyle \Box P\to P} ,$ så för att underlätta förståelsen är beviset nedan uppdelat för att lämna delarna beroende på $\Box P\to P$ till slutet.

Låt $P$ vara vilken modal mening som helst.

1. 
   Av förekomsten av modala fixpunkter för varje formel (särskilt formeln $X\rightarrow P$ ) följer det att det finns en mening $\Psi$ så att $\vdash \Psi \leftrightarrow (\Box \Psi \rightarrow P)$ .
2. ${\displaystyle \vdash \Psi \rightarrow (\Box \Psi \rightarrow P)} ,$ från 1.
3. ${\displaystyle \vdash \Box (\Psi \rightarrow (\Box \Psi \rightarrow P))} ,$ från 2 enligt necessitationsregeln.
4. ${\displaystyle \vdash \Box \Psi \rightarrow \Box (\Box \Psi \rightarrow P)} ,$ från 3 och boxdistributionsregeln.
5. $\vdash \Box (\Box \Psi \rightarrow P)\rightarrow (\Box \Box \Psi \rightarrow \Box P)$ , genom att tillämpa boxdistributionsregeln med $A=\Box \Psi$ och $B=P$ .
6. ${\displaystyle \vdash \Box \Psi \rightarrow (\Box \Box \Psi \rightarrow \Box P)} ,$ från 4 och 5.
7. ${\displaystyle \vdash \Box \Psi \rightarrow \Box \Box \Psi } ,$ från 6 enligt den interna nödvändighetsregeln.
8. 
   
   ${\displaystyle \vdash \Box \Psi \rightarrow \Box P} ,$ från 6 och 7. Nu kommer den del av beviset där hypotesen används.
   
   
9. Antag att $\vdash \Box P\rightarrow P$ . Grovt sett är det ett teorem att om $P$ är bevisbart så är det faktiskt sant. Detta är ett påstående om sundhet .
10. ${\displaystyle \vdash \Box \Psi \rightarrow P} ,$ från 8 och 9.
11. ${\displaystyle \vdash (\Box \Psi \rightarrow P)\rightarrow \Psi } ,$ från 1.
12. ${\displaystyle \vdash \Psi } ,$ från 10 och 11.
13. ${\displaystyle \vdash \Box \Psi } ,$ från 12 enligt nödvändighetsregeln.
14. $\vdash P$ , från 13 och 10.

Exempel

En omedelbar följd av Löbs sats är att om P inte är bevisbart i PA, så är "om P är bevisbart i PA, så är P sant" inte bevisbart i PA. Eftersom vi vet att PA är konsekvent (men PA vet inte att PA är konsekvent), här är några enkla exempel:

• "Om $1+1=3$ är bevisbart i PA, så är $1+1=3$ inte bevisbart i PA, eftersom ${ \displaystyle 1+1=3}$ är inte bevisbart i PA (eftersom det är falskt).
• "Om $1+1=2$ är bevisbart i PA, då är $1+1=2$ " bevisbart i PA, liksom alla påståenden av formen " Om X, då $1+1=2$ ".
• "Om den förstärkta finita Ramsey-satsen är bevisbar i PA, så är den förstärkta finita Ramsey-satsen sann" är inte bevisbar i PA, eftersom "Den förstärkta finita Ramsey-satsen är sann" inte är bevisbar i PA (trots att den är sann).

I doxastisk logik visar Löbs teorem att alla system som klassificeras som en reflexiv " typ 4 "-resonemang också måste vara " blygsam ": en sådan resonerande kan aldrig tro "min tro på P skulle innebära att P är sant", utan att också tro att P är sant.

Gödels andra ofullständighetsteorem följer av Löbs sats $genom$ att P .

Omvänt: Löbs teorem antyder att det finns modala fixpunkter

Inte bara förekomsten av modala fixpunkter innebär Löbs sats, utan det omvända är också giltigt. När Löbs sats ges som ett axiom (schema), förekomsten av en fixpunkt (upp till bevisbar ekvivalens) $p\leftrightarrow A(p)$ för vilken formel A ( p ) som helst som modaliseras i p kan härledas. Sålunda i normal modal logik är Löbs axiom ekvivalent med konjunktionen av axiomschema 4 , ${\displaystyle (\Box A\rightarrow \Box \Box A)} ,$ och förekomsten av modal fix poäng.

Citat

•   Boolos, George S. (1995). Bevisbarhetens logik . Cambridge University Press. ISBN 978-0-521-48325-4 .
•   Löb, Martin (1955), "Solution of a Problem of Leon Henkin", Journal of Symbolic Logic , 20 (2): 115–118, doi : 10.2307/2266895 , JSTOR 2266895
•   Hinman, P. (2005). Grunderna i matematisk logik . AK Peters. ISBN 978-1-56881-262-5 .
• Verbrugge, Rineke (LC) (1 januari 2016). "Provabilitetslogik" . Stanford Encyclopedia of Philosophy . Hämtad 6 april 2016 .

externa länkar

• Löbs sats vid PlanetMath
• The Cartoon Guide to Löbs Theorem av Eliezer Yudkowsky