Nadathur (2023)

Nadathur analyses an implicative as Karttunen's presupposition–proposition pair with causal conditions, her Proposal (32). The verb presupposes that its prerequisite is causally necessary for the complement and, if it is two-way, causally sufficient, both relative to a background situation, and it asserts the prerequisite. Under this causal interpretation of the conditions (causalInterpretation), which is sound at every context of the background, a verb implies what its implication signature says.

In her Dreyfus scenario, an eight-vertex causal model, the nerve that dare names is causally necessary and sufficient for sending the message, so dare is felicitous there and its assertion and denial decide the message (dare_felicitous_for_msg, msg_of_dare, not_msg_of_not_dare). The nerve is necessary but not sufficient for establishing communication and for spying, so dare is infelicitous there (dare_infelicitous_for_com, dare_infelicitous_for_spy). The Finnish fragment's entries carry the implication signatures of the paper's Finnish implicatives (implicative_eq), and each of the paper's minimal pairs implies what its verb's signature says for its matrix polarity (rows_agree).

Implementation notes

A fact is a variable with a value, and the worlds of the causal interpretation are the contexts where the background holds; the interpretation needs the context to reach the model only at its roots, as in the paper's dynamics. The sufficiency verdicts are decided over the finite model; the necessity verdicts are proved through the equations, which make every path to the effect run through the nerve.

Definition 10b ranges over the consistent supersituations of Definition 9b (IsConsistentSupersituation), and over them the verdicts on (34c) and (34d) fail: settling the message, which the background leaves open, reaches communication without the nerve (Consistent.not_nrv_necessary_for_com). The paper argues those verdicts from the background variables alone, so necessity is read over the exogenous settlements, a subset of the consistent supersituations (isConsistentSupersituation_of_isExogenousSettlement).

TODO

The manage examples need set-valued prerequisites, one of them the conjunction of courage, a listener, and an ungarbled message, while the substrate's sufficiency semantics takes a single prerequisite vertex.

References

• [Nad23b]
• [Nad19]
• [BF16]
• [Kar71a]

Consistent supersituations

