Gebruiker:Otto ter Haar/logica4

Logische wetten

De propositionele connectieven

De volgende afleidingsregels zijn een uitwerking van de gebruikelijke interpretatie van de connectieven &, ∨ en →.

 Γ ⊢ φ   Δ ⊢ ψ &I      Γ ⊢ φ & ψ &Er      Γ ⊢ φ & ψ &El
  Γ+Δ ⊢ φ & ψ            Γ ⊢ φ              Γ ⊢ ψ

    Γ ⊢ φ   ∨Ir         Γ ⊢ ψ   ∨Il    Γ ⊢ φ ∨ ψ  Δ+φ ⊢ σ  Ε+ψ ⊢ σ ∨E
 Γ ⊢ φ ∨ ψ           Γ ⊢ φ ∨ ψ                  Γ+Δ+Ε ⊢ σ

  Γ+φ ⊢ ψ  →I       Γ ⊢ φ → ψ →E
 Γ ⊢ φ → ψ           Γ+φ ⊢ ψ

We hebben nog twee afleidingsregels nodig voor het openen van een hypothese (H) en het sluiten van een afgeleide hypothese (Modus ponens MP).

        H   Γ+φ ⊢ ψ   Δ ⊢ φ MP
 φ ⊢ φ           Γ+Δ ⊢ ψ

Terug naar de inhoudsopgave

Antecedentloze implicatieregels

                  H
 Γ ⊢ ψ     φ ⊢ φ &I
   Γ+φ ⊢ ψ & φ &Er
     Γ+φ ⊢ ψ  →I
    Γ ⊢ φ → ψ

Hiermee zijn de volgende regels afgeleid:

  Γ ⊢ ψ  →E0     Γ ⊢ ψ   →I0
 Γ+φ ⊢ ψ       Γ ⊢ φ → ψ

Terug naar de inhoudsopgave

De bi-implicatie

We definiëren het connectief bi-implicatie als volgt:

 Definitie ↔ :  φ ↔ ψ ≡ (φ → ψ) & (ψ → φ)

De logische wetten voor de bi-implicatie leiden we af:

  Γ+φ ⊢ ψ  →I       Δ+ψ ⊢ φ  →I
 Γ ⊢ φ → ψ         Δ ⊢ ψ → φ &I
   Γ+Δ ⊢ (φ → ψ) & (ψ → φ) def↔
         Γ+Δ ⊢ φ ↔ ψ

Dit levert de afgeleide bewijsregel ↔I:

 Γ+φ ⊢ ψ   Δ+ψ ⊢ φ ↔I
    Γ+Δ ⊢ φ ↔ ψ

Vervolgens de afleiding van de introduktieregels:

        Γ ⊢ φ ↔ ψ       def↔            Γ ⊢ φ ↔ ψ      def↔
  Γ ⊢ (φ → ψ) & (ψ → φ) &Er        Γ ⊢ (φ → ψ) & (ψ → φ) &El
        Γ ⊢ φ → ψ →E                    Γ ⊢ ψ → φ →E
         Γ+φ ⊢ ψ   Δ ⊢ φ MP              Γ+ψ ⊢ φ   Δ ⊢ ψ MP
             Γ+Δ ⊢ ψ                         Γ+Δ ⊢ φ

Dit geeft de afgeleide regels ↔El en ↔Er:

 Γ ⊢ φ   Δ ⊢ φ ↔ ψ ↔El      Γ ⊢ ψ   Δ ⊢ φ ↔ ψ ↔Er
      Γ+Δ ⊢ ψ                     Γ+Δ ⊢ φ

                            FV(x,φ)  FV→l                                    FV(x,ψ)  FV→r
                   def↔     FV(x,φ→ψ)     FV&l                      def↔     FV(x,φ→ψ)     FV&r
 φ↔ψ ≡ (φ→ψ)&(ψ→φ)      FV(x,(φ→ψ)&(φ→ψ)) ≡FVr     φ↔ψ ≡ (φ→ψ)&(ψ→φ)     FV(x,(φ→ψ)&(φ→ψ)) ≡FVr
                FV(x,φ ↔ ψ)                                     FV(x,φ ↔ ψ)

