User:Ivo.pezlar/sandbox

Modal logic is a type of formal logic primarily developed in the 1960s.

A. Prior.

Possible structure elements

• Motivation
• Historical development
• Applications
• Formal definition
• Language / Syntax
• Inference Rules / Axioms / Proof theory
• Semantics
• Sample analyses / Examples
• Relation to classical logic
• Controversies
• See also
• Notes
• References
• Further reading
• External links

Development of modal logic

In addition to his non-modal syllogistic, Aristotle also developed a modal syllogistic in Book I of his Prior Analytics (chs 8–22).

Then we recursively define the truth of a formula at a world in a model:

• if $v(w,P)$ then $w\models P$
• $w\models \neg P$ if and only if $w\not \models P$
• $w\models (P\wedge Q)$ if and only if $w\models P$ and $w\models Q$
• $w\models \Box P$ if and only if for every element u of G, if w R u then $u\models P$
• $w\models \Diamond P$ if and only if for some element u of G, it holds that w R u and $u\models P$

Five modes of forming constructions

Variables are the only simple constructions; all other constructions have constituent parts. To define the class of constructions inductively, we must first specify the modes of forming constructions (from non-constructions and other constructions). There are altogether five such modes.

1. Trivialization

Where $X$ is an entity whatsoever, we can consider the trivial construction whose starting point, as well as outcome, is $X$ itself. Let us call this rudimentary construction the trivialization of $X$ and symbolize it as $^{0}\!X$. To carry $^{0}\!X$ out, one starts with $X$ and leave it, so to speak, as it is.

Examples: $^{0}3$ $v$-constructs $3$.

2. Execution

For any entity $X$ we shall also speak of the execution of $X$ and symbolize it as $^{1}\!X$. If $X$ is a construction, $^{1}\!X$ is $X$. (The construction consisting in executing, or carrying out, construction $X$ is clearly none other than $X$ itself.) If, on the other hand, $X$ is not a construction then $^{1}\!X$ is the (abortive) construction whose starting point is $X$ and which yields nothing. (A non-construction cannot be executed.) Thus if $X$ is a $v$-improper construction or not a construction at all, $^{1}\!X$ is $v$-improper; otherwise it $v$-constructs what is $v$-constructed by $X$.

Examples: $^{1}\!3$ is $v$-improper while $^{1}\!x$ (i.e., $x$) $v$-constructs the number assigned to $x$ by $v$.

3. Double execution

If what is constructed by $X$ is itself a construction, one can execute $X$ and go on and execute the result. We shall speak of this two-stage construction as the double execution of $X$ and symbolize it as $^{2}\!X$. For any entity $X$, the construction $^{2}\!X$ is $v$-improper (i.e., yields, relative to $v$, nothing at all) if $X$ is not itself a construction, or if it does not $v$-construct a construction, or if it $v$-constructs a $v$-improper construction. Otherwise $^{2}\!X$ $v$-constructs what is $v$-constructed by what is $v$-constructed by $X$. Note that $^{2}\!X$ is not the same as $^{1}\!$($^{1}\!X$): if $X$ is a construction, $^{1}\!X$ is the same as $X$, hence $^{1}\!$($^{1}\!X$) is the same as $^{1}\!X$, which in turn is $X$. Examples: $^{2}\!x$ is $v$-improper, and $^{2}\!$($^{0}\!x$) $v$-constructs the same as $x$, i.e., the number assigned by $v$ to $x$. To contrast trivialization with execution and double execution, let $c$ be a variable ranging over numerical constructions. Then $^{0}\!c$, $^{1}\!c$, and $^{2}\!c$ are three different constructions. $^{0}\!c$ $v$-constructs $c$ quite independently of $v$. $^{1}\!c$ $v$-constructs whatever numerical construction is assigned by $v$ to $c$. Finally, $^{2}\!c$ $v$-constructs whatever number (if any) is $v$-constructed by the construction which $v$ assigns to $c$. (Note that what is $v$-constructed by $^{2}\!c$ may depend on what $v$ assigns to variables other than $c$.)

4. Composition

