Formules met kwantoren[bewerken | brontekst bewerken]

Vrije en gebonden variabelen worden variabelen en parameters[bewerken | brontekst bewerken]

Het is gangbaar om vrije en gebonden variabelen als één syntactische categorie te beschouwen. Ik liep hierbij echter stuk bij het afleiden van de regel dat een variabele vrij is in een vergelijking als die variabele vrij is in één van de leden van de vergelijking. Dit probleem wordt veroorzaakt door het voorkomen van een gebonden variabele in de definitie van gelijkheid. Daarom heb ik er voor gekozen om van vrije en gebonden variabelen aparte syntactische categorieën te maken. Bijkomend voordeel hiervan is dat de gebruikelijke voorwaarde, dat een term vrij moet zijn voor substitutie voor een variabele, komt te vervallen. Immers, nu vrije en gebonden variabelen altijd verschillend zijn, kan een vrije variabele door substitutie nooit gebonden raken. Vrije variabelen noem ik variabelen; gebonden variabelen noem ik parameters.

Voor de formulering van de afleidingsregels voor de substitutie van een parameter voor een variabele heb ik nieuwe syntactische categorieën nodig die de categorieën termen, atomen en formules uitbreiden. De reden is dat een component van een formule met een kwantor als hoofdvoegteken geen formule is! Er bevindt zich dan namelijk een parameter in de formule, die niet gebonden is. Voor de termen waarin een parameter voorkomt geldt hetzelfde. Zo'n formule waar een bindende kwantor ontbreekt noemt ik een halfformule en evenzo noem ik een term waarin een parameter voorkomt een halfterm. Voor metavariabelen voor parameters, halftermen, halfatomen en halfformules gebruik ik dezelfde tekens als bij variabelen, termen, atomen en formules: alleen met dit verschil dat de metavariabelen uit het woordenboek voor parameters cursief zijn en de gewone metavariabelen recht.

Symbolen[bewerken | brontekst bewerken]

Parameter: y_i.
Kwantoren: ∀, ∃
Operator voor substitutie parameter voor variabele in halfterm: [/]
Operator voor substitutie parameter voor variabele in halfformule: [/]
Predikaat van parameter: parameter
Predikaat van halftermen: halfterm
Predikaat van kwantoren: kwantor
Predikaat van halfformules: halfformule
Relaties tussen variabelen en halftermen: FVT, NFVT
Relaties tussen variabelen en halfformules: FV, NFV
Relaties tussen parameters en halftermen: BVT, NBVT
Relaties tussen parameters en halfformules: BV, NBV, QV, NQV

symbool	naam	categorie	ariteit	argument1	argument2	argument3	notatie
y_i		parameters	0
∀	voor alle	kwantoren	2	parameters	halfformules		∀(.,.)
∃	er is	kwantoren	2	parameters	halfformules		∃(.,.)
parameter	parameter	predikaten	1	parameters			parameter(.)
halfterm	halfterm	predikaten	1	halftermen			halfterm(.)
halfformule	halfformule	predikaten	1	halfformules			halfformule(.)
kwantor	kwantor	predikaten	1	kwantoren			kwantor(.)
[/]	bij . substitutie van . voor .	operatoren	3	halftermen	parameters	variabelen	(.)[./.]
[/]	bij . substitutie van . voor .	operatoren	3	halfformules	parameters	variabelen	(.)[./.]
FVT		relaties	2	variabelen	halftermen		FVT(.,.)
NFVT		relaties	2	variabelen	halftermen		NFVT(.,.)
FV		relaties	2	variabelen	halfformules		FV(.,.)
NFV		relaties	2	variabelen	halfformules		NFV(.,.)
BVT		relaties	2	parameters	halftermen		BVT(.,.)
NBVT		relaties	2	parameters	halftermen		NBVT(.,.)
BV		relaties	2	parameters	halfformules		BV(.,.)
NBV		relaties	2	parameters	halfformules		NBV(.,.)
QV		relaties	2	parameters	halfformules		QV(.,.)
NQV		relaties	2	parameters	halfformules		NQV(.,.)

Metasymbolen[bewerken | brontekst bewerken]

