Inleiding tot rekenlogica

Origineel artikel: https://www.cs.cornell.edu/gries/Logic/Calculational.html

Calculationele propositielogica is een product van onderzoekers op het gebied van de formele ontwikkeling van algoritmen. ( Klik hier voor een korte historie .) C is gaaf en compleet. De nadruk bij bewijzen ligt op de vervanging van gelijken door gelijken, in plaats van op modus ponens. Gelijkheid, of gelijkwaardigheid, speelt een belangrijke rol in plaats van een kleine rol te spelen, zoals in de meeste propositielogica's.

We gebruiken & voor conjunctie, | voor disjunctie, en ~ voor ontkenning (niet).

In onze notatie duidt b = c gelijkheid aan, voor b en c van hetzelfde type, terwijl b == c, of gelijkwaardigheid, alleen wordt gedefinieerd voor b en c van het type boolean. Voor b en c van het type boolean hebben b = c en b == c dezelfde betekenis.

Eén reden voor het hebben van twee symbolen voor gelijkheid boven de Booleans is dat gelijkheid = gewoonlijk als zijnde wordt beschouwd conjunctief:

b = c = d is een afkorting voor b = c & c = d

terwijl b == c associatief gebruikt kan worden , wat voor ons van groot belang is:

b == c == d is gelijk aan b == (c == d) en aan (b == c) == d.

Hieronder vindt u een typisch bewijs in de rekenlogica. De regelnummers zijn alleen aanwezig voor latere discussie. Dit voorbeeld is gekozen omdat het eenvoudig is, maar alle aspecten van het formele bewijssysteem laat zien (zoals later besproken). De stellingnummers verwijzen naar stellingen van A Logical Approach to Discrete Math . Associativiteit en symmetrie van operators worden transparant behandeld, zonder vermelding; dit resulteert in een grote vermindering van het aantal te presenteren stellingen en vereenvoudigt de manipulatie. Merk ten slotte op dat de stijl slechts een formalisering is van de rekenstijl die wordt gebruikt in de algebra op de middelbare school, en inderdaad door veel wetenschappers in hun werk - daarom is de stijl zo nuttig.

Hier is een bewijs van ~p == p == false .

(0) ~p == p == false
(1) = < (3.9), ~(p == q) == ~p == q , met q:= p >
(2) ~(p == p ) == false
(3) = < Identiteit van == (3.9), met q:= p >
(4) ~true == false --(3.8)

Inferentieregels van rekenlogica

Hier zijn de vier gevolgtrekkingsregels van logica C. (P[x:= E] geeft tekstuele vervanging aan van expressie E voor variabele x in expressie P):

Substitutie: Als P een stelling is, dan is P[x:= E] dat ook.

|- P ---> |- P[x:= E]

Leibniz: Als P = Q een stelling is, dan is E[x:= P] = E[x:= Q] dat ook.

|- P = Q ---> |- E[x:= P] = E[x:= Q]

Transitiviteit: Als P = Q en Q = R stellingen zijn, dan is P = R dat ook.

|- P = Q, |- Q = R ---> |- P = R

Gelijkmoedigheid: Als P en P == Q stellingen zijn, dan is Q dat ook.

|- P, |- P == Q ---> |- Q

Uitleg proefformaat

We leggen uit hoe de vier gevolgtrekkingsregels worden gebruikt in bewijzen, met behulp van het bewijs van ~p == p == false .

(0) ~p == p == onwaar

(1) = < (3,9), ~(p == q) == ~p == q , met q:= p >

(2) ~(p == p) == onwaar

(3) = < Identiteit van == (3.9), met q:= p >

(4) ~waar == onwaar --(3.8)

Ten eerste tonen de regels (0)-(2) het gebruik van de gevolgtrekkingsregel Leibniz:

(0) = (2)

is de conclusie van Leibniz, en de premisse ervan ~(p == p) == ~p == p wordt gegeven op regel (1). Op dezelfde manier wordt de gelijkheid op de regels (2)-(4) onderbouwd met behulp van Leibniz.

De "hint" op regel (1) zou een premisse van Leibniz moeten weergeven, die laat zien welke vervanging van gelijken door gelijken wordt gebruikt. Dit uitgangspunt is stelling (3.9) met de substitutie p:= q, dwz

(~(p == q) == ~p == q)[p:=q]

Dit laat zien hoe de gevolgtrekkingsregel Substitutie wordt gebruikt binnen hints.

Uit (0) = (2) en (2) = (4) concluderen we met de gevolgtrekkingsregel Transitiviteit dat (0) = (4). Dit laat zien hoe Transitiviteit wordt gebruikt.

Merk ten slotte op dat regel (4), ~true == false, een stelling is, zoals aangegeven door de hint rechts ervan. Op basis van de gevolgtrekkingsregel Gelijkmoedigheid concluderen we dus dat lijn (0) ook een stelling is. En (0) is wat we wilden bewijzen.

Dit proefformaat heeft verschillende voordelen.

Het gebruik van elke afleidingsregel wordt bepaald door het bewijsformaat, dus de namen van de afleidingsregels hoeven niet te worden vermeld. Dit vermindert de hoeveelheid lees- en schrijfwerk in een proefdruk.
Het bewijs is volledig rigoureus, maar zonder overweldigende complexiteit. Bovendien is het bewijs eenvoudig genoeg voor studenten om te begrijpen. In feite formaliseert het de rekenstijl die op de middelbare school wordt onderwezen.
Over het algemeen wordt er weinig gekopieerd van formules van de ene regel naar de andere - een van de nadelen van bewijzen in Hilbert-stijl.
Met dit format kunnen nuttige bewijsprincipes en -strategieën worden aangeleerd.
Het bewijs kan voorwaarts of achterwaarts worden gelezen.