Karttunen (1971): Some observations on factivity

Karttunen describes a factive verb by meaning postulates rather than by a presupposition split off from its sentence. A sentence is true, false or neither, and one sentence necessitates another, in van Fraassen's term, when the second is true wherever the first is. For a semi-factive such as discover, the sentence and its negation each necessitate the complement. For a true factive such as regret, so do the possibility of the sentence and the possibility of its negation, which Karttunen proposes as the definition of presupposition in general.

An assertion commits its speaker to the sentence and a negative assertion to its negation, while a question and the antecedent of a conditional conversationally imply only that the sentence is possible. The two classes therefore agree in assertions and come apart in the other environments.

Main statements

• Karttunen1971b.projects_iff: the complement follows in every model exactly when the verb is a true factive or the sentence is asserted or negated.
• Karttunen1971b.projection_rows: the paper's judgments on regret, realize and discover are these predictions.
• Karttunen1971b.emphatic_denial: denying that a true factive sentence is true is consistent with the falsity of its complement.

Implementation notes

• Possibility is read on an accessibility relation, of which the paper assumes only that what is the case is possible, so the relation is reflexive and otherwise arbitrary.
• A question and a conditional antecedent are represented by the possibility they conversationally imply.
• The subjunctive poss-ing complements of section 2 are not represented.

References

• [Kar71b]
• [vF68]
• [KK70]

The meaning postulates

def Karttunen1971b.Postulates {W : Type u_1} (c : Presupposition.Factivity) (R : SetRel W W) (A : W → SignType) (s : W → Prop) : Prop

The meaning postulates of a factivity class, for a sentence A with complement s. A semi-factive sentence and its negation each necessitate the complement, (11). For a true factive the possibility of the sentence and the possibility of its negation do, (11′), which is to say that the sentence presupposes its complement (fn. 8).

Equations

• Karttunen1971b.Postulates Presupposition.Factivity.semi R A s = ((fun (x : W) => A x = 1) ≤ s ∧ (fun (x : W) => -A x = 1) ≤ s)
• Karttunen1971b.Postulates Presupposition.Factivity.full R A s = ((ModalLogic.Diamond R fun (x : W) => A x = 1) ≤ s ∧ (ModalLogic.Diamond R fun (x : W) => -A x = 1) ≤ s)

theorem Karttunen1971b.postulates_semi_iff {W : Type u_1} {R : SetRel W W} {A : W → SignType} {s : W → Prop} : Postulates Presupposition.Factivity.semi R A s ↔ (fun (x : W) => A x ≠ 0) ≤ s

A semi-factive sentence has a truth value only where its complement is true.

theorem Karttunen1971b.postulates_full_iff {W : Type u_1} {R : SetRel W W} {A : W → SignType} {s : W → Prop} : Postulates Presupposition.Factivity.full R A s ↔ (ModalLogic.Diamond R fun (x : W) => A x ≠ 0) ≤ s

The complement of a true factive is true wherever its sentence may have a truth value.

theorem Karttunen1971b.postulates_full_iff_le_box {W : Type u_1} {R : SetRel W W} {A : W → SignType} {s : W → Prop} : Postulates Presupposition.Factivity.full R A s ↔ (fun (x : W) => A x ≠ 0) ≤ ModalLogic.Box R.inv s

A true factive sentence has a truth value only where its complement is necessary, along the converse of the accessibility relation.

theorem Karttunen1971b.Postulates.semi {W : Type u_1} {R : SetRel W W} {A : W → SignType} {s : W → Prop} [R.IsRefl] (h : Postulates Presupposition.Factivity.full R A s) : Postulates Presupposition.Factivity.semi R A s

The stronger postulates yield the weaker ones, since what is the case is possible (fn. 9).

Environments

def Karttunen1971b.commitment {W : Type u_1} (R : SetRel W W) (A : W → SignType) : Presupposition.FamilyVariant → W → Prop

What the speaker of a sentence in an environment is committed to. An assertion commits her to the sentence and a negative assertion to its negation. A question and the antecedent of a conditional conversationally imply that the sentence is possible (fn. 5), which a possibility statement asserts, (26).

Equations

• Karttunen1971b.commitment R A Presupposition.FamilyVariant.unembedded = fun (x : W) => A x = 1
• Karttunen1971b.commitment R A Presupposition.FamilyVariant.negation = fun (x : W) => -A x = 1
• Karttunen1971b.commitment R A Presupposition.FamilyVariant.question = ModalLogic.Diamond R fun (x : W) => A x = 1
• Karttunen1971b.commitment R A Presupposition.FamilyVariant.conditionalAntecedent = ModalLogic.Diamond R fun (x : W) => A x = 1
• Karttunen1971b.commitment R A Presupposition.FamilyVariant.epistemicModal = ModalLogic.Diamond R fun (x : W) => A x = 1

