Transparentní intensionální logika (TIL)
Marie Duží
http://www.cs.vsb.cz/duzi/

TIL Studijní podklady najdete na:
¡http://www.cs.vsb.cz/duzi/TIL.html
l
lZejména monografie:
¡http://www.cs.vsb.cz/duzi/aleph.pdf
¡
¡Duží M., Jespersen B., Materna P.: Procedural Semantics for Hyperintensional Logic  (2010)
(Anglická monografie)

Logická sémantika
¡Logika je věda o správném usuzování,
o umění správné argumentace
¡Jak ovlivňuje logická sémantika usuzování?
¡Jestliže usuzujeme, argumentujeme, používáme jazyk.
¡Abychom mohli správně usuzovat a argumentovat, musíme rozumět jednotlivým výrazům a větám, tj.
znát jejich význam.
¡To, jak přesně zachytíme význam v jazyce logiky, ovlivní podstatně, nakolik jsme schopni platné
úsudky formalizovat a dokazovat, nakolik jsme schopni usuzování automatizovat

Logická sémantika
¡Výroková logika
lOmezena na přiřazení T, F atomickým výrokům a skládání těchto atomických výroků pomocí logických
spojek – algebra pravdivostních hodnot
¡Predikátová logika
lNavíc – struktura atomických výroků – vlastnosti a vztahy mezi individui
lTěsnopis matematiky, zvládne mnohé, ale ne vše, zejména problémy s přirozeným jazykem

Logická sémantika
1.Některá prvočísla jsou sudá
2.Některá lichá čísla jsou sudá
3.Někteří chytří lidé jsou líní
lFormalizace v PL1:   $x [P(x) Ù Q(x)]
¡Otázky:
lProč mají věty (1), (2), (3) stejnou analýzu?
lJak je to možné, že výsledná formule má interpretace, ve kterých je pravdivá (modely) a
interpretace, ve kterých je nepravdivá, když je to analýza vět (1) a (2)?
lJak přispívá „překlad“ do formule PL1 k objasnění významu vět ?

Logická sémantika
1.Žádný starý mládenec není ženatý
2.Žádný starý mládenec není bohatý
¡ PL1:   "x [P(x) É ØQ(x)]  nebo
        Ø$x [P(x) Ù Q(x)]
¡Otázky:
lProč mají obě věty stejné dvě formalizace a která z nich je ta „správná“ ?
lVždyť (1) je analyticky pravdivá, zatímco (2) je empirické tvrzení, které je za jistých okolností
pravdivé či ne.

Nedokonalá analýza předpokladů
¡Vadí to?
¡Pokud bychom na základě dané formalizace vždy platně odvodili relevantní důsledky, byla by analýza
v pořádku
¡Můžeme vždy provádět korektní inference, korektní usuzování na základě analýzy premis v
predikátové logice (např. PL1 )?

Paradoxy
¡Nutně, 8 > 5
¡Počet planet je 8
¡ ––––––––––––––––––––
¡Nutně, počet planet je > 5
lModální logika, operátor □
lNesmíme substituovat v dosahu operátoru.
OK, ale proč?
l

Paradoxy
¡Je přikázáno doručit dopis
¡Jestliže je dopis doručen, pak je doručen nebo spálen
¡ –––––––––––––––––––––––––––––––––
¡Je přikázáno dopis doručit nebo spálit
lDeontické logiky, operátor O
lNesmíme substituovat v dosahu operátoru, OK, ale proč?
l

Paradoxy
¡Karel věří, že Praha má 1.048.576 obyvatel
¡1.048.576 = 100 000(16)
¡ –––––––––––––––––––––––––––––––––
¡Karel věří, že Praha má 100 000(16) obyvatel
lDoxastické a Epistémické logiky, operátory B, K
¡Karel ví, že 1+1=2
¡1+1=2 Û Sin(p) = 0
¡ –––––––––––––––––––––––
¡Karel ví, že Sin(p) = 0
lParadox logicko-matematické vševědoucnosti

