A Mechanistic Formalization in Dependent Type Theory
This project presents a formalization of possible-world and situation semantics within Lean 4's dependent type theory, following the higher-order modal and situation-theoretic tradition of Zalta, Fine, and Barwise–Perry. The development proceeds entirely from primitive typed constants, without recourse to any external mathematical library.
The distinguishing commitment of the formalization is mechanistic grounding: wherever a logical principle admits derivation from antecedent definitions, it is established as a theorem rather than postulated. This discipline is most consequential in the modal layer, where the entirety of S5 — including the necessitation rule and the characteristic collapse ◊□φ → □φ — is derived from a single definitional choice in which the accessibility relation is the universal relation on the domain of worlds.
The ontological core follows Zalta's abstract object theory. Situations and worlds are not type-distinct; situationhood and worldhood are predicates over a single domain. Encoding is the primitive relation from which parthood, propositional truth, and the mereology of situations are all constructed. The resulting theory proves Theorems 4–6 of Zalta (1993) — the equivalence of parthood and truth-inclusion, antisymmetry of parthood, and same-parts identity — as mechanically verified results.
The ontology is stratified into three typed domains: a domain of worlds (which comprises both possible worlds and proper situations), a domain of properties, and a domain of propositions. The primitive predicate Situation carves out the sub-domain of situations within the world domain; Worldhood further identifies those situations that are maximal and consistent.
The central primitive is the encoding relation, written enc(s, F), between a situation and a property. A situation encodes exactly those properties of the form VAC(p) — the vacuous abstraction of some proposition p — distinguishing situations from arbitrary abstract objects in Zalta's sense. Parthood is defined encoding-first:
s ⊴ s′ :⟺ ∀F. enc(s, F) → enc(s′, F)Truth-in, written s ⊨ p, is a separate primitive governed by the reduction: a situation s makes p true if and only if s encodes VAC(p). The bridge between the two orderings — encoding-based parthood and truth-based inclusion — is the content of Theorem 4:
s ⊴ s′ ↔ ∀p. (s ⊨ p → s′ ⊨ p)Modal operators are grounded in a Kripke frame whose accessibility relation R is the universal relation: Rwv holds for all worlds w, v. This is the characteristic frame condition of S5. Necessity and possibility are then defined semantically:
□φ(w) :⟺ ∀v. Rwv → φ(v) ◊φ(w) :⟺ ¬□¬φ(w)Because R is definitionally universal, □φ(w) reduces to ∀v. φ(v), making the modal operators fully transparent to the kernel. Reflexivity, transitivity, and symmetry of R are consequences of its definition, not independent postulates. All S5 schemas and the necessitation rule are theorems derivable from this single definitional choice.
Ontological dependence is defined in the tradition of Fine and Correia: a situation s depends on s′, written s ≺ s′, when every situation that includes s also includes s′:
s ≺ s′ :⟺ ∀u. Sit(u) → s ⊴ u → s′ ⊴ uThe meet of two situations is their greatest lower bound under ⊴, characterised by the principle that s ∧ s′ makes precisely the propositions true that both s and s′ make true. The three lattice properties — s ∧ s′ ⊴ s, s ∧ s′ ⊴ s′, and the universal property — are established as theorems once the equivalence of parthood and truth-inclusion is available.
The theory is formulated within Lean 4's dependent type theory over a primitive ontological domain W. No set-theoretic reduction of this domain is presupposed. Situations and worlds are not type-distinct entities but are instead distinguished by predicates over a common domain. Alongside W, the theory contains a domain of properties P and a domain of propositions Π.
The primitive non-logical vocabulary consists of the predicates Obj and Sit, the relations enc and ⊨, and the operation VAC. Formally:
Obj, Sit : W → Prop enc : W × P → Prop ⊨ : W × Π → Prop VAC : Π → PNo further primitive constants are assumed. Every subsequent notion is either postulated explicitly or introduced by definition.
The development rests upon three constitutive principles governing the interaction between situations, properties, and propositions.
First, situations encode only vacuous abstractions:
Sit(s) ∧ enc(s,F) → ∃p(F = VAC(p))Second, every situation is an object:
Sit(s) → Obj(s)Third, truth in a situation is reducible to encoding:
s ⊨ p ↔ enc(s,VAC(p))These principles constitute the entire bridge between the propositional and ontological layers of the theory. All subsequent interaction between truth, encoding, and mereology is mediated through them.
Parthood is introduced as inclusion in encoded content:
s ⊴ s′ :⟺ ∀F(enc(s,F) → enc(s′,F))Accessibility is defined universally:
R(w,v) :⟺ ⊤Necessity and possibility are introduced semantically:
□φ(w) :⟺ ∀v(R(w,v) → φ(v)) ◊φ(w) :⟺ ¬□¬φ(w)Ontological dependence is defined by preservation across all containing situations:
s ≺ s′ :⟺ ∀u(Sit(u) → s ⊴ u → s′ ⊴ u)Because accessibility is definitionally universal, the modal operators reduce to unrestricted quantification over the world domain. Reflexivity, symmetry, and transitivity are therefore consequences of definition rather than independent frame conditions. The normal modal principles K, T, 4, and 5, together with necessitation and the characteristic S5 principle,
◊□φ → □φare all established as theorems. The modal strength of the system is thus generated by a single definitional commitment concerning accessibility, rather than by a collection of independent modal axioms.
The central theorem of the development identifies the mereological and truth-theoretic orderings:
s ⊴ s′ ↔ ∀p(s ⊨ p → s′ ⊨ p)This result establishes that inclusion of encoded content coincides exactly with inclusion of propositional content. From it follow antisymmetry of parthood, identity by common parts, and persistence of truth under inclusion.
s ⊴ s′ ∧ s′ ⊴ s → s = s′ ∀u(u ⊴ s ↔ u ⊴ s′) → s = s′ s ⊨ p ∧ s ⊴ s′ → s′ ⊨ pWorldhood is characterized by maximality and consistency. A world decides every proposition and contains no contradiction.
World(w) → ∀p(w ⊨ p ∨ w ⊨ ¬p) World(w) → ¬∃p(w ⊨ p ∧ w ⊨ ¬p)These assumptions suffice to establish that no proper part of a world can itself be a world.
Binary meets are postulated to exist and are characterized truth-theoretically. The conjunction of two situations makes true precisely those propositions made true by both.
s ∧ s′ ⊨ p ↔ (s ⊨ p ∧ s′ ⊨ p)Once the equivalence between parthood and truth inclusion is available, the lower-bound and greatest-lower-bound properties of the meet operation follow immediately as theorems.
OP-1 Necessitation and the S5 characteristic thesis
The necessitation rule (⊢ φ ⟹ ⊢ □φ) and the S5 collapse (◊□φ → □φ) are not derivable from the schemas K, T, 4, 5 alone. Both were initially postulated. They are now derived consequences of the definitional choice Rwv :⟺ ⊤: necessitation holds because □φ(w) reduces to ∀v. φ(v), and the S5 collapse holds because any ◊-witness already has □φ, which at the universal relation yields φ everywhere.
OP-2 Parthood–truth equivalence
The direction ∀p. (s ⊨ p → s′ ⊨ p) → s ⊴ s′ was not derivable given that ⊴ is defined over encoding while ⊨ is an independent primitive. The gap is closed by the principle that situations encode only vacuous abstractions: given truth-inclusion, any property encoded by s is of the form VAC(p), and truth-inclusion then transfers encoding directly. This yields the full biconditional of Theorem 4 and unlocks Theorems 5, 6, and 8.
OP-3 Situations are objects
The reduction of truth to encoding requires the object predicate as a hypothesis. Since situationhood and objecthood are independent primitives, their overlap had to be postulated: Sit(s) → Obj(s). With this in place, the monotonicity direction of Theorem 4 closes without any open obligation.
OP-4 Lattice structure of meet
The meet is characterised truth-theoretically: s ∧ s′ ⊨ p iff s ⊨ p and s′ ⊨ p. The lattice properties — that the meet is a lower bound and the greatest such — require translating between the truth-based characterisation and the encoding-based definition of ⊴. This translation is exactly the content of Theorem 4, and all three lattice properties follow immediately once that theorem is available.
OP-5 No strict subworld
No proper part of a world is itself a world. The proof proceeds by maximality: if s ⊴ w and both are worlds, then for any proposition p, the maximality of w and the monotonicity of truth under ⊴ force s and w to agree on every proposition, whence extensionality yields s = w, contradicting strict parthood. The two cases — forward and backward agreement — each reduce to a single application of truth-monotonicity or a classical argument through maximality.