meowHEADmain

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
+$...$