160
edits
Semantics: Difference between revisions
Write most of the semantic calculus section
(use the formula thingy) |
(Write most of the semantic calculus section) |
||
| Line 25: | Line 25: | ||
== Semantic calculus == | == Semantic calculus == | ||
Now, we're ready to talk about notation. When you see something like ∃''x'' : kato<sub>w</sub>(''x''). ∃''e''. τ(''e'') ⊆ t ∧ neo<sub>w</sub>(''x'', múao)(''e''), what you're looking at are a bunch of things from the domain of the model. A lot of these words (kato neo ∃ τ ∧) are '''functions'''; some others (múao) represent literal "things" from the domain, like physical objects, people, and ideas, which we'll call '''individuals'''. Together, these words form an expression that shows you how to calculate the truth value of a specific sentence (in this case, {{Derani| |Neo sá kato múao}}), given that you have the model. | |||
There's a key difference here: In languages like English and mathematics, you can use words to form statements such as "The sky is blue" and "x + 1 = 2", or you can use them to form smaller expressions, like "the author of this book" and "{1, 2, 3}". But in the semantic notation we're looking at, there are no statements, only expressions, because the point of semantics is to examine the values that things denote, including the values of statements themselves. As such, it doesn't make sense to call this a "logic notation", because on its own, it can't form statements. Instead, we'll call it a '''semantic calculus'''. | |||
One interesting thing about this notation is that every expression has a '''type''', like some programming languages do. These include: | |||
* <math>\text{e}</math>, the type of individuals, which encompasses everything you can refer in Toaq. This is a rather broad category, so to help us get more specific when we need it, it includes a couple of subtypes: | |||
** <math>\text{v}</math>, the type of [[Event|events]] (things that can happen). More on them later. | |||
** <math>\text{i}</math>, the type of time intervals | |||
* <math>\text{t}</math>, the type of truth values, such as 'true' and 'false' | |||
* <math>\text{s}</math>, the type of worlds (frames of reference to evaluate claims by). More on them later. | |||
There are also functions, for which we use angle brackets: <math>\left\langle \text{v}, \text{t}\right\rangle</math> is the type of functions that take an event as their input, and return a truth value as their output. Functions can take or return other functions: for example, <math>\left\langle\left\langle\text{v}, \text{t}\right\rangle, \left\langle\text{i}, \text{t}\right\rangle\right\rangle</math> is the type of functions that take a function from events to truth values, and return a function from time intervals to truth values. | |||
To keep all these types straight, we give each a dedicated set of variables: | |||
* <math>a,\ b,\ c,\ \dots</math> for individuals | |||
** <math>e,\ e',\ e'',\ \dots</math> for events | |||
** <math>t,\ t',\ t'',\ \dots</math> for time intervals | |||
* <math>w,\ w',\ w'',\ \dots</math> for worlds | |||
It turns out we don't need variables for truth values or functions, so we don't assign them any. | |||
TODO: lambdas | |||
== Events == | == Events == | ||