Intensional Logic: Types and Denotations

[dowty-wall-peters-1981] [Gal75]

Foundations for intensional logic following DWP Ch. 6. Ty is the recursive grammar of semantic types; Denot E W computes denotation domains from explicit entity (E) and index (W) type parameters and a type.

Key definitions

• Ty — semantic types: e, t, ⟨a,b⟩, ⟨s,a⟩
• Denot E W — denotation domains (DWP Def B.3), parameterized by entity and index types
• up, down — intension formation / extension extraction (DWP Rules B.14–B.15)

inductive Intensional.Ty : Type

Semantic types for Intensional Logic.

• e — entities
• t — truth values
• fn a b — functions ⟨a,b⟩
• intens a — intensions ⟨s,a⟩ (functions from indices to a-extensions)

The old Ty.s base type is replaced by the intens constructor: intensionality is a type-forming operation, not a separate domain.

• e : Ty
• t : Ty
• fn : Ty → Ty → Ty
• intens : Ty → Ty

@[implicit_reducible]

instance Intensional.instReprTy : Repr Ty

Equations

• Intensional.instReprTy = { reprPrec := Intensional.instReprTy.repr }

def Intensional.instReprTy.repr : Ty → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Intensional.instReprTy.repr Intensional.Ty.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Intensional.Ty.e")).group prec✝
• Intensional.instReprTy.repr Intensional.Ty.t prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Intensional.Ty.t")).group prec✝

@[implicit_reducible]

instance Intensional.instDecidableEqTy : DecidableEq Ty

Equations

• Intensional.instDecidableEqTy = Intensional.instDecidableEqTy.decEq

def Intensional.instDecidableEqTy.decEq (x✝ x✝¹ : Ty) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Intensional.instDecidableEqTy.decEq Intensional.Ty.e Intensional.Ty.e = isTrue ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.e Intensional.Ty.t = isFalse Intensional.instDecidableEqTy.decEq._proof_1
• Intensional.instDecidableEqTy.decEq Intensional.Ty.e (a ⇒ a_1) = isFalse ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.e a.intens = isFalse ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.t Intensional.Ty.e = isFalse Intensional.instDecidableEqTy.decEq._proof_4
• Intensional.instDecidableEqTy.decEq Intensional.Ty.t Intensional.Ty.t = isTrue ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.t (a ⇒ a_1) = isFalse ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.t a.intens = isFalse ⋯
• Intensional.instDecidableEqTy.decEq (a ⇒ a_1) Intensional.Ty.e = isFalse ⋯
• Intensional.instDecidableEqTy.decEq (a ⇒ a_1) Intensional.Ty.t = isFalse ⋯
• Intensional.instDecidableEqTy.decEq (a ⇒ a_1) a_2.intens = isFalse ⋯
• Intensional.instDecidableEqTy.decEq a.intens Intensional.Ty.e = isFalse ⋯
• Intensional.instDecidableEqTy.decEq a.intens Intensional.Ty.t = isFalse ⋯
• Intensional.instDecidableEqTy.decEq a.intens (a_1 ⇒ a_2) = isFalse ⋯
• Intensional.instDecidableEqTy.decEq a.intens b.intens = if h : a = b then h ▸ have inst := Intensional.instDecidableEqTy.decEq a a; isTrue ⋯ else isFalse ⋯

def Intensional.«term_⇒_» : Lean.TrailingParserDescr

Equations

• Intensional.«term_⇒_» = Lean.ParserDescr.trailingNode `Intensional.«term_⇒_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇒ ") (Lean.ParserDescr.cat `term 25))

@[reducible, inline]

abbrev Intensional.Ty.et : Ty

Standard type abbreviations.

Equations

• Intensional.Ty.et = (Intensional.Ty.e ⇒ Intensional.Ty.t)

@[reducible, inline]

abbrev Intensional.Ty.eet : Ty

Equations

• Intensional.Ty.eet = (Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t)

@[reducible, inline]

abbrev Intensional.Ty.ett : Ty

Equations

• Intensional.Ty.ett = ((Intensional.Ty.e ⇒ Intensional.Ty.t) ⇒ Intensional.Ty.t)

@[reducible, inline]

abbrev Intensional.Ty.prop : Ty

⟨s,t⟩ — propositions (sets of indices).

Equations

• Intensional.Ty.prop = Intensional.Ty.t.intens

@[reducible, inline]

abbrev Intensional.Ty.indConcept : Ty

