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