inductive Phenomena.Entailment.Monotonicity.Position : Type

Type of monotonicity position being tested.

• restrictor : Position
• scope : Position

instance Phenomena.Entailment.Monotonicity.instDecidableEqPosition : DecidableEq Position

Equations

• Phenomena.Entailment.Monotonicity.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Entailment.Monotonicity.instBEqPosition : BEq Position

Equations

• Phenomena.Entailment.Monotonicity.instBEqPosition = { beq := Phenomena.Entailment.Monotonicity.instBEqPosition.beq }

def Phenomena.Entailment.Monotonicity.instBEqPosition.beq : Position → Position → Bool

Equations

• Phenomena.Entailment.Monotonicity.instBEqPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Entailment.Monotonicity.instReprPosition.repr : Position → Nat → Std.Format

Equations

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

instance Phenomena.Entailment.Monotonicity.instReprPosition : Repr Position

Equations

• Phenomena.Entailment.Monotonicity.instReprPosition = { reprPrec := Phenomena.Entailment.Monotonicity.instReprPosition.repr }

inductive Phenomena.Entailment.Monotonicity.Direction : Type

Direction of the set inclusion in the inference.

• upward : Direction
• downward : Direction

instance Phenomena.Entailment.Monotonicity.instDecidableEqDirection : DecidableEq Direction

Equations

• Phenomena.Entailment.Monotonicity.instDecidableEqDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Entailment.Monotonicity.instBEqDirection.beq : Direction → Direction → Bool

Equations

• Phenomena.Entailment.Monotonicity.instBEqDirection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Entailment.Monotonicity.instBEqDirection : BEq Direction

Equations

• Phenomena.Entailment.Monotonicity.instBEqDirection = { beq := Phenomena.Entailment.Monotonicity.instBEqDirection.beq }

instance Phenomena.Entailment.Monotonicity.instReprDirection : Repr Direction

Equations

• Phenomena.Entailment.Monotonicity.instReprDirection = { reprPrec := Phenomena.Entailment.Monotonicity.instReprDirection.repr }

def Phenomena.Entailment.Monotonicity.instReprDirection.repr : Direction → Nat → Std.Format

Equations

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

structure Phenomena.Entailment.Monotonicity.MonotonicityJudgment : Type

A monotonicity inference judgment.

• determiner : String

  The determiner being tested

• position : Position

  Which argument position

• direction : Direction

  Direction of inference

• premise : String

  The premise

• conclusion : String

  The conclusion

• setRelation : String

  Given set relation (e.g., "dogs ⊆ animals")

• judgedValid : Bool

  Do speakers judge this as valid?

def Phenomena.Entailment.Monotonicity.instReprMonotonicityJudgment.repr : MonotonicityJudgment → Nat → Std.Format

Equations

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

instance Phenomena.Entailment.Monotonicity.instReprMonotonicityJudgment : Repr MonotonicityJudgment

Equations

• Phenomena.Entailment.Monotonicity.instReprMonotonicityJudgment = { reprPrec := Phenomena.Entailment.Monotonicity.instReprMonotonicityJudgment.repr }

def Phenomena.Entailment.Monotonicity.everyRestrictorDE : MonotonicityJudgment

"Every" is DE in restrictor: dogs ⊆ animals, but "every animal" ↛ "every dog"

The valid direction is: every animal barks → every dog barks (If every animal barks, and dogs are animals, then every dog barks)

Equations

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

def Phenomena.Entailment.Monotonicity.everyRestrictorNotUE : MonotonicityJudgment

"Every" restrictor: upward is invalid.

"Every dog barks" ↛ "Every animal barks"

Equations

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

def Phenomena.Entailment.Monotonicity.everyScopeUE : MonotonicityJudgment

"Every" is UE in scope: barks ⊆ makes_noise

"Every dog barks" → "Every dog makes noise"

Equations

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

def Phenomena.Entailment.Monotonicity.someRestrictorUE : MonotonicityJudgment

"Some" is UE in restrictor: dogs ⊆ animals

"Some dog barks" → "Some animal barks"

Equations

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

def Phenomena.Entailment.Monotonicity.someScopeUE : MonotonicityJudgment

"Some" is UE in scope: barks ⊆ makes_noise

"Some dog barks" → "Some dog makes noise"

Equations

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

def Phenomena.Entailment.Monotonicity.noRestrictorDE : MonotonicityJudgment

"No" is DE in restrictor: dogs ⊆ animals

"No animal barks" → "No dog barks"

Equations

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

def Phenomena.Entailment.Monotonicity.noScopeDE : MonotonicityJudgment

"No" is DE in scope: barks ⊆ makes_noise

"No dog makes noise" → "No dog barks"

Equations

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

def Phenomena.Entailment.Monotonicity.noScopeNotUE : MonotonicityJudgment

"No" scope: upward is invalid.

"No dog barks" ↛ "No dog makes noise"

Equations

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

def Phenomena.Entailment.Monotonicity.allMonotonicityJudgments : List MonotonicityJudgment

All monotonicity judgments

Equations

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

structure Phenomena.Entailment.Monotonicity.MonotonicityPattern : Type

Summary of determiner monotonicity patterns.

• determiner : String
• restrictorUE : Bool
• scopeUE : Bool

def Phenomena.Entailment.Monotonicity.instReprMonotonicityPattern.repr : MonotonicityPattern → Nat → Std.Format

Equations

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

instance Phenomena.Entailment.Monotonicity.instReprMonotonicityPattern : Repr MonotonicityPattern

Equations

• Phenomena.Entailment.Monotonicity.instReprMonotonicityPattern = { reprPrec := Phenomena.Entailment.Monotonicity.instReprMonotonicityPattern.repr }

def Phenomena.Entailment.Monotonicity.everyPattern : MonotonicityPattern

"Every": DE restrictor, UE scope

Equations

• Phenomena.Entailment.Monotonicity.everyPattern = { determiner := "every", restrictorUE := false, scopeUE := true }

def Phenomena.Entailment.Monotonicity.somePattern : MonotonicityPattern

"Some": UE restrictor, UE scope

Equations

• Phenomena.Entailment.Monotonicity.somePattern = { determiner := "some", restrictorUE := true, scopeUE := true }

def Phenomena.Entailment.Monotonicity.noPattern : MonotonicityPattern

"No": DE restrictor, DE scope

Equations

• Phenomena.Entailment.Monotonicity.noPattern = { determiner := "no", restrictorUE := false, scopeUE := false }

def Phenomena.Entailment.Monotonicity.allPatterns : List MonotonicityPattern

All patterns

Equations

• Phenomena.Entailment.Monotonicity.allPatterns = [Phenomena.Entailment.Monotonicity.everyPattern, Phenomena.Entailment.Monotonicity.somePattern, Phenomena.Entailment.Monotonicity.noPattern]

theorem Phenomena.Entailment.Monotonicity.everyMonotonicity : everyRestrictorDE.judgedValid = true ∧ everyRestrictorNotUE.judgedValid = false ∧ everyScopeUE.judgedValid = true

"Every" has the classic DE-restrictor, UE-scope pattern

theorem Phenomena.Entailment.Monotonicity.someMonotonicity : someRestrictorUE.judgedValid = true ∧ someScopeUE.judgedValid = true

"Some" is UE in both positions

theorem Phenomena.Entailment.Monotonicity.noMonotonicity : noRestrictorDE.judgedValid = true ∧ noScopeDE.judgedValid = true ∧ noScopeNotUE.judgedValid = false

"No" is DE in both positions