Adams (1975): The Logic of Conditionals: An Application of Probability to Deductive Logic

Adams asks when an inference is probabilistically sound: when making the premises certain enough makes the conclusion as certain as one likes. A factual formula's probability is the probability that it is true, and an indicative conditional's is the conditional probability of its consequent given its antecedent. For factual formulas the answer is classical: such an inference is probabilistically sound exactly when it is logically valid, and then the conclusion's uncertainty, its probability of being false, is at most the sum of the premises'. For conditionals the two part ways. Contraposition, the inference of a conditional from a disjunction, the hypothetical syllogism and the strengthening of an antecedent are valid for the material conditional but not probabilistically sound, which is why the English inferences Adams prints are unacceptable; what p-entailment does satisfy is the rules for conditionals of his natural deduction system.

Main results

• tfae_pEntails: for factual formulas, logical consequence, p-entailment, the uncertainty bound under every probability, and the preservation of certainty coincide.
• isPreferential_pEntails: p-entailment from a set of conditionals is closed under the rules for conditionals of Adams's natural deduction system.
• materially_valid_not_pEntailed, printed_inferences: the patterns of conditional inference Adams examines are valid for the material conditional but not p-entailed, and the English inferences he prints are unacceptable instances of them.
• not_isRational_pEntails: unlike the closest-worlds conditional on a total order, p-entailment does not validate rational monotonicity.

Implementation notes

• Possible states of affairs form a measurable space, a formula is the set of states where it is true, and a probability-assignment is a probability measure, after Adams's assumption that a proposition's probability is the measure of the states in which it is true. His assignments are finitely additive on formulas; over finitely many atoms these are the measures on truth assignments, and beyond that countable additivity is an added assumption.
• Every formula is a conditional Formula, a factual one having a tautological antecedent, as rule R1 makes them interderivable; an assignment is proper when it gives each antecedent positive probability. Uncertainty, probability of falsity, is stated directly as μ Aᶜ.
• The natural deduction rules are proved on a discrete space, where every set of states is an event, as for the finite sentential languages Adams considers.

TODO

• The completeness half of Theorem 4.2, that the rules derive every p-entailed conditional, and Theorem 3.3 for conditional premises, that a p-consistent set p-entails only conclusions whose material counterparts its own entail.

References

• E. W. Adams, The Logic of Conditionals: An Application of Probability to Deductive Logic

Formulas of the conditional extension

structure Adams1975.Formula (Ω : Type u_1) : Type u_1

A formula of the conditional extension, if ante then cons.

• ante : Set Ω

  The antecedent.

• cons : Set Ω

  The consequent.

def Adams1975.Formula.fact {Ω : Type u_1} (A : Set Ω) : Formula Ω

The factual formula A, if ⊤ then A.

Equations

• Adams1975.Formula.fact A = { ante := Set.univ, cons := A }

def Adams1975.Formula.material {Ω : Type u_1} (φ : Formula Ω) : Set Ω

The material counterpart of a formula, ante ⊃ cons.

Equations

• φ.material = Conditional.materialImp φ.ante φ.cons

def Adams1975.PEntails {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] (s : Finset ι) (X : ι → Formula Ω) (d : Formula Ω) : Prop

The premises X i, i ∈ s, p-entail d when, however probable d must be, making every premise probable enough makes it so, under every probability proper for them (Definition 2).

Equations

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

