diff options
Diffstat (limited to 'ling/la.md')
| -rw-r--r-- | ling/la.md | 158 |
1 files changed, 158 insertions, 0 deletions
diff --git a/ling/la.md b/ling/la.md new file mode 100644 index 0000000..c483980 --- /dev/null +++ b/ling/la.md @@ -0,0 +1,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 +$...$ |