Let $F$ be a construction of a mapping and $X$ a construction of an argument of the mapping. $F$ and $X$ can be combined into a compound construction which consists in executing $F$, thus obtaining a mapping, then executing $X$, thus obtaining an argument of the mapping, and then applying the mapping to the argument, thus obtaining the value (if any) of the former at the latter. We shall call this compound construction the 'composition' of $F$ and $X$, or briefly, $[FX]$. (Note that the compound symbol $'[FX]'$ names the construction, not the number constructed by it.)

The above is naturally generalized in the following way.

Let $X_{0},X_{1},...,X_{m}$ be arbitrary constructions. By the composition $[X_{0}X_{1}...X_{m}]$ of $X_{0},X_{1},...,X_{m}$ (in this order) we shall understand the construction which consists in: executing $X_{0}$ to obtain an $m$-ary mapping, executing $X_{1},...,X_{m}$ to obtain an $m$-tuple of entities, and then applying that mapping to the $m$-tuple. Thus for any $v$, $[X_{o}X_{1}...X_{m}]$ is $v$-improper if one of $X_{1},...,X_{m}$ is $v$-improper, or if $X_{0}$ does not $v$-construct a mapping which is defined at the $m$-tuple of entities $v$-constructed by $X_{1},...,X_{m}$. If $X_{0}$ does construct such a mapping then $[X_{0}X_{1}...X_{m}]$ $v$-constructs the value the mapping takes at the $m$-tuple.

Example: where $\times$ and $-$ are the multiplication and subtraction mappings, $[^{0}\!-[^{0}\!\times \;xx]^{0}\!3]$ is the (incomplete) construction of multiplying a number by itself and subtracting three from the result.

5. Closure

To introduce the last mode of compounding constructions let us start with an example. It is readily seen that (always assuming that x is the variable with range a defined above) the incomplete construction $[^{0}\!-[^{0}\!\times \;xx]^{0}\!3]$ $v$-constructs $1$ for any $v$ which assigns $2$ to $v$, $6$ for any $v$ which assigns $3$ to $x$, etc; it induces in this way a definite mapping from a into a (see Section 14). The incomplete construction $[^{0}\!-[^{0}\!\times \;xx]^{0}\!3]$ of a number can thus be turned into a complete construction of a mapping from numbers to numbers, namely the mapping which takes any value of the variable $x$ to the number (if any) constructed by $[^{0}\!-[^{0}\!\times \;xx]^{0}\!3]$ when $x$ takes that value. We shall call this complete construction `the $\alpha$-closure of $[^{0}\!-[^{0}\!\times \;xx]^{0}\!3]$ on $x$' and symbolize it as $[\lambda _{\alpha }x[^{0}\!-[^{0}\!\times \;xx]^{0}\!3]]$. (Note that the notation `$[\lambda _{\alpha }x[^{0}\!-[^{0}\!\times \;xx]^{0}\!3]]$' names the construction, not the numerical mapping produced by it.)

To generalize, let $\tau$ be a collection, $x_{1},...,x_{m}$ distinct variables ranging over the respective collections $\xi _{1},...,\xi _{m}$ and $v$ a valuation. Any construction $Y$ can be used in constructing a mapping from $\xi _{1},...,\xi _{m}$ into $\tau$; we shall call this latter construction the '$\tau$-closure of $Y$ on $x_{1},...,x_{m}$, or briefly $[\lambda _{\tau }x_{1},...,x_{m}\;Y]$. For any $v$, $[\lambda _{\tau }x_{1},...,x_{m}\;Y]$ $v$-constructs the mapping which takes any $X_{1},...,X_{m}$ of the respective types $Xi_{1},...,X_{m}$ into that member (if any) of $\tau$ which is $v(X_{1}/x_{1},...,X_{m}/x_{m})$-constructed by $Y$, where $v(X_{1}/x_{1},...,X_{m}/x_{m})$ is like $v$ except for assigning $X_{1}$ to $x_{1}$, and $X_{n}$ to $x_{m}$.

It is readily seen that for any $\tau$, $Y$, $x_{1},...,x_{m}$ and $v$, $[\lambda _{\tau }x_{1},...,x_{m}\;Y]$ is $v$-proper.

This completes the list of the five modes of forming constructions.

Source: FFL

Testing notation

• Trivialization ${}^{0}\!X$ is a construction that $v$-constructs object $X$, i.e., ${}^{0}\!X$ constructs $X$.

• Variable $x$ is a construction that constructs an object of the respective type depending upon a valuation $v$. We say it is $v$-constructed.