Dit geeft de afgeleide regels FV↔l en FV↔r:

   FV(x,φ)   FV↔l       FV(x,ψ)   FV↔r
 FV(x,φ ↔ ψ)          FV(x,φ ↔ ψ)

Terug naar de inhoudsopgave

De kwantoren

Voor de kwantoren ∀ en ∃ gelden de volgende wetten:

 Γ ⊢ φ   FV(x,φ)   NFVC(x,Γ) ∀I                            Γ ⊢ ∀xφ[x/x]  ∀E
        Γ ⊢ ∀xφ[x/x]                                        Γ ⊢ φ[t/x]

 Γ ⊢ φ[t/x]  FV(x,φ) ∃I                      Γ ⊢ ∀x(φ[x/x] → ψ[x/x])   NFV(x,ψ)  Δ ⊢ ∃xφ[x/x]  ∃E
     Γ ⊢ ∃xφ[x/x]                                               Γ+Δ ⊢ ψ

Terug naar de inhoudsopgave

Skolem axioma's

Als het bestaan van een term is afgeleid dan breiden we de taal uit met een symbool voor deze term. Dit gaat met de zogenaamde Skolemaxioma's.

∃wφ[w/w] → φ[cφ/w]

∀x(∃wφ[w/w] → φ[fφ(x)/w])[x/x]

∀x∀y(∃wφ[w/w] → φ[fφ(x,y)/w])[y/y][x/x]

Dit zijn de Skolemaxioma's die constanten, unaire en binaire functies definiëren als gevolg van een existentiële premisse met respectievelijk nul, één of twee vrije variabelen. De definiërende formule is de index van het symbool voor de nieuwe term. Op vergelijkbare wijze kun je functies met meer dan twee variabelen definiëren, maar hier hebben we voorlopig genoeg aan.

Terug naar de inhoudsopgave

Inductie naar de opbouw van termen en formules

We missen nog een belangrijke bewijsmethode. Termen en formules worden inductief opgebouwd. Dit brengt met zich mee dat je stellingen kunt bewijzen met inductie naar de opbouw van een term of met inductie naar de opbouw van een formule.

Inductie naar de opbouw van termen

De bewijsregel voor inductie naar de opbouw van termen:

 ⊤ ⊢ φ[x/t] inductie
   ⊤ ⊢ φ

De inductie hoeft alleen maar voor variabelen bewezen te worden, omdat we geen elementaire constanten of functie in het woordenboek voor termen hebben. Alle constanten en functies worden later aan de formele taal toegevoegd via Skolem-axioma's.

Voorbeelden

Als de te substitueren variabele identiek is met zijn substituut dan blijft de formule hetzelfde.

             611
 φ[x/x] ≡ φ

Deze afleidingsregel is af te leiden met behulp van inductie naar de opbouw van een term voor atomen en met inductie naar de opbouw van een formule voor samengestelde formules. Met dezelfde techniek is te bewijzen dat elke formule met een substitutieoperator identiek is met een formule zonder substitutieoperator.

Lemma: t[x/x] ≡ t

Inductie naar de opbouw van termen:
constante(t) dan NFVT(x,t) dan t[x/x] ≡ t
variabele(t) en t ≡ x dan t[x/x] ≡ x[x/x] ≡ x ≡ t
variabele(t) en t ≢ x dan t[x/x] ≡ t

Subformules

Ik definieer een subformule als een echte subformule: een formule is geen subformule van zichzelf. Atomen hebben dus geen subformules.

                     subformule⊡l                       subformule⊡r
 subformule(φ,φ ⊡ ψ)               subformule(ψ,φ ⊡ ψ)

        FV(x,φ)        subformuleQ
 subformule(φ,Qxφ[x/x])

 subformule(φ,ψ)  subformule(ψ,σ) transitief
         subformule(φ,σ)

Substitutie van subformules

    φ ≡ σ   
 σ[ψ/φ] ≡ ψ

    φ ≢ p  
 p[ψ/φ] ≡ p

           φ ≢ (σ ⊡ τ)         
 (σ ⊡ τ)[ψ/φ] ≡ σ[ψ/φ] ⊡ τ[ψ/φ]

          φ ≢ Qxσ       
 (Qxσ)[ψ/φ] ≡ Qx(σ[ψ/φ])

Terug naar de inhoudsopgave

