Forside/Blogaden
Tekster
UfNet
Musik
Nørderier
Linktree
FB
Om
Bevisteorien for prædikatlogik er en direkte udvidelse af den for udsagnslogik. Så det eneste vi skal her, er et udvide med nye termer, prædiakter osv.
Vi har sole klart at en term er lig med sig selv. Andet ville give hovedpine. Vi får for introduktion: $$ \frac{}{t = t} = i $$ Igen et aksiom siden det ikke afhænger af præmisser. Vi kan også sige at denne regel er en tautologi. Feks. siger vi nogle gange noget som
En hund er en hund
Hvilket er selvindlysende. Lighed er kun mellem termer. For formler bruger vi jo \( \equiv \) - altså at \( \leftrightarrow \) er en tautologi.
For elimination har vi: $$ \frac{t_1 = t_2 \ \ \ \phi[t_1 / x]}{\phi[t_2 / x]} = e $$ Her har vi at \( t_1,t_2 \) skal være fri for \( x \) i \( \phi \). Vi kan bruge de to regler til at vise at lighed er symmetrisk, vi får:
t_1 == t_2 assumption; [l1] t_1 == t_1 by eq_i ; [l2] t_2 == t_1 by eq_e ([x] x == t_1) l2 l1 .Læg mærke til at vi substituerer fra venstre mod højre. Vi kan også lige bevise at lighed er transitiv:
t_1 == t_2 assumption; [l1] t_2 == t_3 assumption; [l2] t_1 == t_3 by eq_e ([x] t_1 == x) l1 l2 .Eliminering er givet ved: $$ \frac{\forall x . \phi}{\phi[t / x]} \forall e $$ Den siger bare at vi kan substituere. Altså givet udtrykket \( \forall x . \phi \), en term \( t \) der er fri for \( x \) i \( \phi \), kan vi lave \( \phi[t/x] \).
Introduktionsreglen er lidt mere kompliceret. Vi har: $$ \frac{x_0 \cdots \phi[x_0 / x]}{\forall x . \phi} \forall i $$ Med den følger et scope - magen til de kasser vi havde i udsagnslogik. I det her scope har vi en variabel/term til rådighed, kald den \( x_0 \). Den ses som arbitrær eller tilfældig. Dermed kan den have form af hvad som helst i domænet. På den måde kan vi generalisere beviser vi har lavet med den. Hvilket vi har brug for da det for denne kvantor jo gælder for alle \( x \) i domænet. Det kan nogle gange være lidt svært at sluge i starten. Ideen er nogenlunde simpel. Vi vil gerne vise at noget gælder for alle \( x \). Men der kan jo være 1000-vis af forskellige værdier. Måske millioner. Måske uendelig mange. I stedet for at bevise hver eneste værdi \( x \) kan antage, vælger vi et \( x_0 \) tilfældigt. På den måde kan \( x_0 \) jo have en hvilken som helst værdi \( x \) kan have, og vi mister ikke det generelle ved beviset. Det er så bare vigtigt at \( x_0 \) ikke forekommer uden for scopet. På engelsk ville man sige at \( x_0 \) skulle være fresh. Jeg ved ikke med ordet frisk. Lad os bare sige for her at i arbitrær indgår at \( x_0 \) skal være fresh.
Nok om det. Vi kan nu bevise følgende $$ \forall x . P(x) \rightarrow Q(x), \forall x . P(x) \vdash \forall x . Q(x) $$ Vi får:
all ([x] P x => Q x) assumption; [l1] all ([x] P x) assumption; [l2] (var [x_0] P x_0 => Q x_0 by all_e x_0 l1 ; [l3] P x_0 by all_e x_0 l2 ; [l4] Q x_0 by imp_e l4 l3 ) ; [all1] all ([x] Q x) by all_i all1 .Introduktionsreglen er som følger: $$ \frac{\phi[t / x]}{\exists x . \phi} \exists x i $$ Den er nogenlunde lige ud ad landevejen. Givet \( t \) fri for \( x \) i \( \phi \), og givet at vi kan bruge dette konkrete \( t \) til at bevise \( \phi \). Ja, så ved vi at der eksisterer en term der kan bevise \( \phi \). Vi hopper fra konkret til abstrakt - konkret term til abstrakt idé om at \( \phi \) kan bevises.
Elimination involverer igen et scope. Vi har: $$ \frac{\exists x . \phi \ \ \ (x_0) \phi[x_o / x] \cdots \chi}{\chi} \exists e $$ Altså givet \( \exists x . \phi \) samt en antagelse om \( x_0 \) er arbitrært valgt. Hvis vi med dette setup kan substituere og bevise \( \chi \), så ved vi at \( \chi \) er sand. Denne regel minder meget om \( \lor e \). Men hvor vi med disjunktion kun har to operander at udføre beviset for, har vi her potentielt set uendeligt mange. Og vi kan ikke sidde herfra og til jordens undergang og lave beviser for alle uendeligt mange tilfælde af \( x \). Løsningen er i stedet som beskrevet ovenfor at vælge et \( x_0 \) arbitrært. Lad os straks komme i gang med at vise følgende: $$ \forall x . P(x) \rightarrow Q(x) , \exists x P(x) \vdash \exists x Q(x) $$ Vi får:
all ([x] P x => Q x) assumption; [l1] exi ([x] P x) assumption; [l2] (var [x_0] P x_0 assumption; [l3] P x_0 => Q x_0 by all_e x_0 l1 ; [l4] Q x_0 by imp_e l3 l4 ; [l5] exi ([x] Q x) by exi_i x_0 l5 ) ; [exi1] exi ([x] Q x) by exi_e l2 exi1 .Vi kan også bevise følgende: $$ \forall x . P(x) \vdash \exists x . P(x) $$ Læg her mærke til at forskellen på de to kvantorer. ∀ gælder for den tomme mængde. Det gør ∃ ikke. Vi ved (feks. fra sandhedstabellerne) at \( \top \rightarrow \bot \) er falsk. Så med den tomme mængde er udtrykket her falsk. Løsningen er at sige at vi udelukker den tomme mængde fra beviset. Vi får:
all ([x] P x) assumption; [l1] P x_0 by all_e x_0 l1 ; [l2] exi ([x] P x) by exi_i x_0 l2 .
Index
Del
Terminus