Metavariabelen voor parameters: w, x, y, z
Metavariabelen voor halftermen: s, t, u, v
Metavariabele voor halfproposities: p
Metavariabelen voor halfformules: σ, τ, φ, ψ
Metavariabele voor kwantoren: Q

metasymbool	naam	categorie	ariteit	argument1	argument2	notatie
w		parameters	0
x		parameters	0
y		parameters	0
z		parameters	0
s		halftermen	0
t		halftermen	0
u		halftermen	0
v		halftermen	0
p		halfproposities	0
σ	sigma	halfformules	0
τ	tau	halfformules	0
φ	phi	halfformules	0
ψ	psi	halfformules	0
Q		kwantoren	2	parameters	halfformules	Q(.,.)

Een kwantor is een operator op een parameter en een halfformule.

Informele beschrijving van de relaties en operatoren[bewerken | brontekst bewerken]

∀(x,φ) is de halfformule, die ontstaat door de parameter x in de halfformule φ te binden met de kwantor ∀.
∃(x,φ) is de halfformule, die ontstaat door de parameter x in de halfformule φ te binden met de kwantor ∃.
(t)[x/x] is de halfterm, die onstaat door de variabele x in de halfterm t te vervangen door de parameter x.
(φ)[x/x] is de halfformule, die ontstaat door de variabele x in de halfformule φ te vervangen door de parameter x.
FVT(x,t) betekent dat de variabele x voorkomt in de halfterm t.
NFVT(x,t) betekent dat de variabele x niet voorkomt in de halfterm t.
FV(x,φ) betekent dat de variabele x voorkomt in de halfformule φ.
NFV(x,φ) betekent dat de variabele x niet voorkomt in de halfformule φ.
BVT(x,t) betekent dat de parameter x voorkomt in de halfterm t.
NBVT(x,t) betekent dat de parameter x niet voorkomt in de halfterm t.
BV(x,φ) betekent dat de parameter x voorkomt in de halfformule φ.
NBV(x,φ) betekent dat de parameter x niet voorkomt in de halfformule φ.
QV(x,φ) betekent dat de parameter x in halfformule φ gebonden is.
NQV(x,φ) betekent dat de parameter x in halfformule φ niet gebonden is.
Q(x,φ) is de halfformule die ontstaat door de parameter x in de halfformule φ te binden met de kwantor Q.

Terug naar de inhoudsopgave

Parameters[bewerken | brontekst bewerken]

   index(i)   _boundIi              i ≢ j  _≢
 parameter(y_i)                    y_i ≢ y_j

Een parameter is geen term. Ik noem het een halfterm.

Halftermen[bewerken | brontekst bewerken]

   term(t)   _{termen⊂halftermen}    parameter(x) _{parameters⊂halftermen}
 halfterm(t)                     halfterm(x)

 unair(f)  halfterm(t)) _unairI          binair(f)  halfterm(s)  halfterm(t) _binairI
      halfterm(f(t))                          halfterm(f(s,t))

Variabele in halfterm[bewerken | brontekst bewerken]

De relatie FVT(x,t) geeft aan dat de variabele x voorkomt in de halfterm t.

 variabele(x) _22B
   FVT(x,x)

  FVT(x,t)  _22C
 FVT(x,f(t))

   FVT(x,s)   _22D
 FVT(x,f(s,t))

   FVT(x,t)   _22E
 FVT(x,f(s,t))

Geen variabele in een halfterm[bewerken | brontekst bewerken]

De relatie NFVT(x,t) geeft aan dat de variabele x niet voorkomt in de halfterm t.

           _22F
 NFVT(x,c)

  x ≢ y   _22G
 NFVT(x,y)

   NFVT(x,t)  _22H
 NFVT(x,f(t))

 NFVT(x,s)  NFVT(x,t) _22I
    NFVT(x,f(s,t))

Een variabele die voorkomt in een halfterm is niet-identiek aan een variabele die niet voorkomt in dezelfde halfterm:

 NFVT(x,t)  FVT(y,t) _≢I
        x ≢ y

We kunnen nu onze eerste stelling afleiden:

                      _22B
 NFVT(x,y)   FVT(y,y) _≢I
       x ≢ y