⟨s,e⟩ — individual concepts (index-dependent individuals).

Equations

• Intensional.Ty.indConcept = Intensional.Ty.e.intens

def Intensional.Ty.isConjoinable : Ty → Bool

A type is conjoinable if it "ends in t" ([PR83] Definition 4). Intension types ⟨s,a⟩ are conjoinable iff the base type is — conjunction is pointwise over indices.

Equations

• Intensional.Ty.t.isConjoinable = true
• Intensional.Ty.e.isConjoinable = false
• (a ⇒ τ).isConjoinable = τ.isConjoinable
• a.intens.isConjoinable = a.isConjoinable

def Intensional.Denot (E W : Type) : Ty → Type

Denotation domains, computed from an entity type E, an index type W, and a semantic type.

DWP's model is ⟨A, W, T, <, F⟩; here E = A (the domain of individuals) and W = W × T (world-time pairs), or just W, or Unit for extensional. Temporal ordering, accessibility relations, etc. are structure on W, not baked in.

D_e = E D_t = Prop D_⟨a,b⟩ = D_a → D_b D_⟨s,a⟩ = W → D_a

Equations

• Intensional.Denot E W Intensional.Ty.e = E
• Intensional.Denot E W Intensional.Ty.t = Prop
• Intensional.Denot E W (a ⇒ a_1) = (Intensional.Denot E W a → Intensional.Denot E W a_1)
• Intensional.Denot E W a.intens = (W → Intensional.Denot E W a)

def Intensional.up {E W : Type} {a : Ty} (x : Denot E W a) : Denot E W a.intens

^α — form the rigid intension of an expression. Maps a denotation to the constant function over indices. Definitionally equal to Intensional.Intension.rigid.

Equations

• Intensional.up x x✝ = x

def Intensional.down {E W : Type} {a : Ty} (s : Denot E W a.intens) (i : W) : Denot E W a

ˇα — extract the extension at index i. Evaluates an intension at a given index. Definitionally equal to Intensional.Intension.evalAt.

Equations

• Intensional.down s i = s i

theorem Intensional.down_up {E W : Type} {a : Ty} (x : Denot E W a) (i : W) : down (up x) i = x

Down-up cancellation: ˇ(^α) = α at any index. DWP Theorem 1.

def Intensional.neg {E W : Type} (p : Denot E W Ty.t) : Denot E W Ty.t

Sentence negation.

Equations

• Intensional.neg p = ¬p

def Intensional.conj {E W : Type} (p q : Denot E W Ty.t) : Denot E W Ty.t

Sentence conjunction.

Equations

• Intensional.conj p q = (p ∧ q)

def Intensional.disj {E W : Type} (p q : Denot E W Ty.t) : Denot E W Ty.t

Sentence disjunction.

Equations

• Intensional.disj p q = (p ∨ q)

theorem Intensional.double_negation {E W : Type} (p : Denot E W Ty.t) : neg (neg p) = p

def Intensional.predicateToSet {E W : Type} (p : Denot E W (Ty.e ⇒ Ty.t)) : Set E

Convert a predicate e → t to a Set (the extension).

Equations

• Intensional.predicateToSet p = {x : E | p x}

def Intensional.setToPredicate {E W : Type} (s : Set E) : Denot E W (Ty.e ⇒ Ty.t)

Convert a set to a predicate.

Equations

• Intensional.setToPredicate s x = (x ∈ s)

def Intensional.inExtension {E W : Type} (p : Denot E W (Ty.e ⇒ Ty.t)) (x : E) : Prop

Membership in a predicate's extension.

Equations

• Intensional.inExtension p x = p x

def Intensional.uncurry {E W : Type} (f : Denot E W (Ty.e ⇒ Ty.e ⇒ Ty.t)) : E × E → Prop

Uncurry a binary relation (obj-first) to a pair relation (subj-first).

Equations

• Intensional.uncurry f (x_1, y) = f y x_1

def Intensional.curry {E W : Type} (r : E × E → Prop) : Denot E W (Ty.e ⇒ Ty.e ⇒ Ty.t)

Curry a pair relation to a binary relation.

Equations

• Intensional.curry r y x = r (x, y)

theorem Intensional.curry_uncurry {E W : Type} (f : Denot E W (Ty.e ⇒ Ty.e ⇒ Ty.t)) : curry (uncurry f) = f

theorem Intensional.uncurry_curry {E : Type} (W : Type) (r : E × E → Prop) : uncurry (curry r) = r