Beweren en bewijzen/de zuilen/Zekerheid/6. Wiskunde
| literatuur
... |
Inhoud
De grenzen van de predicaatlogica
We hebben gezien dat men al gauw tegen de grenzen van propositielogica aanloopt. Propositielogica kan immers slecht redeneren over grote hoeveelheden objecten van hetzelfde type. Propositielogica kan helemaal niet redeneren over een onbekende aftelbare hoeveelheid objecten of een overaftelbare hoeveelheid objecten.
Een zeer nuttige uitbreiding van de propositielogica is daarom de predikaatlogica. Met predicaatlogica bedoelen we hier eerste orde logica. Al snel blijkt dat het handig is als men ook getallen kan gebruiken en dit is grofweg de taal die we in deze cursus gebruiken. Maar ook deze taal heeft haar beperkingen zoals we hieronder zullen zien.
Er bestaan tenminste 10 (verschillende) katten
Stel wel willen formaliseren dat er tenminste 2 (verschillende) katten bestaan. We hebben gezien dat een dergelijke bewering dan voldoet:
∃k1:K, ∃k2:K, ¬(k1 = k2)
Voor 4 katten wordt het al een stuk lastiger:
∃k1:K, ∃k2:K,∃k3:K, ∃k4:K, ¬(k1=k2 ∨ k1=k3 ∨ k1=k4 ∨ k2=k3 ∨ k2=k4 ∨ k3=k4)
In het algemeen moet men voor N katten N*(N-1)/2 vergelijkingen van de vorm k1=k2 etc. opschrijven. Dus voor 10 katten betekent dat 45 vergelijkingen! Hieronder staat hoe het met iets minder vergelijkingen kan maar het blijft veel. Dit voorbeeld geeft de beperkingen van onze taal weer en er zijn voorbeelden te bedenken met nog veel desastreuzere gevolgen voor de op te schrijven beweringen. Om hier op een betere manier mee om te kunnen gaan dient er meer wiskundige theorie aanwezig te zijn.
Optimalisatie
| David en ik heb eens een wedstrijdje gedaan wie met het minste aantal vergelijkingen een bewering voor tenminste 10 katten kon opschrijven. David heeft gewonnen met de volgende oplossing. |  |
|
| Jasper Berendsen → BenB | Remove this comment when resolved! | |
Definition TienVerschillendeKatten (k1:K) (k2:K) (k3:K) (k4:K) (k5:K) (k6:K) (k7:K) (k8:K) (k9:K) (k10:K) := ~(k1 = k2 \/ k1 = k3 \/ k2 = k3 \/ k4 = k5 \/ k4 = k6 \/ k5 = k6 \/ k7 = k8 \/ k7 = k9 \/ k8 = k9) /\ (forall c1:K, c1 = k1 \/ c1 = k2 \/ c1 = k3 -> (forall c2:K, c2 = k4 \/ c2 = k5 \/ c2 = k6 -> (forall c3:K, c3 = k7 \/ c3 = k8 \/ c3 = k9 -> ~(c1 = c2 \/ c1 = c3 \/ c2 = c3 \/ c1 = k10 \/ c2 = k10 \/ c3 = k10)))).
De opbouw van de definitie is: er zijn een aantal (hier: vier) verzamelingen van drie verschillende katten (hier: {k1, k2, k3}, {k4, k5, k6} en {k7, k8, k9}; kat k10 blijft dan over), en als je c(i) uit de (i)de verzameling pikt, zijn c1...c3 weer verschillend, en bovendien verschillen c1...c3 van k10.
Dit levert een lineaire groei op van het aantal vergelijkingen: algemeen kun je, om N verschillende katten te vinden, N/3 verzamelingen van 3 katten vinden, en elke keuze uit die N/3 verzamelingen levert N/3 verschillende katten op. Een beetje spelen met Excel laat zien dat dat (N-2)*3 vergelijkingen oplevert (voor N > 6).
Het werkt ook met verzamelingen van telkens twee verschillende katten, daar kom je ook op (N-2)*3 vergelijkingen (voor N > 4).
Formalisering van de wiskunde
In Coq en andere bewijsassistenten kunnen bibliotheken met wiskundige theorie en notatie geladen worden. Deze wiskunde kan gebruikt worden in de beweringen en bewijzen. In Coq zijn alle wiskundestellingen die worden gebruikt bovendien op hun beurt bewezen, uitgaande van een zeer beperkte grondlogica.
Een voorbeeld is de theorie van Ensembles in Coq dat zijn een soort verzamelingen. Gebruikmakende van de standaard wiskunde bibliotheken in Coq ziet het vorige voorbeeld er als volgt uit:
Require Import BenB. Require Import Classical_sets. Require Import Finite_sets. Open Scope nat_scope. Variable Kat : Set. Variable verzamelingKatten : Ensemble Kat. Definition erZijn10katten : B := exists n:nat, n>10 /\ cardinal Kat verzamelingKatten n.
