Polarity

The polarity of an expression is positive or negative. The two polarities form the group of order two, a negation cancelling a negation; they are the units of ℤ (Polarity.unitsEquiv). Each notion of polarity in the library is an action of this one group:

• the polarity of a sentence acts on propositions, the negative polarity by complement (negative • p = pᶜ), and the orbit of a proposition, the proposition and its negation, is the set of its polarity alternatives (orbit_eq_pair_compl): the focus value of a focused polarity and the answers of the polar question;
• the polarity of an antonym acts on degrees by negation (negative • x = -x) and on scales by duality (Semantics/Degree/Antonymy);
• the relative polarity of a response to an antecedent, [same] or [reverse], is the product of their polarities;
• the direction of a function, strictly monotone or strictly antitone (StrictMonoBy), with directions composing as polarities multiply.

Since these are one group acting in different ways, their interaction is statable: the negative antonym short measures on the dual scale of tall, while sentential negation takes the complement, so not short does not entail tall.

A polarity is a sign: it coerces into SignType as 1 or -1. The three-valued sign also records what a polarity cannot, the absence of a direction: the monotonicity of a context, upward, downward or neither (NaturalLogic.Signature.sign), and a body of evidence or belief bearing on a proposition, for it, against it or neither (Question.BiasValue). UD.Polarity, a morphological feature of the annotation scheme, is a distinct type.

References

• [Wil13]
• [Gut12]

inductive Polarity : Type

The polarity of an expression, positive or negative.

• positive : Polarity
• negative : Polarity

def instReprPolarity.repr : Polarity → ℕ → Std.Format

Equations

• instReprPolarity.repr Polarity.positive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Polarity.positive")).group prec✝
• instReprPolarity.repr Polarity.negative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Polarity.negative")).group prec✝

@[instance_reducible]

instance instReprPolarity : Repr Polarity

Equations

• instReprPolarity = { reprPrec := instReprPolarity.repr }

@[instance_reducible]

instance instDecidableEqPolarity : DecidableEq Polarity

Equations

• instDecidableEqPolarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance instInhabitedPolarity : Inhabited Polarity

Equations

• instInhabitedPolarity = { default := instInhabitedPolarity.default }

@[instance_reducible]

instance instFintypePolarity : Fintype Polarity

Equations

• instFintypePolarity = { elems := { val := ↑Polarity.enumList, nodup := Polarity.enumList_nodup }, complete := instFintypePolarity._proof_1 }

@[instance_reducible]

instance Polarity.instOne : One Polarity

Equations

• Polarity.instOne = { one := Polarity.positive }

@[instance_reducible]

instance Polarity.instMul : Mul Polarity

Polarities compose, two negations cancelling.

Equations

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

@[instance_reducible]

instance Polarity.instCommGroup : CommGroup Polarity

The polarities form the group of order two, each polarity its own inverse.

Equations

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

@[simp]

theorem Polarity.one_eq_positive : 1 = positive

@[simp]

theorem Polarity.inv_eq_self (s : Polarity) : s⁻¹ = s

@[simp]

theorem Polarity.mul_self (s : Polarity) : s * s = positive

@[simp]

theorem Polarity.positive_mul (s : Polarity) : positive * s = s

@[simp]

theorem Polarity.mul_positive (s : Polarity) : s * positive = s

def Polarity.toSignType : Polarity → SignType

A polarity as a sign, positive 1 and negative -1.

Equations

• ↑Polarity.positive = 1
• ↑Polarity.negative = -1

@[instance_reducible]

instance Polarity.instCoeSignType : Coe Polarity SignType

Equations

• Polarity.instCoeSignType = { coe := Polarity.toSignType }

@[simp]

theorem Polarity.coe_positive : ↑positive = 1

@[simp]

theorem Polarity.coe_negative : ↑negative = -1

@[simp]

theorem Polarity.coe_mul (s t : Polarity) : ↑(s * t) = ↑s * ↑t

theorem Polarity.coe_ne_zero (s : Polarity) : ↑s ≠ 0

def Polarity.unitsEquiv : Polarity ≃* ℤˣ

The polarities are the units of ℤ, positive being 1 and negative being -1.

Equations

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

@[simp]

theorem Polarity.positive_smul {M : Type u_1} [MulAction Polarity M] (x : M) : positive • x = x

@[instance_reducible]

instance Polarity.instMulActionSet {α : Type u_1} : MulAction Polarity (Set α)

The polarity of a sentence acts on propositions. The positive polarity leaves a proposition, the negative one takes its complement.

Equations

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

@[simp]

theorem Polarity.negative_smul_set {α : Type u_1} (p : Set α) : negative • p = pᶜ

theorem Polarity.orbit_eq_pair_compl {α : Type u_1} (p : Set α) : MulAction.orbit Polarity p = {p, pᶜ}

The polarity alternatives of a proposition, its orbit under the polarity group, are the proposition and its negation, the focus value of a focused polarity ([Wil13], [Gut12]) and the answers of the polar question.

@[instance_reducible]

instance Polarity.instMulActionOfAddCommGroup {α : Type u_1} [AddCommGroup α] : MulAction Polarity α

A polarity acts on an additive group through the units of ℤ, the negative polarity negating.

Equations

• Polarity.instMulActionOfAddCommGroup = MulAction.compHom α Polarity.unitsEquiv.toMonoidHom

@[simp]

theorem Polarity.negative_smul {α : Type u_1} [AddCommGroup α] (x : α) : negative • x = -x

@[instance_reducible]

instance Polarity.instMulActionSignType : MulAction Polarity SignType

A polarity acts on signs by multiplication, and so pointwise on trivalent propositions, the negative polarity acting as Kleene negation.

Equations

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

@[simp]

theorem Polarity.negative_smul_signType (a : SignType) : negative • a = -a

def Polarity.StrictMonoBy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : Polarity → (α → β) → Prop

A function directed by a polarity is strictly monotone under the positive polarity and strictly antitone under the negative one.

Equations

• Polarity.positive.StrictMonoBy x✝ = StrictMono x✝
• Polarity.negative.StrictMonoBy x✝ = StrictAnti x✝

theorem Polarity.StrictMonoBy.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] {s t : Polarity} {g : β → γ} {f : α → β} (hg : s.StrictMonoBy g) (hf : t.StrictMonoBy f) : (s * t).StrictMonoBy (g ∘ f)

Directions compose as polarities multiply.