Beweren en bewijzen/het verhaal/4. Correctheid/casus Universele radio

Op deze pagina een voorbeeld aangaande een helaas niet functionerende universeel werkende radio. Dit artefact is ter sprake gekomen om een voorbeeld te geven waarbij het van belang is om onderscheid te maken tussen een voedingsbron van 110 volt of 230 volt. Dit in tegenstelling tot de meeste andere artefacten, waarbij het voldoende is om aan te nemen dat de juiste voedingsbron aanwezig is.

Doel van deze pagina is om te laten zien hoe semantische tableaus gebruikt kunnen worden om tegenvoorbeelden te vinden tegen een foute correctheidsstelling. Dit voorbeeld is ook gebruikt bij het college van 10 maart 2010.

Artefact

Het gaat hier om een simpele radio die universeel moet kunnen werken. Op zich werkt hij op 12 volt gelijkspanning. Maar om zowel in Europa als in Amerika te kunnen werken is hij voorzien van een externe ACDC converter die zowel 110 volt wisselspanning als 230 volt wisselspanning kan omzetten in 12 volt gelijkspanning. Om muziek te kunnen produceren heeft de radio naast een voedingsbron ook nog ontvangst nodig.

Specificaties onderdelen

Zoals gezegd bestaat het hele systeem uit twee onderdelen. De ACDC converter en de eigenlijke radio. Dit zijn hun specificaties:

Definition ACDC := (wissel110 -> gelijk12) \/ (wissel230 -> gelijk12).
Definition Radio := gelijk12 /\ ontvangst -> muziek.

Specificatie van het geheel

Uiteindelijk willen we bewijzen dat als een van de twee mogelijke voedingsbronnen aanwezig is en er ontvangst is, dat er dan ook muziek is.

Definition GewensteEigenschap :=(wissel110 \/ wissel230) /\ ontvangst -> muziek.

Correctheidsstelling

Op grond van de bovenstaande definities kan de volgende correctheidsstelling worden opgesteld.

Theorem OveralMuziek: ACDC /\ Radio -> GewensteEigenschap.

Of als we de definities uitschrijven:

Theorem OveralMuziek: ((wissel110 -> gelijk12) \/ (wissel230 -> gelijk12)) /\ (gelijk12 /\ ontvangst -> muziek) -> ((wissel110 \/ wissel230) /\ ontvangst -> muziek).

Semantisch tableau

Zoals reeds bovenaan deze pagina is opgemerkt, geldt deze correctheidsstelling niet. Dat kunnen we natuurlijk bewijzen door de 32-rijen van de bijbehorende waarheidstabel uit te schrijven en op te merken dat er in de kolom bij deze formule niet alleen maar 1-en staan. Echter, het is voldoende om één tegenvoorbeeld te vinden. Vandaar dat we de techniek van semantische tableaus gebruiken om systematisch een tegenvoorbeeld te vinden. Zoals tijdens het college al bleek is het zelfs voor zo'n relatief simpel systeem best een hoop werk om het tableau volledig op te schrijven. Hoewel we natuurlijk kunnen stoppen zodra we één tegenvoorbeeld hebben gevonden, geven we hier toch het volledige tableau weer: Bestand:Sem tab uni radio.pdf. (Om de breedte van het tableau nog een beetje te beperken, zijn de atomaire proposities op een voor de hand liggende manier afgekort. De rode operatoren zijn gebruikt om aan te geven welk voegteken in elke stap is weggewerkt.)

Uit het tableau blijkt dat er twee open takken zijn (herkenbaar aan de referenties 1 en 2). De situatie die het eerste tegenvoorbeeld oplevert kunnen we nu aflezen: de proposities 'ontvangst' en 'wissel110' zijn waar en de proposities 'wissel230', 'gelijk12' en 'muziek' zijn onwaar. Het tweede voorbeeld is symmetrisch in 'wissel110' en 'wissel230': de proposities 'ontvangst' en 'wissel230' zijn waar en de proposities 'wissel110', 'gelijk12' en 'muziek' zijn onwaar.

Wat verder nog interessant is aan het tableau is dat het in deze vorm niet gebalanceerd is. De linkerkant is groter dan de rechterkant. Terwijl dat op grond van symmetrie misschien niet verwacht is. Het komt echter door de verschillende volgordes van het uitvoeren van de stappen. De keuzes die aan de rechterkant gemaakt zijn, waren blijkbaar slimmer dan de keuzes die aan de linkerkant gemaakt zijn! Dit is een algemeen principe: door na te denken over wat er aan de hand is, is het mogelijk om dit soort 'slimmere' keuzes te herkennen.

Verbeterde correctheidsstelling bewijzen met Coq

Het probleem in de correctheidsstelling zit hem in de specificatie van de ACDC converter. Wij hebben hierboven gespecificeerd dat wij tevreden zijn met een apparaat dat ofwel in Europa ofwel in Amerika werkt, terwijl wij een apparaat willen hebben dat op beide plaatsen goed werkt. Met andere woorden: de \/ moet een /\ zijn. Ter illustratie hier een Coq script waarmee de verbeterde correctheidsstelling bewezen kan worden.

(* universeel werkende radio *)

Require Import "BenB".

Variables wissel110 wissel230 gelijk12: Prop.
Variables ontvangst muziek: Prop.

Definition ACDC :=
(wissel110 -> gelijk12) /\ (wissel230 -> gelijk12).

Definition Radio :=
gelijk12 /\ ontvangst -> muziek.

Definition GewensteEigenschap :=
(wissel110 \/ wissel230) /\ ontvangst -> muziek.

