Gebruiker:Otto ter Haar/logica2

Termen

Symbolen

• Constanten: c_φ. φ is hier een metavariabele voor een formule.
• Variabele: x_i. i is een metavariabele voor een index.
• Substitutie-operator voor termen: [/]
• Predicaten van termen: constante, variabele, term
• Predicaten van functies: unair, binair
• Relaties tussen termen: ≡, ≢
• Functies: f_φ, f_ψ. φ en ψ zijn weer metavariabelen voor formules.

symbool	naam	categorie	ariteit	argument1	argument2	argument3	notatie
cφ		constanten	0
xi		variabelen	0
constante	constante	predicaten	1	termen			constante(.)
variabele	variabele	predicaten	1	termen			variabele(.)
term	term	predicaat	1	termen			term(.)
≡	identiek	relaties	2	termen	termen		(.) ≡ (.)
≢	niet identiek	relaties	2	termen	termen		(.) ≢ (.)
[/]	bij . substitutie van . voor .	operatoren	3	termen	termen	termen	(.)[./.]
fφ		functies	1	termen			fφ(.)
fψ		functies	2	termen	termen		fψ(.,.)

Metasymbolen

• Metavariabele voor constanten: c.
• Metavariabelen voor variabelen: w, x, y, z.
• Metavariabelen voor unaire functies: f, g.
• Metavariabelen voor binaire functies: f, g.
• Metavariabelen voor termen: s, t, u, v.

metasymbool	categorie	ariteit	argument1	argument2	notatie
c	constanten	0
w	variabelen	0
x	variabelen	0
y	variabelen	0
z	variabelen	0
f	functies	1	termen		f(.)
g	functies	1	termen		g(.)
f	functies	2	termen	termen	f(.,.)
g	functies	2	termen	termen	g(.,.)
s	termen	0
t	termen	0
u	termen	0
v	termen	0

We onderscheiden de constanten, variabelen en functies uit de formele taal door indicering van de metavariabelen voor constanten, variabelen en functies. Constanten, variabelen en functies die eindsymbolen zijn hebben altijd een index. Het symbool dat de index heeft noem ik de romp van de index. De metavariabelen c, x en f hebben nooit een index. Het symbool c kan zowel een metavariabele voor cijfers als voor constanten zijn. Dit is een voorbeeld van overloading. De index van een variabele is altijd een index. De index van een constante of functie is het Skolem axioma dat de constante of de functie definieert. In principe kan elke formule een index vormen, maar alleen waar een definierend axioma bekend is heeft een dergelijke uitbreiding van de taal zin. Merk op dat ik hier het begrip index in twee betekenissen gebruik: enerzijds het syntactisch object waarvoor het predikaat index geldt en anderzijds het subscript dat samen met zijn romp een syntactisch object vormt. De index van de romp c of f is geen index maar een formule.

Toelichting

• c_φ is een constante. De romp van deze constante is c en de index is φ. Deze index φ zelf is een metavariabele voor een formule.
• (u)[s/t] is de term, die ontstaat door in de term u elke instantie van de term t te vervangen door de term s. Hoe dat vervangen gaat wordt vastgelegd in syntactische afleidingsregels.
• constante(c_φ) is de propositie die stelt dat de romp c met index φ een constante is.
• variabele(z) is de syntactische propositie die stelt dat z een variabele is.
• unair(g(.)) is de propositie die stelt dat g(.) een unaire functie is.
• binair(f_φ(.,.)) is de propositie die stelt dat f_φ(.,.) een binaire functie is.
• (g(x_j,c)) ≡ (f_ψ(w,c_φ)) is de propositie die stelt dat g(x_j,c) identiek is aan f_ψ(w,c_φ).

Vraag: Onder welke voorwaarden is deze propositie waar?

Antwoord: Als w ≡ x_j, c ≡ c_φ en g(.,.) ≡ f_ψ(.,.).

• (c) ≢ (x) is de propositie die stelt dat de constante c niet identiek is aan de variabele x.
• f_φ(u) is een term.
• f_ψ(u,v) is een term.

Categorieën van termen

Er bestaan drie verschillende categorieën termen: constanten, variabelen en samengestelde termen. De categorie samengestelde termen wordt niet als zodanig benoemd. Parameters zijn geen termen, maar halftermen.

Constanten

