|
|
 | | From: | Torkel Franzen | | Subject: | Bokrecension | | Date: | 14 Dec 2004 17:30:14 +0100 |
|
|
 |
Första ordningens logik
Christian Bennet
Studentlitteratur 2004
171 s.
Ingenting tyder på att klassisk första ordningens predikatlogik kommer
att trängas ut som huvudföremål för introduktioner till formell logik,
och årligen utkommer ett antal läroböcker i ämnet. Dock inte många på
svenska, så den logikintresserade kastar sig begärligt över Christian
Bennets bok för att se vad den tillför den magra svenska
logiklitteraturen.
Boken har enligt förordet tillkommit under en oändlig tidsperiod, men
dess omfång är trots detta lyckligtvis begränsat. På de 160 sidorna
text får författaren in allt väsentligt av teori i en
introduktionskurs i logik, och åtskilliga övningar med
lösningar. Framställningen är angenämt läslig, även om den ansluter
sig till en traditionell språklig stollighet genom att tala om
symbolers "ställighet". (Svenska språknämnden påpekade för många år
sedan som svar på en fråga från en filosofistuderande att vi inte talar
om molekylers "atomighet" eller fordons "hjulighet".)
Boken innehåller några felaktigheter. Dessa behöver inte tas upp här,
eftersom författarens webbsida http://maya.phil.gu.se/logik/fol/
ger rättelser till boken.
Boken är skriven för att kunna användas som kurslitteratur. Eftersom
tidigare kompendieversioner av boken använts som kurslitteratur under
många år vid universiteten i Göteborg och Lund kommer den säkerligen
att komma till god användning vid dessa och andra lärosäten under ett
antal år framöver. Mina synpunkter i det följande handlar om
innehållet i boken, helt bortsett från frågan om vad som är lämpligt
eller ändamålsenligt i läroböcker (en fråga där jag inte har någon
bestämd övertygelse).
Predikatlogikens användning av variabler överensstämmer väl med
informellt matematiskt språkbruk, men en formell definition av
predikatlogikens syntax leder raskt till petigheter som handlar om
substitution av termer för variabler. Ett traditionellt sätt att
hantera detta är att införa villkoret att t måste vara fri för x vid
substitution av t för x. I automatisk teorembevisning är det bekvämt
att använda en formalism i vilken man inte behöver kontrollera att
detta villkor är uppfyllt. Det finns också de som föredrar att använda
en sådan formalism även för undervisningssyften eller i teoretiska
sammanhang, och Bennet väljer att använda ett härledningssystem
uppställt av Benson Mates - en form av naturlig deduktion utökad med
fyra logiskt överflödiga kvantifikatorregler - där substitution av t
för x bara sker för variabelfria termer t, och alla formler i
härledningar är slutna. Detta innebär alltså att man resonerar med
användning av konstanter i stället för fria variabler för att komma
fram till allutsagor eller dra slutsatser ur existensutsagor. Dessa
och likartade metoder att undvika "fri för x"-villkoret gör det i viss
mening enklare att uppställa härledningar, men jag är ingalunda
övertygad om att man utanför automatisk teorembevisning gör livet
enklare genom att använda sådana system. Inget sådant system är
vedertaget i teoretiska sammanhang, och när vi börjar tala om PA eller
ZF måste vi hur som helst hantera substitution i det allmänna
fallet. Bennet har inte riktigt fått det hela att gå ihop på denna
punkt. På sidan 41 sägs att i samtliga fall när notationen f(t)
används kommer x att vara den enda fria variabeln i f, och t att vara
en variabelfri term. Detta gäller emellertid enbart i hanteringen av
Mates' system. I formuleringen i senare kapitel av axiom för PA och ZF
används som vanligt substitution där inget av dessa två villkor är
uppfyllt. En uppmärksam läsare kan undra hur dessa teorier alls kan
hanteras med användning av det införda härledningssystemet.
Apropå PA kan en läsare som är bekant med denna teori också undra
varför författaren bland axiomen inkluderar att varje tal skilt från 0
har en omedelbar föregångare (sid 110). Svaret visar sig på sidan 117,
där det sägs att "de första sju axiomen" i PA räcker för
ofullständighet och oavgörbarhet. Den obetydliga formuleringsvinst man
gör på detta är otillräcklig för att motivera att "PA" definieras
på ett sätt som inte överensstämmer med gängse språkbruk, och som
därför kan väcka helt onödig undran och osäkerhet vid läsning av annan
litteratur. Men annars har jag inte något klankade på presentationen
av PA och Gödels sats i avsnitt 9.4, som ger överskådliga bevis, väl
avvägda vad gäller vad som visas och vad som utelämnas.
När det gäller predikatlogiken, för att återgå till framställningen av
denna, ger boken sundhets- och fullständighetsbevis för Mates' system,
där fullständighetsbeviset är en variant av Henkins bevis som jag tror
Mates var först att framlägga i tryck. Leon Henkin har själv i
Bulletin of Symbolic Logic ("The discovery of my completeness proofs",
juni 1996) gett en ingående redogörelse för hur han kom fram till sina
bevis, och nämner först i slutet att han genom att ge logikkurser
själv kom fram först till Hasenjagers förenkling (två steg i stället
för oändligt många steg) och sedan till Mates' (ett steg). Bennet ger
ettstegsresonemanget benämningen "Lindenbaums lemma" (sid 76), vilket
är både historiskt och innehållsligt felaktigt. Annars är beviset
ungefär lika begripligt som vanligt, och kapitlet (Metalogik, kapitel
7) bevisar också kompakthetssatsen och ger ett par typiska
tillämpningar. Löwenheim-Skolems sats ges som övning och nämns också i
kapitel 8 i samband med Lindströms (första) karakterisering av klassisk
predikatlogik, men av någon anledning nämns inte Löwenheim och Skolem
i sammanhanget. Det sista avsnittet 7.4 inför kortfattat begreppet
mekanisk avgörbarhet och formulerar Church-Turings sats om
predikatlogikens oavgörbarhet. Den uppmärksamme läsaren kan bli något
osäker på vad boken egentligen visar om detta resultat. På sidan 67
sägs att "vi skall emellertid senare visa att det för första
ordningens logik inte finns någon generell algoritm för att avgöra om
en sats följer ur en given satsmängd". På sidan 84 förklaras
emellertid att ett bevis av Church-Turings sats dock "skulle leda oss
in i ett helt annat område av logiken, nämligen rekursionsteorin,
varför vi avstår från det här". I avsnitt 9.4 sägs det helt frankt
att "vi har bevisat Church-Turings sats", men detta får nog tolkas
hypotetiskt, utgående från det obevisade påståendet att "de första sju
axiomen i PA" ger en oavgörbar teori.
Henkins bevis för fullständigheten hos första ordningens
predikatlogik, eller någon variant av detta bevis, är vanligt
förekommande i logikböcker, och jag finner det själv beklagligt att så
gott som alla böcker ignorerar hans bevis för fullständigheten hos
typteorin eller hos andra ordningens logik. Beviset för
fullständigheten hos andra ordningens logik (med, låt oss anta,
individvariabler och mängdvariabler) förutsätter en semantik där man
förutom att välja domän för individvariablerna även får välja en domän
för mängdvariablerna. Bennet följer i sin framställning av andra
ordningens logik i kapitel 8 den vanliga inskränkningen att enbart
knyta andra ordningens logik till den semantik i vilken
mängdvariablerna varierar över samtliga delmängder av individdomänen.
Kapitel 10, betitlat "Mängder", förklarar en del mängdteoretiska
begrepp som använts i tidigare kapitel, och eftersom avsnitten
10.1-10.6 inte förutsätter något av det tidigare materialet kan en
läsare som är obekant med dessa mängdteoretiska begrepp studera
kapitel 10 först. Avsnitt 10.4, om axiomatisk mängdlära, använder dock
predikatlogisk formalism och framstår i mina ögon som mer förvirrande
än upplysande, bland annat på grund av mystiska utsagor om
regularitets- och substitutionsaxiomen. Avsnittet innehåller en
intressant passus för den uppmärksamme läsaren, då det sägs att vi kan
i ZF bevisa "att varje ändlig delteori till ZF är konsistent". Den
uppmärksamme läsaren reflekterar att eftersom motsägelsefriheten hos
ZF trivialt följer av att varje ändlig delteori till ZF är
motsägelsefri kan vi alltså i ZF bevisa att ZF är motsägelsefri, och
enligt Gödels andra sats dra slutsatsen att ZF är motsägelsefull.
(Just ett sådant bevis för motsägelsefullheten hos PA har presenterats
av Eduard Wette.) Det är förvisso en smaksak i vilken mån man tycker
att sammanhang som detta bör framhävas och begrundas i en introduktionsbok
i logik, men själv skulle jag gärna ha sett åtminstone en övningsuppgift
för den uppmärkamme läsaren.
Boken framför en frejdig men ounderbyggd övertygelse om den formella
logikens breda tillämplighet, inte bara inom matematik, datalogi, och
närliggande områden, utan inom fysik, kemi, psykologi och sociologi.
I kapitel 9, om första ordningens teorier, sägs inledningsvis att
fastän alla exemplen råkade vara hämtade från matematiken kunde de också
ha hämtats från något av dessa andra områden. Det är för mig höljt i
dunkel vilka första ordningens teorier från dessa områden som kan avses,
och jag skulle gärna ha sett några exempel.
Sammanfattningsvis är mitt intryck att det helt klart finns möjlighet
för en läsare att lära sig åtskilligt om logik genom att studera denna
bok, och att den genom sin allmänna läslighet och sitt hanterliga omfång
inbjuder till sådant studium.
|
|
| | From: | Anders Goeransson | | Subject: | Re: Bokrecension | | Date: | Tue, 14 Dec 2004 18:03:50 +0100 |
|
|
| On 14 Dec 2004 17:30:14 +0100, Torkel Franzen
wrote:
(utelämnad text)
>Boken framför en frejdig men ounderbyggd övertygelse om den formella
>logikens breda tillämplighet, inte bara inom matematik, datalogi, och
>närliggande områden, utan inom fysik, kemi, psykologi och sociologi.
>I kapitel 9, om första ordningens teorier, sägs inledningsvis att
>fastän alla exemplen råkade vara hämtade från matematiken kunde de också
>ha hämtats från något av dessa andra områden. Det är för mig höljt i
>dunkel vilka första ordningens teorier från dessa områden som kan avses,
>och jag skulle gärna ha sett några exempel.
Det låter som om författaren lider av den bland logiker utbredda
vanföreställningen att logik tillämpas inom matematik. Ett mer
belysande sätt att se relationen mellan logik och matematik är att
modern predikatlogik helt enkelt är en liten del av matematik,
utvecklad av matematiker som Frege, Hilbert, von Neumann m fl. där man
studerar matematikens språk med matematiska metoder, ett faktum som
till exempel Brouwer såg klart.
Frege efterapade det matematiska uttrycksättet när han skapade modern
predikatlogik med kvantifikatorer, föga förvånande då att det går att
formulera matematiska teorier i denna predikatlogik...
I den matematik (dvs 99,99%) som inte är logik förekommer väldigt lite
predikatlogik. I (det mycket intressanta) matematikområdet logik
finner man förstås utredningar av hur andra delar av matematik kan ges
en framställning, post festum förstås, i olika axiomsystem. Detta har
dock inte, med få undantag, något intresse för den matematiker som
arbetar inom de områden som utsätts för dylik (miss)behandling.
Att som författaren av boken behandlad ovan gör, inbilla sig att det
är av något som helst intresse att formulera någon del av till exempel
Kemi i predikatlogik är förstås ren och skär logiksjuka, som Torkel
hovsamt formulerar; "jag skulle gärna ha sett några exempel"...
|
|
| | From: | Torkel Franzen | | Subject: | Re: Bokrecension | | Date: | 14 Dec 2004 18:48:23 +0100 |
|
|
| Anders Goeransson writes:
> Det låter som om författaren lider av den bland logiker utbredda
> vanföreställningen att logik tillämpas inom matematik.
Nja, jag uttryckte mig nog en smula vilseledande. Bättre skulle ha
varit att tillskriva författaren tanken att logiken är tillämplig
*på* matematik, och därom torde de lärda inte tvista.
|
|
| | From: | Anders Goeransson | | Subject: | Re: Bokrecension | | Date: | Tue, 14 Dec 2004 19:04:09 +0100 |
|
|
| On 14 Dec 2004 18:48:23 +0100, Torkel Franzen
wrote:
>Anders Goeransson writes:
>
>> Det låter som om författaren lider av den bland logiker utbredda
>> vanföreställningen att logik tillämpas inom matematik.
>
> Nja, jag uttryckte mig nog en smula vilseledande. Bättre skulle ha
>varit att tillskriva författaren tanken att logiken är tillämplig
>*på* matematik, och därom torde de lärda inte tvista.
Ja, det ska bli intressant att se, i tryck, den lärobok i fysik, där
inte bara matematiken som används utan även de fysikaliska teorierna
uttrycks i första ordningens logik.
|
|
| | From: | Alexander Backlund | | Subject: | Re: Bokrecension | | Date: | Wed, 15 Dec 2004 13:09:13 +0100 |
|
|
|
"Anders Goeransson" skrev i meddelandet
news:fcaur05cf7biki05sl6gq21ge0te5fv0va@4ax.com...
> On 14 Dec 2004 18:48:23 +0100, Torkel Franzen
> wrote:
>
>>Anders Goeransson writes:
>>
>>> Det låter som om författaren lider av den bland logiker utbredda
>>> vanföreställningen att logik tillämpas inom matematik.
>>
>> Nja, jag uttryckte mig nog en smula vilseledande. Bättre skulle ha
>>varit att tillskriva författaren tanken att logiken är tillämplig
>>*på* matematik, och därom torde de lärda inte tvista.
>
> Ja, det ska bli intressant att se, i tryck, den lärobok i fysik, där
> inte bara matematiken som används utan även de fysikaliska teorierna
> uttrycks i första ordningens logik.
Det skulle väl låta sig göras (eller eventuellt i andra ordningens
predikatlogik)? Huruvida det vore särskilt upplysande är väl en annan fråga.
|
|
| | From: | Torkel Franzen | | Subject: | Re: Bokrecension | | Date: | 15 Dec 2004 16:18:08 +0100 |
|
|
| "Alexander Backlund" writes:
> Det skulle väl låta sig göras (eller eventuellt i andra ordningens
> predikatlogik)?
Nej, predikatlogisk formalism, vare sig första eller andra
ordningen, är komplett ovidkommande för fysiken. Vi skulle lika gärna
kunna formulera Tusen och en natt i predikatlogik.
|
|
| | From: | Alexander Backlund | | Subject: | Re: Bokrecension | | Date: | Fri, 17 Dec 2004 03:20:44 +0100 |
|
|
|
"Torkel Franzen" skrev i meddelandet
news:vcbr7lr8ua7.fsf@beta19.sm.ltu.se...
> "Alexander Backlund" writes:
>
>> Det skulle väl låta sig göras (eller eventuellt i andra ordningens
>> predikatlogik)?
>
> Nej, predikatlogisk formalism, vare sig första eller andra
> ordningen, är komplett ovidkommande för fysiken. Vi skulle lika gärna
> kunna formulera Tusen och en natt i predikatlogik.
Det tycker jag att du ska försöka göra.
|
|
| | From: | Anders Goeransson | | Subject: | Re: Bokrecension | | Date: | Tue, 14 Dec 2004 19:22:21 +0100 |
|
|
| On 14 Dec 2004 17:30:14 +0100, Torkel Franzen
wrote:
(utelämnad text)
>Kapitel 10, betitlat "Mängder", förklarar en del mängdteoretiska
>begrepp som använts i tidigare kapitel, och eftersom avsnitten
>10.1-10.6 inte förutsätter något av det tidigare materialet kan en
>läsare som är obekant med dessa mängdteoretiska begrepp studera
>kapitel 10 först. Avsnitt 10.4, om axiomatisk mängdlära, använder dock
>predikatlogisk formalism och framstår i mina ögon som mer förvirrande
>än upplysande, bland annat på grund av mystiska utsagor om
>regularitets- och substitutionsaxiomen. Avsnittet innehåller en
>intressant passus för den uppmärksamme läsaren, då det sägs att vi kan
>i ZF bevisa "att varje ändlig delteori till ZF är konsistent". Den
>uppmärksamme läsaren reflekterar att eftersom motsägelsefriheten hos
>ZF trivialt följer av att varje ändlig delteori till ZF är
>motsägelsefri kan vi alltså i ZF bevisa att ZF är motsägelsefri, och
>enligt Gödels andra sats dra slutsatsen att ZF är motsägelsefull.
>(Just ett sådant bevis för motsägelsefullheten hos PA har presenterats
>av Eduard Wette.) Det är förvisso en smaksak i vilken mån man tycker
>att sammanhang som detta bör framhävas och begrundas i en introduktionsbok
>i logik, men själv skulle jag gärna ha sett åtminstone en övningsuppgift
>för den uppmärkamme läsaren.
>
Kanske borde läroböcker i första ordningens logik skrivas i första
ordningens logik? Det skulle kanske göra ämnet en smula otillgängligt
för alla utom den speciellt entusiastiska nybörjaren, men det är det
ju i praktiken ändå.
|
|
|
