Introduktion til beregningslogik
Original artikel:https://www.cs.cornell.edu/gries/Logic/Calculational.html
Calculational propositional logic er et produkt af forskere inden for den formelle udvikling af algoritmer. (Klik her for en kort historie.) C er sund og komplet. Vægten i beviser er på substitution af lige med lige, i stedet for modus ponens. Lighed, eller ækvivalens, indtager en vigtig rolle i stedet for at være en smule spiller, som i de fleste propositionelle logikker.
Vi bruger & til sammenhæng, | for disjunktion, og ~ for negation (ikke).
I vores notation betegner b = c lighed, for b og c af samme type, mens b == c, eller ækvivalens, kun er defineret for b og c af typen boolesk. For b og c af typen boolesk har b = c og b == c samme betydning.
En grund til at have to symboler for lighed over boolerne er, at lighed = normalt betragtes som værende konjunktionel :
b = c = d er en forkortelse for b = c & c = d
mens b == c kan bruges associativt , hvilket er af stor betydning for os:
b == c == d er lig med b == (c == d) og til (b == c) == d .
Nedenfor er et typisk bevis i beregningslogik. Linjenumrene er kun til stede til senere diskussion. Dette eksempel er valgt, fordi det er enkelt, men viser alle aspekter af det formelle bevissystem (som diskuteret senere). Sætningens numre refererer til sætninger fra A Logical Approach to Discrete Math . Associativitet og symmetri af operatører behandles gennemsigtigt, uden omtale; dette resulterer i en stor reduktion i antallet af teoremer, der skal præsenteres og forenkler manipulation. Bemærk endelig, at stilen kun er en formalisering af den udregningsstil, der bruges i algebra på gymnasiet, og faktisk af mange videnskabsmænd i deres arbejde - det er derfor, stilen er så nyttig.
Her er et bevis på ~p == p == falsk .
(0) ~p == p == falsk
(1) = < (3.9), ~(p == q) == ~p == q , med q:= p >
(2) ~(p == p ) == falsk
(3) = < Identitet af == (3.9), med q:= p >
(4) ~sand == falsk --(3.8)
Inferensregler for beregningslogik
Her er de fire inferensregler for logik C. (P[x:= E] angiver tekstlig substitution af udtryk E for variabel x i udtryk P):
- Substitution: Hvis P er en sætning, så er P[x:= E] det også.
|- P ---> |- P[x:= E]
- Leibniz: Hvis P = Q er en sætning, så er E[x:= P] = E[x:= Q] også.
|- P = Q ---> |- E[x:= P] = E[x:= Q]
- Transitivitet: Hvis P = Q og Q = R er sætninger, så er P = R også.
|- P = Q, |- Q = R ---> |- P = R
- Ligevægt: Hvis P og P == Q er sætninger, så er Q det også.
|- P, |- P == Q ---> |- Q
Forklaring af bevisformat
Vi forklarer, hvordan de fire inferensregler bruges i beviser, ved at bruge beviset for ~p == p == falsk .
(0) ~p == p == falsk
(1) = < (3,9), ~(p == q) == ~p == q , med q:= p >
(2) ~(p == p) == falsk
(3) = < Identitet af == (3.9), med q:= p >
(4) ~sandt == falsk --(3.8)
Først viser linjerne (0)-(2) en brug af inferensreglen Leibniz:
(0) = (2)
er Leibniz' konklusion, og dens præmis ~(p == p) == ~p == p er givet på linie (1). På samme måde er ligheden på linje (2)-(4) underbygget ved hjælp af Leibniz.
"Tipet" på linje (1) formodes at give en præmis af Leibniz, der viser, hvilken substitution af liges for lige, der bruges. Denne præmis er sætning (3.9) med substitutionen p:= q, dvs
(~(p == q) == ~p == q)[p:=q]
Dette viser, hvordan inferensregel Substitution bruges i hints.
Ud fra (0) = (2) og (2) = (4), konkluderer vi med inferensregel Transitivitet, at (0) = (4). Dette viser, hvordan Transitivity bruges.
Bemærk endelig, at linje (4), ~sand == falsk, er en sætning, som angivet af hintet til højre. Derfor konkluderer vi ved slutningsregel Ligevægt, at linje (0) også er en sætning. Og (0) er, hvad vi ønskede at bevise.
Dette bevisformat har flere fordele.
- Brugen af hver slutningsregel bestemmes af bevisformatet, så navnene på slutningsreglerne behøver ikke at nævnes. Dette reducerer mængden af læsning og skrivning i et korrektur.
- Beviset er fuldstændig strengt, men uden kompleksitet overvældende. Ydermere er beviset simpelt nok for eleverne at forstå. Faktisk formaliserer det den udregningsstil, man lærer i gymnasiet.
- Generelt er der kun lidt kopiering af formler fra en linje til en anden - en af ulemperne ved Hilbert-lignende beviser.
- Med dette format kan nyttige bevisprincipper og strategier undervises.
- Beviset kan læses frem eller tilbage.
