Schöter (1996a): The Computational Application of Bilattice Logic to Natural Reasoning

This file formalizes the thesis's assessment of the guard connective as a presupposition operator (§6.2.3). Of the two intuitions of [BR89] the thesis weighs, the truth-gap intuition that a carrier whose presupposition fails is undefined, and the salient presuppositional intuition that a sentence and its negation presuppose alike, Fitting's guard φ : ψ (Bilattice.Product.guard), read as ψ presupposing φ, encodes both at the value level. On FOUR it passes the carrier through when the presupposition is at least true and gaps it otherwise (Table 6.1, guard_table), presupposition failure gaps the compound whatever the carrier's value (guard_undefined_of_failure), and the guard commutes with negation of the carrier, so the presuppositional component survives negation (guard_compl). The thesis nevertheless rejects the guard for factive presupposition, since it draws no distinction between the presuppositions of positive and negative carriers, which are cancellable only under negation, and analyzes presupposition instead as a bundle of inference links, a strict modus ponens, a defeasible modus ponens under negation and a modus tollens (Definition 6.5), on the epistemic-state machinery that Studies/Schoter1996b leaves unformalized.

References

• [Sch96b]
• [Sch96a]
• [BR89]
• [Fit94]

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

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

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

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

theorem Schoter1996a.guard_compl {S : Type u_1} [SemilatticeInf S] (x y : Bilattice.Product S S) : x.guard yᶜ = (x.guard y)ᶜ

The salient presuppositional intuition (§6.2.3): the guard commutes with negation of the carrier, so a sentence and its negation carry the same presuppositional component.