Inductie naar de opbouw van atomen

 ⊤ ⊢ σ[⊤/φ]   ⊤ ⊢ σ[sRt/φ] inductie
          ⊤ ⊢ σ[p/φ]

Wat hier staat is het volgende: stel σ is een formule met φ als subformule. Dan geldt dat σ[p/φ] voor elk atoom p, als het geldt voor ⊤ en voor elke atomaire formule van de vorm sRt. Je moet σ hier zien als een formule met φ als variabele subformule.

φ[x/x] ≡ φ

φ[x/x] dus FV(x,φ).
syntax(φ) dan NFV(x,φ)
NFV(x,⊤)
(sRt)[x/x] ≡ (s[x/x]Rt[x/x]) ≡ (lemma) sRt

Inductie naar de opbouw van formules

 ⊤ ⊢ σ[p/φ]  σ[ψ/φ]+σ[τ/φ] ⊢ σ[ψ⊡τ/φ]  σ[ψ/φ]+FV(x,ψ) ⊢ σ[Qxψ[x/x]/φ] inductie
                                  ⊤ ⊢ σ

Vervolg bewijs φ[x/x] ≡ φ

(φ⊡ψ)[x/x] ≡ (253) φ[x/x]⊡ψ[x/x] ≡ (Inductiehypothese+293+294) φ⊡ψ
(Qyφ[y/y])[x/x] ≡ (254) Qyφ[y/y][x/x] ≡ (295+Inductiehypothese) Qyφ[y/y]

Hiermee is afleidingsregel 611 bewezen. Een bijzonder geval van ∀E leiden we hier mee af:

 ∀xφ[x/x] ∀E             611    
 φ[x/x]     φ[x/x] ≡ φ 297
          φ

Dit geeft de afleidingsregel

 ∀xφ[x/x] ∀E 
   φ

Deze regel noem ik ook ∀E.

Nog te bewijzen:

 Substitutiestelling: ⊢ φ ↔ ψ → σ[φ/τ] ↔ σ[ψ/τ]

Terug naar de inhoudsopgave

De axioma's van Zermelo en Fraenkel

Symbool voor Zermelo-Fraenkel

We introduceren hier de ∈-relatie. ∈ is een binaire relatie tussen twee termen. Het is een instantie van de metavariabele R. De introductieregels voor ∈ zijn de axioma's van Zermelo en Fraenkel. Deze volgen hierna in dit hoofdstuk.

• Relatie tussen termen: ∈

symbool	naam	categorie	ariteit	argument1	argument2	notatie
∈	is element van	relatie	2	term	term	(.) ∈ (.)

EXTENSIE - Het extensionaliteitsaxioma

 Definitie = :  s = t ≡ ∀z(z ∈ s ↔ z ∈ t)

 ∀x∀y∀z(x = y → y ∈ z → x ∈ z) Extensionaliteit,∈linkscongruent

Equivalentierelatie en identiteitsrelatie

 ⊢ ∀x(x = x) reflexief

 ⊢ ∀x∀y(x = y → y = x) symmetrisch

 ⊢ ∀x∀y∀z(x = y → y = z → x = z) transitief

 ⊢ ∀x∀y∀z(x ∈ y → y = z → x ∈ z) ∈rechtscongruent

Een relatie die reflexief, symmetrisch en transitief is heet een equivalentierelatie. Een equivalentierelatie die congruent is met betrekking tot elke relatie is een identiteitsrelatie.

Omdat ∈ de enige primitieve relatie is heeft de gedefinieerde =-relatie vanwege het extensionaliteitsaxioma (∈linkscongruent) alle eigenschappen van een identiteitsrelatie.

FV=

    FVT(x,s) FV∈r                           H
   FV(x,z∈s)   FV↔l   NFVT(z,s) ⊢ NFVT(z,s)   FVT(x,s) ≢I  
 FV(x,z∈s↔z∈t)           NFVT(z,s) ⊢ x≢z FVQ
      NFVT(z,s) ⊢ FV(x,∀z(z∈s↔z∈t))      FV→r
 NFVT(z,s) ⊢ FV(x,NFVT(z,t)→∀z(z∈s↔z∈t)) 
 
  FV(x,NFVT(z,s)→NFVT(z,t)→∀z(z∈s↔z∈t)) def=
               FV(x,s = t)