dus

 NFVT(x,y) _22J
   x ≢ y

Parameter in een halfterm[bewerken | brontekst bewerken]

De relatie BVT(x,t) geeft aan dat de parameter x voorkomt in de halfterm t.

          _22B
 BVT(x,x)

  BVT(x,t)  _22C
 BVT(x,f(t))

   BVT(x,s)   _22D
 BVT(x,f(s,t))

   BVT(x,t)   _22E
 BVT(x,f(s,t))

Geen parameter in een halfterm[bewerken | brontekst bewerken]

De relatie NBVT(x,t) geeft aan dat de parameter x niet voorkomt in de halfterm t.

           _22F
 NBVT(x,c)

  x ≢ y   _22G
 NBVT(x,y)

   NBVT(x,t)  _22H
 NBVT(x,f(t))

 NBVT(x,s)  NBVT(x,t) _22I
    NBVT(x,f(s,t))

Een parameter die voorkomt in een halfterm is niet-identiek aan een parameter die niet voorkomt in dezelfde halfterm:

 NBVT(x,t)  BVT(y,t) _≢I
        x ≢ y

We kunnen nu weer een stelling afleiden:

                      _22B
 NBVT(x,y)   BVT(y,y) _≢I
       x ≢ y

dus

 NBVT(x,y) _22J
   x ≢ y

Halfformules[bewerken | brontekst bewerken]

Het syntactisch object dat je krijgt als je een parameter de rol van term laat spelen bij de produktie van formules is geen formule, maar noem ik een halfformule.

                _{halfproposities⊂halfformules}
 halfformule(p)

                        _⊡I
 halfformule((φ) ⊡ (ψ))

Kwantoren[bewerken | brontekst bewerken]

Voor de kwantoren ∀ en ∃ gelden de volgende produktieregels:

             _∀I            _∃I
 kwantor(∀)     kwantor(∃)

 BV(x,φ)    NQV(x,φ) _QI
 halfformule(Q(x,φ))

De haakjes en de komma tussen de argumenten van de kwantor laat ik weer weg als er geen dubbelzinnigheid door kan ontstaan:

 Definitie 24C  Qxφ ≡ Q(x,φ)

Syntactische identiteit[bewerken | brontekst bewerken]

De predikaten, relaties en operatoren (en functies, connectieven en kwantoren, i.e. alle symbolen met positieve ariteit) voldoen aan de regel dat syntactisch identieke objecten verwisseld mogen worden. Dat wordt geformuleerd door afleidingsregels van de volgende vorm:

  FV(x,φ)   x ≡ y _≡FVl      FV(x,φ)   φ ≡ ψ _≡FVr
       FV(y,φ)                   FV(x,ψ)

Analoge regels gelden voor NFV, FVT, NFVT, BV, NBV, BVT, NBVT, QV, NQV, ∀, ∃ en alle versies van (.)[./.].

Rekenen met syntactische contexten[bewerken | brontekst bewerken]

Een halfformule wordt pas een formule als alle parameters, die in de halfformule voorkomen, ook daadwerkelijk gebonden worden door een kwantor. Daarom moet bij halftermen en halfformules een boekhouding worden bijgehouden van de voorkomende parameters. Deze boekhouding noem ik de syntactische context of kortweg de context. Ik geef een context aan met de letters A, B en C. Een speciaal geval is de lege context c. Ik kies hiervoor het symbool c van constante. Als de enige parameter in een halfterm of halfformule een constante is dan komen er geen parameters in voor en is het een term of een formule. Een parameter zelf is ook een context. Contexten concateneer je met het symbool +. Dat een context de context is van een halfterm of halfformule geef je aan met de relatie ⊢.

De parameter x moet gebonden worden om de rol van term te kunnen spelen.

             
 x ⊢ term(x)

  A ⊢ term(t)      A ⊢ term(s) B ⊢ term(t)
 A ⊢ term(f(t))      A+B ⊢ term(f(s,t))

  A ⊢ term(s) B ⊢ term(t)
    A+B ⊢ atoom(s R t)

  A ⊢ formule(φ) B ⊢ formule(ψ)
      A+B ⊢ formule(φ ⊡ ψ)

  A+x ⊢ formule(φ) 
 A ⊢ formule(Q(x,φ))

