159
edits
Semantics: Difference between revisions
Save my half-finished explanation of lambdas
(Add a note to self to explain properties) |
(Save my half-finished explanation of lambdas) |
||
| Line 29: | Line 29: | ||
Now, we're ready to talk about notation. When you see something like <math>\exist x: \text{kato}_\text{w}(x). \exist e. \text{τ}(e) \subseteq \text{t} \land \text{neo}_\text{w}(x, \text{m}\mathrm{\acute{u}}\text{ao})(e)</math>, what you're looking at are a bunch of things from the domain of the model. A lot of these words (<math>\text{kato}</math>, <math>\text{neo}</math>, <math>\exist</math>, <math>\text{τ}</math>, <math>\land</math>) are '''functions'''; some others (<math>\text{m}\mathrm{\acute{u}}\text{ao}</math>) 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. | Now, we're ready to talk about notation. When you see something like <math>\exist x: \text{kato}_\text{w}(x). \exist e. \text{τ}(e) \subseteq \text{t} \land \text{neo}_\text{w}(x, \text{m}\mathrm{\acute{u}}\text{ao})(e)</math>, what you're looking at are a bunch of things from the domain of the model. A lot of these words (<math>\text{kato}</math>, <math>\text{neo}</math>, <math>\exist</math>, <math>\text{τ}</math>, <math>\land</math>) are '''functions'''; some others (<math>\text{m}\mathrm{\acute{u}}\text{ao}</math>) 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 | There's an important subtlety here: In languages like English and mathematics, you can use words to form statements such as "The sky is blue" and "<math>x + 1 = 2</math>", or you can use them to form smaller expressions, like "the author of this book" and "<math>\left\{1, 2, 3\right\}</math>". 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: | One interesting thing about this notation is that every expression has a '''type''', like some programming languages do. These include: | ||
| Line 50: | Line 50: | ||
It turns out we don't need variables for truth values or functions, so we don't assign them any. | It turns out we don't need variables for truth values or functions, so we don't assign them any. | ||
TODO: lambdas | What this language does have though, is a special syntax for writing functions, known as a '''lambda expression'''. They're easy to spot because they start with the Greek letter <math>\lambda</math>, and have two components: a variable name representing the function's input, and an expression representing the function's output. For example, <math>\lambda n.\ 2n + 1</math> is a function that takes a value <math>n</math> as its input, and outputs the value <math>2n + 1</math>. Since <math>n</math> is a variable of type <math>\text{e}</math>, and <math>2n + 1</math> is an expression of type <math>\text{e}</math>, we can tell that this function has type <math>\left\langle e, e \right\rangle</math>. Similarly, <math>\lambda e.\ \text{saqsu}(\text{j}\mathrm{\acute{i}})(e)</math> is a function of type … | ||
TODO: finish lambdas | |||
== Events == | == Events == | ||