def Nadathur2023.IsConsistentSupersituation {U : Type u_1} {V : Type u_2} {α : V → Type u_3} (M : CausalModel U V α) [M.IsAcyclic] (s s' : (v : V) → Flat (α v)) : Prop

IsConsistentSupersituation M s s' says that s' is a consistent supersituation of s (Definition 9b). It extends s, and to each variable with parents that it newly settles it gives the only value the strict development of s could settle there.

Equations

• Nadathur2023.IsConsistentSupersituation M s s' = (s ≤ s' ∧ ∀ (v : V), s v = ⊥ → (∃ (w : V), M.graph.Adj w v) → ∀ (x : α v), s' v = ↑x → ∀ (z : α v), M.CausallyEntails s v z → z = x)

theorem Nadathur2023.isConsistentSupersituation_of_isExogenousSettlement {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [M.IsAcyclic] {s s' : (v : V) → Flat (α v)} (h : M.IsExogenousSettlement s s') : IsConsistentSupersituation M s s'

Every exogenous settlement is a consistent supersituation, since it newly settles no variable with parents.

@[instance_reducible]

instance Nadathur2023.instDecidableIsConsistentSupersituationOfInhabitedOfDecidableEqOfFintypeOfDecidableRelAdjGraph {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [M.IsAcyclic] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [Fintype V] [(v : V) → Fintype (α v)] [DecidableRel M.graph.Adj] (s s' : (v : V) → Flat (α v)) : Decidable (IsConsistentSupersituation M s s')

Equations

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

Proposal (32)

def Nadathur2023.causalInterpretation {U : Type u_1} {V : Type u_2} [DecidableEq V] (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] [M.ContextAtRoots] (s : V → Flat Bool) : Implicative.Interpretation (V × Bool) ↑(M.contexts s)

The causal interpretation of the conditions over the contexts where the background s holds. A fact is a variable with a value, and one fact is sufficient (Definition 10a) or necessary (Definition 10b, over the exogenous settlements) for another relative to s, which does not settle the first (the preamble of Definition 10).

Equations

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

inductive Nadathur2023.V : Type

The vertices of the Dreyfus scenario are INT (Dreyfus intends to spy), NRV (he has the nerve), LST (a German is listening on the correct frequency), BRK (the message is garbled), SEC (he collects secrets), MSG (he sends a radio message), COM (he establishes communication) and SPY (he spies for the Germans) ([Nad23b] §6.1.1, Figure 3).

• INT : V
• NRV : V
• LST : V
• BRK : V
• SEC : V
• MSG : V
• COM : V
• SPY : V

@[instance_reducible]

instance Nadathur2023.instDecidableEqV : DecidableEq V

Equations

• Nadathur2023.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Nadathur2023.instFintypeV : Fintype V

Equations

• Nadathur2023.instFintypeV = { elems := { val := ↑Nadathur2023.V.enumList, nodup := Nadathur2023.V.enumList_nodup }, complete := Nadathur2023.instFintypeV._proof_1 }

@[instance_reducible]

instance Nadathur2023.instReprV : Repr V

Equations

• Nadathur2023.instReprV = { reprPrec := Nadathur2023.instReprV.repr }

def Nadathur2023.instReprV.repr : V → ℕ → Std.Format

Equations

• Nadathur2023.instReprV.repr Nadathur2023.V.INT prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2023.V.INT")).group prec✝
• Nadathur2023.instReprV.repr Nadathur2023.V.NRV prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2023.V.NRV")).group prec✝
• Nadathur2023.instReprV.repr Nadathur2023.V.LST prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2023.V.LST")).group prec✝
• Nadathur2023.instReprV.repr Nadathur2023.V.BRK prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2023.V.BRK")).group prec✝
• Nadathur2023.instReprV.repr Nadathur2023.V.SEC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2023.V.SEC")).group prec✝
• Nadathur2023.instReprV.repr Nadathur2023.V.MSG prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2023.V.MSG")).group prec✝
• Nadathur2023.instReprV.repr Nadathur2023.V.COM prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2023.V.COM")).group prec✝
• Nadathur2023.instReprV.repr Nadathur2023.V.SPY prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nadathur2023.V.SPY")).group prec✝

def Nadathur2023.edges : Finset (V × V)

In the causal graph SEC reads INT, MSG reads INT and NRV, COM reads MSG, LST and BRK, and SPY reads SEC and COM, with INT, NRV, LST and BRK exogenous.

Equations

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

structure Nadathur2023.Context : Type

The context settles the intention, the nerve, the listener, and the garbling.

• INT : Bool
• NRV : Bool
• LST : Bool
• BRK : Bool

@[instance_reducible]

instance Nadathur2023.instDecidableEqContext : DecidableEq Context

Equations

• Nadathur2023.instDecidableEqContext = Nadathur2023.instDecidableEqContext.decEq

def Nadathur2023.instDecidableEqContext.decEq (x✝ x✝¹ : Context) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Nadathur2023.instFintypeContext : Fintype Context

Equations

• Nadathur2023.instFintypeContext = Fintype.ofEquiv ((_ : Bool) × (_ : Bool) × (_ : Bool) × Bool) Nadathur2023.Context.proxyTypeEquiv

@[instance_reducible]

instance Nadathur2023.instInhabitedContext : Inhabited Context

Equations

• Nadathur2023.instInhabitedContext = { default := Nadathur2023.instInhabitedContext.default }

def Nadathur2023.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Nadathur2023.instReprContext : Repr Context

Equations

• Nadathur2023.instReprContext = { reprPrec := Nadathur2023.instReprContext.repr }

def Nadathur2023.dreyfusModel : CausalModel Context V fun (x : V) => Bool

The Dreyfus model, with the negative ¬BRK precondition encoded directly in the COM equation.

Equations

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

@[instance_reducible]

instance Nadathur2023.instDecidableRelVAdjGraphContextBoolDreyfusModel : DecidableRel dreyfusModel.graph.Adj

Equations

• Nadathur2023.instDecidableRelVAdjGraphContextBoolDreyfusModel w v = Nadathur2023.instDecidableRelVAdjGraphContextBoolDreyfusModel._aux_1 w v

instance Nadathur2023.instIsAcyclicContextVBoolDreyfusModel : dreyfusModel.IsAcyclic

def Nadathur2023.dreyfusBg : V → Flat Bool

In the background Dreyfus intends to spy and has already collected secrets (INT = SEC = 1), and NRV, LST and BRK are unresolved.

Equations

• Nadathur2023.dreyfusBg = Function.update (Function.update ⊥ Nadathur2023.V.SEC ↑true) Nadathur2023.V.INT ↑true

instance Nadathur2023.instContextAtRootsContextVBoolDreyfusModel : dreyfusModel.ContextAtRoots

noncomputable def Nadathur2023.dare (e : V) : ↑(dreyfusModel.contexts dreyfusBg) → SignType

Dreyfus dared to e, a verb of the two-way signature +/− under the causal interpretation, with the nerve as the prerequisite.

Equations

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

theorem Nadathur2023.nrv_sufficient_for_msg : ¬dreyfusModel.CausallyEntails dreyfusBg V.NRV true ∧ dreyfusModel.CausallySufficient dreyfusBg V.NRV true V.MSG true

NRV is causally sufficient for MSG, the background settling neither.

The no-alternative clauses follow from the equations: a variable the development settles settles each parent to the value its equation needs (CausalModel.CausallyEntails.parent_eq), so settling MSG true needs NRV true, settling COM true needs MSG true, and settling SPY true needs COM true.

theorem Nadathur2023.nrv_of_msg {s : V → Flat Bool} (hs : s V.MSG = ⊥) (h : dreyfusModel.CausallyEntails s V.MSG true) : dreyfusModel.CausallyEntails s V.NRV true

Settling MSG true, unobserved, settles NRV true, since MSG = INT ∧ NRV.

theorem Nadathur2023.msg_of_com {s : V → Flat Bool} (hs : s V.COM = ⊥) (h : dreyfusModel.CausallyEntails s V.COM true) : dreyfusModel.CausallyEntails s V.MSG true

Settling COM true, unobserved, settles MSG true, since COM = MSG ∧ LST ∧ ¬BRK.

theorem Nadathur2023.com_of_spy {s : V → Flat Bool} (hs : s V.SPY = ⊥) (h : dreyfusModel.CausallyEntails s V.SPY true) : dreyfusModel.CausallyEntails s V.COM true

Settling SPY true, unobserved, settles COM true, since SPY = SEC ∧ COM.

def Nadathur2023.resolved : V → Flat Bool

The Dreyfus background with the nerve, listener and ungarbled message settled.

Equations

• Nadathur2023.resolved = Function.update (Function.update (Function.update Nadathur2023.dreyfusBg Nadathur2023.V.NRV ↑true) Nadathur2023.V.LST ↑true) Nadathur2023.V.BRK ↑false

theorem Nadathur2023.nrv_necessary_for_msg : ¬dreyfusModel.CausallyEntails dreyfusBg V.NRV true ∧ dreyfusModel.CausallyNecessary dreyfusModel.IsExogenousSettlement dreyfusBg V.NRV true V.MSG true

NRV is causally necessary for MSG, the background settling neither.

theorem Nadathur2023.dare_felicitous_for_msg (u : ↑(dreyfusModel.contexts dreyfusBg)) : dare V.MSG u ≠ 0

(34a) Dreyfus dared to send a message to the Germans is felicitous, since at every context of the background NRV is causally necessary and sufficient for MSG.

theorem Nadathur2023.msg_of_dare {u : ↑(dreyfusModel.contexts dreyfusBg)} (h : dare V.MSG u = 1) : dreyfusModel.solve ⊥ (↑u) V.MSG = true

(34a) entails that Dreyfus sent the message.

theorem Nadathur2023.not_msg_of_not_dare {u : ↑(dreyfusModel.contexts dreyfusBg)} (h : (-dare V.MSG) u = 1) : dreyfusModel.solve ⊥ (↑u) V.MSG ≠ true

(34b) Dreyfus did not dare to send a message to the Germans entails that he did not send it.

theorem Nadathur2023.dare_infelicitous_for_com (u : ↑(dreyfusModel.contexts dreyfusBg)) : dare V.COM u = 0

(34c) ?/# Dreyfus dared to establish communication with the Germans is infelicitous, since NRV is not causally sufficient for COM, which stays unsettled while LST and BRK are unresolved.

theorem Nadathur2023.dare_infelicitous_for_spy (u : ↑(dreyfusModel.contexts dreyfusBg)) : dare V.SPY u = 0

(34d) ?/# Dreyfus dared to spy for the Germans is infelicitous, since NRV is not causally sufficient for SPY, whose conditions LST, BRK and COM are all undetermined.

theorem Nadathur2023.nrv_necessary_for_com : dreyfusModel.CausallyNecessary dreyfusModel.IsExogenousSettlement dreyfusBg V.NRV true V.COM true

In (34c) NRV is nevertheless causally necessary for COM. Achievability settles the exogenous LST = 1 and BRK = 0, and every path to COM = 1 runs through NRV = 1.

theorem Nadathur2023.nrv_necessary_for_spy : dreyfusModel.CausallyNecessary dreyfusModel.IsExogenousSettlement dreyfusBg V.NRV true V.SPY true

In (34d) NRV is nevertheless causally necessary for SPY.

Definition 10b over consistent supersituations

Definition 10b quantifies over the consistent supersituations of the background. One of them settles the message, which the background leaves open, together with a listener and an ungarbled message, and so reaches communication and spying without the nerve.

def Nadathur2023.Consistent.messageSent : V → Flat Bool

The Dreyfus background with the message sent, a German listening, and the message ungarbled.

Equations

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

theorem Nadathur2023.Consistent.nrv_necessary_for_msg : dreyfusModel.CausallyNecessary (IsConsistentSupersituation dreyfusModel) dreyfusBg V.NRV true V.MSG true

Over consistent supersituations NRV is still causally necessary for MSG (34a), NRV being a parent of MSG.

theorem Nadathur2023.Consistent.not_nrv_necessary_for_com : ¬dreyfusModel.CausallyNecessary (IsConsistentSupersituation dreyfusModel) dreyfusBg V.NRV true V.COM true

Over consistent supersituations NRV is not causally necessary for COM, against the paper's verdict on (34c), since settling the message reaches communication without the nerve.

theorem Nadathur2023.Consistent.not_nrv_necessary_for_spy : ¬dreyfusModel.CausallyNecessary (IsConsistentSupersituation dreyfusModel) dreyfusBg V.NRV true V.SPY true

Over consistent supersituations NRV is not causally necessary for SPY, against the paper's verdict on (34d), since settling the message reaches spying without the nerve.

The Finnish implicatives

def Nadathur2023.finnish : List (Finnish.Verb × NaturalLogic.ImplicationSignature)

The implication signatures of the Finnish verbs. Onnistua is the bleached two-way verb, and uskaltaa, viitsiä, malttaa, hennoa, kehdata and ehtiä name their prerequisites, courage, engagement, patience, hard-heartedness, the lack of shame and time. Jaksaa names strength and mahtua being small enough, and both imply only when negated, as does pystyä, which the paper also allows might be a modal; laiminlyödä and epäröidä reverse the polarity.

Equations

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

theorem Nadathur2023.implicative_eq (p : Finnish.Verb × NaturalLogic.ImplicationSignature) : p ∈ finnish → p.1.implicative = p.2

Each signature is the one the Fragment's entry carries.

structure Nadathur2023.Row : Type

A minimal-pair member records the implication signature of its verb, the polarity of its matrix, and the polarity of the complement the paper says it implies, if any.

• signature : NaturalLogic.ImplicationSignature
• matrix : Polarity
• entails : Flat Polarity

def Nadathur2023.Row.ofDatum (e : Datum) : Option Row

A row from the paper's features.

Equations

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

theorem Nadathur2023.isSome_ofDatum (e : Datum) : e ∈ Examples.all → (Row.ofDatum e).isSome = true

Every example is a row.

def Nadathur2023.rows : List Row

The rows of the paper's Finnish minimal pairs.

Equations

• Nadathur2023.rows = List.filterMap Nadathur2023.Row.ofDatum Nadathur2023.Examples.all

theorem Nadathur2023.rows_agree (r : Row) : r ∈ rows → r.signature.implied r.matrix = r.entails

Each claim implies what its verb's signature says for its matrix polarity.