Paradoxy
¡Karel počítá 2 + 5
¡2 + 5 = 7
¡ ––––––––––––––
¡Karel počítá 7
lLogiky postojů, … (?)
¡Oidipus hledá vraha svého otce
¡Oidipus je vrah svého otce
¡ –––––––––––––––––––––––––
¡Oidipus hledá Oidipa

Paradoxy
¡President ČR je manžel Ivany
¡Jan Sokol se chtěl stát presidentem ČR
¡ -------------------------------------------
¡Jan Sokol se chtěl stát manželem Ivany
¡
¡
¡
¡Tom si myslí, že francouzský král je moudrý
¡ –––––––––––––––––––––––––
¡Francouzský král existuje

Extenzionální vs. intenzionální kontext
¡Kdy je kontext extenzionální?
¡Kontext je extenzionální, když v něm platí pravidla substituce identit a existenční generalizace
¡A kdy tato pravidla platí?
¡V extenzionálním kontextu
lhmmm

TIL
¡Bohatý strom různých logik
lExtenzionálních, intenzionálních, …
lVyrostl zdola
¡Je to OK? Jedna univerzální logika?
¡TIL – universální logický rámec
l„top down“ přístup

Procedural semantics of TIL
n Expression
n
n
n Sense (procedure, construction)
n
n
n denotation
qOntology of TIL: ramified hierarchy of types
n
•15

3)  TIL: three kinds of context
nHyperintensional; construction of the denoted function is an object of predication
nTom computes Sin(p)
nTom believes that the Pope is wise but does not believe that the Bishop of Rome is wise
nIntensional; the denoted function itself is an object of predication
nSine is a periodic function
nTom wants to become the Pope
nExtensional; value of the denoted function is an object of predication
nSin(p) = 0
nThe Pope is wise.

•17
TIL Ontology (types of order 1)
n(non-procedural objects)
nBasic types
n truth-values {T, F} (o)
n universe of discourse {individuals} (i)
n times or real numbers (t)
n possible worlds (w)
nFunctional types (b a1…an)
partial functions (a1 ´ … ´ an) ® b
qPWS Intensions – entities of type ((at)w); atw

•18
Constructions
nVariables x, y, p, w, t, … v-construct
nTrivialization 0C constructs C (of any type)
qa fixed pointer, reference to C.
qIn order to operate on C, C needs to be grabbed, or ‘called’, first. Trivialization is such a
grabbing mechanism.
nClosure [lx1…xn X] ® (b a1…an)
n        a1        an   b
nComposition [F     X1 … Xn] ® b
n         (b a1…an)   a1             an
nExecution 1X, Double Execution 2X

•19
TIL Ontology (higher-order types)
nConstructions of order 1 (*1)
oà construct entities belonging to a type of order 1
o/ belong to *1 : type of order 2
nConstructions of order 2  (*2)
oà construct entities belonging to a type of order 2 or 1
o/ belong to *2 : type of order 3
nConstructions of order n  (*n)
oà construct entities belonging to a type of order n ³ 1
o/ belong to *n : type of order n + 1
nFunctional entities: (b a1…an) / belong to *n
n (n: the highest of the types to which b, a1, …, an belong)
n
qAnd so on, ad infinitum

explicit intensionalization and temporalization
nconstructions of possible-world intensions directly encoded in the logical syntax:
n lw lt […w….t…]
n0Happy ® (oi)tw; 0Pope ® itw
n lw lt [0Happywt 0Popewt] ® otw
nIn any possible world (lw) at any time (lt):
qTake the property of being happy (0Happy)
qTake the papal office (0Pope)
qExtensoinalize both of them (0Happywt, 0Popewt)
qCheck whether the holder of the Papal office (if any) is happy at that w, t of evaluation
([0Happywt 0Popewt])

Metoda analýzy
1.Přiřadíme typy objektům, o kterých výraz V mluví, tj. objektům označeným podvýrazy výrazu V
včetně V samotného.
2.Spojujeme konstrukce objektů ad 1) tak, abychom zkonstruovali objekt označený výrazem V.
q Přitom sémanticky jednoduchým výrazům přiřadíme Trivializaci označeného objektu
3.Provedeme typovou kontrolu, tj. sestrojíme derivační strom

