Intensional Logic: Frames and Types

@cite{dowty-wall-peters-1981} @cite{gallin-1975}

Foundations for intensional logic following DWP Ch. 6. A Frame provides the entity domain and index set; Ty is the recursive grammar of semantic types; Frame.Denot computes denotation domains from a frame and type.

Key definitions

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

inductive Core.Logic.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 Core.Logic.Intensional.instReprTy : Repr Ty

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

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

@[implicit_reducible]

instance Core.Logic.Intensional.instDecidableEqTy : DecidableEq Ty

Equations

• Core.Logic.Intensional.instDecidableEqTy = Core.Logic.Intensional.instDecidableEqTy.decEq

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

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Core.Logic.Intensional.Ty.et : Ty

Standard type abbreviations.

Equations

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

@[reducible, inline]

abbrev Core.Logic.Intensional.Ty.eet : Ty

Equations

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

@[reducible, inline]

abbrev Core.Logic.Intensional.Ty.ett : Ty

Equations

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

@[reducible, inline]

abbrev Core.Logic.Intensional.Ty.prop : Ty

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

Equations

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

@[reducible, inline]

abbrev Core.Logic.Intensional.Ty.indConcept : Ty

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

Equations

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

def Core.Logic.Intensional.Ty.isConjoinable : Ty → Bool

A type is conjoinable if it "ends in t" (@cite{partee-rooth-1983} Definition 4). Intension types ⟨s,a⟩ are conjoinable iff the base type is — conjunction is pointwise over indices.

Equations

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

structure Core.Logic.Intensional.Frame : Type 1

An IL frame: entity domain + index set.

DWP's model is ⟨A, W, T, <, F⟩. The frame provides the domains:

• Entity = A (the domain of individuals)
• Index = W × T (world-time pairs), or just W, or Unit for extensional

Temporal ordering, accessibility relations, etc. are added as structure on the Index type, not baked into the frame.

• Entity : Type
• Index : Type

def Core.Logic.Intensional.Frame.Denot (F : Frame) : Ty → Type

Denotation domains, computed from a frame and a type.

D_e = F.Entity D_t = Prop D_⟨a,b⟩ = D_a → D_b D_⟨s,a⟩ = F.Index → D_a

Equations

• F.Denot Core.Logic.Intensional.Ty.e = F.Entity
• F.Denot Core.Logic.Intensional.Ty.t = Prop
• F.Denot (a ⇒ a_1) = (F.Denot a → F.Denot a_1)
• F.Denot a.intens = (F.Index → F.Denot a)

def Core.Logic.Intensional.up {F : Frame} {a : Ty} (x : F.Denot a) : F.Denot a.intens

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

Equations

• Core.Logic.Intensional.up x x✝ = x

def Core.Logic.Intensional.down {F : Frame} {a : Ty} (s : F.Denot a.intens) (i : F.Index) : F.Denot a

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

Equations

• Core.Logic.Intensional.down s i = s i

theorem Core.Logic.Intensional.down_up {F : Frame} {a : Ty} (x : F.Denot a) (i : F.Index) : down (up x) i = x

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

def Core.Logic.Intensional.neg {F : Frame} (p : F.Denot Ty.t) : F.Denot Ty.t

Sentence negation.

Equations

• Core.Logic.Intensional.neg p = ¬p

def Core.Logic.Intensional.conj {F : Frame} (p q : F.Denot Ty.t) : F.Denot Ty.t

Sentence conjunction.

Equations

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

def Core.Logic.Intensional.disj {F : Frame} (p q : F.Denot Ty.t) : F.Denot Ty.t

Sentence disjunction.

Equations

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

theorem Core.Logic.Intensional.double_negation {F : Frame} (p : F.Denot Ty.t) : neg (neg p) = p

def Core.Logic.Intensional.predicateToSet {F : Frame} (p : F.Denot (Ty.e ⇒ Ty.t)) : Set F.Entity

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

Equations

• Core.Logic.Intensional.predicateToSet p = {x : F.Entity | p x}

def Core.Logic.Intensional.setToPredicate {F : Frame} (s : Set F.Entity) : F.Denot (Ty.e ⇒ Ty.t)

Convert a set to a predicate.

Equations

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

def Core.Logic.Intensional.inExtension {F : Frame} (p : F.Denot (Ty.e ⇒ Ty.t)) (x : F.Entity) : Prop

Membership in a predicate's extension.

Equations

• Core.Logic.Intensional.inExtension p x = p x

def Core.Logic.Intensional.uncurry {F : Frame} (f : F.Denot (Ty.e ⇒ Ty.e ⇒ Ty.t)) : F.Entity × F.Entity → Prop

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

Equations

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

def Core.Logic.Intensional.curry {F : Frame} (r : F.Entity × F.Entity → Prop) : F.Denot (Ty.e ⇒ Ty.e ⇒ Ty.t)

Curry a pair relation to a binary relation.

Equations

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

theorem Core.Logic.Intensional.curry_uncurry {F : Frame} (f : F.Denot (Ty.e ⇒ Ty.e ⇒ Ty.t)) : curry (uncurry f) = f

theorem Core.Logic.Intensional.uncurry_curry {F : Frame} (r : F.Entity × F.Entity → Prop) : uncurry (curry r) = r