Readings of a conditional

This file defines the two readings of a conditional. A conditional is read as hypothetical when its antecedent is supposed and left open, and as a premise conditional when the antecedent echoes prior discourse and is treated as established, the distinction of Iatridou and Haegeman. On the hypothetical reading if p, q denotes the conditional proposition of whatever operator the theory supplies, and on the premise reading it asserts q with p presupposed, the given that paraphrase. The two readings give the antecedent opposite entailment directions, the source of their opposite polarity-item profiles: for a conditional over a domain that grows with the antecedent, such as the material or the strict conditional, the hypothetical antecedent is downward entailing and every other clause upward entailing, while over the closest antecedent-worlds the antecedent is neither. Languages may lexicalize the split, as Japanese -ra and German falls mark only hypothetical conditionals.

Main definitions

• Conditional.Reading: the hypothetical and premise readings.
• Conditional.Reading.denote: the denotation of if p, q under a reading, a trivalent proposition.
• Conditional.Reading.clauseSignature: the projectivity signature of each clause under a reading, whose sign is Conditional.Reading.clausePolarity.
• Conditional.Marker: a conditional marker with the readings it can mark.

Main results

• Conditional.Reading.soundFor_clauseSignature: over a monotone domain the signatures are sound.
• Conditional.Reading.exists_not_antitone_hypothetical_closestImp: over the closest antecedent-worlds the hypothetical antecedent is not downward entailing.

References

• S. Iatridou, Topics in Conditionals (1991)
• L. Haegeman, Conditional clauses: External and internal syntax (2003)
• D. Lassiter, Sorting Out Left-Nested Conditionals (2025)

inductive Conditional.Reading : Type

The readings of a conditional, on which the antecedent is supposed and left open or echoes prior discourse and is treated as established.

• hypothetical : Reading
• premise : Reading

@[instance_reducible]

instance Conditional.instDecidableEqReading : DecidableEq Reading

Equations

• Conditional.instDecidableEqReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Conditional.instFintypeReading : Fintype Reading

Equations

• Conditional.instFintypeReading = { elems := { val := ↑Conditional.Reading.enumList, nodup := Conditional.Reading.enumList_nodup }, complete := Conditional.instFintypeReading._proof_1 }

@[instance_reducible]

instance Conditional.instReprReading : Repr Reading

Equations

• Conditional.instReprReading = { reprPrec := Conditional.instReprReading.repr }

def Conditional.instReprReading.repr : Reading → ℕ → Std.Format

Equations

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

inductive Conditional.Clause : Type

The two clauses of a conditional.

• antecedent : Clause
• consequent : Clause

@[instance_reducible]

instance Conditional.instDecidableEqClause : DecidableEq Clause

Equations

• Conditional.instDecidableEqClause x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Conditional.instFintypeClause : Fintype Clause

Equations

• Conditional.instFintypeClause = { elems := { val := ↑Conditional.Clause.enumList, nodup := Conditional.Clause.enumList_nodup }, complete := Conditional.instFintypeClause._proof_1 }

def Conditional.instReprClause.repr : Clause → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Conditional.instReprClause : Repr Clause

Equations

• Conditional.instReprClause = { reprPrec := Conditional.instReprClause.repr }

@[simp]

theorem Conditional.Reading.forall {P : Reading → Prop} : (∀ (ct : Reading), P ct) ↔ P hypothetical ∧ P premise

@[simp]

theorem Conditional.Reading.exists {P : Reading → Prop} : (∃ (ct : Reading), P ct) ↔ P hypothetical ∨ P premise

noncomputable def Conditional.Reading.denote {W : Type u_1} (cond : Set W → Set W → Set W) (p q : Set W) : Reading → W → SignType

The denotation of if p, q under a reading, for a conditional operator cond on total propositions. The hypothetical reading is cond p q, and the premise reading asserts q with p presupposed.

Equations

• Conditional.Reading.denote cond p q Conditional.Reading.hypothetical = fun (w : W) => SignType.ofProp (w ∈ cond p q)
• Conditional.Reading.denote cond p q Conditional.Reading.premise = p.indicator fun (w : W) => SignType.ofProp (w ∈ q)

@[simp]

theorem Conditional.Reading.denote_hypothetical_eq_one_iff {W : Type u_1} {cond : Set W → Set W → Set W} {p q : Set W} {w : W} : denote cond p q hypothetical w = 1 ↔ w ∈ cond p q

@[simp]

theorem Conditional.Reading.denote_premise_eq_one_iff {W : Type u_1} {cond : Set W → Set W → Set W} {p q : Set W} {w : W} : denote cond p q premise w = 1 ↔ w ∈ p ∧ w ∈ q