theorem Adams1975.pEntails_of_mem {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {s : Finset ι} {X : ι → Formula Ω} {i : ι} (hi : i ∈ s) : PEntails s X (X i)

A set p-entails each of its members (Theorem 4.1).

theorem Adams1975.one_sub_le_cond_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {A B : Set Ω} {δ : ENNReal} (hA : MeasurableSet A) (hB : MeasurableSet B) (h0 : μ A ≠ 0) : 1 - δ ≤ μ[B | A] ↔ μ (A ∩ Bᶜ) ≤ δ * μ A

A conditional is probable within δ iff its antecedent's falsifying part has at most δ of its antecedent's mass.

Factual inferences

theorem Adams1975.pEntails_fact_iff {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {s : Finset ι} {A : ι → Set Ω} {B : Set Ω} : PEntails s (fun (i : ι) => Formula.fact (A i)) (Formula.fact B) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (μ : MeasureTheory.Measure Ω), MeasureTheory.IsProbabilityMeasure μ → (∀ i ∈ s, 1 - δ ≤ μ (A i)) → 1 - ε ≤ μ B

theorem Adams1975.uncertainty_le_sum {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {s : Finset ι} {A : ι → Set Ω} {B : Set Ω} (h : ⋂ i ∈ s, A i ⊆ B) (μ : MeasureTheory.Measure Ω) : μ Bᶜ ≤ ∑ i ∈ s, μ (A i)ᶜ

The uncertainty of a logical consequence is at most the sum of the premises' uncertainties, the rule of Section I.1 that Theorem 3.1 generalizes.

theorem Adams1975.exists_dirac_of_not_subset {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {s : Finset ι} {A : ι → Set Ω} {B : Set Ω} (hB : MeasurableSet B) (h : ¬⋂ i ∈ s, A i ⊆ B) : ∃ (w : Ω), (∀ i ∈ s, (MeasureTheory.Measure.dirac w) (A i) = 1) ∧ (MeasureTheory.Measure.dirac w) B = 0

A state where the premises hold and the conclusion fails gives a probability measure, its point mass, that makes the premises certain and the conclusion certainly false.

theorem Adams1975.tfae_pEntails {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {s : Finset ι} {A : ι → Set Ω} {B : Set Ω} (hA : ∀ i ∈ s, MeasurableSet (A i)) (hB : MeasurableSet B) : [⋂ i ∈ s, A i ⊆ B, PEntails s (fun (i : ι) => Formula.fact (A i)) (Formula.fact B), ∀ (μ : MeasureTheory.Measure Ω), MeasureTheory.IsProbabilityMeasure μ → μ Bᶜ ≤ ∑ i ∈ s, μ (A i)ᶜ, ∀ (μ : MeasureTheory.Measure Ω), MeasureTheory.IsProbabilityMeasure μ → (∀ i ∈ s, μ (A i) = 1) → μ B = 1].TFAE

Theorems 3.1, 3.3 and 3.4, for factual formulas. Logical consequence, p-entailment, the uncertainty bound under every probability, and the preservation of certainty coincide; for factual premises 3.3 needs no consistency assumption.

theorem Adams1975.exists_of_not_pEntails {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {s : Finset ι} {A : ι → Set Ω} {B : Set Ω} (hA : ∀ i ∈ s, MeasurableSet (A i)) (hB : MeasurableSet B) (h : ¬PEntails s (fun (i : ι) => Formula.fact (A i)) (Formula.fact B)) (ε : ENNReal) : ∃ (μ : MeasureTheory.Measure Ω), MeasureTheory.IsProbabilityMeasure μ ∧ (∀ i ∈ s, 1 - ε ≤ μ (A i)) ∧ μ B ≤ ε

Where the premises do not p-entail the conclusion, premises as probable as one likes are compatible with a conclusion as improbable as one likes (Theorem 3.2, for factual formulas).

theorem Adams1975.lottery_attains_bound (n : ℕ) : have μ := ProbabilityTheory.uniformOn Set.univ; μ (⋂ i ∈ Finset.univ, {i}ᶜ)ᶜ = 1 ∧ ∑ i : Fin (n + 1), μ {i}ᶜᶜ = 1

The lottery. Each of n + 1 tickets loses with uncertainty 1 / (n + 1), yet that every ticket loses is certainly false, so the uncertainty bound holds with equality.

Conditional inferences

theorem Adams1975.pEntails_iff_mass {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {s : Finset ι} [DiscreteMeasurableSpace Ω] {X : ι → Formula Ω} {φ ψ : Set Ω} : PEntails s X { ante := φ, cons := ψ } ↔ ∀ ε > 0, ∃ δ > 0, ∀ (μ : MeasureTheory.Measure Ω), MeasureTheory.IsProbabilityMeasure μ → (∀ i ∈ s, μ (X i).ante ≠ 0) → (∀ i ∈ s, 1 - δ ≤ μ[(X i).cons | (X i).ante]) → μ (φ ∩ ψᶜ) ≤ ε * μ φ

P-entailment of if φ then ψ bounds the mass of the states falsifying it by a fraction of its antecedent's, under every probability proper for the premises.

theorem Adams1975.isPreferential_pEntails {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [DiscreteMeasurableSpace Ω] (s : Finset ι) (X : ι → Formula Ω) : Nonmonotonic.IsPreferential fun (φ ψ : Set Ω) => PEntails s X { ante := φ, cons := ψ }

Theorem 4.2, its rules R2 to R6. P-entailment from a set of conditionals, read as a relation between antecedent and consequent, is reflexive and closed under weakening and conjunction of consequents, disjunction of antecedents, and the strengthening of an antecedent by one of its consequents, the rules from which R2 to R6 follow.

theorem Adams1975.not_pEntails_of_falsify {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {s : Finset ι} [DiscreteMeasurableSpace Ω] {X : ι → Formula Ω} {d : Formula Ω} {v w : Ω} (hv : v ∈ d.ante) (hvd : v ∉ d.cons) (hw : w ∉ d.ante) (hX : ∀ i ∈ s, w ∈ (X i).ante ∧ w ∈ (X i).cons ∨ w ∉ (X i).ante ∧ v ∈ (X i).ante ∧ v ∈ (X i).cons) : ¬PEntails s X d

Two states give a probabilistic counterexample when one, v, falsifies the conclusion, whose antecedent the other, w, misses, and each premise is verified by w, or misses w and is verified by v: weighting v lightly makes every premise probable and the conclusion improbable, as Adams's Venn diagrams depict.

Patterns of conditional inference

The states are the truth-assignments to three atomic formulas A, B and C, and the patterns are those of Section I.3 with Adams's lettering.

@[reducible, inline]

abbrev Adams1975.Assignment : Type

A truth-assignment to the atomic formulas A, B and C.

Equations

• Adams1975.Assignment = (Fin 3 → Bool)

def Adams1975.atom (k : Fin 3) : Set Assignment

The atomic formulas A, B and C.

Equations

• Adams1975.atom k = {v : Adams1975.Assignment | v k = true}

inductive Adams1975.Pattern : Type

The patterns of conditional inference Adams examines.

• firstFallacy : Pattern

  From −A to A ⇒ B, the first fallacy of material implication.

• secondFallacy : Pattern

  From B to A ⇒ B, the second fallacy of material implication.

• contraposition : Pattern

  From B ⇒ −A to A ⇒ −B.

• disjunction : Pattern

  From A ∨ B to −A ⇒ B.

• hypotheticalSyllogism : Pattern

  From A ⇒ B and B ⇒ C to A ⇒ C.

• antecedentRestriction : Pattern

  From B ⇒ C to (A & B) ⇒ C.

@[instance_reducible]

instance Adams1975.instDecidableEqPattern : DecidableEq Pattern

Equations

• Adams1975.instDecidableEqPattern x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Adams1975.instReprPattern.repr : Pattern → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Adams1975.instReprPattern : Repr Pattern

Equations

• Adams1975.instReprPattern = { reprPrec := Adams1975.instReprPattern.repr }

@[instance_reducible]

instance Adams1975.instFintypePattern : Fintype Pattern

Equations

• Adams1975.instFintypePattern = { elems := { val := ↑Adams1975.Pattern.enumList, nodup := Adams1975.Pattern.enumList_nodup }, complete := Adams1975.instFintypePattern._proof_1 }

def Adams1975.Pattern.premises : Pattern → List (Formula Assignment)

The premises of a pattern.

Equations

• Adams1975.Pattern.firstFallacy.premises = [Adams1975.Formula.fact (Adams1975.atom 0)ᶜ]
• Adams1975.Pattern.secondFallacy.premises = [Adams1975.Formula.fact (Adams1975.atom 1)]
• Adams1975.Pattern.contraposition.premises = [{ ante := Adams1975.atom 1, cons := (Adams1975.atom 0)ᶜ }]
• Adams1975.Pattern.disjunction.premises = [Adams1975.Formula.fact (Adams1975.atom 0 ∪ Adams1975.atom 1)]
• Adams1975.Pattern.hypotheticalSyllogism.premises = [{ ante := Adams1975.atom 0, cons := Adams1975.atom 1 }, { ante := Adams1975.atom 1, cons := Adams1975.atom 2 }]
• Adams1975.Pattern.antecedentRestriction.premises = [{ ante := Adams1975.atom 1, cons := Adams1975.atom 2 }]

def Adams1975.Pattern.conclusion : Pattern → Formula Assignment

The conclusion of a pattern.

Equations

• Adams1975.Pattern.firstFallacy.conclusion = { ante := Adams1975.atom 0, cons := Adams1975.atom 1 }
• Adams1975.Pattern.secondFallacy.conclusion = { ante := Adams1975.atom 0, cons := Adams1975.atom 1 }
• Adams1975.Pattern.contraposition.conclusion = { ante := Adams1975.atom 0, cons := (Adams1975.atom 1)ᶜ }
• Adams1975.Pattern.disjunction.conclusion = { ante := (Adams1975.atom 0)ᶜ, cons := Adams1975.atom 1 }
• Adams1975.Pattern.hypotheticalSyllogism.conclusion = { ante := Adams1975.atom 0, cons := Adams1975.atom 2 }
• Adams1975.Pattern.antecedentRestriction.conclusion = { ante := Adams1975.atom 0 ∩ Adams1975.atom 1, cons := Adams1975.atom 2 }

def Adams1975.Pattern.name : Pattern → String

The name a pattern bears in the data.

Equations

• Adams1975.Pattern.firstFallacy.name = "firstFallacy"
• Adams1975.Pattern.secondFallacy.name = "secondFallacy"
• Adams1975.Pattern.contraposition.name = "contraposition"
• Adams1975.Pattern.disjunction.name = "disjunction"
• Adams1975.Pattern.hypotheticalSyllogism.name = "hypotheticalSyllogism"
• Adams1975.Pattern.antecedentRestriction.name = "antecedentRestriction"

def Adams1975.Pattern.MateriallyValid (π : Pattern) : Prop

The pattern is valid for the material conditional.

Equations

• π.MateriallyValid = ∀ (v : Adams1975.Assignment), (∀ φ ∈ π.premises, v ∈ φ.material) → v ∈ π.conclusion.material

def Adams1975.Pattern.PEntailed (π : Pattern) : Prop

The premises p-entail the conclusion.

Equations

• π.PEntailed = Adams1975.PEntails Finset.univ π.premises.get π.conclusion

def Adams1975.Pattern.witnesses : Pattern → Assignment × Assignment

A state that falsifies the conclusion and one that verifies the premises, from Adams's figures.

Equations

• Adams1975.Pattern.firstFallacy.witnesses = (![true, false, false], ![false, false, false])
• Adams1975.Pattern.secondFallacy.witnesses = (![true, false, false], ![false, true, false])
• Adams1975.Pattern.contraposition.witnesses = (![true, true, false], ![false, true, false])
• Adams1975.Pattern.disjunction.witnesses = (![false, false, false], ![true, false, false])
• Adams1975.Pattern.hypotheticalSyllogism.witnesses = (![true, true, false], ![false, true, true])
• Adams1975.Pattern.antecedentRestriction.witnesses = (![true, true, false], ![false, true, true])

theorem Adams1975.materially_valid_not_pEntailed (π : Pattern) : π.MateriallyValid ∧ ¬π.PEntailed

Section I.3. Each pattern is valid for the material conditional but not p-entailed.

theorem Adams1975.printed_inferences (e : Datum) : e ∈ Examples.all → e.judgment = Judgment.unacceptable ∧ ∃ (π : Pattern), e.feature? "pattern" = some π.name ∧ π.MateriallyValid ∧ ¬π.PEntailed

The printed inferences. Each English inference Adams prints is unacceptable and instantiates a pattern valid for the material conditional but not p-entailed.

theorem Adams1975.not_isRational_pEntails : ¬Nonmonotonic.IsRational fun (φ ψ : Set Assignment) => PEntails Finset.univ ![{ ante := atom 1, cons := atom 2 }] { ante := φ, cons := ψ }

P-entailment is not rational. B ⇒ C p-entails neither B ⇒ −A nor, by Antecedent Restriction's counterexample, (B & A) ⇒ C, so rational monotonicity fails, which the closest-worlds conditional on a total order satisfies (Conditional.isRational_closestImp).