Bar-Asher Siegal and Nadathur (2026): Modeling progress

This file formalizes the analysis of telic progressives in [BSN26]. The paper gives up the assumption that an accomplishment predicate P denotes only culminated eventualities. Instead P introduces a causal model in which its culmination condition C_P is a dependent variable, and the model's sufficient sets for C_P are the culmination procedures, the recipes for C_P. A progressive is then about partial realization, not about modal projections of culmination. PROG(P) is felicitous when P has a culmination procedure (33a). It is true when the reference situation has initiated one, not completed any, and not completed a sufficient set for non-culmination (34)–(36).

Situations assign each propositional variable 1, 0 or u, and a structural equation is read in Kleene's three-valued way, as in Figure 1b and Table 2. Causal consistency (29) asks every settled dependent variable to carry the value its equation gives. In a consistent situation, one fact is causally necessary for another (30a) when the first is a causal ancestor of the second and every consistent situation over the same variables that changes the first also changes the second. A consistent situation is causally sufficient for one of its facts (30b) when each of its other facts is necessary for it (IsSufficient). Its kernel is then a sufficient set, which contains the effect itself.

On the dual-route door of Section 4.2 (BarAsherSiegal2026.model) the file checks:

• the two culmination procedures (38) and the three sufficient sets for non-culmination (39);
• that the electronic procedure must include the button, since without it the circuit is undetermined and the situation inconsistent (footnote 39);
• that Nur is opening the door (40) is true after the power has just been switched on, with handle and button unsettled (prog_opening);
• that (40) comes out false in the realistic context where the unturned handle and unpressed button complete a sufficient set for non-culmination, as the paper itself observes (not_prog_realistic);
• that the lock's state is a globally necessary condition (42), so that by (45) the progressive is undefined while the lock's state is unknown (43a) (not_defined_of_lock_unknown).

Implementation notes

Situations are partial assignments over Bool. The three-valued value of an equation is the value on which every completion of its parents' values agrees in every context (Determines), which is Table 2's value for the door's equations. The situations over the same variables as s are its reassignments (reassign), so necessity quantifies over V → Bool. The paper times the initiating fact against the interval just before reference time; here a single pre-reference situation s₀ stands in for that interval. The paper prints the sufficient sets (39b) and (39c) without the effect fact ⟨O,0⟩, which Definition (30b) puts in every sufficient set; sNotElec and sNotCirc include it.

TODO

The paper's repair for the realistic context of (40), which lets a sufficient set for non-culmination be undone by updating a fungible background variable (Section 4.2), is left open, as it is in the paper.

References

• [BSN26]
• [BS26b]
• [BBS25]

Situations and causal consistency

@[reducible, inline]

abbrev BarAsherSiegalNadathur2026.Situation (V : Type u_1) : Type u_1

A situation (28b): each variable is 1, 0, or undetermined.

Equations

• BarAsherSiegalNadathur2026.Situation V = (V → Flat Bool)

def BarAsherSiegalNadathur2026.Determines {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) (s : Situation V) (v : V) (b : Bool) : Prop

The equation for v gives b under s when, in every context, every completion of the values s assigns to v's parents yields b. A completion assigns the parents alone, the other variables being fixed at false, which the equation does not read.

Equations

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

def BarAsherSiegalNadathur2026.Consistent {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) (s : Situation V) : Prop

Causal consistency (29): every settled dependent variable carries the value its equation gives.

Equations

• BarAsherSiegalNadathur2026.Consistent M s = ∀ (v : V), (∃ (w : V), M.graph.Adj w v) → ∀ (b : Bool), s v = ↑b → BarAsherSiegalNadathur2026.Determines M s v b

def BarAsherSiegalNadathur2026.reassign {V : Type u_2} [DecidableEq V] (s : Situation V) (b : V → Bool) : Situation V

The situation over the same variables as s that assigns them the values of b.

Equations

• BarAsherSiegalNadathur2026.reassign s b v = if s v = ⊥ then ⊥ else ↑(b v)

def BarAsherSiegalNadathur2026.Necessary {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableEq V] (s : Situation V) (x y : V) : Prop

