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'
{ (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*) }.

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)) }.

Resolutiebewijs.


Aanname van het tegendeel S.


S ≡ ¬R;
S = { ¬( (x1 A(x,x)) (y1 z1 A(y,z)) ) }.

Resolutie-deductiereeks.


Normaal vorm conversies.


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) = { (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 een

TM

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 een

TM

kunnen niet een oplossing opleveren voor elk wiskundig probleem.

(a)

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.

(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

), zeg

TM

[a], heeft tenminste de volgende standaard capaciteiten:
(1) Elke

TM

[a] kan worden toegepast op een bepaalde invoer, zeg I[i1].
{ a ({a}

TM

*)
  ( i1 ( ({i} I*)

TM

[a](I[i1]) )i1 a}.
(2) Elke

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}.
(3) Elke

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}.
(4) Elke

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}.
(5) Elke

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}.
(6) Elke toepassing van

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}.
(7) Elke toepassing van een

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 termineren: 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}

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}.
(9) Elke toepassing van

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}.
(10) Elke

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}.
(11) Dus elke

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).

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 elke

TM

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)

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 machines

TM

[m1].

TM

* = { m |

TM

[m1] } (m := 1,2, .. ¥).
(3)

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 uit

TM

* 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*) }.
(4)

Matrix


We bekijken de verzameling F* van alle mogelijke toepassingen (rekenoperaties) F[f] =

TM

[m1](i) van programma's

TM

[m1] op invoer-reeksen I[i1].
F* =

TM

* x I*.
F* = { m,i |

TM

[m1](i) }.
{ m1 i1 f ( ( (m

TM

*) (i I*) )
  (F[f] :=

TM

[m1](i)) ) }.
We weten niet tevoren welke toepassing

TM

[m1](i) een uitkomst heeft of niet. Elke toepassing

TM

[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*) }.
(5)

Eisen voor recursiviteit


Recursiviteit van F* vereist dat twee voorwaarden vervuld worden:
(5a)

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* = {

TM

[m1](i) | HALTS(

TM

[m1](i)) }.
{ i1 m1 ( (

TM

[m1](i) G*)
  HALTS(

TM

[m1](i)) );
      RE(G*) }.
(5b)

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* = {

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*) }.
(6)

Programma-als-invoer


Elk programma

TM

[m1] kan als invoer dienen voor een ander programma

TM

[h1].
{ m1 h1

TM

[h1](m) }.
(7)

Zelf-reflexieve toepassing


Elk programma

TM

[m1] kan als invoer dienen voor zichzelf.
{ m1

TM

[m1](m) }.
(8)

De diagonaal


We bekijken nu de deelverzameling K* van F*, van alle toepassingen van programma's

TM

[m1] op zichzelf.
K* =

TM

* x

TM

*.
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)

Bewijs via transponatie van de diagonaal-rij.



(1)

'Beslisprogramma'


Stel dat er een 'universeel beslisprogramma' mogelijk is, een meta-procedure

TM

[x1], waarmee we voor elke mogelijke toepassing

TM

[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} ) }.
Dit blijkt nuttig bij een gecombineerde procedure-toepassing, met name de bewerking:

TM

[x1](

TM

[m1](i)) *

TM

[m1](i).
Wanneer het rekenproces

TM

[m1](i) niets oplevert, komt de uitkomst van

TM

[x1], toegepast op (

TM

[m1](i)), uit op 0, en anders gewoon die op van

TM

[m1](i).
{ x1 m1 i1 ( (

TM

[x1](

TM

[m1](i)) *

TM

[m1](i) )
  {0,

TM

[m1](i)} ) }.
Dankzij de meta-procedure

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)) ) }.
(2) Met het beslisprogramma wordt in principe ook de gehele diagonaal

TM

* x

TM

* berekenbaar.
{ x1 m1 ( ({m,x}

TM

*)
  HALTS(

TM

[x1](

TM

[m1](m)) *

TM

[m1](m)) ) }.
(3) We kunnen aannemen dat dan in

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)) ) }.
(4)

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 in

TM

*, zeg

TM

[t]. Een transponatie

TM

[t] zal, als ze berekenbaar is, weer voor elke combinatie

TM

[m1](i) dankzij

TM

[x1] een uitkomst leveren.
{ t x1 i1 m1 ( ( ({i} I*) ({m,x}

TM

*) )
  HALTS (

TM

[t](

TM

[x1](

TM

[m1] (i)) *

TM

[m1](m))) ) }.
Dit blijkt echter voor de diagonaal-rij van

TM

[k1] al bij simpelste transponatie tot problemen te leiden.
(a) Stel we hebben een simpele transponatie-functie T op I*.
{ T i1 ( T(i) := i +1 ) }.
(b) Deze transponatie is zelf een procedure in

TM

*, zeg

TM

[t].
{ t ( (

TM

[t]

TM

*) (

TM

[t] = T ) );
  t i1 (

TM

[t](i) := i +1 ) }.
(c) Die transponatie kunnen we toepassen op de rij uitkomsten uit

TM

[k1], c.q. op de diagonaal

TM

* x

TM

*.
{ 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 ) ) }.
(d) De laatste toepassing van de transponatie kunnen we weer als aparte procedure in

TM

* definiëren, en verkrijgen daarmee de procedure

TM

[k1] uitgebreid met transponatie

TM

[t], zeg

TM

[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 ) ) }.
(e) Stel dat deze

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) Voor dit laatste rekenproces zijn er dan twee mogelijkheden:

(f.1)

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:
.
Het blijkt dat deze mogelijkheid is uitgesloten.

(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:
.
Deze mogelijkheid is eveneens uitgesloten.
(5) Dit betekent dat een meta-programma

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* =

TM

* x

TM

*.
K* = { m |

TM

[m1](m) }.
(1) Een deelverzameling van K* is de verzameling L* van alle programma's

TM

[m1] die een uitkomst leveren als ze op zichzelf worden toegepast.
L* = { m | ({m} K*) HALTS(

TM

[m1](m)) };
  { m1 ( ({m} L*) HALTS(

TM

[m1](m)) ) }.
(2) L* is een doorsnede van K* en G*, dus deelverzameling van zowel K* als G*.
{ (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

TM

[m1] die géén uitkomst leveren als ze op zichzelf worden toegepast.
N* = (K* - L*);
  N* = { m | ({m} K*) ¬HALTS(

TM

[m1](m)) };
  { m1 ( ¬(m L*) ¬HALTS(

TM

[m1](m)) );
  m1 ( (m N*) ¬HALTS(

TM

[m1](m)) ) }.
(5) N* is een doorsnede van K* en H*, dus deelverzameling van zowel K* als H*.
{ (N* K*) (N* H*) }.
(6) Stel dat de gehele matrix

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.
{ m1 ( ¬(m L*) HALTS(

TM

[m1](m)) ) }.
(8) De combinatie van (4) en (7) levert echter een contradictie.
{ m1 ( ¬(m L*) ( (m N*)
  ( (HALTS(

TM

[m1](m)) ) ¬(HALTS(

TM

[m1](m)) ) ) ) }.
(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*).

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, oktobers 2006.

Zie ook ..