Příklad: „Primátor Ostravy“
nTypy: Primátor(něčeho)/(((ii)t)w) – zkr. (ii)tw, Ostrava/i, Primátor_Ostravy/((it)w) – zkr. itw
nSyntéza: lwlt [0Primátorwt 0Ostrava]
nTypová kontrola:
n lw lt [[[0Primator     w]  t]   0Ostrava]
n          (((ii)t)w)      w
n         ((ii)t)        t
n (ii)          i
n            i
n      (it)
n ((it)w) zkráceně itw (individuový úřad)

„Primátor Ostravy je bohatý“
nTypy: Primátor(něčeho)/(ii)tw, Ostrava/i, Primátor_Ostravy/itw, (Být)Bohatý/(oi)tw
nSyntéza:
lwlt [0Bohatýwt  lwlt [0Primátorwt 0Ostrava]]wt]
nTypová kontrola (zkráceně):
n lw lt [[[0Bohatýwt  lwlt [0Primátorwt 0Ostrava]]wt]
n      (oi) i
n              o
n (ot)
n ((ot)w) zkráceně otw (propozice)
n

TIL vs. Montague’s IL
nIL is an extensional logic, since the axiom of extensionality is valid:   "x (Ax = Bx) ® A = B.
nThis is a good thing. However, the price exacted for the simplification of the language (due to
ghost variables) is too high;
qthe law of universal instantiation, lambda conversion and Leibniz’s Law do not generally hold, all
of which is rather unattractive.
nWorse, IL does not validate the Church-Rosser ‘diamond’. It is a well-known fact that an ordinary
typed l-calculus will have this property. Given a term lx(A)B (the redex), we can simplify the term
to the form [B/x]A, and the order in which we reduce particular redexes does not matter. The
resulting term is uniquely determined up to a-renaming variables.
nTIL does not have this defect; it validates the Church-Rosser property though it works with n-ary
partial functions
qthe functions of TY2 are restricted to unary total functions (Schönfinkel)

TIL: logical core
nconstructions + type hierarchy
(simple and ramified)
nThe ramified type hierarchy organizes all higher-order objects: constructions (types *n), as well
as functions with the domain or range in constructions.
nThe simple type hierarchy organizes first-order objects: non-constructions like extensions
(individuals, numbers, sets, etc.), possible-world intensions (functions from possible worlds) and
their arguments and values.

Hyperintensionality
nwas born out of a negative need, to block invalid inferences
qCarnap (1947, §§13ff); there are contexts that are neither extensional nor intensional (attitudes)
qCresswell; any context in which substitution of necessary equivalent terms fails is
hyperintensional
nYet, which inferences are valid in hyperintensional contexts?
nHow hyper are hyperintensions?
nWhich contexts are intensional / hyperintensional?
nTIL definition is positive:
a context is hyperintensional if the very meaning procedure is an object of predication
•26

Three kinds of context
nhyperintensional context: a meaning construction occurs displayed
qso that the very construction is an object of predication
qthough a construction at least one order higher need to be executed in order to produce the
displayed construction
nintensional context: a meaning construction occurs executed in order to produce a function f
qso that the whole function f is an object of predication
qmoreover, the executed construction does not occur within another displayed construction
nextensional context: the meaning construction is executed in order to produce a particular value
of the so-constructed function f at its argument
qso that the value of the function f is an object of predication
qmoreover, the executed construction does not occur within another intensional or hyperintensional
context.

Hyperintensionality
nExtensional logic of hyperintensions
nTransparency: no context is opaque
nThe same (extensional) logical rules are valid in all kinds of context;
qLeibniz’s substitution of identicals, existential quantification even into hyperintensional
contexts, …
nOnly the types of objects these rules are applied at differ according to a context
nAnti-contextualism: constructions are assigned to expressions as their context-invariant meanings