Causal necessity (30a): the fact s settles at x is necessary for the one it settles at y when x is a causal ancestor of y and every consistent situation over the same variables that changes x changes y.

Equations

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

def BarAsherSiegalNadathur2026.IsSufficient {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableEq V] (s : Situation V) (y : V) (b : Bool) : Prop

Causal sufficiency (30b): s is consistent, settles y at b, and each of its other facts is necessary for that one. The kernel of s is then a sufficient set for ⟨y, b⟩.

Equations

• BarAsherSiegalNadathur2026.IsSufficient M s y b = (BarAsherSiegalNadathur2026.Consistent M s ∧ s y = ↑b ∧ ∀ (x : V), x ≠ y → s x ≠ ⊥ → BarAsherSiegalNadathur2026.Necessary M s x y)

The progressive

def BarAsherSiegalNadathur2026.Felicitous {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableEq V] (c : V) : Prop

Felicity (33a): the predicate has a culmination procedure, a sufficient set for its culmination condition c.

Equations

• BarAsherSiegalNadathur2026.Felicitous M c = ∃ (S : BarAsherSiegalNadathur2026.Situation V), BarAsherSiegalNadathur2026.IsSufficient M S c true

def BarAsherSiegalNadathur2026.Init {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableEq V] (c : V) (s₀ s : Situation V) : Prop

INIT (36a): some fact of a culmination procedure holds at reference time s and did not hold just before, in s₀.

Equations

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

def BarAsherSiegalNadathur2026.Cul {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableEq V] (c : V) (s : Situation V) : Prop

CUL (36b-i): some culmination procedure is completely realized.

Equations

• BarAsherSiegalNadathur2026.Cul M c s = ∃ (S : BarAsherSiegalNadathur2026.Situation V), BarAsherSiegalNadathur2026.IsSufficient M S c true ∧ S ≤ s

def BarAsherSiegalNadathur2026.Term {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableEq V] (c : V) (s : Situation V) : Prop

TERM (36b-ii): some sufficient set for non-culmination is completely realized.

Equations

• BarAsherSiegalNadathur2026.Term M c s = ∃ (S : BarAsherSiegalNadathur2026.Situation V), BarAsherSiegalNadathur2026.IsSufficient M S c false ∧ S ≤ s

def BarAsherSiegalNadathur2026.Prog {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableEq V] (c : V) (s₀ s : Situation V) : Prop

The progressive (35): initiated and neither culminated nor terminated.

Equations

• BarAsherSiegalNadathur2026.Prog M c s₀ s = (BarAsherSiegalNadathur2026.Init M c s₀ s ∧ ¬(BarAsherSiegalNadathur2026.Cul M c s ∨ BarAsherSiegalNadathur2026.Term M c s))

def BarAsherSiegalNadathur2026.GloballyNecessary {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableEq V] (c v : V) (b : Bool) : Prop

A globally necessary condition (42): the fact ⟨v, b⟩ is globally necessary for c when its negation together with non-culmination is a sufficient set for non-culmination.

Equations

• BarAsherSiegalNadathur2026.GloballyNecessary M c v b = BarAsherSiegalNadathur2026.IsSufficient M (Function.update (Function.update ⊥ v ↑!b) c ↑false) c false

def BarAsherSiegalNadathur2026.Defined {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableEq V] (c : V) (s : Situation V) : Prop

Definedness (45): the progressive is defined when every globally necessary condition is settled at reference time.

Equations

• BarAsherSiegalNadathur2026.Defined M c s = ∀ (v : V) (b : Bool), BarAsherSiegalNadathur2026.GloballyNecessary M c v b → s v ≠ ⊥

@[instance_reducible]

instance BarAsherSiegalNadathur2026.instDecidableDetermines {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableEq V] [Fintype V] [Fintype U] [DecidableRel M.graph.Adj] (s : Situation V) (v : V) (b : Bool) : Decidable (Determines M s v b)

Equations

• BarAsherSiegalNadathur2026.instDecidableDetermines M s v b = id inferInstance

