1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
---
layout: linguistics
title: a natural semantic meta language
---
# a natural semantic meta language
This is a formal description of a universal¹ natural semantic meta-language, $Lₐ$. \
This is based off of the language described in [*Invitation to Formal Semantics*](https://eecoppock.info/bootcamp/semantics-boot-camp.pdf).
I intend to use this language in describing any formal semantics anywhere on this wiki.
¹: that is the goal, at least. It doesn't meet it now, and probably won't, ever. But it is good enough.
## Syntax
The following are formulas:
- variables: $x$, $y$, etc
- predicates: $\text{happy}$, $\text{loves}$, $\text{gives}$, etc
If $φ$ and $ψ$ are formulas, then so are
- $¬φ$, $[φ ∧ ψ]$, $[φ ∨ ψ]$, $[φ = ψ]$
- $☐φ$, $◇φ$, $∂φ$
If $φ$ is a formula and $x$ is a variable, then so are
- $[λx.φ]$, $∀x.φ$, $∃x.φ$, $ιx.φ$
If $[λx.φ]$ is a formula with $x$ a variable and $φ$ a formula, then $[λx.φ]$ is a function. \
If $[λx.φ]$ is a function and $φ$ is not a function, then $[λx.φ]$ is a function of arity $1$. \
If $[λx.φ]$ is a function and $φ$ is a function of arity $n$, then $[λx.φ]$ is a function of arity $n+1$. \
A function of arity $0$ is not a function. [note: this is clunky]
If $γ$ is a function of arity $n$ and $α$ is a term, then $γ(α)$ is a formula and a function of arity $n-1$. \
If $γ$ is a function of arity $n$, and $(α_1, ..., α_n)$ is a sequence of terms, then $γ(α_1, ..., α_n)$ is a formula. \
If $φ(t)$ is a formula with $t$ a bound variable of type $i$, then $φ^t$ is a formula. \
We freely omit brackets $[]$ when unambiguous.
<!--
If $p$ is a predicate and $t$ is a bound variable of type $i$, then $pᵗ$ is a ?????
If $[λt.φ]$ is a function and $t$ is a variable of type $i$, then $φᵗ$ is a function. \
-->
We additionally freely use the following derived forms:
- $[φ ⇒ ψ]$, $[φ ⇔ ψ]$, $[φ ⥽ ψ]$, $[φ ⊕ ψ]$, $[φ ↓ ψ]$, $[φ ↑ ψ]$
- $[φ ∪ ψ]$, $[φ ∩ ψ]$, $[φ ⧵ ψ]$, $[φ ⊆ ψ]$, $[φ ∈ ψ]$, $|φ|$...
## Types
The following are types:
- $e$: entities
- $t$: truth values
- $i$: time intervals
- $v$: events
- $???$: situations
If $σ$ and $τ$ are types, and $s$ is a possible world, then so are
- $⟨σ,τ⟩$: functions
- $⟨s,σ⟩$: functions from possible worlds
Note that possible worlds are not concrete in a type. It is impossible to directly quantify over them.
## Model
A model $M$ is an ordered pair $⟨D, W, I, g, c, <, ⊆⟩$, where
- $D$ denotes the *domain of discourse*, housing types that may be quantified over with $∀$ and $∃$.
- *All* types in $D$ may be quantified over. As such, we house possible worlds separately.
- $W$ denotes the *possible worlds* accessible from the current world
- $I$ denotes the *interpretation function* for individual predicates
- $I$ associates a denotation in $D_σ$ to all non-logical constants.
- $g$ denotes the *assignment function* ...
- $C$ denotes the *context of utterance* ...
- $C$ is a set of contexts $c$ such that $\text{now}(c) ∈ D_i$, $\text{speaker}(c) ∈ D_e$, and $\text{receiver}(c) ∈ D_e$
- $<$ denotes a *precedence relation* among the elements of $D_t$
- $<$ is a linear order: it is transitive, irreflexive, and total.
- $⊆$ denotes a *containment relation* among the elements of $D_t$
The domain of discourse $D$ is...
- $D_e = \{\#_e, x, y ...\}$
- $D_t = \{\#_t, 0, 1\}$
- $D_i = \{\#_i, \text{now}, ...\}$
- $D_{⟨σ,τ⟩} = \{\#_{⟨σ,τ⟩}, f_{⟨σ,τ⟩} ...\}$ (where $σ,τ$ are any types)
The $\#$ entity is the *undefined entity* and signals a presupposition error. \
$\#_{⟨σ,τ⟩}$ is the constant function $\#_{⟨σ,τ⟩}(x) = \#_τ$.
The ordered pair $⟨D,W⟩$ is also called a *frame*. This distinction is useful, on occasion.
## Semantics
$↝ ⟦⟧^M ...$
todo: use expressions and formulas consistently
## Predicates
- **variables**: if $x$ is a variable, then
- $⟦x⟧^M$ is $g(x)$
- **predicates**: if $π$ is a predicate, then
- $⟦π⟧^M$ is $I(π)$
- **predication**: if $π$ is a predicate with arity $n$ and $α_1, ... α_n$ are terms, then
- $⟦π(α_1, ... α_n)⟧^M = 1$ iff $⟨⟦α_1⟧^M, ..., ⟦α_n⟧^M⟩ ∈ ⟦π⟧^M$
- **complex terms**: if $γ$ is a function with arity $n$, and $α_1, ... α_n$ are terms, then
- $⟦γ(α_1, ..., α_n)⟧^M = 1$ iff $⟦γ⟧^M (⟨⟦α_1⟧^M, ..., ⟦α_n⟧^M⟩)$
- **connectives**: if $φ$ and $ψ$ are formulas, then
- $⟦¬φ⟧^M = 1$ iff $⟦φ⟧^M = 0$
- $⟦φ ∧ ψ⟧^M = 1$ iff $⟦φ⟧^M = 1$ and $⟦ψ⟧^M = 1$
- $⟦φ ∨ ψ⟧^M = 1$ iff $⟦φ⟧^M = 1$ or $⟦ψ⟧^M = 1$
- $⟦φ = ψ⟧^M = 1$ iff $⟦α⟧^M = ⟦ψ⟧^M$
Given an expression $φ$ and an expression $ψ$, we also have derived forms:
- **exclusive or**: $[φ ⊕ ψ]$ is defined as $[[φ ∨ ψ] ∧ ¬[φ ∧ ψ]]$
- **joint denial**: $[φ ↓ ψ]$ is defined as $¬[φ ∨ ψ]$
- **alternative denial**: $[φ ↑ ψ]$ is defined as $¬[φ ∧ ψ]$
- **material conditional**: $[φ ⇒ ψ]$ is defined as $[¬φ ∨ ψ]$
- **material biconditional**: $[φ ⇔ ψ]$ is defined as $[[φ ⇒ ψ] ∧ [ψ ⇒ φ]]$
- **strict conditional**: $[φ ⥽ ψ]$ is defined as $☐[φ ⇒ ψ]$
## Functions
- **abstraction**: if $α$ is an expression of type $τ$ and $x$ a variable of type $σ$, then
- $⟦λx_σ.α_τ⟧^M$ is a function $f_{⟨D_σ, D_τ⟩} : ∀o ∈ D_σ, f(o) = ⟦α⟧^{M[g[x ↦ o]]}$
- **application**: if $α$ is an expression of type $⟨σ,τ⟩$ and $β$ an expression of type $σ$, then
- $⟦α(β)⟧^M = ⟦α⟧^M(⟦β⟧^M)$
- **α-conversion**: if $[λx.φ](α)$ is a formula and $y$ does not appear free in $φ$, then
- $[λx.φ]$ can be converted to $[λy.φ[x := y]]$
- **β-reduction**: if $[λx.φ](α)$ is a formula and $α$ does not contain any free variables in $φ$, then
- $[λx.φ](α)$ can be reduced to $φ[x := α]$ <!-- (note: should be term?? occur later) -->
- **η-expansion**: if $φ$ is a formula such that $x$ does not appear free in $φ$ and $α$ is any term, then
- $φ$ can be expanded to $[λx.φ](α)$
## Quantification
- **universal quantification**: if $φ$ is a formula and $x$ a variable of type $σ$, then
- $⟦∀x.φ⟧^M = 1$ iff $∀k ∈ D_σ : ⟦φ⟧^{M[g[x ↦ k]]} = 1$
- **existential quantification**: if $φ$ is a formula and $x$ a variable of type $σ$, then
- $⟦∃x.φ⟧^M = 1$ iff $∃k ∈ D_σ : ⟦φ⟧^{M[g[x ↦ k]]} = 1$
todo: $\#$
## Presupposition
- **presupposition**: if $φ$ is an expression of type $σ$, then
- $⟦∂φ⟧^M = 1$ iff $⟦φ⟧^M = 1$ and $\#_σ$ otherwise
- **definitive**: if $φ$ is a formula and $x$ a variable of type $σ$, then
- $⟦ιx.φ⟧^M = 1$ iff $∃_1 d ∈ D_σ : ⟦φ⟧^{M[g[x↦d]]} = 1$ and $\#_σ$ otherwise
<!--
- **identity**: if $φ$ and $ψ$ are expressions of type $t$, then
- $⟦φ=ψ⟧^M = \#_t$ iff $⟦φ⟧^M = \#_t$ or $⟦ψ⟧^M = \#_t$
-->
## Temporal Semantics
$...$
The function $τ(e): ⟨σ, i⟩$ takes a term of any type $σ$ to its *temporal extent*.
## Intensional Semantics
$☐, ◇ ...$
## Event Semantics
$...$
|