theorem Conditional.Reading.denote_hypothetical_materialImp_eq_premise {W : Type u_1} {p q : Set W} {w : W} (hw : w ∈ p) : denote materialImp p q hypothetical w = denote materialImp p q premise w

Where the antecedent holds, the hypothetical reading of the material conditional and the premise reading agree.

Entailment directions

The clauses of a conditional over a domain of antecedent-worlds have the projectivity signatures of natural logic: the hypothetical antecedent is antitone when the domain grows with the antecedent, and every other clause is monotone. The material and the strict conditional have such domains; the conditional of the closest antecedent-worlds does not, since antecedent strengthening fails for it.

def Conditional.Reading.clauseSignature : Reading → Clause → NaturalLogic.Signature

The projectivity signature of a clause under a reading is antitone for the hypothetical antecedent and monotone for every other clause.

Equations

• Conditional.Reading.hypothetical.clauseSignature Conditional.Clause.antecedent = NaturalLogic.Signature.anti
• x✝¹.clauseSignature x✝ = NaturalLogic.Signature.mono

def Conditional.Reading.clausePolarity (ct : Reading) (c : Clause) : SignType

The entailment direction of a clause under a reading, the sign of its signature.

Equations

• ct.clausePolarity c = (ct.clauseSignature c).sign

def Conditional.Reading.clauseMap {W : Type u_1} (cond : Set W → Set W → Set W) (p q : Set W) (ct : Reading) : Clause → Set W → Set W

The function of a clause under a reading, the other clause held fixed, on truth sets.

Equations

• Conditional.Reading.clauseMap cond p q ct Conditional.Clause.antecedent = fun (p' : Set W) => Trivalent.posExt (Conditional.Reading.denote cond p' q ct)
• Conditional.Reading.clauseMap cond p q ct Conditional.Clause.consequent = fun (q' : Set W) => Trivalent.posExt (Conditional.Reading.denote cond p q' ct)

theorem Conditional.Reading.antitone_posExt_hypothetical {W : Type u_1} {D : W → Set W → Set W} (hD : ∀ (w : W), Monotone (D w)) (q : Set W) : Antitone fun (p : Set W) => Trivalent.posExt (denote (ofDomain D) p q hypothetical)

The hypothetical antecedent is antitone over a domain that grows with the antecedent.

theorem Conditional.Reading.monotone_posExt_premise {W : Type u_1} (cond : Set W → Set W → Set W) (q : Set W) : Monotone fun (p : Set W) => Trivalent.posExt (denote cond p q premise)

The premise antecedent is monotone for every operator.

theorem Conditional.Reading.monotone_posExt_consequent {W : Type u_1} {D : W → Set W → Set W} (ct : Reading) (p : Set W) : Monotone fun (q : Set W) => Trivalent.posExt (denote (ofDomain D) p q ct)

The consequent is monotone on either reading of a conditional over a domain.

theorem Conditional.Reading.soundFor_clauseSignature {W : Type u_1} {D : W → Set W → Set W} (hD : ∀ (w : W), Monotone (D w)) (p q : Set W) (ct : Reading) (c : Clause) : (ct.clauseSignature c).SoundFor (clauseMap (ofDomain D) p q ct c)

Over a domain that grows with the antecedent, each clause's signature is sound for the clause's function.

theorem Conditional.Reading.exists_not_antitone_hypothetical_closestImp : ∃ (ord : Fin 3 → Preorder (Fin 3)) (q : Set (Fin 3)), ¬Antitone fun (p : Set (Fin 3)) => Trivalent.posExt (denote (closestImp ord) p q hypothetical)

Over the closest antecedent-worlds the hypothetical antecedent is not antitone — with three worlds ranked 0 < 1 < 2 from 0, if 1 or 2, then 1 holds at 0 while if 2, then 1 does not.

structure Conditional.Marker : Type

A conditional marker is a form together with the readings it can mark. Japanese -ra and German falls mark only hypothetical conditionals, and nara, wenn and English if mark either ([Las25]).

• form : String

  The marker's citation form.

• readings : Finset Reading

  The readings the marker can mark.

def Conditional.instDecidableEqMarker.decEq (x✝ x✝¹ : Marker) : Decidable (x✝ = x✝¹)

Equations

• Conditional.instDecidableEqMarker.decEq { form := a, readings := a_1 } { form := b, readings := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Conditional.instDecidableEqMarker : DecidableEq Marker

Equations

• Conditional.instDecidableEqMarker = Conditional.instDecidableEqMarker.decEq