Om de laatste afleidingsregel gaat het allemaal. Zo wordt een gekwantiseerde formule gecreëerd. Als alle parameters in A gebonden zijn, heb je van een halfformule een formule gemaakt.

Voor contexten gelden nog een aantal rekenregels:

          _c-absorptieR
 A+c ≡ A

Contexten zien er als volgt uit: x, x+y, x+y+z,... Herhaling van een parameter verandert een context niet, de volgorde van de parameters is niet van belang en het samenvoegen van contexten is associatief.

          _{autoabsorptie}              _+commutatief
 A+A ≡ A                 A+B ≡ B+A

                   _+associatief
 A+(B+C) ≡ (A+B)+C

Tenslotte geldt nog:

 Definitie  c ⊢ formule(φ) ≡ formule(φ)

Syntactische relaties[bewerken | brontekst bewerken]

Variabele in halfformule[bewerken | brontekst bewerken]

Het predikaat FV(x,φ) geeft aan dat de variabele x voorkomt in de halfformule φ. Generieke binaire relatie tussen termen R.

   FVT(x,s)  _FVRl             FVT(x,t)  _FVRr
 FV(x,s R t)                FV(x,s R t)

   FV(x,φ)   _FV⊡l             FV(x,ψ)   _FV⊡r
 FV(x,φ ⊡ ψ)                FV(x,φ ⊡ ψ)

  FV(x,φ)  _FVQ 
 FV(x,Qxφ)

Geen variabele in halfformule[bewerken | brontekst bewerken]

Het predikaat NFV(x,φ) geeft aan dat de variabele x niet voorkomt in de halfformule φ.
Voor semiatomen:

          _NFV⊤    NFVT(x,s)  NFVT(x,t) ₂₈₁
 NFV(x,⊤)             NFV(x,s R t)

Voor samengestelde halfformules:

 NFV(x,φ)  NFV(x,ψ) ₂₈₂
    NFV(x,φ ⊡ ψ)

  NFV(x,φ)  ₂₈₃
 NFV(x,Qxφ)

Parameter in halfformule[bewerken | brontekst bewerken]

   BVT(x,s)  _BVRl            BVT(x,t)   _BVRr
 BV(x,s R t)                BV(x,s R t)

   BV(x,φ)   _BV⊡l             BV(x,ψ)   _BV⊡r
 BV(x,φ ⊡ ψ)                BV(x,φ ⊡ ψ)

  BV(x,φ)  _BVQ
 BV(x,Qxφ)

Geen parameter in halfformule[bewerken | brontekst bewerken]

          _NBVp            NBV(x,φ)  NBV(x,ψ) _NBV⊡
 NBV(x,p)                   NBV(x,φ ⊡ ψ)

  NBV(x,φ)   _NBVQ
 NBV(x,Qyφ)

Gekwantiseerde parameter in halfformule[bewerken | brontekst bewerken]

           _QV                 QV(x,φ)  _QVQ
 QV(x,Qxφ)                   QV(x,Qyφ)

   QV(x,φ)   _QV⊡l             QV(x,ψ)   _QV⊡r
 QV(x,φ ⊡ ψ)                QV(x,φ ⊡ ψ)

Niet gekwantiseerde parameter in halfformule[bewerken | brontekst bewerken]

          _NQVp            NQV(x,φ)  NQV(x,ψ) _NQV⊡
 NQV(x,p)                   NQV(x,φ ⊡ ψ)

 NQV(x,φ)  x ≢ y  _NQVQ
    NQV(x,Qyφ)

Terug naar de inhoudsopgave

Prioriteitsregels[bewerken | brontekst bewerken]

De volgende regels zijn geen axioma's maar definities van notaties.
Substitutie bindt sterker dan kwantoren en propositionele connectieven en kwantoren binden sterker dan propositionele connectieven:

 Definitie 261   Qxφ[s/t] ≡ Qx(φ[s/t])
 Definitie 262   (φ ⊡ ψ[s/t]) ≡ φ ⊡ (ψ)[s/t]
 Definitie 263   (Qxφ ⊡ ψ) ≡ Qx(φ) ⊡ ψ

