--- 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. 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 := α]$ - **η-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 ## Temporal Semantics $...$ The function $τ(e): ⟨σ, i⟩$ takes a term of any type $σ$ to its *temporal extent*. ## Intensional Semantics $☐, ◇ ...$ ## Event Semantics $...$