´ a´ logika - pˇrednaˇ
´ ska 1
Predikatov
7. 12. 2014
()
´ a´ logika - pˇrednaˇ
´ ska 1
Predikatov
7. 12. 2014
1/1
Matematicka´ logika
(teorie mnoˇzin), teorie modelu,
u,
˚ teorie dukaz
˚
˚ aritmeticke´
teorie, vyˇc´ıslitelnost/teorie rekurze, (dnes: v´ypoˇctova´
sloˇzitost)
´ ı logicke´ systemy
´
formaln´
a matematicke´ struktury
´
´ a´ logika prvn´ıho ˇradu;
´
klasick´y system:
predikatov
mnoho
´ u˚ (intuicionisticka´ logika, logiky vyˇssˇ ´ıch ˇrad
´ u,
dalˇs´ıch system
˚
´ ı logiky, fuzzy logika, substrukturaln´
´ ı logiky,
modaln´
´ ı logiky, . . . )
infinitarn´
()
´ a´ logika - pˇrednaˇ
´ ska 1
Predikatov
7. 12. 2014
2/1
´
Dveˇ roviny - semantika
a syntax
1
Syntax
´ eˇ v ramci
´
kalkulus koneˇcn´ych sekvenc´ı symbolu˚ (formaln
teorie mnoˇzin, pro koneˇcne´ jazyky ovˇsem staˇc´ı aritmetika
pˇrirozen´ych cˇ ´ısel)
ˇ a,
´ term, formule, dukazov´
pojmy: jazyk, promenn
y
˚
´
system/kalkulus,
axiom, teorie, dukaz,
˚
spornost/bezespornost, kompletnost, . . .
´
lze ji vybudovat bez ohledu na semantiku,
ovˇsem i pro
ˇ
ˇ
ˇ
dukazy
ciste syntaktick´ych tvrzen´ı casto vhodne´ pˇrej´ıt k
˚
´
´
semantick
e´ strance
2
´
Semantika
´ v teorii mnoˇzin)
struktury (definovany
pojmy: univerzum, realizace symbolu, struktura, ohodnocen´ı,
ˇ
platnost, splnenost,
model, hodnota formule, podstruktura,
...
cˇ asto definujeme s ohledem na syntax (napˇr. struktura pro
dan´y jazyk)
()
´ a´ logika - pˇrednaˇ
´ ska 1
Predikatov
7. 12. 2014
3/1
Syntax
´ e´ logiky prvn´ıho ˇradu
´
Jazyk L predikatov
obsahuje
1
logicke´ symboly
ˇ ych: v0 , v1 , v2 . . . (ˇcasto p´ısˇ eme
spoˇcetneˇ mnoho promenn´
x, y, z . . . )
ˇ ych se znaˇc´ı Var
mnoˇzina promenn´
´
zavorky
logicke´ spojky: ∧, ∨, →, ¬, ↔
´
kvantifikatory:
∀, ∃
2
mimologicke´ symboly
relaˇcn´ı symboly (s uvedenou aritou), jejich mnoˇzina se znaˇc´ı
RL
funkˇcn´ı symboly (s uvedenou aritou), jejich mnoˇzina se
znaˇc´ı FL
konstantn´ı symboly, jejich mnoˇzina se znaˇc´ı CL
3
pˇr´ıpadneˇ symbol = (pokud nen´ı uvedeno jinak, pracujeme v
jazyce s rovnost´ı)
()
´ a´ logika - pˇrednaˇ
´ ska 1
Predikatov
7. 12. 2014
4/1
´
Poznamky:
ˇZadn´
´ y symbol nemuˇ
˚ ze vystupovat ve v´ıce rol´ıch – tj.
uvedene´ mnoˇziny symbolu˚ jsou po dvou disjunktn´ı.
´
Arita kaˇzdeho
symbolu je pˇrirozene´ cˇ ´ıslo. Konstantn´ı
´
symboly muˇ
jako funkˇcn´ı symboly arity 0.
˚ zeme chapat
Jazyk zapisujeme cˇ asto pouze jako mnoˇzinu mimologick´ych
symbolu.
˚ Dalˇs´ı informace se dodaj´ı slovneˇ cˇ i jsou zˇrejme´ z
kontextu.
Pˇr´ıklad
Jazyk aritmetiky: L = {0, 1, +, ·, ≤}, kde 0, 1 jsou konstantn´ı
´ ı funkˇcn´ı symboly, ≤ binarn´
´ ı relaˇcn´ı symbol.
symboly, +, · binarn´
Pozor! S v´yjimkou symbolu = nemaj´ı funkˇcn´ı, relaˇcn´ı a
konstantn´ı symboly dan´y pevn´y v´yznam, ani aritu. Symbol +
tedy muˇ
˚ ze vystupovat (v ruzn´
˚ ych jazyc´ıch) jako konstanta, cˇ i
relace libovolne´ arity.
()
´ a´ logika - pˇrednaˇ
´ ska 1
Predikatov
7. 12. 2014
5/1
Definice (Induktivn´ı definice termu)
Bud’ L jazyk, mnoˇzina vˇsech termu˚ jazyka L se znaˇc´ı TermL . Je
ˇ ıc´ı nasleduj´
´
to nejmenˇs´ı mnoˇzina splnuj´
ıc´ı:
ˇ a´ je term).
Var ⊆ TermL (kaˇzda´ promenn
CL ⊆ TermL (kaˇzda´ konstanta je term).
Je-li t0 , . . . , tn−1 ∈ TermL a F ∈ L je funkˇcn´ı symbol arity n,
pak F (t0 , . . . , tn−1 ) ∈ TermL (aplikac´ı funkˇcn´ıho symbolu na
ˇ term).
jiˇz vytvoˇrene´ termy vznikne opet
()
´ a´ logika - pˇrednaˇ
´ ska 1
Predikatov
7. 12. 2014
6/1
´
Poznamky:
´ eˇ utvoˇren´y v´yraz pro (matematick´y)
Term je tedy spravn
”
objekt“.
´
ˇ znou notaci
M´ısto prefixn´ı notace +(x, y) cˇ asto uˇz´ıvame
beˇ
infixn´ı x + y.
Pˇr´ıklad
Termy jazyka aritmetiky jsou napˇr´ıklad
´ Zda
0, (x + 0) · (1 + y), ((0 + 1) + 0). Termy 1 a 1 + 0 jsou ruzn
˚ e.
´ z´ı na realizaci symbolu˚
v dane´ struktuˇre plat´ı 1 = 1 + 0 zaleˇ
´ struktuˇre (tedy neplat´ı to automaticky).
1, 0, + v teto
()
´ a´ logika - pˇrednaˇ
´ ska 1
Predikatov
7. 12. 2014
7/1
Definice (Atomicka´ formule)
´
Bud’ L jazyk. Atomicka´ formule pro jazyk L je zapis
tvaru
´ ı relaˇcn´ı symbol (R ∈ L, cˇ i R je =)
R(t0 , . . . , tn−1 ), kde R je n-arn´
a t0 , . . . , tn−1 ∈ TermL . Mnoˇzina vˇsech atomick´ych formul´ı pro
jazyk L se znaˇc´ı AFmL
´
Poznamky:
´ eˇ utvoˇren´y v´yraz pro
Atomicka´ formule je tedy spravn
”
´ tvrzen´ı“.
jednoduche´ (matematicke)
´
ˇ znou notaci
M´ısto prefixn´ı notace ≤ (x, y) cˇ asto uˇz´ıvame
beˇ
infixn´ı x ≤ y.
´ ı relaˇcn´ı symbol, pak R je atomicka´ formule.
Je-li R nularn´
()
´ a´ logika - pˇrednaˇ
´ ska 1
Predikatov
7. 12. 2014
8/1
Definice (Induktivn´ı definice formule)
Bud’ L jazyk. Mnoˇzina vˇsech formul´ı jazyka L se znaˇc´ı FmL . Je
ˇ ıc´ı nasleduj´
´
to nejmenˇs´ı mnoˇzina splnuj´
ıc´ı:
AFmL ⊆ FmL (atomicka´ formule je formule).
Bud’ ϕ, ψ ∈ FmL , x ∈ Var . Potom ϕ ∧ ψ, ϕ ∨ ψ, ϕ → ψ,
ϕ ↔ ψ, ¬ϕ, (∀x)ϕ, (∃x)ϕ jsou v FmL (z jiˇz vytvoˇren´ych
formul´ı dostaneme formuli aplikac´ı v´yrokov´ych spojek cˇ i
kvantifikac´ı).
´
Poznamky:
´ eˇ utvoˇren´y v´yraz pro (matematicke)
´
Formule je tedy spravn
”
tvrzen´ı“.
´
ˇ zna´ zjednoduˇsen´ı notace – napˇr. vhodn´ym
Pouˇz´ıvame
beˇ
´ ame
´
´
zpusobem
vynechav
zavorky.
˚
()
´ a´ logika - pˇrednaˇ
´ ska 1
Predikatov
7. 12. 2014
9/1
´
Semantika
´
´
Zakladn´
ım semantick´
ym pojmem je pojem struktury. Dana´
struktura urˇcuje v´yznam symbolu˚ jazyka.
Definice (Struktura)
Bud’ L jazyk. Struktura pro jazyk L je dvojice A = hA, LA i, kde
A 6= ∅; A se naz´yva´ univerzum/nosna´ mnoˇzina
´ ych a
LA je mnoˇzina realizac´ı funkˇcn´ıch, predikatov´
konstantn´ıch symbolu˚
´ ı relaˇcn´ı symbol, jeho realizace R A je
je-li R ∈ L n-arn´
ˇ a)
´ n-arn´
´ ı relace na A
(nejak
´ ı funkˇcn´ı symbol, jeho realizace F A je
je-li F ∈ L n-arn´
ˇ a)
´ n-arn´
´ ı funkce na A
(nejak
ˇ y)
je-li c ∈ L konstantn´ı symbol, jeho realizace c A je (nejak´
prvek A
realizace symbolu = je relace identity na A
()
´ a´ logika - pˇrednaˇ
´ ska 1
Predikatov
7. 12. 2014
10 / 1
Strukturu cˇ asto zapisujeme jako mnoˇzinu, nikoli jako
´
uspoˇradanou
dvojici.
Pˇr´ıklad
Struktura A = {N, 0N , 1N , +N , ·N , ≤N }, kde 0N , 1N , +N , ·N , ≤N jsou
ˇ zne´ sˇc´ıtan´
´ ı, nasoben´
´
´ an´
´ ı pˇrirozen´ych
po rˇadeˇ 0, 1, beˇ
ı a uspoˇrad
ˇc´ısel je strukturou pro jazyk aritmetiky.
()
´ a´ logika - pˇrednaˇ
´ ska 1
Predikatov
7. 12. 2014
11 / 1
Download

Predikátová logika