Terug naar de inhoudsopgave

Identiek zijn van formules[bewerken | brontekst bewerken]

Voor substitutie-eliminatie hebben we regels voor de syntactische identiteit van formules nodig. De identiteitsrelatie van formules is reflexief, transitief en symmetrisch:

       _≡reflexief   φ ≡ ψ   ψ ≡ σ _{≡transitief}  φ ≡ ψ _≡symmetrie
 φ ≡ φ                 φ ≡ σ                 ψ ≡ φ

Identiteit van termen zet zich voort in atomen.

     s ≡ v      ₂₉₁       t ≡ v      ₂₉₂
 s R t ≡ v R t       s R t ≡ s R v

Hierbij is in de premisse ≡ een relatie tussen termen en in de conclusie een relatie tussen atomen.
Als twee formules identiek zijn dan kun je de één voor de ander substitueren. Dat geldt zowel voor atomen als voor samengestelde formules:

      φ ≡ σ     ₂₉₃               ψ ≡ σ      ₂₉₄
 φ ⊡ ψ ≡ σ ⊡ ψ               φ ⊡ ψ ≡ φ ⊡ σ

        φ ≡ ψ        ₂₉₅           φ ≡ ψ      ₂₉₆
 Qxφ[x/x] ≡ Qxψ[x/x]          φ[s/t] ≡ ψ[s/t]

We kunnen de identiteitsrelatie elimineren met behulp van:

 φ  φ ≡ ψ ₂₉₇
    ψ

Terug naar de inhoudsopgave

Niet-identiek zijn van formules[bewerken | brontekst bewerken]

In de axioma's voor substitutie van formules gebruiken we premissen waarin gesteld wordt dat formules niet-identiek zijn. De definitie van het niet-identiek zijn van formules gaat rechttoe rechtaan.

Formules zijn verschillend als ze een verschillend hoofdvoegteken hebben. Het hoofdvoegteken van een formule is het voegteken dat het laatste is toegevoegd bij de opbouw van die formule. Zijn de hoofdvoegtekens gelijk dan zijn formules verschillend als ten minste één van de componenten verschillend is. Dit zet zich door tot de atomen, die verschillen als de variabelen verschillend zijn. Formules met een hoofdvoegteken zijn niet-identiek met een atoom.

 φ ≢ ψ _≢symmetrie
 ψ ≢ φ

De atomen:

             _2A1
 a ≢ (ψ ⊡ σ)

             _2A2
 a ≢ Qxψ[x/x]

            _2A3
 ⊤ ≢ s R t

De hoofdvoegtekens:

                _2A4
 φ & ψ ≢ σ ∨ τ

                _2A5
 φ & ψ ≢ σ → τ

                 _2A6
  φ & ψ ≢ σ ≢ τ

                 _2A7
 φ & ψ ≢ (σ ≡ τ)

                  _2A8
 φ ⊡ ψ ≢ Qxσ[x/x]

                _2A9
 φ ∨ ψ ≢ σ → τ

                _2AA
 φ ∨ ψ ≢ σ ≢ τ

                 _2AB
 φ ∨ ψ ≢ (σ ≡ τ)

                _2AC
 φ → ψ ≢ σ ≢ τ

                 _2AD
 φ → ψ ≢ (σ ≡ τ)

                   _2AE
 (φ ≢ ψ) ≢ (σ ≡ τ)

                     _2AF
 ∀xφ[x/x] ≢ ∃xψ[x/x]

de inductiestappen:

       φ ≢ σ       _2AG                ψ ≢ σ       _2AH
 (φ ⊡ ψ) ≢ (σ ⊡ ψ)              (φ ⊡ ψ) ≢ (φ ⊡ σ)

        φ ≢ ψ        _2AI            x ≢ y        _2AJ
 Qxφ[x/x] ≢ Qxψ[x/x]        Qxφ[x/x] ≢ Qyφ[y/y]

Terug naar de inhoudsopgave

Substitutie parameter voor een variabele[bewerken | brontekst bewerken]

Metavariabelen voor parameters zijn cursief en metavariabelen voor variabelen zijn recht. Variabelen hebben altijd een index. De metavariabelen c, f en x hebben nooit een index.

