Schöter's thesis: the guard as a presupposition operator

[Sch96b]

[Sch96b] (the dissertation behind [Sch96a]) analyzes presupposition in EBL two ways: as defeasible inference links (the route its §6.2.3 shares with [Sch96a] §4), and — in material not carried over to the paper — through Fitting's guard connective φ : ψ (Bilattice.Evidential.guard), read as "ψ presupposing φ". The guard encodes Burton-Roberts' truth-gap intuition: the compound has a value only when the presupposition is at least true, and is otherwise the gap U, whatever the carrier's value. Its Table 6.1 gives the guard's four-valued table on FOUR.

The thesis's salient presuppositional intuition — a presupposition is implied equally by a sentence and by its negation — holds for the guard by construction: negating the carrier commutes with guarding (guard_neg, a definitional equality), so the presuppositional component is untouched by negation. This is the projection-under-negation test at the value level.

Main results

• guard_table — the guard's four-valued table on FOUR (Table 6.1)
• guard_undefined_of_failure — presupposition failure yields the gap U, whatever the carrier (the truth-gap intuition)
• guard_neg — the guard commutes with negation of the carrier (the salient presuppositional intuition, by rfl)

theorem Schoter1996Thesis.guard_table (y : Bilattice.FOUR) : Bilattice.Evidential.guard Bilattice.FOUR.T y = y ∧ Bilattice.Evidential.guard Bilattice.FOUR.U y = Bilattice.FOUR.U ∧ Bilattice.Evidential.guard Bilattice.FOUR.F y = Bilattice.FOUR.U ∧ Bilattice.Evidential.guard Bilattice.FOUR.I y = y

The guard's four-valued table on FOUR ([Sch96b] Table 6.1): a true or overdefined presupposition passes the carrier through; an unknown or false presupposition gaps the compound.

theorem Schoter1996Thesis.guard_undefined_of_failure {S : Type u_1} [SemilatticeInf S] [BoundedOrder S] (ψ : Bilattice.Evidential S) : Bilattice.Evidential.guard (Bilattice.Product.mk ⊥ ⊤) ψ = Bilattice.Product.mk ⊥ ⊥

The truth-gap intuition ([Sch96b] §6.2.3): when the presupposition is false, the compound is the gap U whatever the carrier's value.

theorem Schoter1996Thesis.guard_neg {S : Type u_1} [SemilatticeInf S] (x y : Bilattice.Evidential S) : x.guard (Bilattice.Product.neg y) = Bilattice.Product.neg (x.guard y)

The salient presuppositional intuition ([Sch96b] §6.2.3): the guard commutes with negation of the carrier, so a sentence and its negation carry the same presuppositional component — projection under negation, by construction.