Elke constante is een term. Vooralsnog zijn er geen constanten gedefinieerd.

 constante(c) constanten⊂termen
    term(c)

Variabelen

Voor elke index is er een variabele:

   index(i)    varIi      variabele(x) variabelen⊂termen
 variabele(xi)              term(x)

Samengestelde termen

Unaire en binaire functies van termen zijn termen. Merk op dat er nog geen unaire of binaire functies gedefinieerd zijn! Hieronder staan axiomaschema's met metavariabelen waar nog geen eindsymbolen voor gedefinieerd zijn.

  term(t)  unairI
 term(f(t))

 term(s)  term(t) binairI
   term(f(s,t))

Identiek zijn van termen

We laten in formules de haakjes om de argumenten van relaties tussen termen weg:

 Definitie 221  s ≡ t ≡ (s) ≡ (t)

Een term is identiek met zichzelf.

       ≡reflexief
 t ≡ t

De identiteitsrelatie van termen is transitief en symmetrisch:

 s ≡ t   t ≡ u ≡transitief       s ≡ t ≡symmetrie
      s ≡ u                     t ≡ s

Terug naar de inhoudsopgave

Niet-identiek zijn van termen

De niet-identiek-relatie is symmetrisch:

s≢t _≢symmetrie

t≢s

Twee vrije variabelen zijn verschillend als hun indices verschillend zijn. Het niet-identiek zijn van twee variabelen kan met onderstaande regel worden afgeleid:

  i≢j   _i≢j

x_i≢x_j

Substitutie in termen

Als je in een term s elke instantie van de term u vervangt door de term t krijg je de term (s)[t/u]:

                223
 term((s)[t/u])

Bij constanten en variabelen geeft het geen verwarring als we bij de substitutie-operator de haakjes om de term waarin gesubstitueerd wordt weglaten:

 Definitie 224 s[t/u] ≡ (s)[t/u]

We identificeren een term waarin een substitutie wordt toegepast met het resultaat van de substitutie.

    s ≡ u   225        c ≢ u    226           x ≢ u   227
 s[t/u] ≡ t          c[t/u] ≡ c            x[t/u] ≡ x

       f(s) ≢ u       228              f(s,v) ≢ u           229
 f(s)[t/u] ≡ f(s[t/u])        f(s,v)[t/u] ≡ f(s[t/u],v[t/u])

De identiteitsrelatie tussen termen blijft behouden na substitutie:

      s ≡ t      22A
 s[u/v] ≡ t[u/v]

Terug naar de inhoudsopgave

Proposities

Symbolen

• Atomen: ⊤
• Propositionele relaties, connectieven: &, ∨, →, ≢, ≡
• Substitutie-operator voor term in propositie: [/]
• Substitutie-operator voor subpropositie in propositie: [/]
• Predikaat van propositionele connectieven: connectief
• Predikaten van proposities: atoom, propositie

symbool	naam	categorie	ariteit	argument1	argument2	argument3	notatie
⊤	waar	atoom	0
&	en	connectieven	2	proposities	proposities		(.) & (.)
∨	of	connectieven	2	proposities	proposities		(.) ∨ (.)
→	als . dan .	connectieven	2	proposities	proposities		(.) → (.)
≢	niet identiek	connectieven	2	proposities	proposities		(.) ≢ (.)
≡	identiek	connectieven	2	proposities	proposities		(.) ≡ (.)
connectief	connectief	predikaten	1	connectieven			connectief(.)
atoom	atoom	predikaten	1	proposities			atoom(.)
propositie	propositie	predikaten	1	proposities			propositie(.)
[/]	bij . substitutie van . voor .	operatoren	3	proposities	termen	termen	(.)[./.]
[/]	bij . substitutie van . voor .	operatoren	3	proposities	proposities	proposities	(.)[./.]

Connectieven zijn relaties tussen proposities.

Metasymbolen

• Metavariabele voor atomen: a
• Metavariabele voor relatie tussen termen: R
• Metavariabelen voor proposities: p, q, r
• Metavariabele voor propositionele connectieven: ⊡

metasymbool	naam	categorie	ariteit	argument1	argument2	notatie
a		atomen	0
R		relaties	2	termen	termen	(.) R (.)
⊡	punt in vierkant	connectieven	2	proposities	proposities	(.) ⊡ (.)
p		proposities	0
q		proposities	0
r		proposities	0

