Methode Meta-Logica:
Beslisbaarheid
Logisch meta-niveau II
Bewijscapaciteit van logische systemen.
Beslisbaarheid van systemen, verzamelingen en redeneringen.
Beslisbaarheid volgens Church-Turing
1.
Beslisbaarheid van logische systemen
Beslisbaarheid van een systeem in de formele logica is de mogelijkheid om tevoren voor �lle welgevormde formules in de taal van het systeem met zekerheid te kunnen bepalen �f ze vervulbaar, waar, geldig zijn - of niet. Willen we daarbij maximale betrouwbaarheid dan kan dit alleen met een formeel bewijs gebeuren: dat wil zeggen via een expliciet, eenduidig en eindig traject. Het beslisproces levert dan in eindige tijd een eenduidige einduitkomst, dus termineert.
De gehele verzameling van wff formules in het systeem zou dan recursief zijn (recursive, RC), en daardoor volledig determinaat.
T!
is beslisbaar:als er een correcte formele procedure bestaat die voor elke welgevormde formule F in de taal van
T!
op afzienbare termijn precies ��n (accuraat) antwoord geeft uit drie specifieke antwoordmogelijkheden:(1) 'F is waar';
(2) 'F is contingent';
(3) 'F is onwaar'
Beslisbaarheid van een verzameling formules:
(2) 'F is contingent';
(3) 'F is onwaar'
{ (
j1 ( (G[j1]
WFF*(
(
(AXM*(
G[j1])
(AXM*( �G[j1]
) ) ) )j1 
DCDBL(
j1 ( (G[j1]
WFF*(T!
)) (
(AXM*(T!
) G[j1])
(AXM*(T!
) �G[j1]
) ) ) )j1 DCDBL(T!
) }.Beslisbaarheid van een verzameling formules:
{ (k1 ( (K[j1]
K*) ( (K*
K[k1]) (K*
�K[k1]) ) ) )k1
DCDBL(K*) }.
k1 ( (K[j1]
K*) ( (K*
K[k1]) (K*
�K[k1]) ) ) )k1
DCDBL(K*) }.2.
De onbeslisbaarheid van de predikatenlogica.
2.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?"
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 vervulbaar of geldig is. "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).2.2.
Het algemene beslisbaarheidsprobleem volgens Church.
Enkele jaren later werd het Entscheidungsproblem door Alonzo Church (1903-1995) 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).
Het algemene beslisbaarheidsprobleem heeft een heel praktisch belang: als het voor een bepaald systeem, of klasse of verzameling van formules, niet tevoren kan worden aangetoond dat het volledig beslisbaar is, dan kunnen we van een willekeurige formule in dat systeem niet van te voren weten (voorspellen) of het haalbaar is (feasible ) om haar (a) te interpreteren, (b) te valueren c.q. te vervullen, (c) haar waarheidswaarde te evalueren, of (d) haar validiteit te toetsen of te bewijzen. We kunnen zelfs geen geschikte procedure selecteren om dit uit te vinden.
Door Alonzo Church werd het formele bewijs geleverd dat het validiteitsprobleem van de eerste-orde predikatenlogica (PDL-I) niet volledig beslisbaar is. 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.Church publiceerde zijn bewijs het eerst op 19 april 1935 in een paper onder de titel ' An unsolvable problem of elementary number theory'.
{Overigens blijken bepaalde klassen van formules in de eerste-orde predikatenlogica
wel degelijk beslisbaar, zodat de
PDL
-I als geheel kan gelden als 'semi-beslisbaar'. Dit betekent dat het in ieder geval voor formules die aan specifieke formele kenmerken voldoen theoretisch haalbaar is om ze te gaan oplossen.}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.
Voorbeeld van onbeslisbare stelling in PDL
.
Bewijs via Resolutie.
{Zie voor uitleg: Inleiding Resolutielogica
.}
Gegeven formule R:
R = { (x1 A(x,x)) 
(
y1 z1 A(y,z)) }.
Formule R is niet resolutie-beslisbaar geldig.
{ �Rsl
(PDL-I R) };
�RE(G)
{ m1 k1 ( (Ks
*[k1] K*)
�(
�Rsl h1
j1 (
F[j1]) j1,h1 ) )k1,m1 }.
�CO-RE(K*)
R = { (
x1 A(x,x)) (
y1 z1 A(y,z)) }.Resolutiebewijs.
•
S ≡ �R;
S = { �( (x1 A(x,x))
(y1
z1 A(y,z)) ) }.
Formule S is niet beslisbaar onvervulbaar.
Aanname van het tegendeel S.
S ≡ �R;S = { �( (x1 A(x,x))
(y1
z1 A(y,z)) ) }.Resolutie-deductiereeks.
•
S(Sk,r,i,Cl,n) = { A(x,x), �A(y,f(y)) ·[y:=x] };
= { L1:A(x,x), L2:A(x,f(x)) };
•
L1[x:=f(y)];
L1:A(f(y),f(y));
L2[x:=f(y)]; L2:A(f(y)),f(f(y))); .. etc..
Oneindige circulariteit.
Normaal vorm conversies.
•
· Conjunctief normaal vorm:S = { �( (�
x1 A(x,x)) (y1
z1 A(y,z)) ) }.
· Negatief normaal vorm:S = { (
x1 A(x,x)) �(y1
z1 A(y,z)) };
· Kwantor prefix vorm:S = { (
x1 A(x,x)), (y1
z1 �A(y,z)) };
• Semantische parafrase-conversies.
· Conjunctief normaal vorm:
S = { �( (�
x1 A(x,x)) (y1
z1 A(y,z)) ) }.· Negatief normaal vorm:
S = { (
x1 A(x,x)) �(y1
z1 A(y,z)) };· Kwantor prefix vorm:
S = { (
x1 A(x,x)), (y1
z1 �A(y,z)) };Syntactische Comprimaties.
· Skolem Normaal Vorm: S(Sk
+1) = { (x1 A(x,x)), (
y1 �A(y,f(y))) };
· Recursieve functie Vorm:S(Sk,r) = { (x1
· Universeel instantiatie Vorm:S(Sk,r,i) =
{ ( A(x,x)), ( �A(y,f(y))) };
· Clausule Normaal Vorm:S(Sk,r,i,Cl) =
{ 1:A(x,x), 2:�A(y,f(y)) }.
• S(Sk
+1) = { (x1 A(x,x)), (
y1 �A(y,f(y))) };· Recursieve functie Vorm:
S(Sk,r) = { (x1
|
A(x,x)), (y1|
�A(y,f(y))) };· Universeel instantiatie Vorm:
S(Sk,r,i) =
{ ( A(x,x)), ( �A(y,f(y))) };· Clausule Normaal Vorm:
S(Sk,r,i,Cl) =
{ 1:A(x,x), 2:�A(y,f(y)) }.Variabelen-herbenoeming(en), Reductie(s).
S(Sk,r,i,Cl,n) = { A(x,x), �A(y,f(y)) ·[y:=x] };= { L1:A(x,x), L2:A(x,f(x)) };
•
Unificatie(s).
L1[x:=f(y)];
L1:A(f(y),f(y)); L2[x:=f(y)]; L2:A(f(y)),f(f(y))); .. etc..Oneindige circulariteit.Formule S is niet beslisbaar onvervulbaar.Formule R is niet resolutie-beslisbaar geldig.{ �Rsl
(PDL-I R) };�RE(G){ m1 k1 ( (Ks
*[k1] K*)�(TM
[m1](K*)�
Rsl h1
j1 (TM
[h1](Ks*[k1])F[j1]) j1,h1 ) )k1,m1 }.�CO-RE(K*)
TM
3.
De onbeslisbaarheid van de elementaire rekenkunde.
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.
Stelling van Church-Turing.
Turing heeft allereerst, tegelijk met Alonzo Church, laten zien dat elk wiskundig probleem, wil het oplosbaar zijn, te beschrijven moet zijn met een mechanische procedure, of een algoritme.
Vervolgens heeft Turing laten zien dat de logische mogelijkheid bestaat van een algoritme dat niet afhankelijk is van externe, kwantitatieve of fysieke beperkingen, doordat het de beschikking heeft over een onbeperkte externe geheugencapaciteit: een Turing machine (
TM
). De capaciteit van eenTM
wordt dan ook niet beperkt door het niveau van (kwantitatieve) complexiteit van de wiskundige problemen die het bewerkt. Maar zelfs algoritmen met de capaciteit van eenTM
kunnen niet een oplossing opleveren voor elk wiskundig probleem.(a)
Doordat de combinatiemogelijkheden van syntactische patronen in principe onbeperkt zijn, kunnen die patronen sterk vari�ren in complexiteit. De grondslag van die complexiteit bestaat in het aantal dimensies dat het patroon kent, bijvoorbeeld:
(b)
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' (
(c)
Een willekeurige Turing Machine (
(d)
Zo'n algoritme, of Turing Machine, 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.
{ a ({a}
( i1 ( ({i}
I*)
( comptable
Turing Machine comptable
(e)
De volgende eigenschappen gelden enkel voor Turing machines
(f)
We hebben het dan over de verzameling van berekenbare bewerkingen in de wiskunde. Deze blijkt overeen te komen met de volgende begrippen:
Niveau's van complexiteit van informatie.
Doordat de combinatiemogelijkheden van syntactische patronen in principe onbeperkt zijn, kunnen die patronen sterk vari�ren in complexiteit. De grondslag van die complexiteit bestaat in het aantal dimensies dat het patroon kent, bijvoorbeeld:
° Een lineair verloop (o.a. sequentie, partitionering: A*x +b).
° Een polynomiaal verloop, of netwerk-structuur, die parallel c.q. simultaan kan zijn (kwadratisch: x**2 ), ruimtelijk (kubisch: x**3), of van hogere orde (meerdimensionaal: x**n).
° Of nog complexer: exponentieel verloop (bijvoorbeeld n**x).
° Of zelfs hyper-exponentieel verloop (bijvoorbeeld n**m**x).
° En zo verder, tot aan niet-algoritmisch onoplosbaar en zelfs categorisch onoplosbaar.
° Een polynomiaal verloop, of netwerk-structuur, die parallel c.q. simultaan kan zijn (kwadratisch: x**2 ), ruimtelijk (kubisch: x**3), of van hogere orde (meerdimensionaal: x**n).
° Of nog complexer: exponentieel verloop (bijvoorbeeld n**x).
° Of zelfs hyper-exponentieel verloop (bijvoorbeeld n**m**x).
° En zo verder, tot aan niet-algoritmisch onoplosbaar en zelfs categorisch onoplosbaar.
(b)
Algoritme.
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
).(c)
Kenmerken van een algoritme.
Een willekeurige Turing Machine (
TM
), zegTM
[a], heeft tenminste de volgende standaard capaciteiten:(1) Elke
{ a ({a}
( i1 ( ({i}
I*)
(2) Elke
{ a ({a}
( i1 ( ({i}
I*) (SIZE(I*) ≤ 
0) ) )i1 a}.
(3) Elke
{ a ({a}
( i1 ( ({i}
I*) ( (SIZE(I[i1]) <
0) ) ) )i1 a}.
(4) Elke
{ a ({a}
( r ( (
R![a,r]) (a=r)
(SIZE(R![a,r]) < 0) ) )
r a}.
(5) Elke
{ a ({a}
( i1 ( ( ({i}
I*)
( s ( (
S![a,s])
(i=s) (SIZE(S![a,s]) ≤ 0)
) )s ) )i1 a}.
(6) Elke toepassing van
{ a ({a}
( i1 ( ( ({i}
I*)
( q ( (Q![a,q]) (i=q)
(SIZE(Q![a,q]) ≤ 0) ) )
q ) )i1 a}.
(7) Elke toepassing van een
TM
[a] kan worden toegepast op een bepaalde invoer , zeg I[i1].{ a ({a}
TM
*) ( i1 ( ({i}
I*) TM
[a] (I[i1]) )i1 a}.TM
[a] kan worden toegepast op een onbegrensd referentieel domein, zeg I* (bijv. een populatie).{ a ({a}
TM
*) ( i1 ( ({i}
I*) TM
[a] (I[i1])(SIZE(I*) ≤
0) ) )i1 a}.TM
[a] kan uitsluitend een eindige invoer I[i1] verwerken (bijv. een steekproef).{ a ({a}
TM
*) ( i1 ( ({i}
I*) ( TM
[a](I[i1])(SIZE(I[i1]) <
0) ) ) )i1 a}.TM
[a] bevat precies ��n eindige, geordende verzameling formules, instructies of commando's, d.i. een redeneerschema, programma of procedure, zeg R![a,r].{ a ({a}
TM
*) ( r ( (TM
[a]R![a,r]) (a=r)
(SIZE(R![a,r]) < 0) ) )
r a}.TM
[a] kent bij elke invoer I[i1] een eindige verzameling van mogelijke verschillende, discrete interne toestanden, zeg S![a,s].{ a ({a}
TM
*) ( i1 ( ( ({i}
I*) TM
[a] (I[i1]) ) ( s ( (TM
[a] (I[i1])S![a,s])
(i=s) (SIZE(S![a,s]) ≤ 0)
) )s ) )i1 a}.TM
[a] maakt bij elke I[i1] gebruik van een onbegrensde opslagruimte: opslagcapaciteit, geheugen, 'kladpapier', zeg Q![a,q].{ a ({a}
TM
*) ( i1 ( ( ({i}
I*) TM
[a] (I[i1]) ) ( q ( (TM
[a] (I[i1])Q![a,q]) (i=q)
(SIZE(Q![a,q]) ≤ 0) ) )
q ) )i1 a}.TM
[a] op een I[i1] bestaat uit een rekenproces.(d)
De Church-Turing these.
Zo'n algoritme, of Turing Machine, 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.
{ a ({a}
TM
*) ( i1 ( ({i}
I*) ( comptable TM
[a](I[i1])Turing Machine comptable TM
[a] (I[i1]) ) ) )i1 a}.(e)
Kenmerken van een beslisbaar algoritme
De volgende eigenschappen gelden enkel voor Turing machines
TM
[a] die voor elke invoer term ineren: een zgn. Decider (Sipser, 1996) of Total Turing machine (Kozen, 1997).(8) Elke afzonderlijke toepassing behelst een eindige verzameling
van acties, stappen of berekeningen, een bewijsreeks P![a,p].
{ a ({a}
( i1 ( ( ({i}
I*)
( p ( (
P![a,p]) (i=p)
(SIZE(P![a,p]) ≤ 0) ) )
p ) )i1 a}.
(9) Elke toepassing van
{ a ({a}
( i1 ( ( ({i}
I*)
( p ( (P![a,p]) (i=p)
HALTS(P![a,p]) ) )p ) )i1 a}.
(10) Elke
Elke
{ a ({a}
( i1 ( ( ({i}
I*)
( u1 ( (U[a,u1])
(i=u) (SIZE(U[a,u1]) ≤ 0)
) )s ) )i1 a}.
(11) Dus elke
{ a DCDBL(
{ a ({a}
TM
*) ( i1 ( ( ({i}
I*) TM
[a] (I[i1]) ) ( p ( (TM
[a] (I[i1])P![a,p]) (i=p)
(SIZE(P![a,p]) ≤ 0) ) )
p ) )i1 a}.TM
[a] 'termineert': d.i. het rekenproces P![a,p] zal altijd, in elk afzonderlijk geval, in eindige tijd eindigen.{ a ({a}
TM
*) ( i1 ( ( ({i}
I*) TM
[a] (I[i1]) ) ( p ( (TM
[a] (I[i1])P![a,p]) (i=p)
HALTS(P![a,p]) ) )p ) )i1 a}.TM
[a] levert dus bij elke (eindige) invoer I[i1] precies ��n eindige uitkomst, U[a,u1].Elke
TM
[a] levert dus een uitkomst die definiet is: d.i. sluitend logisch voorspelbaar uit de combinatie van invoer I[i1] en procedure R![r].{ a ({a}
TM
*) ( i1 ( ( ({i}
I*) TM
[a] (I[i1]) ) ( u1 ( (TM
[a] (I[i1])U[a,u1])
(i=u) (SIZE(U[a,u1]) ≤ 0)
) )s ) )i1 a}.TM
[a] is volledig determinaat, dat wil zeggen beslisbaar.{ a DCDBL(TM
[a]) }.(f)
De verzameling deterministische algoritmen.
We hebben het dan over de verzameling van berekenbare bewerkingen in de wiskunde. Deze blijkt overeen te komen met de volgende begrippen:
· De verzameling van mathematische functies die door middel van een '
effectieve methode' kunnen worden berekend, bij David Hilbert (1900) en Hilbert & Ackerman (1928).
· De verzameling van recursive algorithms (recursive functions), bij Kurt G�del (1934) en Jacques Herbrand (1932).
· De verzameling van lambda-definable functions in de lambda calculus, bij Alonzo Church (1932, 1936a, 1941) en Stephen Kleene (1935).
· De verzameling van Turing machine computable functions; bij Alan Turing (1936-1937).
· De verzameling van recursive algorithms (recursive functions), bij Kurt G�del (1934) en Jacques Herbrand (1932).
· De verzameling van lambda-definable functions in de lambda calculus, bij Alonzo Church (1932, 1936a, 1941) en Stephen Kleene (1935).
· De verzameling van Turing machine computable functions; bij Alan Turing (1936-1937).
4.
Turing's aanpak van het Entscheidungsproblem
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
(nl. een meta-oordeel over de berekenbaarheid, binnen het zelfde systeem, van de invoer). De vraag is dus
of er een 'meta-TM
' mogelijk is (genaamd een Halting Machine) 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 positieve oplossing.
Het bewijs van Turing verloopt als volgt.
Turing's bewijs voor de Onbeslisbaarheid van de elementaire rekenkunde.
4.1.
Samenvatting:
Bewijsroute (I): via transponatie van de diagonaal-rij.
Als we ons een matrix voorstellen van alle mogelijke algoritmische patronen bij alle mogelijke invoerpatronen, en we passen een simpele rekenkundige bewerking (transponatie) toe op de (definiete) uitkomsten van de algoritmes toegepast op zichzelf (de zgn. 'diagonaal'), dan blijkt dat de hypothetische effectieve universele beslissingsprocedure toegepast op het algoritme van deze transponatie wanneer dit 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.
Bewijsroute (II): via het complement van het berekenbare deel van de diagonaal.
Langs een andere route: als er een verzameling bestaat van alle programma's die een uitkomst leveren als ze op zichzelf worden toegepast, en als de complement-verzameling daarvan bestaat, en we nemen aan dat de gehele bovengenoemde matrix beslisbaar is, dan moet elk element van de compliment-verzameling (die geen uitkomsten kent) tot een uitkomst leiden, hetgeen een contradictie is.
4.2.
Stap voor stap:
(1)
We bekijken de verzameling I* van alle mogelijke wiskundige problemen, invoer-reeksen I[i1].
We bekijken daarnaast de verzameling
(3)
De vraag is of I* geheel formeel beslisbaar is. Dit houdt in dat er voor elke invoer I[i1] in I* formeel kan worden bepaald of er minstens ��n wiskundige procedure
{ ( i1
m1 ( ( ({i} I*)
({m}
HALTS(
RC(I*) }.
(4)
We bekijken de verzameling F* van alle mogelijke toepassingen (rekenoperaties) F[f] =
{ i1
m1 ( ( ({i} 
I*)
({m}
HALTS(
RC(F*) }.
(5)
Recursiviteit van F* vereist dat twee voorwaarden vervuld worden:
Elk programma
{ m1
h1
(7)
Elk programma
{ m1
(8)
We bekijken nu de deelverzameling K* van F*, van alle toepassingen van programma's
Vanaf dit punt zijn er diverse bewijs-routes mogelijk.
Hieronder twee voorbeelden:
Wiskundige problemen
We bekijken de verzameling I* van alle mogelijke wiskundige problemen, invoer-reeksen I[i1].
I* = { i | I[i1] } (i := 1,2, .. ¥).
(2) Procedures
We bekijken daarnaast de verzameling
TM
* van alle mogelijke wiskundige procedures, programma's of abstracte machinesTM
[m1].TM
* = { m |TM
[m1] } (m := 1,2, .. ¥).Recursiviteit
De vraag is of I* geheel formeel beslisbaar is. Dit houdt in dat er voor elke invoer I[i1] in I* formeel kan worden bepaald of er minstens ��n wiskundige procedure
TM
[m1] is uitTM
* die bij die invoer een uitkomst levert - en dus termineert - of niet. In dat geval is I* recursief, zeg RC.{ ( i1
m1 ( ( ({i} I*)
({m} TM
*) )HALTS(TM
[m1](i)) ) )RC(I*) }.Matrix
We bekijken de verzameling F* van alle mogelijke toepassingen (rekenoperaties) F[f] =
TM
[m1](i) van programma'sTM
[m1] op invoer-reeksen I[i1].F* =
F* = { m,i |
{ m1 i1
f ( ( (m (i I*) )
(F[f] :=
We weten niet tevoren welke toepassing TM
* x I*.F* = { m,i |
TM
[m1](i) }.{ m1 i1
f ( ( (m TM
*) (i I*) )(F[f] := TM
[m1](i)) ) }.TM
[m1](i) een uitkomst heeft of niet. Elke toepassingTM
[m1](i) is zelf dus ook weer een wiskundig probleem, en behoort dus net zo goed tot de mogelijke invoerreeksen I* waarvoor de vraag naar beslisbaarheid opgaat. De vraag is daarom of geheel F* recursief is.{ i1
m1 ( ( ({i} I*)
({m} TM
*) )HALTS(TM
[m1](i)) )RC(F*) }.Eisen voor recursiviteit
Recursiviteit van F* vereist dat twee voorwaarden vervuld worden:
(5a)
Voor elk element F[f] van F* dat w�l een uitkomst heeft, moet dat tevoren te bepalen zijn.
In dat geval is het bijbehorende gedeelte van F*, zeg G*, berekenbaar (Turing computable) en dus recursief opsombaar (RE).
(G* is dan een halting set).
Voor elk element F[f] van F* dat n�et een uitkomst heeft, moet dat eveneens tevoren te bepalen zijn.
In dat geval is dit gedeelte van F*, zeg H* (het complement van G*) eveneens berekenbaar (Turing computable) en dus recursief opsombaar (RE).
In dat geval is G* co-recursief opsombaar (CO-RE).
(6) Recursief opsombaar
Voor elk element F[f] van F* dat w�l een uitkomst heeft, moet dat tevoren te bepalen zijn.
In dat geval is het bijbehorende gedeelte van F*, zeg G*, berekenbaar (Turing computable) en dus recursief opsombaar (RE).
(G* is dan een halting set).
G* = {
{ i1 m1 ( (
G*)
HALTS(
RE(G*) }.
(5b) TM
[m1](i) | HALTS(TM
[m1] (i)) }.{ i1 m1 ( (
TM
[m1](i) G*)HALTS(TM
[m1](i)) );RE(G*) }.Co-recursief opsombaar
Voor elk element F[f] van F* dat n�et een uitkomst heeft, moet dat eveneens tevoren te bepalen zijn.
In dat geval is dit gedeelte van F*, zeg H* (het complement van G*) eveneens berekenbaar (Turing computable) en dus recursief opsombaar (RE).
In dat geval is G* co-recursief opsombaar (CO-RE).
H* = {
{ i1 m1 (
( H*)
�HALTS(
{ ( i1
m1 ( ( H
*) j1 HALTS(
RE(H*);
CO-RE(G*) }.
TM
[m1](i) | �HALTS(TM
[m1] (i)) }. { i1 m1 (
(TM
[m1](i) H*)�HALTS(TM
[m1](i)) ) }; { ( i1
m1 ( (TM
[m1](i) H
*) j1 HALTS(TM
[j1] (TM
[m1](i))) ) )RE(H*);CO-RE(G*) }.Programma-als-invoer
Elk programma
TM
[m1] kan als invoer dienen voor een ander programmaTM
[h1].{ m1
h1 TM
[h1](m) }.Zelf-reflexieve toepassing
Elk programma
TM
[m1] kan als invoer dienen voor zichzelf.{ m1 TM
[m1](m) }.De diagonaal
We bekijken nu de deelverzameling K* van F*, van alle toepassingen van programma's
TM
[m1] op zichzelf.K* =
K* = { m |
{ m1 ( ({m}
(K(m) :=
TM
* xTM
*.K* = { m |
TM
[m1](m) }.{ m1 ( ({m}
TM
*)(K(m) := TM
[m1](m)) ) }.Vanaf dit punt zijn er diverse bewijs-routes mogelijk.
Hieronder twee voorbeelden:
(I)
(II)
We gaan nogmaals uit van de deelverzameling K* van F*, van alle toepassingen van programma's
Bewijs via transponatie van de diagonaal-rij.
(1)
Stel dat er een 'universeel beslisprogramma' mogelijk is, een meta-procedure
Als een toepassing berekenbaar is dan komt de meta-procedure
{ x1
m1 i1 (
{0, 1} ) }.
Dit blijkt nuttig bij een gecombineerde procedure-toepassing, met name de bewerking:
Wanneer het rekenproces
{ x1
m1 i1 ( (
{0,
Dankzij de meta-procedure
Als
{ x1
m1 i1 ( ( ({i}
I*) ({m,x}
HALTS(
(2) Met het beslisprogramma wordt in principe ook de gehele diagonaal
{ x1
m1 ( ({m,x}
HALTS(
(3) We kunnen aannemen dat dan in
{ x1
k1 m1 ( ({k,m,x}
(
k1
m1 ( ({k,m}
HALTS(
(4)
Op de uitkomsten van een bepaalde procedure in
{ t
x1 i1 m1 ( ( ({i}
I*) ({m,x}
HALTS (
Dit blijkt echter voor de diagonaal-rij van
'Beslisprogramma'
Stel dat er een 'universeel beslisprogramma' mogelijk is, een meta-procedure
TM
[x1], waarmee we voor elke mogelijke toepassingTM
[m1](i) kunnen berekenen of die eindigt in een uitkomst, of niet.Als een toepassing berekenbaar is dan komt de meta-procedure
TM
[x1] bijvoorbeeld uit op 1, en anders op 0.{ x1
m1 i1 ( TM
[x1](TM
[m1](i)){0, 1} ) }.TM
[x1](TM
[m1](i)) *TM
[m1](i).Wanneer het rekenproces
TM
[m1](i) niets oplevert, komt de uitkomst vanTM
[x1], toegepast op (TM
[m1](i)), uit op 0, en anders gewoon die op vanTM
[m1](i).{ x1
m1 i1 ( ( TM
[x1](TM
[m1](i)) *TM
[m1](i) ){0, TM
[m1](i)} ) }.TM
[x1] kan dus elke cel {i · m} in de tabel worden ingevuld.Als
TM
[x1] mogelijk is dan is de gehele tabel M x I berekenbaar, dus recursief en dus beslisbaar.{ x1
m1 i1 ( ( ({i}
I*) ({m,x} TM
* ) )HALTS(TM
[x1](TM
[m1] (i)) *TM
[m1](i)) ) }.TM
* xTM
* berekenbaar.{ x1
m1 ( ({m,x} TM
*)HALTS(TM
[x1](TM
[m1] (m)) *TM
[m1](m)) ) }.TM
* ook een programma k bestaat om de gehele diagonaal te berekenen.{ x1
k1 m1 ( ({k,m,x}
TM
*) ( TM
[k1](m) := (TM
[x1](TM
[m1](m)) *TM
[m1](m)) ) );k1
m1 ( ({k,m} TM
*)HALTS(TM
[k1](m)) ) }.Transponatie van de tabel
Op de uitkomsten van een bepaalde procedure in
TM
* kunnen we altijd opnieuw een specifieke rekenkundige bewerking uitvoeren (een transponatie), zeg T. Zo'n transponantie T vormt op zichzelf weer een procedure inTM
*, zegTM
[t]. Een transponatieTM
[t] zal, als ze berekenbaar is, weer voor elke combinatieTM
[m1](i) dankzijTM
[x1] een uitkomst leveren.{ t
x1 i1 m1 ( ( ({i}
I*) ({m,x}
TM
*) )HALTS (TM
[t](TM
[x1](TM
[m1](i)) *TM
[m1](m))) ) }.TM
[k1] al bij simpelste transponatie tot problemen te leiden.(a) Stel we hebben een simpele transponatie-functie T op I*.
{ t ( ( (
t i1 (
(c) Die transponatie kunnen we toepassen op de rij uitkomsten uit
{ t
k1 x1 m1 (
t k1
x1 m1 (
(d) De laatste toepassing van de transponatie kunnen we weer als aparte procedure in
{ j1
t k1 x1
m1 (
j1 x1
m1 (
(e) Stel dat deze
{ j1
t x1 m1 (
{ j1 t
x1 (
j1 x1 (
(f) Voor dit laatste rekenproces zijn er dan twee mogelijkheden:
(5) Dit betekent dat een meta-programma { T i1 ( T
(i) := i +1 ) }.
(b) Deze transponatie is zelf een procedure in T i1 ( T
(i) := i +1 ) }.TM
*, zegTM
[t].{ t ( (TM
[t] TM
*)(
TM
[t] = T ) );t i1 (
TM
[t](i) := i +1 ) }.TM
[k1], c.q. op de diagonaalTM
* xTM
*.{ t
k1 x1 m1 ( TM
[t](TM
[k1](m)) :=TM
[t](TM
[x1](TM
[m1](m)) *TM
[m1](m)) );t k1
x1 m1 ( TM
[t](TM
[k1](m)) := (TM
[x1](TM
[m1](m)) *TM
[m1](m)) +1 ) ) }.TM
* defini�ren, en verkrijgen daarmee de procedureTM
[k1] uitgebreid met transponatieTM
[t], zegTM
[j1]:{ j1
t k1 x1
m1 ( TM
[j1](m) :=TM
[t](TM
[k1](m)); :=TM
[t](TM
[x1](TM
[m1](m)) *TM
[m1](m)) );j1 x1
m1 ( TM
[j1](m) := ((TM
[x1](TM
[m1](m)) *TM
[m1](m)) +1 ) ) }.TM
[j1] wordt toegepast op invoerreeksen uit I* en daarbij zichzelf tegenkomt als invoer:{ j1
t x1 m1 ( TM
[j1](m) ·[m:=j1] :=TM
[j1](j) );{ j1 t
x1 ( TM
[j1](j) :=TM
[t](TM
[x1](TM
[j1](j)) *TM
[j1](j)) );j1 x1 (
TM
[j1](j) := (TM
[x1](TM
[j1](j)) *TM
[j1](j)) +1 ) ) }.(f.1)
{ HALTS(
Maar substitutie van deze term in (e) levert:
�HALTS(
Deze mogelijkheid leidt tot contradictie met de voorlopige aanname (onder f.1), nl. dat M[j[(j) juist w�l stopt:
.
Het blijkt dat deze mogelijkheid is uitgesloten.
(f.2)
{ �HALTS(
Maar substitutie van deze term in (e) levert:
HALTS(
Maar deze uitkomst is ook strijdig met de voorlopige aanname (onder f.2), nl. dat
.
Deze mogelijkheid is eveneens uitgesloten.
De eerste mogelijkheid.
TM
[j1](j) stopt:{ HALTS(TM
[j1](j));TM
[x1](TM
[j1](j)) :=1;Maar substitutie van deze term in (e) levert:
TM
[j1](j) = (1 *TM
[j1](j)) +1;TM
[j1](j) =TM
[j1](j) +1;TM
[j1](j) =TM
[j1](j) +1 +1 .. ¥;�HALTS(TM
[j1](j)) }.Deze mogelijkheid leidt tot contradictie met de voorlopige aanname (onder f.1), nl. dat M[j[(j) juist w�l stopt:
.(f.2)
De tweede mogelijkheid.
TM
[j1](j) stopt niet:{ �HALTS(TM
[j1](j));TM
[x1](TM
[j1](j)) :=0;Maar substitutie van deze term in (e) levert:
TM
[j1](j) = (0 *TM
[j1](j)) +1;TM
[j1](j) = 0 +1;TM
[j1](j) = 1;HALTS(TM
[j1](j)) }.Maar deze uitkomst is ook strijdig met de voorlopige aanname (onder f.2), nl. dat
TM
[j1] (j) juist n�et stopt:.TM
[x1] niet mogelijk is, en dus dat verzameling F * niet recursief is, en dus dat de elementaire rekenkunde niet beslisbaar is.(II)
Bewijs via het complement van het berekenbare deel van de diagonaal.
We gaan nogmaals uit van de deelverzameling K* van F*, van alle toepassingen van programma's
TM
[m1] op zichzelf.K* =
K* = { m |
TM
* xTM
*.K* = { m |
TM
[m1](m) }.(1) Een deelverzameling van K* is de verzameling L* van alle programma's
{ (L* K*
) (L* G*) }.
(3) Omdat elk programma in L* een uitkomst levert, is L* - per definitie - net als G*
recursief opsombaar (RE).
RE(L*).
(4) Het complement van L* is dan de verzameling N* van alle programma's
{ (N* K*
) (N* H*) }.
(6) Stel dat de gehele matrix ? DCDBL(F*).
{ m1 ( �(m
L*) HALTS(
(8) De combinatie van (4) en (7) levert echter een contradictie.
{ m1 ( �(m
L*) ( (m
N*)
( (HALTS(�(HALTS(
(9) N* kan dus niet recursief opsombaar zijn.
�RE(N*);
(10) Dus is L* niet co-recursief opsombaar, en evenmin G*.
�CO-RE(L*);
�CO-RE(G*).
(11) Maar dan is F* niet recursief, en dus niet beslisbaar.
�RC(F*);
�DCDBL(F*).
TM
[m1] die een uitkomst leveren als ze op zichzelf worden toegepast.L* = { m | ({m} K*)
HALTS(
{ m1 ( ({m}
L*) HALTS(
(2) L* is een doorsnede van K* en G*, dus deelverzameling van zowel K* als G
*. K*)
HALTS(TM
[m1](m)) };{ m1 ( ({m}
L*) HALTS(TM
[m1] (m)) ) }.{ (L* K*
) (L* G*) }.RE(L*).TM
[m1] die g��n uitkomst leveren als ze op zichzelf worden toegepast.N* = (K* - L*);
N* = { m | ({m} K*)
�HALTS(
{ m1 ( �(m
L*) �HALTS(
m1 ( (m
N*) �HALTS(
(5) N* is een doorsnede van K* en H*, dus deelverzameling van zowel K* als H
*.N* = { m | ({m} K*)
�HALTS(TM
[m1](m)) };{ m1 ( �(m
L*) �HALTS(TM
[m1](m)) );m1 ( (m
N*) �HALTS(TM
[m1](m)) ) }.{ (N* K*
) (N* H*) }.TM
* x I*, d.i. verzameling F*, beslisbaar is.? DCDBL(F*).(a) Dan moet F* recursief zijn.
RC(F*).
(b) Dit betekent: dan moet G* recursief opsombaar zijn, dus ook L*.
RE(G*);
RE(L*).
(c) En bovendien moet G* co-recursief opsombaar zijn, net als L*.
CO-RE(G*);
CO-RE(L*).
(d) Maar dan moet het complement van L*, d.i. N*, recursief opsombaar zijn.
RE(N*).
(7) Het laatste betekent dat elk element van N* tot een uitkomst moet leiden.RC(F*).RE(G*);
RE(L*).CO-RE(G*);
CO-RE(L*).RE(N*).{ m1 ( �(m
L*) HALTS(TM
[m1] (m)) ) }.{ m1 ( �(m
L*) ( (m
N*)( (HALTS(TM
[m1](m)) )�(HALTS(TM
[m1](m)) ) ) ) }.�RE(N*);�CO-RE(L*);
�CO-RE(G*).�RC(F*);
�DCDBL(F*).5
Conclusie van Turing's bewijs
De conclusie van Turing's bewijs is dat de mogelijkheid van een universele beslissingsprocedure voor de meest elementaire rekenkunde is uitgesloten. Dus linksaf of rechtsaf blijkt het wiskundige systeem niet volledig beslisbaar.
C.P. van der Velde, oktober 2006.
Zie ook ..
§ {Zie ook:
Beperkingen van formele systemen.