Theorem OveralMuziek:
ACDC /\ Radio -> GewensteEigenschap.
Proof.
unfold ACDC.
unfold Radio.
unfold GewensteEigenschap.
tauto.
Qed.

De 'unfold' stappen zijn noodzakelijk omdat het commando 'tauto' alleen maar werkt als de formules zijn uitgeschreven in de atomaire proposities.

Hieronder nog een voorproefje van natuurlijke deductie. Op dit moment hoef je nog niet te weten wat de commando's allemaal betekenen, maar voer het bewijs nog eens uit als je de technieken wel kent.

Theorem OveralMuziekMetNatuurlijkeDeductie:
ACDC /\ Radio -> GewensteEigenschap.
Proof.
imp_i a1.
unfold GewensteEigenschap.
imp_i a2.
unfold Radio in a1.
imp_e (gelijk12 /\ ontvangst).
con_e2 (ACDC).
assumption.
con_i.
unfold ACDC in a1.
dis_e (wissel110 \/ wissel230) a4 a5.
con_e1 ontvangst.
assumption.
imp_e (wissel110).
con_e1 (wissel230 -> gelijk12).
con_e1 (Radio).
assumption.
assumption.
imp_e (wissel230).
con_e2 (wissel110 -> gelijk12).
con_e1 (Radio).
assumption.
assumption.
con_e2 (wissel110 \/ wissel230).
assumption.
Qed.

Bewijs in natuurlijke taal van verbeterde correctheidsstelling

We willen de tautologie |= ACDC /\ Radio -> GewensteEigenschap bewijzen. Dit is een 'als-dan' bewering. De meest voor de hand liggende manier om zo'n bewering te bewijzen is om het 'als' gedeelte aan te nemen en daarmee het 'dan' gedeelte te bewijzen. Dit is dan ook de strategie die wij hier gaan toepassen.

• (1) Neem aan dat het 'als' gedeelte waar is, dus dat ACDC /\ Radio waar is.
• (2) Op grond van de definitie van /\ volgt dan uit aanname (1) de conclusie dat ACDC waar is.
  • (2a) Als we de definitie van ACDC uitschrijven en nogmaals de definitie van de /\ toepassen op conclusie (2) , kunnen we dus de conclusie trekken dat wissel110 -> gelijk12 waar is.
  • (2b) Net zo kunnen we uit conclusie (2) concluderen dat wissel230 -> gelijk12 waar is.
• (3) Op dezelfde manier als hiervoor kunnen we uit aanname (1) de conclusie trekken dat Radio waar is. Uitschrijven van de definitie van Radio levert dan dat gelijk12 /\ ontvangst -> muziek waar is.

Samengevat hebben we aanname (1) dus gebruikt om de conclusies (2a), (2b) en (3) te trekken, die wij in de rest van het bewijs dus kunnen gebruiken om het uiteindelijke doel (het 'dan' deel) GewensteEigenschap te bewijzen. Als we nu eens kijken naar dat doel dan zien wij dat GewensteEigenschap een afkorting is voor de formule (wissel110 \/ wissel230) /\ ontvangst -> muziek. Dit doel is op zich ook weer een 'als-dan' bewering. Dus ook hier geldt dat we deze bewering kunnen bewijzen door het 'als' deel aan te nemen en vervolgens het 'dan' deel te bewijzen.

• (4) Neem aan dat (wissel110 \/ wissel230) /\ ontvangst waar is.
  • (4a) Uit aanname (4) kunnen we weer de conclusie wissel110 \/ wissel230 waar is.
  • (4b) Netzo volgt uit aanname (4) de conclusie ontvangst.

Samengevat hebben we nu dus uit de aannames (1) en (4) de conclusies (2a), (2b), (3), (4a) en (4b) gebruikt die we mogen gebruiken om het doel muziek te bewijzen.

Merk op dat conclusie (4a) een \/-teken bevat. Dat betekent dat we niet weten of nu het linkerdeel van die bewering of juist het rechterdeel waar is. Daarom maken we een gevalsonderscheiding: we nemen aan dat wissel110 waar is en proberen daaruit ons doel muziek te bewijzen en daarna nemen we aan dat wissel230 waar is en proberen daar ook weer het doel muziek uit te bewijzen.

• (4aa) Neem aan dat wissel110 waar is.
  • (5) Aanname (4aa) is precies het linkerdeel van conclusie (2a), dus mogen we concluderen dat het rechterdeel van conclusie (2a), gelijk12, waar is.
  • (6) Uit conclusie (5) en conclusie (4b), mogen we concluderen dat gelijk12 /\ ontvangst waar is.
  • (7) Conclusie (6) is precies het linkerdeel van conclusie (3), dus mogen we concluderen dat het rechterdeel van conclusie (3), muziek waar is. Dat was precies ons doel.
• (4ab) Neem aan dat wissel230 waar is.
  • (8) Aanname (4ab) is precies het linkerdeel van conclusie (2b), dus mogen we concluderen dat het rechterdeel van conclusie (2b), gelijk12, waar is.
  • (9) Uit conclusie (8) en conclusie (4b), mogen we concluderen dat gelijk12 /\ ontvangst waar is.
  • (10) Conclusie (9) is precies het linkerdeel van conclusie (3), dus mogen we concluderen dat het rechterdeel van conclusie (3), muziek waar is. Dat was wederom precies ons doel.

We hebben nu gezien dat in beide gevallen (4aa) en (4ab) we de conclusie kunnen trekken dat muziek waar is. Maar dan volgt muziek dus uit (4a) en natuurlijk de andere conclusies (2a), (2b), (3) en (4b). Uiteindelijk hebben we dus uit de aannames (1) en (4) muziek kunnen bewijzen. Maar dat betekent dat de oorspronkelijke stelling dus waar is.