Intensional Logic: Types and Denotations

[DWP81] [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.

The core e, t, ⟨a,b⟩, ⟨s,a⟩ grammar is [DWP81] Ch. 6 (equivalently [HK98]'s (5) plus intensions); the degree and eventuality sorts are the standard extensions of degree and neo-Davidsonian event semantics. Following [YAS23]'s convention, v is the sort of events and s the sort of states — so ⟨e,⟨s,t⟩⟩ is an individual/state relation (a stative or property-concept root) and ⟨e,⟨v,t⟩⟩ an individual/event relation (a change-of-state root).

• e : Ty
• t : Ty
• d : Ty

  Degrees (type d): the scale sort of degree semantics ([Hei01], [Wel15]). Denoted by ℚ, the repo's exact degree carrier.

• v : Ty

  Events (type v): the neo-Davidsonian event sort ([Dav67], [Par90]).

• s : Ty

  States (type s): the state sort, distinguished from events per [YAS23]'s convention (v events, s states); not the Montagovian index sort, which is intens.

• fn : Ty → Ty → Ty
• intens : Ty → Ty

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✝
• Intensional.instReprTy.repr Intensional.Ty.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Intensional.Ty.d")).group prec✝
• Intensional.instReprTy.repr Intensional.Ty.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Intensional.Ty.v")).group prec✝
• Intensional.instReprTy.repr Intensional.Ty.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Intensional.Ty.s")).group prec✝

@[instance_reducible]

instance Intensional.instReprTy : Repr Ty

Equations

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

@[instance_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 Intensional.Ty.d = isFalse Intensional.instDecidableEqTy.decEq._proof_2
• Intensional.instDecidableEqTy.decEq Intensional.Ty.e Intensional.Ty.v = isFalse Intensional.instDecidableEqTy.decEq._proof_3
• Intensional.instDecidableEqTy.decEq Intensional.Ty.e Intensional.Ty.s = isFalse Intensional.instDecidableEqTy.decEq._proof_4
• 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_7
• Intensional.instDecidableEqTy.decEq Intensional.Ty.t Intensional.Ty.t = isTrue ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.t Intensional.Ty.d = isFalse Intensional.instDecidableEqTy.decEq._proof_8
• Intensional.instDecidableEqTy.decEq Intensional.Ty.t Intensional.Ty.v = isFalse Intensional.instDecidableEqTy.decEq._proof_9
• Intensional.instDecidableEqTy.decEq Intensional.Ty.t Intensional.Ty.s = isFalse Intensional.instDecidableEqTy.decEq._proof_10
• Intensional.instDecidableEqTy.decEq Intensional.Ty.t (a ⇒ a_1) = isFalse ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.t a.intens = isFalse ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.d Intensional.Ty.e = isFalse Intensional.instDecidableEqTy.decEq._proof_13
• Intensional.instDecidableEqTy.decEq Intensional.Ty.d Intensional.Ty.t = isFalse Intensional.instDecidableEqTy.decEq._proof_14
• Intensional.instDecidableEqTy.decEq Intensional.Ty.d Intensional.Ty.d = isTrue ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.d Intensional.Ty.v = isFalse Intensional.instDecidableEqTy.decEq._proof_15
• Intensional.instDecidableEqTy.decEq Intensional.Ty.d Intensional.Ty.s = isFalse Intensional.instDecidableEqTy.decEq._proof_16
• Intensional.instDecidableEqTy.decEq Intensional.Ty.d (a ⇒ a_1) = isFalse ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.d a.intens = isFalse ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.v Intensional.Ty.e = isFalse Intensional.instDecidableEqTy.decEq._proof_19
• Intensional.instDecidableEqTy.decEq Intensional.Ty.v Intensional.Ty.t = isFalse Intensional.instDecidableEqTy.decEq._proof_20
• Intensional.instDecidableEqTy.decEq Intensional.Ty.v Intensional.Ty.d = isFalse Intensional.instDecidableEqTy.decEq._proof_21
• Intensional.instDecidableEqTy.decEq Intensional.Ty.v Intensional.Ty.v = isTrue ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.v Intensional.Ty.s = isFalse Intensional.instDecidableEqTy.decEq._proof_22
• Intensional.instDecidableEqTy.decEq Intensional.Ty.v (a ⇒ a_1) = isFalse ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.v a.intens = isFalse ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.s Intensional.Ty.e = isFalse Intensional.instDecidableEqTy.decEq._proof_25
• Intensional.instDecidableEqTy.decEq Intensional.Ty.s Intensional.Ty.t = isFalse Intensional.instDecidableEqTy.decEq._proof_26
• Intensional.instDecidableEqTy.decEq Intensional.Ty.s Intensional.Ty.d = isFalse Intensional.instDecidableEqTy.decEq._proof_27
• Intensional.instDecidableEqTy.decEq Intensional.Ty.s Intensional.Ty.v = isFalse Intensional.instDecidableEqTy.decEq._proof_28
• Intensional.instDecidableEqTy.decEq Intensional.Ty.s Intensional.Ty.s = isTrue ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.s (a ⇒ a_1) = isFalse ⋯
• Intensional.instDecidableEqTy.decEq Intensional.Ty.s 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) Intensional.Ty.d = isFalse ⋯
• Intensional.instDecidableEqTy.decEq (a ⇒ a_1) Intensional.Ty.v = isFalse ⋯
• Intensional.instDecidableEqTy.decEq (a ⇒ a_1) Intensional.Ty.s = 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 Intensional.Ty.d = isFalse ⋯
• Intensional.instDecidableEqTy.decEq a.intens Intensional.Ty.v = isFalse ⋯
• Intensional.instDecidableEqTy.decEq a.intens Intensional.Ty.s = 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))

Functional application at type level

def Intensional.Ty.apply : Ty → Ty → Option Ty

Type-level functional application ([HK98]'s Functional Application, on types): a function type applied to a matching argument type yields the value type; anything else is a type mismatch (none). Composition failures are computed, not stipulated.

Equations

• (a ⇒ b).apply x✝ = if a = x✝ then some b else none
• x✝¹.apply x✝ = none

theorem Intensional.Ty.apply_eq_some_iff {f x c : Ty} : f.apply x = some c ↔ f = (x ⇒ c)

@[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
• Intensional.Ty.d.isConjoinable = false
• Intensional.Ty.v.isConjoinable = false
• Intensional.Ty.s.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

The eventuality sorts v and s denote in the empty domain: the extensional DWP fragment carries no eventuality domain, and nothing here constructs event-typed denotations. Event-semantic interpretation is the extension point — a carrier-parametric variant of Denot supplying event and state domains — and lands with the first study that composes event-typed denotations.

Equations

• Intensional.Denot E W Intensional.Ty.e = E
• Intensional.Denot E W Intensional.Ty.t = Prop
• Intensional.Denot E W Intensional.Ty.d = ℚ
• Intensional.Denot E W Intensional.Ty.v = Empty
• Intensional.Denot E W Intensional.Ty.s = Empty
• 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)

theorem Intensional.Denot.apply_sound {E W : Type} {f x c : Ty} (h : f.apply x = some c) : Denot E W f = (Denot E W x → Denot E W c)

Soundness of type-level application: when apply succeeds, the denotation domain of the function type is exactly the function space from the argument's domain to the value's.

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