Toelichting

• ⊤ is een atomaire propositie.
• (p) → (q) is de propositie die ontstaat door de propositie p met het connectief → te verbinden met de propositie q.
• (p) ≡ ((⊤) ∨ (q)) is syntactische propositie die stelt dat p en (⊤) ∨ (q) dezelfde propositie zijn.
• (p)[s/t] is de propositie die ontstaat door in de propositie p elke instantie van de term t te vervangen door de term s.
• (p)[q/r] is de propositie die ontstaat door in de propositie p elke instantie van de propositie r te vervangen door de propositie q.
• connectief(&) is de propositie die stelt dat & een connectief is.
• atoom(r) is de propositie die stelt dat de propositie r atomair is.
• propositie ((p) ⊡ (⊤)) is de propositie die stelt dat (p) ⊡ (⊤) een propositie is.

Atomen

Merk op dat R een metavariabele is waar geen instantie voor is gedefinieerd.

          ⊤I      term(s)  term(t) RI
 atoom(⊤)         atoom((s) R (t))

 Definitie 231  s R t ≡ (s) R (t)

Atomen zijn formules:

  atoom(p)  atomen⊂formules
 formule(p)

Proposities

Voor de propositionele connectieven gelden de volgende produktieregels:

               &I                ∨I                →I                ≢I                ≡I
 connectief(&)    connectief(∨)     connectief(→)     connectief(≢)     connectief(≡)

 formule(φ)  connectief(⊡)  formule(ψ) ⊡I
          formule((φ) ⊡ (ψ))

De haakjes laat ik weg, als er geen verwarring door kan ontstaan, zoals wanneer φ en ψ atomair zijn.

 Definitie 241  (φ ⊡ ψ) ≡ (φ) ⊡ (ψ)

Prioriteitsregels

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

Connectieven associëren naar rechts:

Definitie 264 (φ ⊡ ψ ⊡ σ) ≡ (φ ⊡ (ψ ⊡ σ))

Het connectief & bindt sterker dan ∨, ∨ sterker dan →, → bindt sterker dan ≢ en ≢ sterker dan ≡:

Definitie 265 φ & ψ ∨ σ ≡ (φ & ψ) ∨ σ

Definitie 266 φ ∨ ψ & σ ≡ φ ∨ (ψ & σ))

Definitie 267 φ & ψ → σ ≡ (φ & ψ) → σ

Definitie 268 φ → ψ & σ ≡ φ → (ψ & σ)

Definitie 269 φ & ψ ≢ σ ≡ (φ & ψ) ≢ σ

Definitie 26A φ ≢ ψ & σ ≡ φ ≢ (ψ & σ)

Definitie 26B (φ & ψ ≡ σ) ≡ ((φ & ψ) ≡ σ)

Definitie 26C (φ ≡ ψ & σ) ≡ (φ ≡ (ψ & σ))

Definitie 26D φ ∨ ψ → σ ≡ (φ ∨ ψ) → σ

Definitie 26E φ → ψ ∨ σ ≡ φ → (ψ ∨ σ)

Definitie 26F φ ∨ ψ ≢ σ ≡ (φ ∨ ψ) ≢ σ

Definitie 26G φ ≢ ψ ∨ σ ≡ φ ≢ (ψ ∨ σ)

Definitie 26H (φ ∨ ψ ≡ σ) ≡ ((φ ∨ ψ) ≡ σ)

Definitie 26I (φ ≡ ψ ∨ σ) ≡ (φ ≡ (ψ ∨ σ))

Definitie 26J φ → ψ ≢ σ ≡ (φ → ψ) ≢ σ

Definitie 26K φ ≢ ψ → σ ≡ φ ≢ (ψ → σ)

Definitie 26L (φ → ψ ≡ σ) ≡ ((φ → ψ) ≡ σ)

Definitie 26M (φ ≡ ψ → σ) ≡ (φ ≡ (ψ → σ))

Definitie 26N (φ ≢ ψ ≡ σ) ≡ ((φ ≢ ψ) ≡ σ)

Definitie 26O (φ ≡ ψ ≢ σ) ≡ (φ ≡ (ψ ≢ σ))

• Terug naar de inhoudsopgave
• Verder naar formules met kwantoren
• Verder naar logische wetten