Ækvivalenser

[17.12.2023] [Nørderier/Teori]

• Intro
• Udvidelse af udsangslogik
• Syntaks
• Semantik
• Naturlig Deduktion
• Ækvivalenser

Der er en række ækvivalenser forbundet med prædikatlogik. Nogle er ret intuitive, feks. er "der er ikke tilfældet at alle pattedyr er mennesker" det samme som at sige "der eksisterer mindst et pattedyr der ikke er et menneske". Nogle af ækvivalenserne er bevist. Måske kun den ene vej. Vi har helt generelt:

1. \( \neg \forall x . \phi \dashv \vdash \exists x . \neg \phi \)
2. \( \neg \exists x . \phi \dashv \vdash \forall x . \neg \phi \)

Derudover antag \( x \) ikke er fri for \( \psi \), og vi har:

1. \( \forall x . \phi \land \psi \dashv \vdash \forall x . (\phi \land \psi) \)
2. \( \forall x . \phi \lor \psi \dashv \vdash \forall x . (\phi \lor \psi) \)
3. \( \exists x . \phi \land \psi \dashv \vdash \exists x . (\phi \land \psi) \)
4. \( \exists x . \phi \lor \psi \dashv \vdash \exists x . (\phi \lor \psi) \)
5. \( \forall x . (\phi \rightarrow \psi) \dashv \vdash \phi \rightarrow \forall x . \psi \)
6. \( \exists x . (\phi \rightarrow \psi) \dashv \vdash \forall x . \phi \rightarrow \psi \)
7. \( \forall x . (\phi \rightarrow \psi)\dashv \vdash \exists x . \phi \rightarrow \psi \)
8. \( \exists x . (\phi \rightarrow \psi)\dashv \vdash \phi \rightarrow \exists x . \psi \)
9. \( \forall x . (\phi \land \psi)\dashv \vdash \forall x . \phi \land \forall x . \psi \)
10. \( \exists x . (\phi \lor \psi) \dashv \vdash \exists x . \phi \lor \exists x . \psi \)
11. \( \forall x . \forall y . \phi \dashv \vdash \forall y . \forall x . \phi \)
12. \( \exists x . \exists y . \phi \dashv \vdash \exists y . \exists x . \phi \)

Læg mærke til at (i) ikke er sand for disjunktion. Antag feks. at vi har \( \forall x . (P(x) \lor Q(x)) \), hvor \( P(x) \) er sand for den ene halvdel af alle \( x \), og hvor \( Q(x) \) er sand for den anden. Er domænet mennesker, kan vi sige at \( P(x) \) læses som \( x \) er mand, og \( Q(x) \) læses som at \( x \) er kvinde. Altså i det omfang køn er binært. Men nu har vi hverken \( \forall x. P(x) \) eller \( \forall x . Q(x) \). På nogenlunde samme måde gælder (j) ikke for konkjunktion.

Beviser for nogle af ækvivalenserne

Højre retning af (i):

~ all ([x] P x) assumption; [l1] ( ~ exi ([x] ~ P x) assumption; [l2] (var [x_0] ( ~ P x_0 assumption; [l3] exi ([x] ~ P x) by exi_i x_0 l3 ; [l4] bot by neg_e l4 l2 ) ; [pbc1] P x_0 by pbc pbc1 ) ; [all1] all ([x] P x) by all_i all1 ; [l6] bot by neg_e l6 l1 ) ; [pbc2] exi ([x] ~ P x) by pbc pbc2 .

Højre retning af (ii):

~ exi ([x] P x) assumption; [l1] (var [x_0] ( P x_0 assumption; [l2] exi ([x] P x) by exi_i x_0 l2 ; [l3] bot by neg_e l3 l1 ) ; [neg1] ~ P x_0 by neg_i neg1 ) ; [all1] all ([x] ~ P x) by all_i all1 .

Venstre retning af (j), vi får:

all ([x] P x) /\ all ([x] Q x) assumption; [l1] (var [x_0] all ([x] P x) by con_e1 l1 ; [l2] all ([x] Q x) by con_e2 l1 ; [l3] P x_0 by all_e x_0 l2 ; [l4] Q x_0 by all_e x_0 l3 ; [l5] P x_0 /\ Q x_0 by con_i l4 l5 ) ; [all1] all ([x] P x /\ Q x) by all_i all1 .

Højre retning af (j):

exi ([x] P x \/ Q x) assumption; [l1] (var [x_0] P x_0 \/ Q x_0 assumption; [l2] ( P x_0 assumption; [l3] exi ([x] P x) by exi_i x_0 l3 ; [l4] exi ([x] P x) \/ exi ([x] Q x) by dis_i1 l4 ) ; [dis1] ( Q x_0 assumption; [l3] exi ([x] Q x) by exi_i x_0 l3 ; [l4] exi ([x] P x) \/ exi ([x] Q x) by dis_i2 l4 ) ; [dis2] exi ([x] P x) \/ exi ([x] Q x) by dis_e l2 dis1 dis2 ) ; [exi1] exi ([x] P x) \/ exi ([x] Q x) by exi_e l1 exi1 .

Og det var vist det for nu :-).

Index Del