Beperkingen van Formele Systemen
De grenzen die de logica aan zichzelf stelt.
Inhoudsopgave
1. Een eerste barst in Cantor's verzamelingenleer: de Paradox van Russell
2. De onvermijdelijke dubbelzinnigheid van de predikatenlogica voor de wiskunde.
3. De onvolledige bewijskracht van rekenkundige systemen die consistent zijn.
4. De onbeslisbaarheid van de predikatenlogica.
5. De beperkte mechaniceerbaarheid van wiskundige operaties.
1. Een eerste barst in Cantor's verzamelingenleer: de Paradox van Russell.
In 1901 ontdekte Bertrand Russell (1872-1970) een eenvoudige paradox in de zgn. 'naďeve versie' van de verzamelingen-theorie van Georg Cantor (1845-1918).
{Nb. Een ontdekking overigens die de voetsporen volgde van Cantor zelf (1895), en daarnaast Cesare Burali-Forti (1897),
David Hilbert (ca. 1896-1899), en Ernst Zermelo (1900).}
Samenvatting:
De Paradox van Russell.
De zgn. 'Paradox van Russell' houdt in dat als verzamelingen
zonder meer deelverzameling kunnen zijn van zichzelf, er ook een verzameling
van al dat soort verzamelingen moet bestaan, maar dan zal nog steeds het complement van die verzameling bestaan,
omdat dan immers nog steeds niet alle verzamelingen deelverzameling zullen zijn van zichzelf, hetgeen onvermijdelijk
tot een paradox leidt:
(a) Stel dat de bedoelde complement-verzameling deel is van zichzelf, dan kan ze niet tot haar eigen klasse behoren, en dus geen deel zijn van zichzelf.
(b) Stel dat ze geen deel is van zichzelf, dan moet ze wel tot haar eigen klasse behoren, dus een verzameling zijn die geen deel is zichzelf, maar dan behoort ze tot zichzelf.
(a) Stel dat de bedoelde complement-verzameling deel is van zichzelf, dan kan ze niet tot haar eigen klasse behoren, en dus geen deel zijn van zichzelf.
(b) Stel dat ze geen deel is van zichzelf, dan moet ze wel tot haar eigen klasse behoren, dus een verzameling zijn die geen deel is zichzelf, maar dan behoort ze tot zichzelf.
Dit resultaat betekent dat het begrip 'is deel van' tegelijk waar en onwaar kan zijn: dus inherent contradictie behelst.
Maar volgens een grondprincipe van de 'naďeve' verzamelingen-leer, Cantor's Comprehensie Axioma ( Naives Komprehensionsaxiom) omvat het 'een-element-zijn van een ding a ten opzichte van een verzameling A' juist de toestand dat a de eigenschappen heeft die door A vertegenwoordigd worden! Dit axioma blijkt nu inconsistent, dus niet geschikt voor beslissingen over lidmaatschappen van verzamelingen ..
Hieruit volgt dat aan afzonderlijke verzamelingen geen inhoudelijk onderscheid kan worden gegeven: dus geen betekenis, naast hun syntactische c.q. kwantitatieve notatie. De conclusie is dat verzamelingen louter formele constructies blijken, die syntactisch wčl maar semantisch géén inhoud hebben .. anders gezegd, de wiskundige verzamelingenleer raakt dan ook zeker nergens de wereld van concrete objecten en ervaringen op een eenduidige manier, waarvoor ze juist ooit bedoeld was ..
In antwoord op Russell's paradox publiceerde Ernst Zermelo (1871-1953) in 1908 een alternatief stel axioma's voor het problematische Comprehensie Axioma. Met name Zermelo's Axiom of Foundation (Fundierungsaxiom ) zorgt ervoor dat een niet-lege verzameling altijd minstens één ding omvat dat niet samenvalt met de verzameling zelf, zodat deze niet tegelijk volledig deel kan zijn van zichzelf. We zullen echter zien dat dergelijke voorzieningen de kloof tussen syntax en semantiek voor de verzamelingenleer nog niet hebben kunnen dichten ..
2. De onvermijdelijke dubbelzinnigheid van de predikatenlogica voor de wiskunde.
Voortbouwend op het werk van Leopold Löwenheim (1878-1957) dat in 1915 werd gepubliceerd, presenteerde Thoralf Albert Skolem (1887-1963) in 1920 zijn bewijs voor het zgn. Löwenheim-Skolem theorema (L-S). Dit theorema raakt de geschiktheid van het logische systeem dat gebruikt pleegt te worden om de axioma's van de verzamenlingenleer te definiëren: de predikatenlogica.
2.1. Het kader van de predikatenlogica
De predikatenlogica (
PDL
) is een vorm van formele logica, een uitbreiding van de propositielogica (PPL
). Grondlegger van de predikaten calculus was Gottlob Frege (1848-1925), zie diens Grundgesetze der Arithmetik I en II (1893, 1903). Terwijl dePPL
beperkt is tot relaties tussen elementaire beweringen c.q. proposities, heeft het systeem van dePDL
het voordeel dat geredeneerd kan worden binnen elementaire beweringen, en wel over eigenschappen en relaties van dingen in een bepaalde verzameling, een domein. Daarbij maakt dePDL
verdere nuanceringen mogelijk door kwantifikatie van eigenschappen over dingen, met behulp van zgn. kwantoren. Daarom wordt dePDL
ook wel kwantorlogica genoemd. Door deze eigenschappen biedt dePDL
veel meer mogelijkheden dan dePPL
om logische verbanden uit te drukken - zowel die in natuurlijke taal, als in wiskunde en andere wetenschapsgebieden.
{Nb. Met de kanttekening dat in de 'eerste orde' versie (
)
geen stellingen over meta-eigenschappen (eigenschappen van eigenschappen) zijn toegelaten.}
PDL
-I
)
geen stellingen over meta-eigenschappen (eigenschappen van eigenschappen) zijn toegelaten.}Predikatie
In de
PDL
kunnen eigenschappen en relaties via begrippen - predikaten en functies - door de 'gebruiker' van het systeem naar eigen goeddunken worden toegekend aan objecten in het domein. De enige beperking hierbij is dat dit alleen op zinvolle wijze kan wanneer de regels worden gevolgd van de 'taal' van het systeem, de expressieregels of syntax.Hoe dan ook is de taal van de logica op zichzelf altijd inherent inhoudsvrij, oftewel ongeďnterpreteerd. Ook de objecten in een domein hebben zelf binnen het systeem verder géén eigenschappen: het zijn volkomen 'anonieme' en onderling verwisselbare individuen zonder eigen intrinsieke betekenis of inherente eigenschap.
Minimaal domein
Een stelling in de predikatenlogica kan dus via predicaat-toewijzing, of predikatie, verwijzen naar een aantal objecten (d.i. minstens één). In dat geval veronderstelt ze uiteraard het bestaan van minstens één verzameling bestaande uit minstens zoveel verschillende objecten als in de stelling worden onderscheiden: een zgn. 'minimaal domein' voor de stelling. Maar die verzameling hóeft natuurlijk niet te bestaan: allereerst niet in het abstracte domein, en nog minder in het empirische, fysische of welk ander domein ook. Dat heeft dan wel consequenties voor de mogelijkheid om de betreffende stelling 'waar te maken'.
Interpretatie
We kunnen met een logische stelling pas iets van een inhoudelijke voorstelling van zaken weergeven nádat we haar een interpretatie geven. We wijzen daarbij een domein aan (bijvoorbeeld een bevolking), en geven aan waar de gebruikte codes voor objecten, predikaten en functies voor staan (bijvoorbeeld personen, werkwoorden en 'netwerkrelaties' tussen personen). Maar, met een inhoudelijke voorstelling van zaken hebben we natuurlijk nog niet automatisch een ware bewering.
Voorafgaand aan interpretatie bestaat een bewering in de logica enkel uit een 'kale' syntactische structuur. In dat stadium veronderstelt de
PDL
-I
alleen dat sommige verzamelingen kúnnen bestaan,
van welke omvang ook, maar niet dŕt ze ook daadwerkelijk bestaan. Daardoor kunnen we deze kale structuur
in principe naar eigen goeddunken 'projecteren' op elk domein, concreet of abstract, reëel of fictief.
De mate waarin de structuur past op het gekozen domein is mede beslissend voor de waarheidswaarde van die structuur
volgens de logica.Waarheidsvervulling
Om nu een bewering of redenering in de taal van de
PDL
als waar te laten gelden dient allereerst aan één randvoorwaarde te worden voldaan: dat ze verenigbaar is met de toestand van het domein. Dit betekent dat aan minstens drie volgende eisen voldaan moet worden:
(1) de logische relaties in de stelling (vergelijkbaar met voegwoorden in de natuurlijke taal) en de verwijzingsrelaties
van predikaten en functies leveren onderling geen contradictie op;
(2) het gekozen domein voor de variabelen en objecten is ruim genoeg;
(3) en eventuele inhoudelijke aannamen over toestanden in het domein zijn juist.
(2) het gekozen domein voor de variabelen en objecten is ruim genoeg;
(3) en eventuele inhoudelijke aannamen over toestanden in het domein zijn juist.
Voor een waarheids-vervullende interpretatie - een zgn. model voor de betreffende stelling - is in ieder geval zoals gezegd een 'minimaal domein' nodig: een domein dat een voldoende aantal verschillende objecten bevat, om recht te doen aan de verscheidenheid en combinaties van objecten die de betreffende redenering veronderstelt. Het domein hoeft dus voor waarheids-vervulling alleen te voldoen aan een minimale omvang (c.q. kardinaliteit), oftewel een benedengrens. Maar voor waarheids-vervulling stelt de
PDL
-I
geen bovengrens aan het domein.Pas als we aannemen dat een stelling - inclusief al haar predicaties - voor 'waar' kan doorgaan, kunnen we aannemen dat het minimale domein ervoor inderdaad bestaat. In dat geval stelt die stelling logischerwijze alleen 'minimale' kwantitatieve eisen aan dat domein, geen enkele eis aan de maximale omvang, en zeker geen kwalitatieve eisen aan type, categorie, essentie en dergelijke.
Kortom, elke stelling in de logica - dus ook de predikatenlogica - is volkomen onafhankelijk van welk specifiek domein of gebied van de werkelijkheid dan ook. Juist daardoor is de logica toepasbaar op welk specifiek domein of gebied van de werkelijkheid dan ook.
Het systeem van de
PDL
werd aan het begin van de twintigste eeuw gezien als voldoende krachtig čn eenduidig beslisbaar om de verzamelingen theorie in te definiëren, ook die volgens de axioma's van Ernst F.F. Zermelo (1871-1953) en Adolf A.H. Fraenkel (1891-1965) - het Zermelo-Fraenkel systeem (ZF).Er waren echter twijfels gerezen over de geschiktheid van de predikatenlogica om de domein en van de verzamelingenleer te definiëren. Deze twijfels hadden ironisch genoeg juist te maken met de sterke eigenschappen van de
PDL
-I
, die al op onweerlegbare wijze waren bewezen.2.2. De kracht van de PDL
-I
PDL
-ICorrectheid (Soundness in-formele-zin).
De meerwaarde van logische systemen ligt allereerst in de mogelijkheid van absoluut sluitende bewijsvoering van stellingen. Dat laatste kan alleen door middel van strikt eenduidige afleidingen van conclusies uit basisaannamen (premissen), die ook volledig betrouwbaar zijn. Een eerste vereiste aan een formeel systeem is dan ook Correctheid: de uitkomsten van formele bewijzen behoren in overeenstemming te zijn met de conclusies die inhoudelijk uit de premissen volgen.
Formeel gesteld:
{ (
G) 
(
G). }
T
G) (T
G). }Consistentie.
Maar als een logisch correct systeem een formele contradictie oplevert, zal dit ook een inhoudelijke strijdigheid betekenen, en dus resulteren in onwaarheid.
Formeel gesteld:
{ ( 
)
(
); 
(
T
)
(T
); (T
$
0). }Maar volgens de elementaire logische wetten van de
PPL
impliceert een conclucie die uitsluitend onwaar is (per contrapositie) dat ook alle premissen onwaar zijn. Het laatste betekent echter dat het gehele systeem uitsluitend onwaarheid oplevert: dus van weinig waarde is.
Formeel gesteld:
{ ((¬
((
(
¬((
)
¬
$
0$
1)((
T
$
0)(
$
1 ¬T
)))((
T
)
¬T
). }Een volgende belangrijke eigenschap van formele systemen is dan ook Consistentie: dat uit het formele systeem geen (formele) contradicties volgen.
Formeel gesteld:
{ ¬(( G) 
( ¬G)); oftewel: ¬((G ¬G)); oftewel: ¬( ). }
T
G) (T
¬G)); oftewel: ¬(T
(G ¬G)); oftewel: ¬(T
). }Volgens het Fundamenteel Theorema, of Model Existentie Theorema is elke verzameling van welgevormde formules in de taal van de predikatenlogica die (syntactisch) consistent is ook (semantisch) vervulbaar.
Formeel gesteld:
{ ¬( )
¬(
); ¬(
T
)
¬(T
); ¬(T
$
0). }
Samenvatting:
Bewijs van het Model Existence Theorem voor
In grote lijnen verloopt dit bewijs als volgt.
(1)
Neem een verzameling
Om te bewijzen dat zo'n verzameling K*[consis] altijd vervulbaar is, moeten we aantonen dat er een interpretatie, of zgn. (domein-) structuur bestaat die haar vervult, met andere woorden, haar een adequaat model verschaft (in de logica kortweg 'model' genoemd). Dit bewijs is constructief van aard.
(2)
Neem aan dat de betreffende verzameling K*[consis] existentiële kwantoren kan bevatten.
Het domein van het benodigde model moet altijd minstens zoveel elementen bevatten als het aantal existentieel gekwantificeerde formules c.q. predicaties c.q. variabelen in de verzameling zinnen die het met zekerheid vervult.
Houd er ook rekening mee dat de kardinaliteit van de verzameling K*[consis] aftelbaar oneindig kan zijn: dus ook het aantal existentiële kwantoren. De omvang of signatuur van het model moet dan ook voldoende zijn: dus mogelijk aftelbaar oneindig.
We hebben dus een taalsysteem nodig dat rijk en omvangrijk genoeg is om de gehele verzameling zinnen K*[consis] weer te geven.
Construeer daarom eerst een uitgebreide versie van het taalsysteem
(3)
(Henkinizatie: Voeg daarna aan elke existentiële formule in de verzameling een valide inferentie toe die stelt dat dezelfde formule haar geďnstantieerde versie impliceert, zodanig dat in de laatste elke existentiële variabele-naam is vervangen door een nieuwe en unieke object-constante-naam - zgn. Henkin constante - ontleend aan de uitgebreide taal
(Henkinizatie: door substitutie, via instantiatie, via Skolemizatie).
Het resultaat bevat voor alle existentiële predicaties zgn. 'getuigen', oftewel witnesses (dit zijn a.h.w. de syntactische pendanten van grondinstantiaties in zgn. Herbrandinterpretaties).
(4)
Het is dan eenvoudig aantoonbaar dat elke mogelijke (conjunctieve) combinatie van zulke willekeurig welke Henkin -versies van willekeurig welke formules uit een verzameling die consistent is, eveneens consistent is. En daaruit volgt dat de gehele machtsverzameling (power set) van een verzameling Henkin-formules opgebouwd uit zulke combinaties, de Henkin extensie van de verzameling, zeg K *[henkin] ook consistent is. Dit volgens het Henkin Extension Lemma.
(5)
Vervolgens geldt op grond van het Lindenbaum Lemma dat elke consistente verzameling - dus ook de Henkin extensie daarvan - vervat is in een verzameling die de grootst mogelijke uitbreiding ervan vormt met behoud van consistentie: een maximaal consistente verzameling K *[consis-max]. Deze heeft onder meer als eigenschappen,
Het bovenstaande combinerend kunnen we afleiden dat voor elke oorspronkelijke K *[consis] een maximaal consistente Henkin extensie bestaat, K *[henkin-max].
(6)
Omdat alle existentiële predicaties in deze 'super'-verzameling witnesses hebben, heeft ze de kenmerken van een zgn. Hintikka verzameling, K*[hintikka]: volgens het Hintikka lemma.
(In een Hintikka verzameling zijn kort gezegd alle complexe formules volledig gereduceerd tot literalen, alle gekwantificeerde predicaties volledig geďnstantieerd, en ze bevat geen contradictoire atomen/literalen).
(7)
Tenslotte geldt volgens het Satisfiability Lemma dat elke Hintikka set vervulbaar is: dus ook K*[henkin-max].
(8)
Omdat elke willekeurige verzameling K*[consis] hiervan deelverzameling is, volgt hieruit dat zij eveneens vervulbaar is (QED).
Bewijs van het Model Existence Theorem voor PDL
-I
.
PDL
-IIn grote lijnen verloopt dit bewijs als volgt.
(1)
Gegeven: een consistente verzameling welgevormde formules.
Neem een verzameling
L!
[wff] van welgevormde formules in een formalisme, of taalL!
in de predikatenlogica. Stel dat deze ( syntactisch) consistent is.Om te bewijzen dat zo'n verzameling K*[consis] altijd vervulbaar is, moeten we aantonen dat er een interpretatie, of zgn. (domein-) structuur bestaat die haar vervult, met andere woorden, haar een adequaat model verschaft (in de logica kortweg 'model' genoemd). Dit bewijs is constructief van aard.
(2)
Extensie van de formele taal met oneindig veel namen.
Neem aan dat de betreffende verzameling K*[consis] existentiële kwantoren kan bevatten.
Het domein van het benodigde model moet altijd minstens zoveel elementen bevatten als het aantal existentieel gekwantificeerde formules c.q. predicaties c.q. variabelen in de verzameling zinnen die het met zekerheid vervult.
Houd er ook rekening mee dat de kardinaliteit van de verzameling K*[consis] aftelbaar oneindig kan zijn: dus ook het aantal existentiële kwantoren. De omvang of signatuur van het model moet dan ook voldoende zijn: dus mogelijk aftelbaar oneindig.
We hebben dus een taalsysteem nodig dat rijk en omvangrijk genoeg is om de gehele verzameling zinnen K*[consis] weer te geven.
Construeer daarom eerst een uitgebreide versie van het taalsysteem
L!
door toevoeging van oneindig veel nieuwe, unieke namen c.q. symbolen voor object-constanten, met als resultaat de geëxtendeerde taalL!
[inf].(3)
Extensie met alle benodigde Henkin grondinstantiaties als witnesses.
(Henkinizatie: Voeg daarna aan elke existentiële formule in de verzameling een valide inferentie toe die stelt dat dezelfde formule haar geďnstantieerde versie impliceert, zodanig dat in de laatste elke existentiële variabele-naam is vervangen door een nieuwe en unieke object-constante-naam - zgn. Henkin constante - ontleend aan de uitgebreide taal
L!
[inf].(Henkinizatie: door substitutie, via instantiatie, via Skolemizatie).
Het resultaat bevat voor alle existentiële predicaties zgn. 'getuigen', oftewel witnesses (dit zijn a.h.w. de syntactische pendanten van grondinstantiaties in zgn. Herbrandinterpretaties).
(4)
Consistentie van de Henkin extensie.
Het is dan eenvoudig aantoonbaar dat elke mogelijke (conjunctieve) combinatie van zulke willekeurig welke Henkin -versies van willekeurig welke formules uit een verzameling die consistent is, eveneens consistent is. En daaruit volgt dat de gehele machtsverzameling (power set) van een verzameling Henkin-formules opgebouwd uit zulke combinaties, de Henkin extensie van de verzameling, zeg K *[henkin] ook consistent is. Dit volgens het Henkin Extension Lemma.
(5)
Geďmpliceerd is een omvattende maximaal-consistente verzameling.
Vervolgens geldt op grond van het Lindenbaum Lemma dat elke consistente verzameling - dus ook de Henkin extensie daarvan - vervat is in een verzameling die de grootst mogelijke uitbreiding ervan vormt met behoud van consistentie: een maximaal consistente verzameling K *[consis-max]. Deze heeft onder meer als eigenschappen,
(a) dat er geen formule aan kan worden toegevoegd zonder dat de verzameling inconsistent wordt;
(b) dat voor elke welgevormde formule hetzij de bevestiging, hetzij het tegendeel er onderdeel van is;
en (c) dat elke formule die ertoe behoort ook eruit afleidbaar is.
(b) dat voor elke welgevormde formule hetzij de bevestiging, hetzij het tegendeel er onderdeel van is;
en (c) dat elke formule die ertoe behoort ook eruit afleidbaar is.
Het bovenstaande combinerend kunnen we afleiden dat voor elke oorspronkelijke K *[consis] een maximaal consistente Henkin extensie bestaat, K *[henkin-max].
(6)
De maximaal-consistente verzameling is een Hintikka verzameling.
Omdat alle existentiële predicaties in deze 'super'-verzameling witnesses hebben, heeft ze de kenmerken van een zgn. Hintikka verzameling, K*[hintikka]: volgens het Hintikka lemma.
(In een Hintikka verzameling zijn kort gezegd alle complexe formules volledig gereduceerd tot literalen, alle gekwantificeerde predicaties volledig geďnstantieerd, en ze bevat geen contradictoire atomen/literalen).
(7)
Een maximaal-consistente Hintikka verzameling is vervulbaar.
Tenslotte geldt volgens het Satisfiability Lemma dat elke Hintikka set vervulbaar is: dus ook K*[henkin-max].
(8)
De consistente verzameling is vervulbaar.
Omdat elke willekeurige verzameling K*[consis] hiervan deelverzameling is, volgt hieruit dat zij eveneens vervulbaar is (QED).
Volledigheid
Een belangrijke eigenschap van formele systemen is vervolgens Volledigheid: alles wat we inhoudelijk kunnen weten of afleiden met betrekking tot een aantal premissen, dient als het even kan in het systeem formeel bewijsbaar te zijn. Preciezer gezegd: een systeem is volledig als geldigheid van een redenering in het systeem impliceert dat die redenering ook formeel afleidbaar is in dat systeem.
Formeel gesteld:
{ ( G) ( G). }
T
G) (T
G). }Voor de simpelste vorm van formele logica, de propositielogica (
PPL
), werd volledigheid al in 1920 bewezen door Emil L. Post (1897-1954). Ook blijkt het validiteitsprobleem beslisbaar voor een uitbreiding van dePPL
, de modale logica (MdL).
{Nb. Dit geldt voor diverse varianten, zie o.a. McNaughton, 1951; Chang, 1958, 1959; Rose/Rosser, 1958. }
PDL
-I
in ieder geval aan Volledigheid voldoet.Eindige bewijzen
Een andere, wezenlijke eigenschap van logische systemen is dat elk bewijs tot een kenbare einduitkomst moet leiden. Met de Volledigheid van het systeem is gegarandeerd dat we niet eindeloos hoeven door te zoeken naar een eindconclusie, maar dat elk bewijs vroeg of laat eindigt - termineert - in een definiete bevestiging. Dit betekent dat elk bewijs tenminste moet bestaan uit een eindige reeks van (verschillende) redeneerstappen.
Compactheid
Uit de bevestiging van Volledigheid volgt het zgn. Compactheid theorema voor de
PDL
-I
: als we een oneindige verzameling van beweringen hebben,
en als vaststaat dat elke eíndige deelverzameling van die verzameling als waar kan worden geďnterpreteerd (d.i.
vervulbaar is), dan is de gehele verzameling eveneens vervulbaar.
Samenvatting:
Bewijs voor de Compactheid van
De redering is vrij simpel. Neem een oneindige verzameling T* van beweringen, waarvan elke eindige deelverzameling van T* vervulbaar is. Stel nu dat T* als geheel niet vervulbaar zou zijn. Dan zou T* inconsistent zijn. Dus dan zou minstens één van de deelverzamelingen Ts[i] van T* - volgens Gödel's Volledigheidsbewijs voor de
- een bewijsreeks voor
contradictie moeten opleveren. Maar elke bewijsreeks die een resultaat oplevert is noodzakelijk eindig.
Dus zal zo'n deelverzameling Ts[i] tegelijk eindig čn inconsistent moeten zijn.
Maar dan is ze niet tegelijk eindig čn vervulbaar. Uitgangspunt was echter, dat elke eindige deelverzameling van T
* vervulbaar is. Dus kan geen van die deelverzamelingen een logische contradictie opleveren.
Dan is het onmogelijk om aan te tonen - in een eindig bewijs - dat de gehele verzameling onvervulbaar is.
En dus volgt dat de gehele verzameling eveneens vervulbaar is - ook al kunnen we daar geen expliciet
en eindig, positief bewijs voor opstellen.
Bewijs voor de Compactheid van PDL
-I
.
PDL
-IDe redering is vrij simpel. Neem een oneindige verzameling T* van beweringen, waarvan elke eindige deelverzameling van T* vervulbaar is. Stel nu dat T* als geheel niet vervulbaar zou zijn. Dan zou T* inconsistent zijn. Dus dan zou minstens één van de deelverzamelingen Ts[i] van T* - volgens Gödel's Volledigheidsbewijs voor de
PDL
-I
- een bewijsreeks voor
contradictie moeten opleveren. Maar elke bewijsreeks die een resultaat oplevert is noodzakelijk eindig.
Dus zal zo'n deelverzameling Ts[i] tegelijk eindig čn inconsistent moeten zijn.
Maar dan is ze niet tegelijk eindig čn vervulbaar. Uitgangspunt was echter, dat elke eindige deelverzameling van T
* vervulbaar is. Dus kan geen van die deelverzamelingen een logische contradictie opleveren.
Dan is het onmogelijk om aan te tonen - in een eindig bewijs - dat de gehele verzameling onvervulbaar is.
En dus volgt dat de gehele verzameling eveneens vervulbaar is - ook al kunnen we daar geen expliciet
en eindig, positief bewijs voor opstellen.2.3. Kwantitatieve grenzen aan de expressieve kracht van de predikatenlogica
De Löwenheim-Skolem theorema's.
In het theorema van Löwenheim-Skolem worden de eigenschappen Soundness, Volledigheid, en Compactheid gecombineerd, met onthutsende resultaten.
Samenvatting:
I. Upward Löwenheim-Skolem theorema.
De eerste consequentie wordt beschreven in de Upward versie van het L-S theorema.
Conclusie: een bewering die vervulbaar is met een eindig model (c.q. domein) is net zo goed vervulbaar met een oneindig model (c.q. domein).
(1) Wil een bewering in
vervulbaar zijn,
dan vereist die zoals gezegd een interpretatie (model) die minstens zoveel onderscheidingen toelaat
als de bewering veronderstelt, en dus een 'minimaal domein'.
(2) Er wordt echter geen bovengrens gesteld aan de vereiste omvang van het domein. Dit betekent dat elk domein met een grotere omvang dan dat minimale domein net zo exact voldoet voor een model dat de bewering vervult.
PDL
-I
vervulbaar zijn,
dan vereist die zoals gezegd een interpretatie (model) die minstens zoveel onderscheidingen toelaat
als de bewering veronderstelt, en dus een 'minimaal domein'.(2) Er wordt echter geen bovengrens gesteld aan de vereiste omvang van het domein. Dit betekent dat elk domein met een grotere omvang dan dat minimale domein net zo exact voldoet voor een model dat de bewering vervult.
Conclusie: een bewering die vervulbaar is met een eindig model (c.q. domein) is net zo goed vervulbaar met een oneindig model (c.q. domein).
II. Downward Löwenheim-Skolem theorema.
Vervolgens komt de 'Skolem-paradox' aan het licht:
Uit deze strijdigheid volgt de Downward versie van het L-S theorema: een zin die vervulbaar is met een over-aftelbaar model (c.q. domein) is net zo goed vervulbaar met een aftelbaar model (c.q. domein).
(1) Het is duidelijk dat een stelling in de
altijd een syntactisch
e structuur zal hebben, en dus gesteld is in een formele reeks tekens,
en daarmee nooit méér onderscheidingen kan weergeven dan aftelbaar oneindig (de omvang van bijvoorbeeld
de verzameling van alle natuurlijke getallen). En dus zal een domein van aftelbaar veel objecten altijd voldoende zijn
om een stelling in de
te vervullen.
(2) Tegelijk worden in de verzamelingenleer echter stellingen geponeerd over bijvoorbeeld de verzameling der reële getallen: die een over-aftelbare kardinaliteit heeft.
PDL
-I
altijd een syntactisch
e structuur zal hebben, en dus gesteld is in een formele reeks tekens,
en daarmee nooit méér onderscheidingen kan weergeven dan aftelbaar oneindig (de omvang van bijvoorbeeld
de verzameling van alle natuurlijke getallen). En dus zal een domein van aftelbaar veel objecten altijd voldoende zijn
om een stelling in de PDL
-I
te vervullen.(2) Tegelijk worden in de verzamelingenleer echter stellingen geponeerd over bijvoorbeeld de verzameling der reële getallen: die een over-aftelbare kardinaliteit heeft.
Uit deze strijdigheid volgt de Downward versie van het L-S theorema: een zin die vervulbaar is met een over-aftelbaar model (c.q. domein) is net zo goed vervulbaar met een aftelbaar model (c.q. domein).
Consequenties van Löwenheim-Skolem theorema
De over-all conclusie uit de L-S theorema's is dat de eerste orde logica niet bruikbaar is om eenduidig onderscheid te maken tussen eindige en oneindige domeinen, en tussen aftelbare en over-aftelbare domeinen. Maar daardoor is de eerste orde logica niet eenduidig te gebruiken voor allerlei formele systemen waarin die onderscheidingen essentieel zijn, zoals de verzamelingen-theorie volgens de axioma's van Zermelo-Fraenkel (ZF), en de rekenkunde voor rationele en voor reële getallen. En dat terwijl het hele nut van formalisering juist ligt in absolute eenduidigheid van uitdrukkingen!
Een bijkomend probleem is dat de predikatenlogica zo lastig te 'verbeteren' of te 'repareren' is. Het blijkt dat alle 'hogere' of meer geavanceerde systemen dan de eerste orde logica - bijvoorbeeld meerwaardige logica, fuzzy logic, quantum logica, enz. - nog veel méér beperkingen kennen op cruciale eigenschappen zoals Soundness, Volledigheid en Compactheid .. zodat verdere sophistication geen soelaas biedt. Volgens sommigen betekent dit dat hiermee een absolute begrenzing aan de mogelijkheden van formele systemen wordt gesteld.
3. De onvolledige bewijskracht van rekenkundige systemen die consistent zijn.
Zoals gezegd is Volledigheid een belangrijke eigenschap van formele systemen.
Een systeem is volledig als geldigheid van een redenering in het systeem impliceert dat die redenering ook formeel afleidbaar is in dat systeem.
Formeel gesteld:
{ ( G) ( G). }
T
G) (T
G). }Voor de simpelste vorm van formele logica, de propositielogica (
PPL
), werd Volledigheid al in 1920 bewezen door Emil L. Post (1897-1954).De Volledigheid van de predikatenlogica werd door Kurt Friedrich Gödel (1906-1978) bewezen met diens Volledigheidstheorema (dissertatie 1929; artikel 1930). Dit resultaat houdt in dat voor elke welgevormde formule in deze taal die logisch geldig is, een formeel bewijs kan worden geleverd. Zodoende geldt, dat als een bewering in de
PDL
-I
logisch geldig is,
dan is deze formeel c.q. mechanisch bewijsbaar. Anders gezegd, alle geldige formules in PDL
-I
kunnen bewezen worden via een formele procedure. Met andere woorden, de verzameling van formules in de
PDL
-I
blijkt recursief opsombaar (recursively enumerable, RE).Met Gödel's Volledigheidstheorema was dus bewezen dat de
PDL
-I
aan Volledigheid voldoet.De volgende vraag die Gödel zich stelde was of Volledigheid ook gold voor de wiskunde - om te beginnen de elementaire rekenkunde voor natuurlijke getallen: first-order theory of natural numbers.
{Nb. Met name de rekenkunde van Sorites (Sorites arithmetic, SA), die gebaseerd is op de predicatenlogica,
PDL
, en de eerste vier postulaten van de rekenkunde volgens Guiseppe Peano (1858-1932; 1891), de PA. Een voorbeeld van zo'n systeem, of calculus, werd beschreven door Bertrand Russell en Alfred N. Whitehead ( Principia Mathematica, 1910-1913 resp. 1962).}Kort hierna, in 1931, presenteerde Gödel zijn Eerste Onvolledigheidstheorema. Hiermee bewees hij dat een eerste orde systeem van de elementaire rekenkunde, ook al is het consistent, geen bewijs kan leveren voor elke zin die in de taal van dat systeem kan worden geformuleerd. Dit geldt zelfs als van zo'n zin vaststaat dat ze waar is.
Samenvatting:
Eerste Onvolledigheidstheorema of First Incompletenesstheorem (Kurt Gödel, 1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme 1).
De elementaire rekenkunde (first-order theory of natural numbers vloeit voort uit het logicistisch onderzoeksprogramma, dat gebaseerd was op de klassieke logica in het Organon van Aristotelis, en was uitgewerkt in de Grundgesetze der Arithmetik van F.L. Gottlob Frege (1893, 1903) en de Principia Mathematica van Bertrand Russell en Alfred North Whitehead, delen I-III (1910, 1912, 1913).
De 'fatale uitzondering' die Gödel gebruikt voor zijn bewijs, de zgn. 'Gödel-zin' (G), is een variant van de bekende 'Kretenzer paradox', of 'paradox' van de leugenaar', en luidt: 'Deze zin is niet bewijs baar in dit systeem'. Het type zin G betreft een globaal, negatief zelf-reflexief meta-oordeel: dat moet haast wel tot problemen leiden. G draait als het ware in zichzelf rond.
Hierdoor is ze al volgens onze logische intuďtie in betekenis duidelijk paradoxaal, daarom inhoudelijk onwaar, en daardoor niet te bevestigen dan wel te bewijzen.
Daarnaast blijkt dat zo'n zin bij een gewone, directe interpretatie of 'lezing' door een formeel systeem in de vorm tot oneindige circulariteit leidt. Dit laatste probleem ligt direct in het recursieve gebruik van de 'bewijs baar'-functie. Gödel erkent zčlf al dat deze functie niet zonder meer recursief kan worden gebruikt. Hij presenteert een lijst van 46 formele notities voor elementen en operaties die hij gebruikt bij zijn bewijsvoering, en plaatst daarbij de opmerking: "Bew(x) [=Beweisbar x] is the only one of the notions 1-46 of which we cannot assert that it is recursive." (Gödel, 1931, pp.162-171).
Kortom, het zou kunnen zijn dat zin G al bij voorbaat niet toelaatbaar is in systeem T. Met andere woorden, bij een voor de hand liggende codering van zin G in de taal van G, is geen afleiding mogelijk die op afzienbare termijn eindigt in een definiete uitkomst.
Op grond van intuďtief oordeel is de waarheidswaarde van zin G dus niet door een formeel systeem T procedureel te bewijzen, of zelfs maar te beslissen - en dat betekent dat zin G inhoudelijk wel degelijk waar is! (Een conclusie die uiteraard géén paradox is met de premisse: het 'waar' zijn van de gehele zin staat in een meta-relatie tot het 'niet-bewijsbaar' zijn dat bínnen de zin wordt genoemd). Vanuit dit oogpunt is de onvolledige bewijskracht van formele systemen een tamelijk triviaal gegeven. Kurt Gödel was trouwens de eerste om dit toe te geven.
"How indeed could one think of expressing metamathematics [i.e. rules about mathematics] in the mathematical systems themselves, if the latter are to be considered to consist of meaningless symbols which acquire some substitute of meaning only through [that same] metamathematics?." (Kurt Gödel, in: Feferman, S., 1984, 'Kurt Gödel: Conviction and Caution').
Het is Gödel echter gelukt om, met behulp van een speciale getalscodering, de zgn. 'Gödelnummering', het probleem van de oneindige recursie te omzeilen. Uitgangspunt waren de axioma's van de rekenkunde voor natuurlijke getallen, die gedefinieerd waren in stellingen van de
.
Daarbij was duidelijk dat elke stelling in de
bestaat uit een tekenreeks
met een lengte die niet groter is dan de omvang van de verzameling van natuurlijke getallen (die aftelbaar oneindig is).
Als gezegd had Gödel al aangetoond dat de verzameling van stellingen in
recursief opsombaar was. Daardoor konden ze worden gecodeerd in termen van berekenbare functies (
computable functions). De formele taal die Gödel hiervoor ontwierp was het systeem van de primitieve recursieve
functies.
Vervolgens toonde Gödel aan dat alle stellingen van de
één-op-één kunnen worden gepaard aan een corresponderend getal. Daardoor zijn al die stellingen
eenduidig te coderen met een unieke numerieke code, een 'Gödelnummer'.
Dit betekende dat ook alle stellingen in de rekenkunde met Gödelnummers te coderen zijn, inclusief axioma's,
en inclusief rekenkundige problemen. Dankzij dit formalisme wist Gödel formeel aan tonen,
in de taal van de rekenkunde, dat de zin G, gesteld in-die-codering, onder elke waarheidswaarde,
en bij elke formele afleiding binnen een consistent rekenkundig systeem T, zou leiden tot contradictie
- en dus niet beoordeelbaar is.
Dit resultaat betekent allereerst dat er in de taal van de rekenkunde kennelijk een formele 'route' bestaat om te bewijzen dat het consistente systeem niet elke ware bewering kan bewijzen die zijn eigen bewijs mogelijkheden betreft. Inhoudelijk lijkt deze uitkomst niet erg verwonderlijk, maar de consequenties zijn verstrekkend: in elk formeel systeem dat consistent is zijn er welgevormde beweringen mogelijk die waar zijn en tegelijk in datzelfde systeem niet beoordeelbaar zijn. En dus is zo'n systeem in logische zin per definitie onvolledig.
Andere consequenties van Gödel's bewijs waren, naar de mening van Gödel, dat de menselijke rede creatief is (in plaats van louter lineair-mechanisch), en dat 'synthetische a priori waarheden' mogelijk zijn.
Gödel's bewijs voor de Onvolledigheid van de elementaire rekenkunde.
Eerste Onvolledigheidstheorema of First Incompletenesstheorem (Kurt Gödel, 1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme 1).
De elementaire rekenkunde (first-order theory of natural numbers vloeit voort uit het logicistisch onderzoeksprogramma, dat gebaseerd was op de klassieke logica in het Organon van Aristotelis, en was uitgewerkt in de Grundgesetze der Arithmetik van F.L. Gottlob Frege (1893, 1903) en de Principia Mathematica van Bertrand Russell en Alfred North Whitehead, delen I-III (1910, 1912, 1913).
De 'fatale uitzondering' die Gödel gebruikt voor zijn bewijs, de zgn. 'Gödel-zin' (G), is een variant van de bekende 'Kretenzer paradox', of 'paradox' van de leugenaar', en luidt: 'Deze zin is niet bewijs baar in dit systeem'. Het type zin G betreft een globaal, negatief zelf-reflexief meta-oordeel: dat moet haast wel tot problemen leiden. G draait als het ware in zichzelf rond.
Hierdoor is ze al volgens onze logische intuďtie in betekenis duidelijk paradoxaal, daarom inhoudelijk onwaar, en daardoor niet te bevestigen dan wel te bewijzen.
Daarnaast blijkt dat zo'n zin bij een gewone, directe interpretatie of 'lezing' door een formeel systeem in de vorm tot oneindige circulariteit leidt. Dit laatste probleem ligt direct in het recursieve gebruik van de 'bewijs baar'-functie. Gödel erkent zčlf al dat deze functie niet zonder meer recursief kan worden gebruikt. Hij presenteert een lijst van 46 formele notities voor elementen en operaties die hij gebruikt bij zijn bewijsvoering, en plaatst daarbij de opmerking: "Bew(x) [=Beweisbar x] is the only one of the notions 1-46 of which we cannot assert that it is recursive." (Gödel, 1931, pp.162-171).
Kortom, het zou kunnen zijn dat zin G al bij voorbaat niet toelaatbaar is in systeem T. Met andere woorden, bij een voor de hand liggende codering van zin G in de taal van G, is geen afleiding mogelijk die op afzienbare termijn eindigt in een definiete uitkomst.
Op grond van intuďtief oordeel is de waarheidswaarde van zin G dus niet door een formeel systeem T procedureel te bewijzen, of zelfs maar te beslissen - en dat betekent dat zin G inhoudelijk wel degelijk waar is! (Een conclusie die uiteraard géén paradox is met de premisse: het 'waar' zijn van de gehele zin staat in een meta-relatie tot het 'niet-bewijsbaar' zijn dat bínnen de zin wordt genoemd). Vanuit dit oogpunt is de onvolledige bewijskracht van formele systemen een tamelijk triviaal gegeven. Kurt Gödel was trouwens de eerste om dit toe te geven.
"How indeed could one think of expressing metamathematics [i.e. rules about mathematics] in the mathematical systems themselves, if the latter are to be considered to consist of meaningless symbols which acquire some substitute of meaning only through [that same] metamathematics?." (Kurt Gödel, in: Feferman, S., 1984, 'Kurt Gödel: Conviction and Caution').
Het is Gödel echter gelukt om, met behulp van een speciale getalscodering, de zgn. 'Gödelnummering', het probleem van de oneindige recursie te omzeilen. Uitgangspunt waren de axioma's van de rekenkunde voor natuurlijke getallen, die gedefinieerd waren in stellingen van de
PDL
-I
.
Daarbij was duidelijk dat elke stelling in de PDL
-I
bestaat uit een tekenreeks
met een lengte die niet groter is dan de omvang van de verzameling van natuurlijke getallen (die aftelbaar oneindig is).
Als gezegd had Gödel al aangetoond dat de verzameling van stellingen in
PDL
-I
recursief opsombaar was. Daardoor konden ze worden gecodeerd in termen van berekenbare functies (
computable functions). De formele taal die Gödel hiervoor ontwierp was het systeem van de primitieve recursieve
functies.Vervolgens toonde Gödel aan dat alle stellingen van de
PDL
-I
één-op-één kunnen worden gepaard aan een corresponderend getal. Daardoor zijn al die stellingen
eenduidig te coderen met een unieke numerieke code, een 'Gödelnummer'.
Dit betekende dat ook alle stellingen in de rekenkunde met Gödelnummers te coderen zijn, inclusief axioma's,
en inclusief rekenkundige problemen. Dankzij dit formalisme wist Gödel formeel aan tonen,
in de taal van de rekenkunde, dat de zin G, gesteld in-die-codering, onder elke waarheidswaarde,
en bij elke formele afleiding binnen een consistent rekenkundig systeem T, zou leiden tot contradictie
- en dus niet beoordeelbaar is.Dit resultaat betekent allereerst dat er in de taal van de rekenkunde kennelijk een formele 'route' bestaat om te bewijzen dat het consistente systeem niet elke ware bewering kan bewijzen die zijn eigen bewijs mogelijkheden betreft. Inhoudelijk lijkt deze uitkomst niet erg verwonderlijk, maar de consequenties zijn verstrekkend: in elk formeel systeem dat consistent is zijn er welgevormde beweringen mogelijk die waar zijn en tegelijk in datzelfde systeem niet beoordeelbaar zijn. En dus is zo'n systeem in logische zin per definitie onvolledig.
Andere consequenties van Gödel's bewijs waren, naar de mening van Gödel, dat de menselijke rede creatief is (in plaats van louter lineair-mechanisch), en dat 'synthetische a priori waarheden' mogelijk zijn.
{Nb. Zie verder: Het Onvolledigheidsbewijs van Gödel.}
4. De onbeslisbaarheid van de predikatenlogica.
4.1. Hilbert's Entscheidungsproblem
Al in 1900 formuleerde David Hilbert een cruciale vraag over de reikwijdte van de bewijskracht van formele systemen: het 'beslisbaarheidsprobleem' (Entscheidungsproblem, of decision problem). Bestaat er een algemene formele procedure waarmee we voor elk wiskundig probleem kunnen bepalen of het oplosbaar is?
Begin van de twintigste eeuw werd nog aangenomen dat de wiskunde sluitend was te axiomatiseren in een vorm van logica, met name de predikatenlogica. Als deze aanname juist was, en de beslisbaarheid van de predikatenlogika kon worden bewezen, dan zou daarmee de gehele wiskunde beslisbaar blijken. Daarom vertaalde Hilbert het probleem van de beslisbaarheid van de wiskunde in dat van de vervulbaarheid van de predikatenlogika (
PDL
). De vraag is dan in hoeverre voor elke mogelijke formule in dePDL
kan worden bepaald of die onder een bepaalde interpretatie waar kan zijn, of niet.Het probleem van vervulbaarheid is vervolgens indirect te vertalen in dat van logische geldigheid oftewel validiteit . Als een bewering algemeen geldig is (valide) dan wordt ze door elke interpretatie vervuld; dus heeft ze minstens één interpretatie waaronder ze vervuld wordt (een model), en daarmee is ze vervulbaar. Oftewel, een geldige bewering is in ieder geval vervulbaar.
Formeel gesteld:
{ (( G) (¬
¬G)). }
G) (¬
¬G)). }Is een bewering echter niet vervulbaar, dan is het tegendeel ervan geldig.
Formeel gesteld:
(( ¬G) 
( (¬
G)). }
¬G) ( (¬
G)). }Voor het vervulbaarheidsprobleem van de
PDL
zocht Hilbert naar een meta-procedure, wat hij noemde een ' effectieve methode', om voor elke stelling in de predikatenlogika in een eindig aantal stappen te kunnen bepalen of die onder een bepaalde interpretatie waar kan zijn. " The Entscheidungsproblem is solved when we know a procedure that allows for any given logical expression to decide by finitely many operations its validity or satisfiability [..] The entscheidungsproblem must be considered the main problem of mathematical logic." (Hilbert & Ackerman, 1928)Al in 1900 formuleerde David Hilbert (Hilbert & Ackerman, 1928)
Enkele jaren later werd het Entscheidungsproblem door Alonzo Church als volgt geformuleerd: " By the Entscheidungsproblem of a system of symbolic logic is here understood the problem to find an effective method by which, given any expression Q in the notation of the system, it can be determined whether or not Q is provable in the system." (A. Church, 1936[b], p.41).
Met Gödel's Volledigheidstheorema van 1930 was nog geen oplossing gevonden voor Hilbert's Entscheidungsproblem. Volledigheid, als logisch meta-criterium, gaat uit van de verzameling van alle geldige beweringen in een logisch systeem, en concludeert dat voor al die beweringen binnen het systeem een formeel bewijs te vinden is. De verzameling van alle geldige beweringen is in dat systeem dan recursief opsombaar.
Probleem is dan nog steeds het traceren van de ongeldige formules in het betreffende logische systeem. Voor een ongeldige formule is het dan immers nog steeds onduidelijk hoe die formeel is op te sporen. En als we van te voren niet weten of een formule valide is, dan kunnen we ook geen procedure selecteren om erop los te laten .. Bewezen zou nog moeten worden, in termen van Gödel's calculus, dat de gehele verzameling van formules in dat systeem ook recursief was.
Gödel's Onvolledigheidsbewijs van 1931 leverde voor deze vraag evenmin uitsluitsel. Dit had enkel betrekking op de bewijskracht van consistente systemen van de rekenkunde van formules waarvan we weten dat ze waar zijn. De conclusie luidt dat hier niet altijd een formeel bewijs voor te vinden is. Dat is voldoende voor het bewijs van Onvolledigheid.
4.2. Beslisbaarheid
Nog onopgelost was het tevoren kunnen bepalen voor ŕlle formules van het systeem ňf ze waar of onwaar zijn. Was hier ook nog een formele procedure voor te vinden? In dat geval zou voor elke formule in
PDL
-I
met zekerheid kunnen worden bepaald of deze waar, onwaar of onbeslisbaar is.Een veel sterkere eigenschap dan Volledigheid is nu beslisbaarheid: elke bewering die in het systeem kan worden geformuleerd is hetzij bewijsbaar, hetzij weerlegbaar door middel van het systeem.
Formeel gesteld ('
#
' betekent 'OF .. OF ..):
{ (( G) G)). }
T
G) #
¬(T
G)). }De verzameling van
PDL
-I
formules zou dan recursief zijn (recursive, R),
en daardoor volledig determinaat.
Samenvatting:
De oplossing van het probeem is altijd formeel afleidbaar met een eindig bewijs.
Recursief: Onder alle invoer 'halting' (terminerend in eindige tijd).
De oplossing van het probeem is niet altijd formeel afleidbaar met een eindig bewijs.
Niet-recursief: Onder sommige invoer (mogelijk) oneindig 'looping'.
Beslisbaarheid en Recursiviteit.
I. Probleem is beslisbaar, Decidable.
De oplossing van het probeem is altijd formeel afleidbaar met een eindig bewijs.
Recursief: Onder alle invoer 'halting' (terminerend in eindige tijd).
I.1. Recursief opsombaar:
Als het probleem een uitkomst heeft, is dat altijd aantoonbaar.I.2. Co-recursief opsombaar:
Als het probleem geen uitkomst heeft, is dat altijd aantoonbaar.II. Probleem is niet beslisbaar, Undecidable.
De oplossing van het probeem is niet altijd formeel afleidbaar met een eindig bewijs.
Niet-recursief: Onder sommige invoer (mogelijk) oneindig 'looping'.
II.1. Niet recursief opsombaar:
Als het probleem een uitkomst heeft, is dat niet altijd aantoonbaar.II.2. Niet co-recursief opsombaar:
Als het probleem geen uitkomst heeft, is dat niet altijd aantoonbaar.Door Alonzo Church (1903-1995) werd vrijwel gelijktijdig met Alan Mathison Turing (1912-1954) in mei 1936 een beslissend antwoord gegeven op het zgn. Entscheidungsproblem dat was geformuleerd door David Hilbert (1900). Church leverde het formele bewijs dat het validiteitsprobleem van de eerste-orde predikatenlogica (
PDL
-I
) niet volledig beslisbaar is.4.3. Berekenbaarheid vereist een algoritme.
Church en Turing hebben laten zien dat elk wiskundig probleem, wil het oplosbaar zijn, te beschrijven moet zijn met een volkomen mechanische procedure, of een algoritme.
We hebben het dan over een verzameling van berekenbare bewerkingen in de wiskunde.
Een algoritme is een rekenvoorschrift waarbij bewerkingen stap voor stap worden uitgevoerd (sequentieel), in een eindige reeks, waarbij voorwaarden kunnen worden gesteld (nesting) en 'herhaalrecepten' toegepast ( recursie of looping). Kortom, eigenschappen die we tegenwoordig kennen van een 'computerprogramma', dat in algemene, abstracte vorm al langere tijd in logica en wiskunde bekend is. Het concept werd ontworpen door Charles Babbage (1792-1871) in samenwerking met Lady Ada Augusta, gravin van Lovelace (1815-1852) en door hen ' analytical engine' gedoopt. Later werd het bekend als 'abstract automaton', 'discrete state machine', 'Logical Computing Machine' (
LCM
) en 'Turing device' c.q. 'Turing Machine ' (TM
).
De volgende begrippen blijken overeen te komen:
-
Algoritme.
-
'Analytical engine' bij Charles Babbage (1792-1871) en Lady Ada Augusta, gravin van Lovelace (1815-1852).
-
'Effectieve methode' bij David Hilbert (1900) en Hilbert & Ackerman (1928).
-
Recursive algorithm (recursive function), Kurt Gödel (1934) en Jacques Herbrand (1932).
-
Lambda-definable function in de lambda calculus, bij Alonzo Church (1932, 1936a, 1941)
en Stephen Kleene (1935).
-
Turing machine computable function, c.q. 'Turing device', c.q. 'Turing Machine' (
TM
), bij Alan Turing (1936-1937).
-
Verder: 'Abstract automaton', 'discrete state machine', 'Logical Computing Machine' (
LCM
).
Met een algoritme c.q.
TM
is een strikt eenduidige en volledig gedetermineerde procedure mogelijk: met kennis van de uitgangsgegevens is het verloop tevoren perfect voorspelbaar. Tegelijk is het mogelijk dat bewerkingen bij recursie 'oneindig' herhaald worden (de 'eeuwige loop'), zodat er voor de uitkomsten twee mogelijkheden zijn: hetzij ze worden sluitend vastgesteld (ze zijn definiet), hetzij ze blijven 'eeuwig' onbekend.Zo'n algoritme is vervolgens uitvoerbaar met een seriële digitale computer. Deze stelling is bekend geworden als de Church-Turing these: Elke uitvoerbare berekening kan worden uitgevoerd door een algoritme werkzaam op een computer, zolang voldoende tijd en opslagruimte beschikbaar zijn.
Church publiceerde zijn bewijs het eerst op 19 april 1935 in een paper onder de titel ' An unsolvable problem of elementary number theory'. Hierin definieert Church allereerst de uitdrukking ' effectively calculable' als de aanduiding van een methode die effectief genoeg is om de waarden van een procedure of functie te berekenen. Een effectieve functie, zeg F, zal een algoritme hebben, die na een eindige reeks stappen tot een uitkomst zal leiden. ".. the fact that the algorithm has terminated becomes effectively known and the value of F(n) is effectively calculable" (Church, 1936a; reprint in: M. Davis, ed., 1965, p.100).
Vervolgens definieert Church het begrip 'effectieve berekenbaarheid' ('effective calculability') allereerst in termen van recursieve functies die door Gödel en Herbrand (zie Herbrand 1932, Gödel 1934) waren uitgewerkt.
Tevens presenteert Church een nieuwe formele taal, de lambda calculus, waarmee alle natuurlijke getallen kunnen worden weergegeven als abstracte functies. Met dit apparaat kon hij aantonen dat elke 'effectief berekenbare' functie samenviel met een 'lambda-definable' functie (zie: Church, 1932, 1936a, 1941; Kleene, 1935).
"[We ..] define the notion [..] of an effectively calculable function of positive integers by identifying it with the notion of a recursive function of positive integers (or of a lambda-definable function of positive integers)". (Church, 1936a, p.356).
4.4. PDL
-I
blijkt niet beslisbaar.
PDL
-IMet behulp van deze systematiek bewees Church dat niet alle formules in de
PDL
-I
kunnen worden beslist door functies in termen van de lambda-calculus;
en dus door geen enkele andere effectieve procedure. Dat wil zeggen dat er geen algoritmische procedure
c.q. rekenvoorschrift bestaat waarmee voor elke welgevormde formule in PDL
-I
kan worden beslist of deze logisch geldig c.q. valide is.
{Nb. Overigens blijken bepaalde klassen van formules in de eerste-orde predikatenlogica wel degelijk beslisbaar,
zodat de
als geheel kan gelden als 'semi-beslisbaar').}
PDL
-I
als geheel kan gelden als 'semi-beslisbaar').}Bovendien bewees Church dat er geen algemene algoritmische procedure mogelijk is voor het bepalen van de berekenbaarheid (computability) van problemen in de theorie van de natuurlijke getallen. Dit geniale bewijs werd echter al snel overtroffen door het briljante werk van Alan Turing, dat we hieronder zullen bespreken.
5. De beperkte mechaniceerbaarheid van wiskundige operaties.
Vrijwel gelijktijdig met Church heeft Alan Mathison Turing (1912-1954) in mei 1936 een beslissend antwoord gegeven op het zgn. Entscheidungsproblem dat was geformuleerd door David Hilbert (1900). Hij leverde het definitieve bewijs dat de door Hilbert beoogde 'effectieve' procedure niet bestaat. En dus dat er geen oplossing is voor het Beslisbaarheidsprobleem.
In een
TM
kan een enorm scala aan gegevens en probleemstellingen worden weergegeven door het principe van getalscodering: alle elementaire onderscheidingen van invoer en uitvoer kunnen in een één-op-één correspondentie met de reeks van natuurlijke getallen worden gebracht, evenals de tussenliggende bewerkingen. Die numerieke codes kunnen vervolgens - meer efficiënt - in binaire waarden worden vertaald, oftewel de 'ja'/'nee' beslissingen die we sinds Aristoteles kennen van het meest elementaire logische systeem, de propositielogica (PPL
). Hierdoor is alle informatie in eenTM
lineair, sequentieel en dichotoom.Gelet op de sterke eigenschappen van Turing Machines is het een interessante vraag of člke cijferreeks in principe door één of andere
TM
te berekenen zal zijn op een manier die een andere cijferreeks als definiete uitkomst oplevert. Dit is de vraag naar de berekenbaarheid (computability) van verschillende soorten wiskundige problemen.Hilbert's Entscheidungsproblem kan nu in termen van Turing Machines worden geherformuleerd: kan er een Turing Machine worden ontworpen die voor člke mogelijke probleemstelling kan bepalen of er een oplossing is? In dat geval zou het systeem voor elke eindige invoer gegarandeerd een eindige, definiete uitkomst moeten leveren.
De vraag is dus of er een effectieve, universele beslissingsprocedure mogelijk is, een '
UTM
' of 'meta-TM
', die voor elkeTM
kan bepalen of deze voor elke tekenreeks voorspelbaar binnen een eindig aantal stappen - 'in eindige tijd' - tot een specifieke, definiete eindtoestand komt, anders gezegd, uiteindelijk stopt (termineert). Dit is het zgn. Stop Probleem (Halting Problem,HP
).Hierop is het antwoord volgens het Theorema van Turing onverbiddelijk: voor het Stop Probleem is geen oplossing.
Turing's methode om het negatieve bewijs te leveren was veel krachtiger dan die van Church, wat door de laatste ruiterlijk werd erkend in zijn bespreking van Turing's resultaten: "[..] computability by a Turing machine [..] has the advantage of making the identification with effectiveness in the ordinary (not explicitly defined) sense evident immediately" (Church, 1937a, p.43).
Bovendien had Church alleen gekeken naar functies van natuurlijke getallen (positive integers), terwijl Turing's bewijs betrekking had op, in zijn eigen woorden "[all] computable functions of an integral variable or a real or computable variable, computable predicates, and so forth" (Turing, 1936, p.230).
Samenvatting:
We kunnen ons een matrix voorstellen van alle mogelijke algoritmische patronen bij alle mogelijke invoerpatronen. Als een universeel beslissingsprogramma kan bestaan dat in alle gevallen effectief is, dan zal dit voor elke combinatie c.q. cel in deze matrix een welbepaalde, definiete uitkomst leveren (nl. wel of niet beslisbaar), met andere woorden, dan is elke cel in de matrix beslisbaar en dus is de gehele matrix beslisbaar. Dan is ook de 'diagonaal' in de matrix volledig vervuld, nl. door alle uitkomsten van alle algoritmes toegepast op zichzelf.
Dus de genoemde matrix kan nooit volledig beslisbaar zijn, dus kan er geen procedure zijn die over elk algoritme onder elke mogelijke invoer beslist, en dus kan geen universele beslisprocedure bestaan die in alle gevallen effectief is.
De conclusie van Turing's bewijs is dat de mogelijkheid van een effectieve universele beslissingsprocedure, of meta-procedure (
Turing's bewijs voor de Onbeslisbaarheid van de elementaire rekenkunde.
We kunnen ons een matrix voorstellen van alle mogelijke algoritmische patronen bij alle mogelijke invoerpatronen. Als een universeel beslissingsprogramma kan bestaan dat in alle gevallen effectief is, dan zal dit voor elke combinatie c.q. cel in deze matrix een welbepaalde, definiete uitkomst leveren (nl. wel of niet beslisbaar), met andere woorden, dan is elke cel in de matrix beslisbaar en dus is de gehele matrix beslisbaar. Dan is ook de 'diagonaal' in de matrix volledig vervuld, nl. door alle uitkomsten van alle algoritmes toegepast op zichzelf.
(I) Eerste bewijsroute: Als de complete matrix met uitkomsten bestaat, en we een simpele rekenkundige bewerking (
transponatie) toepassen op alle uitkomsten in de matrix, dan blijkt dat de universele beslissingsprocedure
waar deze wordt toegepast op de diagonaal in de matrix en wordt uitgebreid met zo'n transponatie,
en vervolgens wordt toegepast op zichzelf, tot contradicties leidt: ze kan niet stoppen want dan gaat ze oneindig door,
en ze kan niet oneindig doorgaan want dan stopt ze.
(II) Langs een andere route: Als de complete matrix met uitkomsten bestaat, dan bestaat de diagonaal uit twee verzamelingen: die van alle algoritmes die een uitkomst leveren als ze op zichzelf worden toegepast, en de complement-verzameling daarvan. Maar dan moet het beslisprogramma ook voor elk element van de complement-verzameling (die voor geen van haar leden uitkomsten kent) tot een uitkomst leiden, hetgeen een contradictie is.
(II) Langs een andere route: Als de complete matrix met uitkomsten bestaat, dan bestaat de diagonaal uit twee verzamelingen: die van alle algoritmes die een uitkomst leveren als ze op zichzelf worden toegepast, en de complement-verzameling daarvan. Maar dan moet het beslisprogramma ook voor elk element van de complement-verzameling (die voor geen van haar leden uitkomsten kent) tot een uitkomst leiden, hetgeen een contradictie is.
Dus de genoemde matrix kan nooit volledig beslisbaar zijn, dus kan er geen procedure zijn die over elk algoritme onder elke mogelijke invoer beslist, en dus kan geen universele beslisprocedure bestaan die in alle gevallen effectief is.
De conclusie van Turing's bewijs is dat de mogelijkheid van een effectieve universele beslissingsprocedure, of meta-procedure (
UTM
), voor de meest elementaire rekenkunde is uitgesloten.Dus linksaf of rechtsaf blijkt het wiskundige systeem niet volledig beslisbaar.
Appendix: Schema's Logische niveau's en criteria.