• Composition: If $C$ $v$-constructs a function $f$ of type $(\alpha \beta _{1}\ldots \beta _{n})$ and $C_{1},\ldots ,C_{n}$ $v$-construct objects $x_{1},\ldots ,x_{n}$ of type $\beta _{1}\ldots \beta _{n}$, respectively, then the Composition $[CC_{1}\ldots C_{n}]$ $v$-constructs the value of $f$ on the argument tuple $\langle c_{1},\ldots ,c_{n}\rangle$. Otherwise the composition $[CC_{1}\ldots C_{n}]$ is $v$-improper, i.e., it does not $v$-construct anything.

• Closure: If variables $x_{1},\ldots ,x_{n}$ range over $\beta _{1}\ldots \beta _{n}$, respectively and $C$ is a construction $v$-constructing $\alpha$-objects, then $[\lambda x_{1}\ldots x_{n}C]$ is construction called Closure. It $v$-constructs the following function $f$ of type $(\alpha \beta _{1}\ldots \beta _{n})$: let $\langle b_{1},\ldots ,b_{n}\rangle$ be a tuple of objects of type $\beta _{1}\ldots \beta _{n}$, respectively, and $v'$ be a valuation that associates $x_{i}$ with $b_{i}$ and is identical to $v$ otherwise. Then the value of function $f$ on argument tuple $\langle b_{1},\ldots ,b_{n}\rangle$ is the $\alpha$-object $v'$-constructed by $C$. If $C$ is $v'$-improper, then $f$ is undefined on $\langle b_{1},\ldots ,b_{n}\rangle$.

Further reading

• Marcus, Ruth Barcan, Modalities, OUP 1993.
• D.M. Gabbay, A. Kurucz, F. Wolter and M. Zakharyaschev, Many-Dimensional Modal Logics: Theory and Applications, Elsevier, Studies in Logic and the Foundations of Mathematics, volume 148, 2003, ISBN 0-444-50826-0. Covers many varieties of modal logics, e.g. temporal, epistemic, dynamic, description, spatial from a unified perspective with emphasis on computer science aspects, e.g. decidability and complexity.

Original version

Transparent Intensional Logic (frequently abbreviated as TIL) is a logical system created by Pavel Tichý. Due to its rich procedural semantics TIL is in particular apt for the logical analysis of natural language. From the formal point of view, TIL is a hyperintensional, partial, typed lambda-calculus. TIL applications cover a wide range of topics from formal semantics, philosophy of language, epistemic logic, philosophical, and formal logic. TIL provides an overarching semantic framework for all sorts of discourse, whether colloquial, scientific, mathematical or logical. The semantic theory is a procedural one, according to which sense is an abstract, pre-linguistic procedure detailing what operations to apply to what procedural constituents to arrive at the product (if any) of the procedure. TIL procedures, known as constructions, are hyperintensionally individuated. Construction is the single most important notion of Transparent Intensional Logic, being a philosophically well-motivated and formally worked-out conception of Frege’s notion of mode of presentation. Constructions, and the entities they construct, are organized into a ramified type theory incorporating a simple type theory. The semantics is tailored to the hardest case, as constituted by hyperintensional contexts, and generalized from there to intensional and extensional contexts. The underlying logic is a Frege-style function/argument one, treating functions, rather than relations or sets, as primitive, together with a Church-style logic, centred around the operations of functional abstraction and application.

Key constraints informing TIL approach to semantic analysis are compositionality and anti-contextualism. The assignment of constructions to expressions as their meanings is context-invariant. Depending on the sort of logical context in which a construction occurs, what is context-dependent is the logical manipulation of the respective meaning itself rather than the meaning assignment.

See also

• Intensional logic

Other modal logics

See also: Intensional logic

Significantly, modal logics can be developed to accommodate most of these idioms; it is the fact of their common logical structure (the use of "intensional" sentential operators) that make them all varieties of the same thing.

External links

• TIL home page
• Internet Encyclopedia of Philosophy: Rudolf Carnap's Modal Logic
• Stanford Encyclopedia of Philosophy:
  • "Modal logic" – by James Garson.
  • "Provability Logic" – by Rineke Verbrugge.
• Edward N. Zalta, 1995, "Basic Concepts in Modal Logic."

References

Category:Non-classical logic Category:Philosophical logic