The Table

This file defines the context structure of [FB10]: the participants' discourse commitments, the common ground, and the Table, a stack of the issues under discussion with the most recent on top. A declarative raises its proposition as an issue, Question.ofSet p, and a polar interrogative raises Question.polar p; the complete answers of an issue are its alternatives, Question.alt, the interrogative denotation of [Kar77b], and a common ground decides an issue when it entails one of them. Each issue on the Table projects the common grounds that would decide it, and the projected set is derived from the common ground and the stack. The moves of the paper are functions on the structure, and the file proves what each does to the projected set, the commitment lists, and the Table. Parenthesized numbers are the paper's example and definition numbers.

A Table is a discourse state in both projections: its common ground is the commonGround coordinate (HasCommonGround) and its current issue is the top of the stack (Discourse.HasIssue). It is not a HasAssertion instance under its own assert, which leaves the common ground alone and moves only the projected set.

Main definitions

• Question.DecidedBy P f: the common ground f entails a complete answer of the issue P.
• Commitment.Table A W: the context structure, with Table.discourseCommitments a the propositions a has publicly committed to and Table.projectedSet the projected set, the fold of the paper's ps ∪ P over the stack.
• Table.IsStable: the Table is empty.
• Table.InCrisis: the common ground is inconsistent or no projected common ground is.
• Table.Shared: every participant is committed to the proposition.
• Table.assert, Table.polarQuestion, Table.settle, Table.agreeToDisagree: the default assertion (9), which commits its author as in [Gun01], the default polar question (12), the common-ground increasing operation M' (17), and agreeing to disagree (23). Assertion confirmation (16) is Table.commit of the proposition on top of the Table, and total denial (22) is assert of its negation.

Main results

• Table.le_commonGround_of_mem_projectedSet, Table.decidedBy_of_mem_projectedSet_of_mem_stack: a projected common ground refines the current one and decides every issue on the Table.
• Table.inCrisis_iff: with the projected set derived, crisis is having no consistent projected common ground; the inconsistent-common-ground clause is subsumed.
• Table.projectedSet_assert_assert_compl, Table.inCrisis_assert_assert_compl: a denied assertion projects nothing consistent (21) and leaves the conversation in crisis.
• Table.settle_push_of_decidedBy, Table.settle_assert_self, Table.discourseCommitments_settle: M' pops the issues the new common ground decides and strips the shared proposition from every commitment list.
• Table.agreeToDisagree_assert_assert, Table.inCrisis_agreeToDisagree_assert_assert: agreeing to disagree keeps the commitments, restores the Table, and restores the crisis status of the input context (23).

Implementation notes

• The paper notes that the projected set can always be rebuilt from the common ground and the Table, so it is derived rather than stored.
• A common ground is a filter of propositions, so a proposition follows from it when it belongs to the filter. This is the intersection-based entailment the paper's footnote 8 sets aside as too coarse-grained: here every necessary proposition is decided by every common ground, and Question.decidedBy_top records that the trivial issue is always decided.
• M' (17) applies in the paper only once the proposition is on every commitment list; Table.settle is the operation itself, and the trigger is a hypothesis on the caller, Table.Shared. Its popping clause is read as "pop from the top while decided", which follows the stack wording of (17) and agrees with the paper's examples; the gloss after (17) can also be read as removing every decided item from anywhere in the stack, and the clause pops on an entailed complete answer where the gloss says a decided one, which differ for a declarative whose negation the new common ground entails. Whether a common ground entails a complete answer is not decidable, so Table.settle is classical and noncomputable.
• Agreeing to disagree requires a denial on top of the assertion it denies, which is where total denial (22) leaves the Table, and removes both; Table.agreeToDisagree pops twice and does not check the precondition.

References

• D. F. Farkas and K. B. Bruce, On Reacting to Assertions and Polar Questions (2010)
• C. Gunlogson, True to Form: Rising and Falling Declaratives as Questions in English (2001)
• L. Karttunen, Syntax and Semantics of Questions (1977)

def Question.DecidedBy {W : Type u_1} (P : Question W) (f : Filter W) : Prop

The common ground f decides the issue P when it entails one of its complete answers.

Equations

• P.DecidedBy f = ∃ q ∈ P.alt, q ∈ f

theorem Question.DecidedBy.mono {W : Type u_1} {P : Question W} {f g : Filter W} (h : f ≤ g) : P.DecidedBy g → P.DecidedBy f

theorem Question.DecidedBy.ker_mem {W : Type u_1} {P : Question W} {f : Filter W} (h : P.DecidedBy f) : f.ker ∈ P

