Symmetric alternatives

Two alternatives are symmetric for an assertion when they partition it: negating either one asserts the other, so no theory that strengthens an assertion by negating alternatives can negate one of them without the other. This is the configuration of [Kro72]'s symmetry problem for scalar implicature, and [FK11]'s definition of it. The file defines IsSymmetric, shows that the second symmetric alternative is the assertion without the first, that symmetric alternatives are complements below the assertion (isSymmetric_iff_isCompl), and that a set of propositions closed under negation and conjunction, a BooleanSubalgebra, contains both or neither. The namespace Alternatives is the owner of terms of the theory of formal alternatives about sets of propositions, Fox and Katzir's symmetric alternatives here.

References

• [Kro72]
• [Hor72]
• [Kat07]
• [FK11]

structure Alternatives.IsSymmetric {W : Type u_1} (s s₁ s₂ : Set W) : Prop

s₁ and s₂ are symmetric alternatives of s: they partition it.

• union : s₁ ∪ s₂ = s
• disjoint : Disjoint s₁ s₂

theorem Alternatives.isSymmetric_sdiff {W : Type u_1} {s t : Set W} (h : t ⊆ s) : IsSymmetric s t (s \ t)

The assertion without an alternative it entails is that alternative's symmetric partner.

theorem Alternatives.isSymmetric_iff_isCompl {W : Type u_1} {s s₁ s₂ : Set W} (h₁ : s₁ ⊆ s) (h₂ : s₂ ⊆ s) : IsSymmetric s s₁ s₂ ↔ IsCompl ⟨s₁, h₁⟩ ⟨s₂, h₂⟩

Symmetric alternatives of s are complements in the lattice of subsets of s.

theorem Alternatives.IsSymmetric.symm {W : Type u_1} {s s₁ s₂ : Set W} (h : IsSymmetric s s₁ s₂) : IsSymmetric s s₂ s₁

theorem Alternatives.IsSymmetric.subset_left {W : Type u_1} {s s₁ s₂ : Set W} (h : IsSymmetric s s₁ s₂) : s₁ ⊆ s

theorem Alternatives.IsSymmetric.subset_right {W : Type u_1} {s s₁ s₂ : Set W} (h : IsSymmetric s s₁ s₂) : s₂ ⊆ s

theorem Alternatives.IsSymmetric.sdiff_eq {W : Type u_1} {s s₁ s₂ : Set W} (h : IsSymmetric s s₁ s₂) : s \ s₁ = s₂

The second symmetric alternative is the assertion without the first.

theorem Alternatives.IsSymmetric.not_subset_left {W : Type u_1} {s s₁ s₂ : Set W} (h : IsSymmetric s s₁ s₂) (hne : s₂.Nonempty) : ¬s ⊆ s₁

theorem Alternatives.IsSymmetric.ssubset_left {W : Type u_1} {s s₁ s₂ : Set W} (h : IsSymmetric s s₁ s₂) (hne : s₂.Nonempty) : s₁ ⊂ s

theorem Alternatives.IsSymmetric.mem_of_mem {W : Type u_1} {s s₁ s₂ : Set W} (h : IsSymmetric s s₁ s₂) {R : BooleanSubalgebra (Set W)} (hs : s ∈ R) (h₁ : s₁ ∈ R) : s₂ ∈ R

Contextual restriction cannot break symmetry: a set of propositions closed under negation and conjunction that contains the assertion and one symmetric alternative contains the other.

theorem Alternatives.isSymmetric_coe {W : Type u_1} [DecidableEq W] (A B C : Finset W) : IsSymmetric ↑A ↑B ↑C ↔ B ∪ C = A ∧ B ∩ C = ∅

Symmetry over finite sets is decidable through the underlying finsets.