We laten haakjes waar mogelijk weg:

 Definitie 242 (φ)[x/x] ≡ φ[x/x]

De substitutie is gedefinieerd met de volgende equivalenties:

            ₂₄₃
 c[x/x] ≡ c

            ₂₄₄
 x[x/x] ≡ x

    x ≢ y    ₂₄₅
 y[x/x] ≡ y

             ₂₄₆
 ⊤[x/x] ≡ ⊤

                        ₂₄₇
 f(s)[x/x] ≡  f(s[x/x])
 
                                 ₂₄₈
 f(s,t)[x/x] ≡  f(s[x/x],t[x/x])

                                ₂₄₉
 (s R t)[x/x] ≡ s[x/x] R t[x/x]

                                  _24A
 (φ ⊡ ψ)[x/x] ≡ (φ[x/x] ⊡ ψ[x/x])

                         _24B
 (Qyφ)[x/x] ≡ Qy(φ[x/x])

Bij de 24B maakt het geen verschil of x ≢ y of x ≡ y.

Terug naar de inhoudsopgave

Substitutie van termen in formules[bewerken | brontekst bewerken]

Substitutie geeft aparte formules.

Geen syntactische voorwaarden bij substitutie[bewerken | brontekst bewerken]

                   _substitutieI
 formule((φ)[s/t])

De afleidingsregels ∀E en ∃I hebben wel syntactische premissen. Dit komt aan de orde bij de logische wetten.

Eigenschappen van substitutie[bewerken | brontekst bewerken]

We laten de haakjes om φ weer weg wanneer dat niet tot dubbelzinnigheid leidt.

 Definitie 251 φ[s/t] ≡ (φ)[s/t]

Substitutie in atomen distribueert over de termen in het atoom:

                                ₂₅₂
 (s R t)[u/v] ≡ s[u/v] R t[u/v]

Hier is de substitutie in het linkerlid substitutie van termen in een formule en in het rechterlid substitutie in termen.
Substitutie distribueert over propositionele connectieven voorzover de te vervangen variabele voorkomt in de argumenten van het connectief:

                                ₂₅₃
 (φ ⊡ ψ)[s/t] ≡ φ[s/t] ⊡ ψ[s/t]

De substitutie-operator commuteert met kwantoren omdat parameters een aparte syntactische categorie vormen:

                          ₂₅₄
 (Qxφ)[s/t] ≡ Qx(φ[s/t])

Terug naar de inhoudsopgave

Stellingen[bewerken | brontekst bewerken]

Een stelling is een relatie tussen een context en een formule, die noteert dat die formule afleidbaar is uit de betreffende context. Een context is een rij formules. De formules in de context heten ook wel hypothesen. De afleidbaarheidsrelatie wordt weergegeven met het symbool ⊢. Γ ⊢ φ spreek je uit als: φ is afleidbaar uit Γ. De relatie ⊢ bindt zwakker dan kwantoren en propositionele connectieven.

Symbolen[bewerken | brontekst bewerken]

Operatie op contexten: +
Predikaat van contexten: context
Relatie tussen een variabele en een context: NFVC
Relatie tussen een context en een formule: ⊢
Relatie tussen contexten: ≡

symbool	naam	categorie	ariteit	argument1	argument2	notatie
+	plus	operatoren	2	contexten	contexten	(.)+(.)
context	context	predikaten	1	contexten		context(.)
NFVC		relaties	2	variabelen	contexten	NFVC(.,.)
≡	identiek	relaties	2	contexten	contexten	(.) ≡ (.)
⊢	bewijst	relaties	2	contexten	formules	(.) ⊢ (.)

Metasymbolen[bewerken | brontekst bewerken]

Metavariabelen voor contexten: Γ, Δ, Ε.

metasymbool	naam	categorie
Γ	gamma	contexten
Δ	delta	contexten
Ε	epsilon	contexten

Introductie van contexten[bewerken | brontekst bewerken]

Een context bouw je op met de volgende regels:

             _contextI                         _+I
 context(φ)                 context((Γ)+(Δ))