@[instance_reducible]

instance BarAsherSiegalNadathur2026.instDecidableConsistent {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableEq V] [Fintype V] [Fintype U] [DecidableRel M.graph.Adj] (s : Situation V) : Decidable (Consistent M s)

Equations

• BarAsherSiegalNadathur2026.instDecidableConsistent M s = id inferInstance

@[instance_reducible]

instance BarAsherSiegalNadathur2026.instDecidableNecessary {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableEq V] [Fintype V] [Fintype U] [DecidableRel M.graph.Adj] (s : Situation V) (x y : V) : Decidable (Necessary M s x y)

Equations

• BarAsherSiegalNadathur2026.instDecidableNecessary M s x y = id inferInstance

@[instance_reducible]

instance BarAsherSiegalNadathur2026.instDecidableIsSufficient {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableEq V] [Fintype V] [Fintype U] [DecidableRel M.graph.Adj] (s : Situation V) (y : V) (b : Bool) : Decidable (IsSufficient M s y b)

Equations

• BarAsherSiegalNadathur2026.instDecidableIsSufficient M s y b = id inferInstance

@[instance_reducible]

instance BarAsherSiegalNadathur2026.instDecidableGloballyNecessary {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableEq V] [Fintype V] [Fintype U] [DecidableRel M.graph.Adj] (c v : V) (b : Bool) : Decidable (GloballyNecessary M c v b)

Equations

• BarAsherSiegalNadathur2026.instDecidableGloballyNecessary M c v b = id inferInstance

theorem BarAsherSiegalNadathur2026.IsSufficient.eq_of_le {U : Type u_1} {V : Type u_2} {M : CausalModel U V fun (x : V) => Bool} [DecidableEq V] {S s : Situation V} {y : V} {b : Bool} (h : IsSufficient M S y b) (hle : S ≤ s) : s y = ↑b

A sufficient set contains its effect, so a situation that realizes one settles the effect.

theorem BarAsherSiegalNadathur2026.not_cul_or_term {U : Type u_1} {V : Type u_2} {M : CausalModel U V fun (x : V) => Bool} [DecidableEq V] {c : V} {s : Situation V} (h : s c = ⊥) : ¬(Cul M c s ∨ Term M c s)

A situation that leaves the culmination condition unsettled neither culminates nor terminates: every sufficient set contains its effect.

The dual-route door (Section 4.2)

def BarAsherSiegalNadathur2026.sMech : Situation BarAsherSiegal2026.V

The mechanical procedure (38a): handle turned, door unlocked, door open.

Equations

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

def BarAsherSiegalNadathur2026.sElec : Situation BarAsherSiegal2026.V

The electronic procedure (38b): door unlocked, power on, button pressed, circuit closed, door open.

Equations

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

def BarAsherSiegalNadathur2026.sLock : Situation BarAsherSiegal2026.V

Non-culmination by the lock (39a).

Equations

• BarAsherSiegalNadathur2026.sLock = Function.update (Function.update ⊥ BarAsherSiegal2026.V.doorOpens ↑false) BarAsherSiegal2026.V.lock ↑true

def BarAsherSiegalNadathur2026.sNotElec : Situation BarAsherSiegal2026.V

Non-culmination with the handle unturned and no power (39b), with the effect fact.

Equations

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

def BarAsherSiegalNadathur2026.sNotCirc : Situation BarAsherSiegal2026.V

Non-culmination with the handle unturned and the button unpressed (39c), with the effect fact.

Equations

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

theorem BarAsherSiegalNadathur2026.sMech_sufficient : IsSufficient BarAsherSiegal2026.model sMech BarAsherSiegal2026.V.doorOpens true

theorem BarAsherSiegalNadathur2026.sElec_sufficient : IsSufficient BarAsherSiegal2026.model sElec BarAsherSiegal2026.V.doorOpens true

theorem BarAsherSiegalNadathur2026.sLock_sufficient : IsSufficient BarAsherSiegal2026.model sLock BarAsherSiegal2026.V.doorOpens false