Hiermee is niet afgeleid:

  FVT(x,s)  FV=l
 FV(x,s = t)

Op dezelfde wijze is evenmin af te leiden:

  FVT(x,t)  FV=r
 FV(x,s = t)

Terug naar de inhoudsopgave

Reflexiviteit=

                                       22E
            H            H    FVT(z,z) FV∈l              NFV⊤
 z∈x ⊢ z∈x   z∈x ⊢ z∈x ↔I   FV(z,z∈x)   FV↔l   NFV(z,⊤) 321
   ⊤ ⊢ z ∈ x ↔ z ∈ x      FV(z,z∈x↔z∈x)       NFVC(z,⊤) ∀I
              ⊤ ⊢ ∀z(z ∈ x ↔ z ∈ x)     →I0
        ⊤ ⊢ NFVT(z,x)→∀z(z ∈ x ↔ z ∈ x)      →I0             22E             NFV⊤
   ⊤ ⊢ NFVT(z,x)→NFVT(z,x)→∀z(z ∈ x ↔ z ∈ x) def=   FVT(x,x)  FV=l  NFV(x,⊤) 321
                          ⊤ ⊢ x = x                FV(x,x = x)     NFVC(x,⊤) ∀I
                                               ⊤ ⊢ ∀x(x = x) def313
                                                ⊢ ∀x(x = x)

Substitutiestellingen

 ⊢ s = t → u[s/v] = u[t/v]

 ⊢ s = t → φ[s/v] = φ[t/v]

Terug naar de inhoudsopgave

LEEG - De lege verzameling

 ∃w∀x∀y(x ∈ y → x ∈ w)

 Skolem-axioma voor ∅ : ∃w∀x∀y(x ∈ y → x ∈ w) → ∀x∀y(x ∈ y → x ∈ ∅)

PAAR - Het paringsaxioma

 ∀x∀y∃w(x ∈ w & y ∈ w)

 Skolem-axioma voor {.,.} : ∀x∀y(∃w(x ∈ w & y ∈ w) → x ∈ {x,y} & y ∈ {x,y})

SOM - Het somverzamelingsaxioma

 ∀x∃w∀y∀z(z ∈ y → y ∈ x → z ∈ w)

 Definitie 741 ∪t ≡ ∪(t)

 Skolem-axioma voor ∪ : ∀x(∃w∀y∀z(z ∈ y → y ∈ x → z ∈ w) → ∀y∀z(z ∈ y → y ∈ x → z ∈ ∪x))

Definitie van vereniging s ∪ t:

 Definitie 742 s ∪ t ≡ (s)∪(t)

 Definitie (.)∪(.) : s ∪ t ≡ ∪{s,t}

Merk op dat er hier sprake is van overloading van het symbool ∪. Het is zowel een unaire als een binaire functie.

Terug naar de inhoudsopgave

MACHT - Het machtsverzamelingsaxioma

 Definitie ⊂ : s ⊂ t ≡ ∀x(x ∈ s → x ∈ t)

 ∀x∃w∀y(y ⊂ x → y ∈ w)

ONEINDIG - Het oneindigheidsaxioma

 Definitie suc(.) : suc(t) ≡ t ∪ {t,t}

 ∃w(∅ ∈ w & ∀x(x ∈ w → suc(x) ∈ w))

AFSCHEIDING - Het afscheidingsaxiomaschema

 NFV(w,φ) → ∀x∃w∀y(y ∈ x → φ → y ∈ w))

SUBSTITUTIE - Het substitutieaxiomaschema

 NFV(w,φ) → NFV(z,φ) → ∀x∃y(φ & ∀z(φ[z/y] → y = z)) → ∀z∃w∀y(∃x(x ∈ z) → φ → y ∈ w)

Het is hierbij mogelijk, maar niet noodzakelijk dat FV(x,φ), dat FV(y,φ) en dat freefor(z,y,φ). Je kunt substitutie ook zo definieren dat de laatste voorwaarde wel noodzakelijk is.

∈-INDUCTIE - Inductie naar de opbouw van een verzameling

 ∀y(∀x(x ∈ y → φ) → φ[y/x]) → ∀xφ

Terug naar de inhoudsopgave