LogickaAnalyza

nemůže být funkce F samotná, neboť F je vyššího typu než její
argumenty a hodnoty. Atd.
Musíme však hierarchii budovat na základě nějaké báze. Touto bází bude soubor vzájemně
disjunktních neprázdných množin. Prvky těchto bázových množin jsou atomické prvky.
Z hlediska analýzy běžného přirozeného jazyka pracujeme s tzv. epistémickou bází. Je to
soubor, ve kterém jistě potřebujeme mít množinu pravdivostních hodnot (značíme ο), dále
množinu individuí (universum diskursu, značíme ι), množinu časových okamžiků τ (které
mohou za předpokladu časového kontinua hrát také roli reálných čísel) a množinu možných
světů ω – logický prostor jazyka. Termín možný svět vyvolává často nepatřičné konotace,
jakoby šlo o fyzikálně alternativní světy. Tyto úvahy ponecháme doméně sci-fi.
Předpokládáme, že náš fyzikální svět je jen jeden. Ovšem v tomto světě může nastávat
v každém časovém okamžiku nekonečně mnoho událostí, faktů. Všechny tyto možnosti jsou
stejně objektivní, avšak v každém časovém okamžiku je pouze jedna z nich skutečně
realizovaná. Takovéto časové posloupnosti všech možných událostí (faktů) pak nazýváme
možnými světy a ta chronologie faktů, která je skutečně realizovaná, se nazývá aktuální svět.
Musíme si však uvědomit, že aktuální svět nemůžeme nikdy znát. Znamenalo by to znát
všechna fakta, všechny události, které nastaly, nastávají či budou nastávat, tedy boží
vševědoucnost.
Začneme tedy „v přízemí“, kde se nachází nestrukturované entity 1. řádu. Z hlediska
mereologického (vztah „celek – část“) mohou tyto entity být strukturované, tedy mohou
obsahovat prvky, části. Z hlediska pojmového (procedurálního, algoritmického) jsou však
8
nestrukturované, tyto entity nejsou instrukce (pokyny), ani jejich části nejsou instrukce. Již
zde v přízemí (na úrovni 1. řádu) máme nekonečnou hierarchii parciálních funkcí, které
přiřazují n-tici prvků jakýchkoli typů 1. řádu nanejvýš jeden prvek typu 1. řádu.
Poznamenejme však, že tento řád nemá nic společného s řádem predikátových logik.
Z hlediska predikátové logiky jsou všechny tyto entity, kromě atomických prvků bázových
typů, vyšších řádů.
V „prvním patře“ se nacházejí entity, které konstruují entity 1. řádu, nazýváme je
konstrukce 1. řádu a všechny tyto konstrukce tvoří typ řádu 2, značíme jej ∗1. Rovněž zde
máme nekonečnou hierarchii parciálních funkcí, které přiřazují n-ticím prvků typů řádu 2
nanejvýš jeden prvek typu řádu 2. Ve „druhém patře“ se nacházejí entity, které konstruují
entity 1. nebo 2. řádu, nazýváme je konstrukce 2. řádu a všechny tyto konstrukce tvoří typ
řádu 3, značíme jej ∗2. Rovněž zde máme nekonečnou hierarchii parciálních funkcí, které
přiřazují n-ticím prvků typů řádu 3 nanejvýš jeden prvek typu řádu 3. Atd., až do nekonečna.
Abychom zachovali homogenitu funkcionálních typů, budeme považovat každý typ řádu
menšího než n rovněž za typ řádu n.
Pojem konstrukce je snad nejdůležitějším pojmem TILu: Právě použití tohoto pojmu
umožňuje vysokou expresivní sílu TILu a můžeme říct, že v podstatě téměř všechny známé
„neřešitelné problémy“, se kterými se potýkají ostatní „denotační“ logické systémy, jsou
pomocí konstrukcí snadno a průzračně řešitelné. Podobnou sémantickou koncepci užívá
pouze řecký logik a informatik Yannis Moschovakis, který explikuje význam jako „ideální
algoritmus“. Uvědomme si však, že formule symbolické logiky jsou vlastně jakási schémata
takovýchto konstrukcí a kdykoli potřebujeme něco vypovídat a vlastnostech těchto formálních
systémů v rámci těchto systémů (tedy ne v metajazyce), potřebujeme nějakým způsobem
identifikovat právě způsoby konstruování označených entit. Proto např. potřeboval Kurt
Gödel zavést jedno-jednoznačné očíslování formulí a důkazů. Konstrukce je abstraktní
procedura, která na základě daných vstupů po konečném počtu kroků dodává určitý výstup
(nebo může také selhat). Nesmíme však zaměňovat proceduru s jejím provedením, které
probíhá v čase a prostoru. Procedura samotná je pouze jakýsi návod, recept, jak po konečném
počtu kroků dospět k žádanému výstupu (k označené entitě v případě výrazu). Části tohoto
návodu, jednotlivé kroky, mohou být opět pouze procedury (instrukce). Ovšem návod musí
zmiňovat ostatní (i neprocedurální) objekty, aby celá procedura mohla na základě vstupů
identifikovat výstupní objekt. Smyslem výrazů je tedy deklarovat, specifikovat takové
procedury, konstrukce jsou proto přiřazovány výrazům jako jejich význam. Empirické
procedury jsou ty, které mají dva vstupní parametry, a to stav světa (modální parametr ω) a
čas (temporální parametr τ). Tyto procedury konstruují intense, tj. parciální funkce, zobrazení
z možných světů do chronologií prvků libovolného typu α: (ω → (τ → α)), a jsou
přiřazovány empirickým výrazům jako jejich význam. Tak např. smyslem empirické věty je
specifikovat návod na vyhodnocení pravdivostních podmínek, tedy způsob, jak na základě
daného aktuálního stavu světa v určitém časovém okamžiku dospějeme (nebo i nedospějeme)
k pravdivostní hodnotě pravda či nepravda. Logická analýza věty (empirického výrazu)
spočívá v nalezení tohoto návodu, konstrukce propozice (intense). Její vlastní empirické
vyhodnocení, určení pravdivostní hodnoty dané proposice (extense výrazu = hodnoty intense)
v daném stavu světa a čase, tj. provedení zadané procedury, je již mimo oblast a priori
logické disciplíny.
Pavel Tichý definoval šest typů konstrukcí, které později Jiří Zlatuška rozšířil o další dva
typy pro práci s n-ticemi pro potřeby konceptuální analýzy. Uvedeme zatím pouze čtyři
základní typy konstrukcí. Musíme opět začít s jistými atomickými konstrukcemi, které
identifikují (zmiňují) vstupní objekty přímo, tj. „bez pomoci“ jiných instrukcí. Jsou to
proměnné a trivialisace. Zbylé dvě konstrukce jsou již více strukturované, obsahují jako části
jiné instrukce, jejichž výstupy používají pro konstrukci výstupního objektu. Jsou to
9
kompozice, která specifikuje způsob aplikace funkce na argument, a uzávěr, který udává, jak
pomocí lambda-abstrakce vytvořit funkci.
Než přistoupíme k přesné formulaci jednotlivých definic, shrneme ještě obsah tohoto
odstavce ve formě tabulky znázorňující nekonečnou ontologickou hierarchii entit:
I. Nestrukturované entity.
Entity typů 1. řádu: Nestrukturované (z algoritmického hlediska, i když mohou obsahovat
prvky a části, avšak jejich částmi nejsou nikdy instrukce).
a) Bázové (atomické) entity jsou prvky bázových množin:
• Pravdivostní hodnoty jsou prvky ο = {Pravda, Nepravda}
• Individua jsou prvky universa diskursu: ι = množina individuí
• Časové okamžiky nebo reálná čísla jsou prvky množiny τ = reálná čísla
• Možné světy jsou prvky logického prostoru ω = množina možných světů
b) Funkcionální (molekulární) entity 1. řádu jsou parciální funkce typu α1 ×…× αn → β,
kde α1, …, αn, β jsou typy 1. řádu. Používáme obrácenou notaci: (β α1…αn).
Nejdůležitějšími funkcemi z hlediska analýzy přirozeného jazyka jsou intense, tj. funkce
z možných světů do chronologií prvků daného typu α: ((ατ)ω), značíme zkráceně ατω.
Extense pak jsou entity, které nejsou funkce z možných světů.
II. Strukturované entity (z algoritmického hlediska): Procedury (instrukce, návody) nebo
takové entity, jejichž částmi jsou procedury (instrukce):
Entity typů 2. řádu: Konstrukce 1.řádových entit, všechny patří do typu 2. řádu ∗1.
• Proměnné x, y, w, t, p, …
– Konstruují v závislosti na valuaci v:
– pro každý typ α je k dispozici spočetně nekonečně mnoho proměnných x1, x2, …
– prvky typu α můžeme uspořádat do nekonečně mnoha posloupností:
a11, a12, a13, …
a21, a22, a23, …
…
ai1, ai2, ai3, …
…
– daná valuace v vybere jednu z těchto posloupností, např. ai1, ai2, ai3, ….
Proměnná x1 pak v-konstruuje první prvek posloupnosti vybrané valuací v, tj. ai1
Proměnná x2 v-konstruuje druhý prvek posloupnosti vybrané valuací v, tj. ai2, atd.
• Trivializace 0X objektu X konstruuje X beze změny.
• Uzávěr: [λ x1 ... xn C] → Funkci / (β α1...αn)
α1 αn β
• Kompozice: [C X1 … Xn] → Hodnotu funkce, tj. prvek typu β
(β α1...αn) α1 αn
Příklady:
λx [0+ x 01], x, 01, 05 / ∗1 ( ‘/’ = patří do typu)
10
x → τ, λx [0+ x 01] → (τ τ) (‘→ ‘ = konstruuje prvek typu)
[ λx [0+ x 01] 05 ] → 6 / τ
Entity typů 3. řádu: Konstrukce entit typu 2. nebo 1. řádu, všechny patří do typu 3. řádu ∗2.
Příklady:
0[λx [0+ x 01]] / ∗2, konstruuje [λx [0+ x 01]] / ∗1
Přičtení 1 je aritmetická procedura:
Ar / (ο ∗1) – třída aritmetických konstrukcí 1. řádu
[0Ar 0[λx [0+ x 01]] ] / ∗2, konstruuje hodnotu Pravda
Atd.
Nyní již můžeme přistoupit k přesným induktivním definicím.
Definice 1 (Typy řádu 1) – Jednoduchá hierarchie typů.
Nechť B je báze, tj. kolekce vzájemně disjunktních neprázdných množin.
i) Každý prvek báze B je (elementární) typ řádu 1 nad B.
ii) Nechť α, β1, ..., βn jsou typy řádu 1 nad B. Pak množina všech (parciálních) funkcí -
zobrazení z β1 × ... × βn do α, značená (α β1 ... βn), je (funkcionální) typ řádu 1 nad B.
iii) Typ řádu 1 nad B je pouze dle i) a ii).
Definice 2 (Konstrukce)
i) Atomické konstrukce jsou proměnné. Pro každý typ máme k dispozici spočetně
nekonečně mnoho proměnných, což jsou neúplné konstrukce, které konstruují objekt
příslušného typu v závislosti na valuaci. Říkáme, že proměnná v-konstruuje, kde v je
parametr valuace.
ii) Je-li X jakýkoli objekt (i konstrukce), pak 0X je konstrukce zvaná trivializace. 0X
konstruuje jednoduše X bez jakékoli změny.
iii) Nechť X je konstrukce, která v-konstruuje funkci F / (α β1 ... βn ) a nechť X1,...,Xn jsou
konstrukce, které v-konstruují entity b1 / β1,...,bn / βn. Pak [X X1...Xn] je konstrukce zvaná
kompozice (nebo tradičně aplikace). Jestliže funkce F není definována na n-tici objektů
b1,...bn, pak kompozice [X X1...Xn] je v-nevlastní (tj. nekonstruuje nic). Jinak v-konstruuje
hodnotu F na .
iv) Nechť x1,...,xn jsou navzájem různé proměnné a X konstrukce. Pak [λx1...xn X] je
konstrukce zvaná uzávěr (nebo tradičně abstrakce), která v-konstruuje následující funkci
F: Nechť v’ je valuace, která přiřazuje proměnným xi objekty bi (1 ≤ i ≤ n) a je jinak
stejná jako valuace v. Pak jestliže X je v’-nevlastní, je F nedefinována na . Jinak
je hodnotou funkce F na objekt v’-konstruovaný konstrukcí X.
v) Nic není konstrukce než dle i) - iv).
„Jazyk konstrukcí“ – transparentní okna do procedur, model = valuace proměnných,
„opravdová“ konstanta = trivializace. Valuace - vysvětlit
TIL je logika založená na teorii typů, což nám umožňuje vyhnout se nebezpečí
bludného kruhu a díky nekonečné hierarchii typů nejsme omezeni na určitý řád. Jednoduchá
teorie typů však není dostatečně silná, neboť potřebujeme zacházet s konstrukcemi jako s
‘plnoprávnými objekty’, jinými slovy, v přirozeném jazyce se můžeme vyjadřovat nejen o
‘normálních’ objektech 1. řádu, ale také o konstrukcích (pojmech) a konstrukce (pojmy)
mohou být nejen užívány, ale také zmiňovány. Proměnná nebo konstrukce však nemůže patřit
11
do svého oboru hodnot, tedy každá konstrukce je (patří do) určitého typu a konstruuje entitu
nižšího typu. Následující definice je v jistém smyslu zobecněním Russellovy rozvětvené
teorie typů.
Definice 3 (Rozvětvená teorie typů)
Nechť B je báze, tj. kolekce vzájemně disjunktních neprázdných množin.
T1 - typy řádu 1: Byly definovány definicí 1.
Cn - konstrukce řádu n
i) Nechť x je proměnná, jejíž obor proměnnosti je typ řádu n. Pak x je konstrukce řádu n.
ii) Nechť X je prvek typu řádu n. Pak 0X je konstrukce řádu n.
iii) Nechť X, X1, ..., Xm jsou konstrukce řádu n. Pak [X X1 ... Xm] je konstrukce řádu n.
iv) Nechť x1, ..., xm, X jsou konstrukce řádu n. Pak [λx1...xm X] je konstrukce řádu n.
Tn+1 - typy řádu n + 1
Nechť ∗n je množina všech konstrukcí řádu n.
i) ∗n a každý typ řádu n jsou typy řádu n + 1.
ii) Jestliže α, β1, ..., βm jsou typy řádu n + 1, pak (α β1 ... βm) jsou typy řádu n + 1.
iii) Nic není typ řádu n + 1 než dle i), ii).
Notace: Objekt O typu α budeme zapisovat jako α-objekt nebo O / α. Skutečnost, že
konstrukce C konstruuje objekt O / α budeme značit C → O / α, nebo pouze O → α.
Poznámky:
Pouze kompozice může být „špatným návodem“, při jehož užití nikam nedospějeme. Jinými
slovy, pouze kompozice může být (v-)nevlastní. Tento případ může nastat ze dvou důvodů:
a) Komponenta X konstruuje funkci F / (α β1 ... βn) a komponenty X1, …, Xn konstruují
β1-, …, βn- objekty, avšak funkce F není definována na těchto objektech
b) Některé z komponent X, X1, …, Xn „nedodaly vstupy/výstupy“, jsou v-nevlastní.
Případ, kdy komponenty X, X1, …, Xn konstruují objekty nevyhovujících typů, je dle definice
vyloučen.
Podle této definice tedy rozlišíme případ, kdy má sice výraz naprosto dobrý smysl, ale
neoznačuje žádný objekt (např. největší prvočíslo, či věta Největší prvočíslo je sudé), od
případu, kdy je výraz zcela nesmyslný, nevyjadřuje žádný pojem (např. “category mistake” -
Pětka je student, některá prvočísla jsou červená, …) a typová kontrola tak plní svůj účel.
Definice 4. Kvantifikátory
Kvantifikátory ∀α – obecný a ∃α – existenční nejsou „logické symboly“, ale funkcionální
objekty typu (ο(οα)). Je-li B → ο, x → α, pak konstrukce [0∀α λx B] konstruuje Pravdu,
pokud konstrukce [λx B] konstruuje celý typ α, jinak Nepravdu. Konstrukce [0∃α λx B]
konstruuje Pravdu, pokud konstrukce [λx B] konstruuje neprázdnou podmnožinu typu α,
jinak Nepravdu.
Singularizátor Iα je objekt typu (α(οα)). Konstrukce [0Iα λx B] konstruuje jediný prvek
množiny konstruované [λx B], pokud je tato množina singleton (jednoprvková), jinak je tato
konstrukce nevlastní, nekonstruuje nic.
Notace. Místo [0∀α λx...], [0∃α λx...] budeme používat obvyklou notaci ∀x..., ∃x... . Podobně
místo [0Iα λx...] budeme psát ιx... (to jediné x takové, že ...). Budeme rovněž používat
standardní infixní notaci bez trivializace pro logické spojky (funkce typu (οοο), resp. (οο)).
TIL je intenzionální logika, tedy je založená na sémantice možných světů.
Definice 5. Epistémická báze, intense, extense.
Báze v TILu je tzv. epistémická báze, což je kolekce {ο, ι, τ, ω}, kde ο je množina
pravdivostních hodnot, ι je universum diskursu a jeho prvky jsou individua, τ je množina
12
časových okamžiků (nebo také reálných čísel) a ω je množina možných světů. Empirické
výrazy označují intenze, což jsou funkce z možných světů a časových okamžiků do jistého
typu α. Tedy (α-)intenze jsou prvky typu ((ατ)ω), což budeme zkracovat jako ατω,
(α-)extense pak nejsou funkce z možných světů.
Notace: Budeme standardně používat proměnnou w s oborem proměnnosti ω a t s oborem
proměnnosti τ. Je-li X konstrukce konstruující intensi typu ατω, budeme psát Xwt místo
[[Xw]t].
Příklady typických intensí:
a) Propozice jsou zobrazení typu οτω. Empirické věty jako Největší hora je v Asii,
označují propozice.
b) Vztahy mezi prvky typů β1,...,βn jsou zobrazení typu (οβ1...βn)τω. Např. vztah (mezi
individui) být starší než je objekt typu (οιι)τω.
c) Vlastnosti individuí , jako být bohatý, být člověkem jsou objekty typu (οι)τω.
d) Individuové úřady (Churchovy individuální koncepty) jsou objekty typu ιτω. Příkladem
jsou objekty označené výrazy jako největší hora, president České republiky, starosta
města Dunedin. Liší se od vlastností (jako „být presidentem ČR“) tím, že v závislosti
na světech a časech nevracejí množinu individuí, ale nanejvýš jedno individuum.
e) Empirické funkce – atributy jsou objekty typu (αβ)τω. Příkladem jsou objekty
označené výrazy jako věk (daného individua), adresa (daného individua), president
(daného státu), děti (dané osoby), apod.
f) Vlastnosti propozic , jako být nutná, být analytická, být empirická, být pravdivá, atd.,
jsou objekty typu (ο οτω)τω.
Definice 6. Volné a vázané proměnné, uzavřená vs. otevřená konstrukce.
Nechť C je konstrukce a x proměnná. Nechť C obsahuje alespoň jeden výskyt proměnné x.
a)Jestliže C je x, pak x je volná v C.
b)Jestliže C je 0X, pak x je ο-vázaná v C.
c)Jestliže C je [XX1...Xn], pak x je volná v C pokud alespoň jeden výskyt x je volný v X
nebo X1,... nebo Xn.
d)Jestliže C je [λx1...xm X], pak x je volná v C pokud je různá od x1,...,xm a je volná v X.
Proměnné x1,...,xm jsou λ-vázané v C pokud nejsou ο-vázané v X.
e)Proměnná x je volná nebo ο- (λ-)vázaná v C pouze pokud nastane a) - d).
Definice 7 Logická analýza
(Z hlediska TIL) logická analýza (empirického) výrazu E spočívá v nalezení konstrukce P
vyjádřené výrazem E, která v-konstruuje objekt D označený výrazem E.
Je-li význam výrazu E úplný, tj. nezávislý na kontextu, ve kterém je výraz užit, pak E
vyjadřuje pojem, tj. uzavřenou konstrukci.
Analytické pojmy identifikují (konstruují) extense.
Empirické pojmy identifikují (konstruují) intense.
Pozn.:
V případě analytického (matematického) výrazu se může stát, že označený objekt chybí,
přesto může výraz E vyjadřovat svůj význam, tedy konstrukci.
Pravidlo β-redukce (neboli λ-transformace)
13
Základním pravidlem pro odvozování důsledků v λ-kalkulu je tzv. β-pravidlo. Rovněž při
odvozování v „jazyce konstrukcí“ budeme toto pravidlo potřebovat. Definujeme proto nyní
jeho objektuální podobu. Vysvětlíme nejprve jeho použití na příkladě. Chceme-li vypočítat
hodnotu nějaké funkce F na určitém argumentu a, pak tuto funkci na argument a aplikujeme.
Například hodnotou funkce následníka Succ / (ττ) na argumentu 1 bude 2, na argumentu 2
bude 3, atd. Funkci Succ však můžeme definovat pomocí uzávěru: 0Succ = λx [0+ x 01] neboli
zkráceně 0Succ = λx [x + 01]. Hodnotu funkce na argumentu konstruuje kompozice. Tedy
[0Succ 01] = [λx [x + 01] 01] = 02, [0Succ 02] = [λx [x + 01] 02] = 03, atd.
Ovšem jaký je smysl uzávěru [λx [x + 01]? Volně řečeno: Pro jakýkoli argument x přiřaď jako
hodnotu výsledek aplikace funkce + na tento argument x a číslo 1. Dodáme-li nyní určitý
argument a a chceme vypočítat hodnotu funkce na tomto argumentu, neznamená to nic jiného,
než dosadit a za x. Tedy musí platit, že [λx [x + 01] a] = [a + 01]. V žargonu programovacích
jazyků můžeme připodobnit uzávěr [λx [x + 01] deklaraci funkce s formálním parametrem x a
kompozici [λx [x + 01] a] volání funkce se skutečným parametrem a. Tedy
[λx [x + 01] 01] = [01 + 01] = 02, [λx [x + 01] 02] = [02 + 01] = 03, atd.
Dříve, než budeme moci definovat pravidlo β-redukce obecně, musíme definovat volné /
vázané proměnné a otevřené /uzavřené konstrukce:
Definice 8. Pravidlo β-redukce.
Nechť C je konstrukce, která obsahuje volné proměnné x1 → α1, …, xn → αn a nechť
C1 → α1,…, Cn → αn jsou konstrukce s volnými proměnnými y1,…, ym. Označme C(x1/C1…
xn/Cn) konstrukci, která vznikne z konstrukce C substitucí po řadě konstrukcí C1,…,Cn za
proměnné x1,…,xn takovou, že nedojde ke kolisi proměnných. To znamená, že žádná
z proměnných y1,…, ym se nestane po substituci vázanou. Pak řekneme, že konstrukce
C(x1/C1…xn/Cn) vznikla z konstrukce [ [λx1…xn C] C1…Cn ] aplikací pravidla β-redukce.
Tvrzení: Jestliže konstrukce C1,…,Cn v-konstruují po řadě objekty a1/α1,…,an/αn, pak je
pravidlo β-redukce [ [λx1…xn C] C1…Cn ] |– C(x1/C1…xn/Cn) korektní, tj, obě konstrukce jsou
ekvivalentní a v-konstruují hodnotu funkce v-konstruované [λx1…xn C] na argum