A common ground deciding an issue has a context set resolving it.

@[simp]

theorem Question.decidedBy_top {W : Type u_1} {f : Filter W} : ⊤.DecidedBy f

The trivial issue is decided by every common ground.

@[simp]

theorem Question.decidedBy_ofSet {W : Type u_1} {f : Filter W} {p : Set W} : (ofSet p).DecidedBy f ↔ p ∈ f

@[simp]

theorem Question.decidedBy_polar {W : Type u_1} {f : Filter W} {p : Set W} : (polar p).DecidedBy f ↔ p ∈ f ∨ pᶜ ∈ f

A proposition is decided relative to a common ground when it or its negation follows from it; that is the polar question of p being decided.

structure Commitment.Table (A : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

The context structure K of [FB10]: the Table as a stack of issues, the participants' discourse commitments, and the common ground.

• stack : List (Question W)
• commitments : State A W
• commonGround : Filter W

theorem Commitment.Table.ext_iff {A : Type u_1} {W : Type u_2} {x y : Table A W} : x = y ↔ x.stack = y.stack ∧ x.commitments = y.commitments ∧ x.commonGround = y.commonGround

theorem Commitment.Table.ext {A : Type u_1} {W : Type u_2} {x y : Table A W} (stack : x.stack = y.stack) (commitments : x.commitments = y.commitments) (commonGround : x.commonGround = y.commonGround) : x = y

Projecting an issue

def Commitment.Table.project {W : Type u_2} (ps : Set (Filter W)) (P : Question W) : Set (Filter W)

ps ∪ P: add each complete answer of P to each projected common ground, discarding the inconsistent results.

Equations

• Commitment.Table.project ps P = Set.image2 (fun (f : Filter W) (q : Set W) => f ⊓ Filter.principal q) ps P.alt \ {⊥}

@[simp]

theorem Commitment.Table.mem_project {W : Type u_2} {ps : Set (Filter W)} {f : Filter W} {P : Question W} : f ∈ project ps P ↔ (∃ g ∈ ps, ∃ q ∈ P.alt, g ⊓ Filter.principal q = f) ∧ f ≠ ⊥

theorem Commitment.Table.ne_bot_of_mem_project {W : Type u_2} {ps : Set (Filter W)} {f : Filter W} {P : Question W} (h : f ∈ project ps P) : f ≠ ⊥

theorem Commitment.Table.exists_le_of_mem_project {W : Type u_2} {ps : Set (Filter W)} {f : Filter W} {P : Question W} (h : f ∈ project ps P) : ∃ g ∈ ps, f ≤ g

theorem Commitment.Table.decidedBy_of_mem_project {W : Type u_2} {ps : Set (Filter W)} {f : Filter W} {P : Question W} (h : f ∈ project ps P) : P.DecidedBy f

Every projected common ground decides the issue it was projected from.

theorem Commitment.Table.project_singleton_ofSet {W : Type u_2} {f : Filter W} {p : Set W} (h : f ⊓ Filter.principal p ≠ ⊥) : project {f} (Question.ofSet p) = {f ⊓ Filter.principal p}

A single common ground consistent with p projects the one common ground with p.

theorem Commitment.Table.project_singleton_polar {W : Type u_2} {f : Filter W} {p : Set W} (hp : f ⊓ Filter.principal p ≠ ⊥) (hnp : f ⊓ Filter.principal pᶜ ≠ ⊥) : project {f} (Question.polar p) = {f ⊓ Filter.principal p, f ⊓ Filter.principal pᶜ}

A single common ground consistent with p and with ¬p projects both resolutions.

def Commitment.Table.empty {A : Type u_1} {W : Type u_2} : Table A W

The initial context: nothing on the Table, no commitments, the trivial common ground.

Equations

• Commitment.Table.empty = { stack := [], commitments := ∅, commonGround := ⊤ }

@[instance_reducible]

instance Commitment.Table.instInhabited {A : Type u_1} {W : Type u_2} : Inhabited (Table A W)

Equations

• Commitment.Table.instInhabited = { default := Commitment.Table.empty }

@[instance_reducible]

instance Commitment.Table.instHasCommonGround {A : Type u_1} {W : Type u_2} : HasCommonGround (Table A W) W

Equations

• Commitment.Table.instHasCommonGround = { commonGround := Commitment.Table.commonGround }

@[instance_reducible]

instance Commitment.Table.instHasIssue {A : Type u_1} {W : Type u_2} : Discourse.HasIssue (Table A W) W

The current issue is the top of the Table, the trivial issue when the Table is empty.

Equations

• Commitment.Table.instHasIssue = { toIssue := fun (K : Commitment.Table A W) => K.stack.headD ⊤ }

def Commitment.Table.IsStable {A : Type u_1} {W : Type u_2} (K : Table A W) : Prop

A conversation is stable when its Table is empty.

Equations

• K.IsStable = (K.stack = [])

def Commitment.Table.discourseCommitments {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) : Set (Set W)

DC_a: the propositions a has publicly committed to.

Equations

• K.discourseCommitments a = Commitment.contents (Commitment.ofCommitter K.commitments a)

def Commitment.Table.Shared {A : Type u_1} {W : Type u_2} (K : Table A W) (p : Set W) : Prop

Every participant is committed to p.

Equations

• K.Shared p = ∀ (a : A), p ∈ K.discourseCommitments a

The projected set

def Commitment.Table.projectedSet {A : Type u_1} {W : Type u_2} (K : Table A W) : Set (Filter W)

The projected set, rebuilt from the common ground by the issues on the Table, oldest first: the common grounds that canonically settle what is at issue.

Equations

• K.projectedSet = List.foldr (fun (P : Question W) (ps : Set (Filter W)) => Commitment.Table.project ps P) {K.commonGround} K.stack

def Commitment.Table.InCrisis {A : Type u_1} {W : Type u_2} (K : Table A W) : Prop

A conversation is in crisis when its common ground or every projected common ground is inconsistent.

Equations

• K.InCrisis = (K.commonGround = ⊥ ∨ ∀ f ∈ K.projectedSet, f = ⊥)

Moves

def Commitment.Table.push {A : Type u_1} {W : Type u_2} (K : Table A W) (P : Question W) : Table A W

Place an issue on the Table.

Equations

• K.push P = { stack := P :: K.stack, commitments := K.commitments, commonGround := K.commonGround }

def Commitment.Table.pop {A : Type u_1} {W : Type u_2} (K : Table A W) : Table A W

Remove the top issue.

Equations

• K.pop = { stack := K.stack.tail, commitments := K.commitments, commonGround := K.commonGround }

def Commitment.Table.commit {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) (force : Force := Force.doxastic) (source : Source := Source.selfGenerated) : Table A W

Commit a to p.

Equations

• K.commit a p force source = { stack := K.stack, commitments := insert (Commitment.commit a p force source) K.commitments, commonGround := K.commonGround }

def Commitment.Table.assert {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) : Table A W

Default assertion (9): a commits to p and places the declarative's issue on the Table.

Equations

• K.assert a p = (K.commit a p).push (Question.ofSet p)

def Commitment.Table.polarQuestion {A : Type u_1} {W : Type u_2} (K : Table A W) (p : Set W) : Table A W

Default polar question (12): place the interrogative's issue on the Table.

Equations

• K.polarQuestion p = K.push (Question.polar p)

noncomputable def Commitment.Table.settle {A : Type u_1} {W : Type u_2} (K : Table A W) (p : Set W) : Table A W

The common-ground increasing operation M' (17), applied once p is on every commitment list: p enters the common ground, leaves the individual commitment lists, and the issues the new common ground decides are popped from the top of the Table.

Equations

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

def Commitment.Table.agreeToDisagree {A : Type u_1} {W : Type u_2} (K : Table A W) : Table A W

Agreeing to disagree (23), from a Table with the denial on top of the assertion it denies: the contradictory pair leaves the Table and the commitments stay.

Equations

• K.agreeToDisagree = K.pop.pop

Coordinates of the moves

@[simp]

theorem Commitment.Table.stack_empty {A : Type u_1} {W : Type u_2} : empty.stack = []

@[simp]

theorem Commitment.Table.commitments_empty {A : Type u_1} {W : Type u_2} : empty.commitments = ∅

@[simp]

theorem Commitment.Table.commonGround_empty {A : Type u_1} {W : Type u_2} : empty.commonGround = ⊤

@[simp]

theorem Commitment.Table.stack_push {A : Type u_1} {W : Type u_2} (K : Table A W) (P : Question W) : (K.push P).stack = P :: K.stack

@[simp]

theorem Commitment.Table.commitments_push {A : Type u_1} {W : Type u_2} (K : Table A W) (P : Question W) : (K.push P).commitments = K.commitments

@[simp]

theorem Commitment.Table.commonGround_push {A : Type u_1} {W : Type u_2} (K : Table A W) (P : Question W) : (K.push P).commonGround = K.commonGround

@[simp]

theorem Commitment.Table.stack_pop {A : Type u_1} {W : Type u_2} (K : Table A W) : K.pop.stack = K.stack.tail

@[simp]

theorem Commitment.Table.commitments_pop {A : Type u_1} {W : Type u_2} (K : Table A W) : K.pop.commitments = K.commitments

@[simp]

theorem Commitment.Table.commonGround_pop {A : Type u_1} {W : Type u_2} (K : Table A W) : K.pop.commonGround = K.commonGround

@[simp]

theorem Commitment.Table.stack_commit {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) (force : Force) (source : Source) : (K.commit a p force source).stack = K.stack

@[simp]

theorem Commitment.Table.commitments_commit {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) (force : Force) (source : Source) : (K.commit a p force source).commitments = insert (Commitment.commit a p force source) K.commitments

@[simp]

theorem Commitment.Table.commonGround_commit {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) (force : Force) (source : Source) : (K.commit a p force source).commonGround = K.commonGround

@[simp]

theorem Commitment.Table.stack_assert {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) : (K.assert a p).stack = Question.ofSet p :: K.stack

@[simp]

theorem Commitment.Table.commitments_assert {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) : (K.assert a p).commitments = insert (Commitment.commit a p) K.commitments

@[simp]

theorem Commitment.Table.commonGround_assert {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) : (K.assert a p).commonGround = K.commonGround

@[simp]

theorem Commitment.Table.stack_polarQuestion {A : Type u_1} {W : Type u_2} (K : Table A W) (p : Set W) : (K.polarQuestion p).stack = Question.polar p :: K.stack

@[simp]

theorem Commitment.Table.commitments_polarQuestion {A : Type u_1} {W : Type u_2} (K : Table A W) (p : Set W) : (K.polarQuestion p).commitments = K.commitments

@[simp]

theorem Commitment.Table.commonGround_polarQuestion {A : Type u_1} {W : Type u_2} (K : Table A W) (p : Set W) : (K.polarQuestion p).commonGround = K.commonGround

@[simp]

theorem Commitment.Table.stack_settle {A : Type u_1} {W : Type u_2} (K : Table A W) (p : Set W) : (K.settle p).stack = List.dropWhile (fun (P : Question W) => decide (P.DecidedBy (K.commonGround ⊓ Filter.principal p))) K.stack

@[simp]

theorem Commitment.Table.commitments_settle {A : Type u_1} {W : Type u_2} (K : Table A W) (p : Set W) : (K.settle p).commitments = {c : Commitment A W | c ∈ K.commitments ∧ c.content ≠ p}

@[simp]

theorem Commitment.Table.commonGround_settle {A : Type u_1} {W : Type u_2} (K : Table A W) (p : Set W) : (K.settle p).commonGround = K.commonGround ⊓ Filter.principal p

@[simp]

theorem Commitment.Table.stack_agreeToDisagree {A : Type u_1} {W : Type u_2} (K : Table A W) : K.agreeToDisagree.stack = K.stack.tail.tail

@[simp]

theorem Commitment.Table.commitments_agreeToDisagree {A : Type u_1} {W : Type u_2} (K : Table A W) : K.agreeToDisagree.commitments = K.commitments

@[simp]

theorem Commitment.Table.commonGround_agreeToDisagree {A : Type u_1} {W : Type u_2} (K : Table A W) : K.agreeToDisagree.commonGround = K.commonGround

@[simp]

theorem HasCommonGround.commonGround_table {A : Type u_1} {W : Type u_2} (K : Commitment.Table A W) : commonGround K = K.commonGround

@[simp]

theorem Commitment.Table.toIssue_empty {A : Type u_1} {W : Type u_2} : Discourse.HasIssue.toIssue empty = ⊤

@[simp]

theorem Commitment.Table.toIssue_push {A : Type u_1} {W : Type u_2} (K : Table A W) (P : Question W) : Discourse.HasIssue.toIssue (K.push P) = P

@[simp]

theorem Commitment.Table.toIssue_commit {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) (force : Force) (source : Source) : Discourse.HasIssue.toIssue (K.commit a p force source) = Discourse.HasIssue.toIssue K

@[simp]

theorem Commitment.Table.toIssue_assert {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) : Discourse.HasIssue.toIssue (K.assert a p) = Question.ofSet p

@[simp]

theorem Commitment.Table.toIssue_polarQuestion {A : Type u_1} {W : Type u_2} (K : Table A W) (p : Set W) : Discourse.HasIssue.toIssue (K.polarQuestion p) = Question.polar p

Stability

@[simp]

theorem Commitment.Table.empty_isStable {A : Type u_1} {W : Type u_2} : empty.IsStable

theorem Commitment.Table.not_isStable_push {A : Type u_1} {W : Type u_2} (K : Table A W) (P : Question W) : ¬(K.push P).IsStable

theorem Commitment.Table.toIssue_eq_top_of_isStable {A : Type u_1} {W : Type u_2} {K : Table A W} (h : K.IsStable) : Discourse.HasIssue.toIssue K = ⊤

A stable conversation has no issue.

theorem Commitment.Table.isStable_settle_of_isStable {A : Type u_1} {W : Type u_2} {K : Table A W} (p : Set W) (h : K.IsStable) : (K.settle p).IsStable

Discourse commitments

@[simp]

theorem Commitment.Table.discourseCommitments_empty {A : Type u_1} {W : Type u_2} (a : A) : empty.discourseCommitments a = ∅

@[simp]

theorem Commitment.Table.discourseCommitments_push {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (P : Question W) : (K.push P).discourseCommitments a = K.discourseCommitments a

@[simp]

theorem Commitment.Table.discourseCommitments_pop {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) : K.pop.discourseCommitments a = K.discourseCommitments a

@[simp]

theorem Commitment.Table.discourseCommitments_polarQuestion {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) : (K.polarQuestion p).discourseCommitments a = K.discourseCommitments a

@[simp]

theorem Commitment.Table.discourseCommitments_agreeToDisagree {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) : K.agreeToDisagree.discourseCommitments a = K.discourseCommitments a

@[simp]

theorem Commitment.Table.discourseCommitments_commit_self {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) (force : Force) (source : Source) : (K.commit a p force source).discourseCommitments a = insert p (K.discourseCommitments a)

theorem Commitment.Table.discourseCommitments_commit_of_ne {A : Type u_1} {W : Type u_2} {K : Table A W} {a : A} {p : Set W} {force : Force} {source : Source} {b : A} (h : b ≠ a) : (K.commit a p force source).discourseCommitments b = K.discourseCommitments b

theorem Commitment.Table.mem_discourseCommitments_commit_iff {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) (force : Force) (source : Source) {b : A} {q : Set W} : q ∈ (K.commit a p force source).discourseCommitments b ↔ b = a ∧ q = p ∨ q ∈ K.discourseCommitments b

theorem Commitment.Table.mem_discourseCommitments_commit_self {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) (force : Force) (source : Source) : p ∈ (K.commit a p force source).discourseCommitments a

@[simp]

theorem Commitment.Table.discourseCommitments_assert {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) : (K.assert a p).discourseCommitments a = insert p (K.discourseCommitments a)

theorem Commitment.Table.discourseCommitments_assert_of_ne {A : Type u_1} {W : Type u_2} {K : Table A W} {a : A} {p : Set W} {b : A} (h : b ≠ a) : (K.assert a p).discourseCommitments b = K.discourseCommitments b

theorem Commitment.Table.mem_discourseCommitments_assert {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) : p ∈ (K.assert a p).discourseCommitments a

The asserted proposition enters the author's commitments.

theorem Commitment.Table.discourseCommitments_settle {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) : (K.settle p).discourseCommitments a = K.discourseCommitments a \ {p}

M' strips the shared proposition from every commitment list.

The moves on the Table

theorem Commitment.Table.settle_push_of_decidedBy {A : Type u_1} {W : Type u_2} {K : Table A W} {p : Set W} {P : Question W} (h : P.DecidedBy (K.commonGround ⊓ Filter.principal p)) : (K.push P).settle p = K.settle p

M' pops a decided issue from the top of the Table and goes on popping.

theorem Commitment.Table.stack_settle_push_of_not_decidedBy {A : Type u_1} {W : Type u_2} {K : Table A W} {p : Set W} {P : Question W} (h : ¬P.DecidedBy (K.commonGround ⊓ Filter.principal p)) : ((K.push P).settle p).stack = P :: K.stack

M' stops at the first undecided issue.

theorem Commitment.Table.settle_commit_self {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) (force : Force) (source : Source) : (K.commit a p force source).settle p = K.settle p

The commitment that triggers M' is stripped along with the rest.

theorem Commitment.Table.settle_assert_self {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) : (K.assert a p).settle p = K.settle p

M' with the asserted proposition pops the assertion and strips its commitment.

theorem Commitment.Table.settle_polarQuestion_self {A : Type u_1} {W : Type u_2} (K : Table A W) (p : Set W) : (K.polarQuestion p).settle p = K.settle p

M' with the sentence radical of a polar question pops the question.

theorem Commitment.Table.agreeToDisagree_assert_assert {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) (b : A) (q : Set W) : ((K.assert a p).assert b q).agreeToDisagree = (K.commit a p).commit b q

Agreeing to disagree after two assertions, the denial being the case q = pᶜ, leaves the Table and the common ground as before them, with both commitments recorded.

theorem Commitment.Table.inCrisis_agreeToDisagree_assert_assert {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) (b : A) (q : Set W) : ((K.assert a p).assert b q).agreeToDisagree.InCrisis ↔ K.InCrisis

Agreeing to disagree restores the crisis status of the context before the assertions.

Projected common grounds

theorem Commitment.Table.projectedSet_of_isStable {A : Type u_1} {W : Type u_2} {K : Table A W} (h : K.IsStable) : K.projectedSet = {K.commonGround}

A stable conversation projects only its common ground.

theorem Commitment.Table.le_commonGround_of_mem_projectedSet {A : Type u_1} {W : Type u_2} {K : Table A W} {f : Filter W} (h : f ∈ K.projectedSet) : f ≤ K.commonGround

A projected common ground refines the current one.

theorem Commitment.Table.decidedBy_of_mem_projectedSet_of_mem_stack {A : Type u_1} {W : Type u_2} {K : Table A W} {P : Question W} {f : Filter W} (hf : f ∈ K.projectedSet) (hP : P ∈ K.stack) : P.DecidedBy f

Every projected common ground decides every issue on the Table.

theorem Commitment.Table.settles_of_mem_projectedSet {A : Type u_1} {W : Type u_2} {K : Table A W} {f : Filter W} (hf : f ∈ K.projectedSet) : Discourse.HasIssue.settles f.ker K

Every projected common ground settles the current issue.

theorem Commitment.Table.mem_of_mem_projectedSet_assert {A : Type u_1} {W : Type u_2} {K : Table A W} {a : A} {p : Set W} {f : Filter W} (h : f ∈ (K.assert a p).projectedSet) : p ∈ f

The asserted proposition holds in every projected common ground.

theorem Commitment.Table.mem_or_compl_mem_of_mem_projectedSet_polarQuestion {A : Type u_1} {W : Type u_2} {K : Table A W} {p : Set W} {f : Filter W} (h : f ∈ (K.polarQuestion p).projectedSet) : p ∈ f ∨ pᶜ ∈ f

The sentence radical of a polar question is decided in every projected common ground.

@[simp]

theorem Commitment.Table.projectedSet_empty {A : Type u_1} {W : Type u_2} : empty.projectedSet = {⊤}

@[simp]

theorem Commitment.Table.projectedSet_push {A : Type u_1} {W : Type u_2} (K : Table A W) (P : Question W) : (K.push P).projectedSet = project K.projectedSet P

@[simp]

theorem Commitment.Table.projectedSet_commit {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) (force : Force) (source : Source) : (K.commit a p force source).projectedSet = K.projectedSet

@[simp]

theorem Commitment.Table.projectedSet_assert {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) : (K.assert a p).projectedSet = project K.projectedSet (Question.ofSet p)

An assertion projects confirmation: its content is added to each projected common ground.

@[simp]

theorem Commitment.Table.projectedSet_polarQuestion {A : Type u_1} {W : Type u_2} (K : Table A W) (p : Set W) : (K.polarQuestion p).projectedSet = project K.projectedSet (Question.polar p)

A polar question projects resolution: each alternative is added to each projected common ground.

theorem Commitment.Table.inCrisis_iff {A : Type u_1} {W : Type u_2} (K : Table A W) : K.InCrisis ↔ ∀ f ∈ K.projectedSet, f = ⊥

With the projected set derived, a conversation is in crisis exactly when no projected common ground is consistent.

theorem Commitment.Table.projectedSet_assert_assert_compl {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) (b : A) : ((K.assert a p).assert b pᶜ).projectedSet = ∅

After an assertion has been denied, nothing consistent is projected (21).

theorem Commitment.Table.inCrisis_assert_assert_compl {A : Type u_1} {W : Type u_2} (K : Table A W) (a : A) (p : Set W) (b : A) : ((K.assert a p).assert b pᶜ).InCrisis

A denied assertion leaves the conversation in crisis.