def Karttunen1971b.Projects (c : Presupposition.Factivity) (e : Presupposition.FamilyVariant) : Prop

The complement of a factive of class c follows in environment e when, in every model where what is the case is possible, the complement of a sentence obeying the postulates of c is true wherever the speaker's commitment is.

Equations

• Karttunen1971b.Projects c e = ∀ (W : Type) (R : SetRel W W) [R.IsRefl] (A : W → SignType) (s : W → Prop), Karttunen1971b.Postulates c R A s → Karttunen1971b.commitment R A e ≤ s

theorem Karttunen1971b.Postulates.commitment_le {W : Type u_1} {R : SetRel W W} {A : W → SignType} {s : W → Prop} {c : Presupposition.Factivity} {e : Presupposition.FamilyVariant} [R.IsRefl] (h : Postulates c R A s) (hce : c = Presupposition.Factivity.full ∨ e = Presupposition.FamilyVariant.unembedded ∨ e = Presupposition.FamilyVariant.negation) : commitment R A e ≤ s

theorem Karttunen1971b.exists_semi_not_diamond_le : ∃ (R : SetRel Bool Bool) (_ : R.IsRefl) (A : Bool → SignType) (s : Bool → Prop), Postulates Presupposition.Factivity.semi R A s ∧ ¬(ModalLogic.Diamond R fun (x : Bool) => A x = 1) ≤ s

The possibility of a semi-factive sentence does not necessitate its complement, since from the fact that one may discover something it does not follow that it is the case, (26b) and (26c).

theorem Karttunen1971b.projects_iff {c : Presupposition.Factivity} {e : Presupposition.FamilyVariant} : Projects c e ↔ c = Presupposition.Factivity.full ∨ e = Presupposition.FamilyVariant.unembedded ∨ e = Presupposition.FamilyVariant.negation

The complement follows exactly when the verb is a true factive or the sentence is asserted or negated.

@[instance_reducible]

instance Karttunen1971b.instDecidableProjects (c : Presupposition.Factivity) (e : Presupposition.FamilyVariant) : Decidable (Projects c e)

Equations

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

theorem Karttunen1971b.Projects.commitment_le {W : Type u_1} {R : SetRel W W} {A : W → SignType} {s : W → Prop} {c : Presupposition.Factivity} {e : Presupposition.FamilyVariant} [R.IsRefl] (hp : Projects c e) (h : Postulates c R A s) : commitment R A e ≤ s

In a model of any universe, the complement is true wherever the commitment is.

theorem Karttunen1971b.exists_complement {W : Type u_1} {R : SetRel W W} {c : Presupposition.Factivity} {e : Presupposition.FamilyVariant} {ι : Type u_2} {S : ι → Prop} {A : ι → W → SignType} {s : ι → W → Prop} [R.IsRefl] (hp : Projects c e) (hA : ∀ (x : ι), Postulates c R (A x) (s x)) {w : W} (h : ∃ (x : ι), S x ∧ commitment R (A x) e w) : ∃ (x : ι), S x ∧ s x w

The postulates apply instance by instance under a quantifier that binds into the complement. If some senators regret that they voted for the SST, (5), or possibly regret it, (14), then some senators voted for it.

The rows

theorem Karttunen1971b.projection_rows (row : Datum) : row ∈ Examples.all → row.feature? "diagnostic" = some "projection" → ∀ e ∈ row.environment?, ∀ b ∈ row.projective?, ∃ v ∈ English.Verbs.verbs, row.feature? "verb" = some v.form ∧ ∃ c ∈ v.factivity, b = true ↔ Projects c e

The judgments of (2), (22) and (24)–(26) are the predictions of the postulates for the English entry of each verb, the complement of regret following everywhere and that of realize and discover in assertions and under negation only.

The emphatic denial

theorem Karttunen1971b.emphatic_denial : ∃ (R : SetRel Unit Unit) (_ : R.IsRefl) (A : Unit → SignType) (s : Unit → Prop), Postulates Presupposition.Factivity.full R A s ∧ -SignType.ofProp (A () = 1) = 1 ∧ ¬ModalLogic.Diamond R (fun (x : Unit) => A x ≠ 0) () ∧ ¬s ()

The emphatic denial of a true factive sentence, it is not true that John regretted that he had not told the truth, is consistent with the falsity of the complement, (23). It is the external negation of three-valued logic, from which neither the possibility of the sentence nor that of its negation follows (fn. 7).