We laten de haakjes weer weg als er geen verwarring te duchten is. De operator + associeert naar rechts.

 Definitie 311  Γ+Δ ≡ (Γ)+(Δ)
 Definitie 312  Γ+Δ+Ε ≡ Γ+(Δ+Ε)

De propositie ⊤ is het atoom waar. Het speelt de rol van neutrale hypothese. Het toevoegen of opzeggen van de hypothese waar verandert de context niet. Een formule die geen enkele hypothese nodig heeft voor zijn afleiding heeft waar als context. Deze lege context laten we gemakshalve meestal weg. Als de context leeg is laten we zelfs het symbool voor de bewijsrelatie (⊢) weg. Dat is niet eenvoudig te definiëren. De lezer wordt geacht een goed verstaander te zijn. Bij de meeste syntactische afleidingen is er sprake van een lege context en noteren we alleen de conclusie van een stelling.

          _{⊤-absorptieR}
 Γ+⊤ ≡ Γ

 Definitie 313  (⊢ φ) ≡ (⊤ ⊢ φ)

Contexten zien er als volgt uit: φ, φ+ψ, φ+ψ+σ,... Herhaling van een hypothese verandert een context niet, de volgorde van hypothesen is niet van belang en het samenvoegen van contexten is associatief.

          _{autoabsorptie}              _+commutatief
 Γ+Γ ≡ Γ                 Γ+Δ ≡ Δ+Γ

                   _+associatief
 Γ+(Δ+Ε) ≡ (Γ+Δ)+Ε

Terug naar de inhoudsopgave

Prioriteitsregels[bewerken | brontekst bewerken]

De volgende regels zijn geen axioma's maar definities van notaties.

Vanwege het beperkte alfabet voor contexten kunnen we de haakjes om de argumenten weglaten zonder dat dit tot verwarring leidt. Vanwege de overloading van ≡ moeten er bij de volgende definities haakjes om de atomen die equivalent aan elkaar zijn.

 Definitie 26P   (Γ ⊢ φ) ≡ ((Γ) ⊢ (φ))
 Definitie 26Q   (Γ ≡ Δ) ≡ ((Γ) ≡ (Δ))

De bewijsrelatie bindt zwakker dan de equivalentierelatie van contexten, propositionele connectieven en substitutie:

 Definitie 26R   (Γ ≡ Δ ⊢ φ) ≡ ((Γ ≡ Δ) ⊢ φ)
 Definitie 26S   (Γ ⊢ φ ⊡ ψ) ≡ (Γ ⊢ (φ ⊡ ψ))
 Definitie 26T   (Γ ⊢ φ[s/t]) ≡ (Γ ⊢ (φ[s/t]))

Terug naar de inhoudsopgave

Variabele komt niet voor in context[bewerken | brontekst bewerken]

 NFV(x,φ)  ₃₂₁    NFVC(x,Γ)  NFVC(x,Δ)  ₃₂₂
 NFVC(x,φ)             NFVC(x,Γ+Δ)

Identiek zijn van contexten[bewerken | brontekst bewerken]

 Γ ≡ Δ  _≡symmetrie      Γ ≡ Δ  Δ ≡ Ε  _{≡transitief}
 Δ ≡ Γ                     Γ ≡ Ε

   Γ ≡ Ε    _L+-congruent
 Γ+Δ ≡ Ε+Δ

 Γ ⊢ φ    Γ ≡ Δ  _{⊢-congruent}
     Δ ⊢ φ

De laatste afleidingsregel is nodig om de identiteitsrelatie voor contexten te kunnen elimineren en is de eerste afleidingsregel met een niet-lege context.

+R-congruent[bewerken | brontekst bewerken]

                        Δ ≡ Ε   _L+-congruent            _+commutatief
           _+commutatief Δ+Γ ≡ Ε+Γ             Ε+Γ ≡ Γ+Ε _{≡transitief}
 Γ+Δ ≡ Δ+Γ                     Δ+Γ ≡ Γ+Ε _{≡transitief}
               Γ+Δ ≡ Γ+Ε

Hiermee is de volgende regel afgeleid:

      Δ ≡ Ε   _+R-congruent
    Γ+Δ ≡ Γ+Ε

Terug naar de inhoudsopgave
Verder naar logische wetten