theorem BarAsherSiegalNadathur2026.sNotElec_sufficient : IsSufficient BarAsherSiegal2026.model sNotElec BarAsherSiegal2026.V.doorOpens false

theorem BarAsherSiegalNadathur2026.sNotCirc_sufficient : IsSufficient BarAsherSiegal2026.model sNotCirc BarAsherSiegal2026.V.doorOpens false

theorem BarAsherSiegalNadathur2026.not_sufficient_as_printed : ¬IsSufficient BarAsherSiegal2026.model (Function.update (Function.update ⊥ BarAsherSiegal2026.V.electricity ↑false) BarAsherSiegal2026.V.handle ↑false) BarAsherSiegal2026.V.doorOpens false

(39b) as printed, without the effect fact, is not a sufficient set under Definition (30b), which puts the effect in every sufficient set.

theorem BarAsherSiegalNadathur2026.felicitous : Felicitous BarAsherSiegal2026.model BarAsherSiegal2026.V.doorOpens

open the door has a culmination procedure, so its progressive is felicitous (33a).

theorem BarAsherSiegalNadathur2026.not_sufficient_without_button : ¬IsSufficient BarAsherSiegal2026.model (Function.update (Function.update (Function.update (Function.update ⊥ BarAsherSiegal2026.V.doorOpens ↑true) BarAsherSiegal2026.V.circuit ↑true) BarAsherSiegal2026.V.electricity ↑true) BarAsherSiegal2026.V.lock ↑false) BarAsherSiegal2026.V.doorOpens true

The electronic procedure needs the button (footnote 39): without it the circuit, whose equation reads the button, is settled against an undetermined equation value.

def BarAsherSiegalNadathur2026.beforeSwitch : Situation BarAsherSiegal2026.V

Just before reference time the door is unlocked and the power is off.

Equations

• BarAsherSiegalNadathur2026.beforeSwitch = Function.update (Function.update ⊥ BarAsherSiegal2026.V.electricity ↑false) BarAsherSiegal2026.V.lock ↑false

def BarAsherSiegalNadathur2026.switchedOn : Situation BarAsherSiegal2026.V

At reference time Nur has switched the power on; handle and button are unsettled, as in the first highlighted row of Table 2.

Equations

• BarAsherSiegalNadathur2026.switchedOn = Function.update (Function.update ⊥ BarAsherSiegal2026.V.electricity ↑true) BarAsherSiegal2026.V.lock ↑false

theorem BarAsherSiegalNadathur2026.prog_opening : Prog BarAsherSiegal2026.model BarAsherSiegal2026.V.doorOpens beforeSwitch switchedOn

(40) Nur is opening the door is true once the power is switched on: the electronic procedure is initiated by the power, and neither culmination nor non-culmination is settled.

def BarAsherSiegalNadathur2026.realistic : Situation BarAsherSiegal2026.V

The realistic context of (40), the second highlighted row of Table 2: Nur has turned neither the handle nor the button, so the door is closed.

Equations

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

theorem BarAsherSiegalNadathur2026.not_prog_realistic : ¬Prog BarAsherSiegal2026.model BarAsherSiegal2026.V.doorOpens beforeSwitch realistic

In the realistic context the unturned handle and unpressed button complete a sufficient set for non-culmination (39c), so (40) comes out false, against intuition, as the paper observes.

theorem BarAsherSiegalNadathur2026.lock_globallyNecessary : GloballyNecessary BarAsherSiegal2026.model BarAsherSiegal2026.V.doorOpens BarAsherSiegal2026.V.lock false

The door's being unlocked is globally necessary for it to open (42): the lock alone makes a sufficient set for non-culmination.

theorem BarAsherSiegalNadathur2026.not_defined_of_lock_unknown {s : Situation BarAsherSiegal2026.V} (h : s BarAsherSiegal2026.V.lock = ⊥) : ¬Defined BarAsherSiegal2026.model BarAsherSiegal2026.V.doorOpens s

(43a) ??Nur is opening the door: while the lock's state is unknown, the progressive is not defined, whatever Nur has done (45).