inductive Phenomena.Imprecision.InferencePreservation.AlternativeType : Type

Type of alternative relationship.

• scalar : AlternativeType
• subdomain : AlternativeType
• conjunct : AlternativeType
• numeral : AlternativeType

def Phenomena.Imprecision.InferencePreservation.instReprAlternativeType.repr : AlternativeType → Nat → Std.Format

Equations

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

instance Phenomena.Imprecision.InferencePreservation.instReprAlternativeType : Repr AlternativeType

Equations

• Phenomena.Imprecision.InferencePreservation.instReprAlternativeType = { reprPrec := Phenomena.Imprecision.InferencePreservation.instReprAlternativeType.repr }

instance Phenomena.Imprecision.InferencePreservation.instDecidableEqAlternativeType : DecidableEq AlternativeType

Equations

• Phenomena.Imprecision.InferencePreservation.instDecidableEqAlternativeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Phenomena.Imprecision.InferencePreservation.InferenceRelation : Type

Inference relation between expression and alternative.

• entails : InferenceRelation
• contradicts : InferenceRelation
• independent : InferenceRelation

def Phenomena.Imprecision.InferencePreservation.instReprInferenceRelation.repr : InferenceRelation → Nat → Std.Format

Equations

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

instance Phenomena.Imprecision.InferencePreservation.instReprInferenceRelation : Repr InferenceRelation

Equations

• Phenomena.Imprecision.InferencePreservation.instReprInferenceRelation = { reprPrec := Phenomena.Imprecision.InferencePreservation.instReprInferenceRelation.repr }

instance Phenomena.Imprecision.InferencePreservation.instDecidableEqInferenceRelation : DecidableEq InferenceRelation

Equations

• Phenomena.Imprecision.InferencePreservation.instDecidableEqInferenceRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Phenomena.Imprecision.InferencePreservation.NumeralBlockingDatum : Type

Numeral alternative blocking datum.

The alternatives of a numeral n include nearby numerals. If n contradicts m on precise reading, imprecise construal can't be compatible with m.

Source: Dissertation Chapter 6, @cite{sauerland-stateva-2007}

• numeral : Nat

  The numeral

• round : Bool

  Is it round?

• alternative : Nat

  Key alternative

• alternativeInSet : Bool

  Is alternative in the alternative set?

• inferenceRelation : InferenceRelation

  Inference relation (precise reading)

• imprecisionBlocked : Bool

  Is imprecision blocked?

• explanation : String

  Explanation

instance Phenomena.Imprecision.InferencePreservation.instReprNumeralBlockingDatum : Repr NumeralBlockingDatum

Equations

• Phenomena.Imprecision.InferencePreservation.instReprNumeralBlockingDatum = { reprPrec := Phenomena.Imprecision.InferencePreservation.instReprNumeralBlockingDatum.repr }

def Phenomena.Imprecision.InferencePreservation.instReprNumeralBlockingDatum.repr : NumeralBlockingDatum → Nat → Std.Format

Equations

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

def Phenomena.Imprecision.InferencePreservation.ninetyNineBlocked : NumeralBlockingDatum

Equations

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

def Phenomena.Imprecision.InferencePreservation.hundredNotBlocked : NumeralBlockingDatum

Equations

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

structure Phenomena.Imprecision.InferencePreservation.AlternativeSetAsymmetry : Type

The asymmetry depends on conventionalized alternative sets.

Round numbers have "coarse" alternative sets. Non-round numbers have "fine" alternative sets that include round neighbors.

Source: Dissertation Chapter 6

• roundNumeral : Nat

  Round numeral

• roundAlternatives : List Nat

  Its alternative set (simplified)

• nonRoundNumeral : Nat

  Non-round numeral

• nonRoundAlternatives : List Nat

  Its alternative set (simplified)

• explanation : String

  Asymmetry explanation

def Phenomena.Imprecision.InferencePreservation.instReprAlternativeSetAsymmetry.repr : AlternativeSetAsymmetry → Nat → Std.Format

Equations

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

instance Phenomena.Imprecision.InferencePreservation.instReprAlternativeSetAsymmetry : Repr AlternativeSetAsymmetry

Equations

• Phenomena.Imprecision.InferencePreservation.instReprAlternativeSetAsymmetry = { reprPrec := Phenomena.Imprecision.InferencePreservation.instReprAlternativeSetAsymmetry.repr }

def Phenomena.Imprecision.InferencePreservation.hundredNinetyNineAsymmetry : AlternativeSetAsymmetry

Equations

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

structure Phenomena.Imprecision.InferencePreservation.ConjunctionBlockingDatum : Type

Conjunction blocking datum.

Conjunctions have conjuncts as alternatives. "A and B are P" entails "A is P" and "B is P". Non-maximal reading would fail to preserve these entailments.

Source: Dissertation Chapter 7

• sentence : String

  The conjunction sentence

• conjuncts : List String

  The conjuncts

• alternatives : List String

  Alternatives (the conjuncts as sentences)

• entailmentHolds : Bool

  Entailment holds on precise reading?

• nonMaxPreservesEntailment : Bool

  Would non-max preserve entailment?

• nonMaxBlocked : Bool

  Is non-max blocked?

• explanation : String

  Explanation

instance Phenomena.Imprecision.InferencePreservation.instReprConjunctionBlockingDatum : Repr ConjunctionBlockingDatum

Equations

• Phenomena.Imprecision.InferencePreservation.instReprConjunctionBlockingDatum = { reprPrec := Phenomena.Imprecision.InferencePreservation.instReprConjunctionBlockingDatum.repr }

def Phenomena.Imprecision.InferencePreservation.instReprConjunctionBlockingDatum.repr : ConjunctionBlockingDatum → Nat → Std.Format

Equations

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

def Phenomena.Imprecision.InferencePreservation.annBertConjunction : ConjunctionBlockingDatum

Equations

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

def Phenomena.Imprecision.InferencePreservation.threeStudentsConjunction : ConjunctionBlockingDatum

Equations

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

structure Phenomena.Imprecision.InferencePreservation.NumeralDefiniteBlockingDatum : Type

Numeral-modified definites: "the four doors"

These have homogeneity gaps but resist non-maximality. The numeral creates subdomain alternatives.

Source: @cite{brisson-1998}, Križ (2015), dissertation Chapter 7

• sentence : String

  The sentence

• numeral : Nat

  The numeral

• subNumeralAlternatives : List Nat

  Sub-numeral alternatives

• entailsSubNumerals : Bool

  Does sentence entail sub-numeral alternatives?

• nonMaxBlocked : Bool

  Is non-max blocked?

• explanation : String

  Explanation

def Phenomena.Imprecision.InferencePreservation.instReprNumeralDefiniteBlockingDatum.repr : NumeralDefiniteBlockingDatum → Nat → Std.Format

Equations

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

instance Phenomena.Imprecision.InferencePreservation.instReprNumeralDefiniteBlockingDatum : Repr NumeralDefiniteBlockingDatum

Equations

• Phenomena.Imprecision.InferencePreservation.instReprNumeralDefiniteBlockingDatum = { reprPrec := Phenomena.Imprecision.InferencePreservation.instReprNumeralDefiniteBlockingDatum.repr }

def Phenomena.Imprecision.InferencePreservation.fourDoorsBlocking : NumeralDefiniteBlockingDatum

Equations

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

structure Phenomena.Imprecision.InferencePreservation.CollectiveCumulativeException : Type

Collective and cumulative predicates sometimes permit non-maximality even with conjunctions.

This is an exception that inference preservation needs to handle.

Source: Dissertation Chapter 7

• sentence : String

  The sentence

• predicateType : String

  Predicate type

• nonMaxPossible : Bool

  Is non-max possible?

• explanation : String

  Why?

instance Phenomena.Imprecision.InferencePreservation.instReprCollectiveCumulativeException : Repr CollectiveCumulativeException

Equations

• Phenomena.Imprecision.InferencePreservation.instReprCollectiveCumulativeException = { reprPrec := Phenomena.Imprecision.InferencePreservation.instReprCollectiveCumulativeException.repr }

def Phenomena.Imprecision.InferencePreservation.instReprCollectiveCumulativeException.repr : CollectiveCumulativeException → Nat → Std.Format

Equations

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

def Phenomena.Imprecision.InferencePreservation.collectiveMeetException : CollectiveCumulativeException

Equations

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

def Phenomena.Imprecision.InferencePreservation.cumulativeCarryException : CollectiveCumulativeException

Equations

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

structure Phenomena.Imprecision.InferencePreservation.InferencePreservationConstraint : Type

Inference preservation constraint (informal statement).

For an imprecise construal of φ to be available:

• For all alternatives ψ of φ:
  • If precise(φ) |= ψ, then imprecise(φ) |= ψ
  • If precise(φ) |= ¬ψ, then imprecise(φ) |= ¬ψ

Source: Dissertation Chapters 6-7

• name : String

  Name of constraint

• statement : String

  Informal statement

• appliesToEntailments : Bool

  Applies to entailments?

• appliesToContradictions : Bool

  Applies to contradictions?

• appliesToAllAlternatives : Bool

  Applies to all alternatives?

instance Phenomena.Imprecision.InferencePreservation.instReprInferencePreservationConstraint : Repr InferencePreservationConstraint

Equations

• Phenomena.Imprecision.InferencePreservation.instReprInferencePreservationConstraint = { reprPrec := Phenomena.Imprecision.InferencePreservation.instReprInferencePreservationConstraint.repr }

def Phenomena.Imprecision.InferencePreservation.instReprInferencePreservationConstraint.repr : InferencePreservationConstraint → Nat → Std.Format

Equations

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

def Phenomena.Imprecision.InferencePreservation.inferencePreservation : InferencePreservationConstraint

Equations

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

structure Phenomena.Imprecision.InferencePreservation.InferencePreservationPrediction : Type

Predictions of Inference Preservation.

• construction : String

  Construction

• prediction : String

  Prediction

• confirmed : Bool

  Is prediction borne out?

instance Phenomena.Imprecision.InferencePreservation.instReprInferencePreservationPrediction : Repr InferencePreservationPrediction

Equations

• Phenomena.Imprecision.InferencePreservation.instReprInferencePreservationPrediction = { reprPrec := Phenomena.Imprecision.InferencePreservation.instReprInferencePreservationPrediction.repr }

def Phenomena.Imprecision.InferencePreservation.instReprInferencePreservationPrediction.repr : InferencePreservationPrediction → Nat → Std.Format

Equations

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

def Phenomena.Imprecision.InferencePreservation.prediction1 : InferencePreservationPrediction

Equations

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

def Phenomena.Imprecision.InferencePreservation.prediction2 : InferencePreservationPrediction

Equations

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

def Phenomena.Imprecision.InferencePreservation.prediction3 : InferencePreservationPrediction

Equations

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

def Phenomena.Imprecision.InferencePreservation.prediction4 : InferencePreservationPrediction

Equations

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

structure Phenomena.Imprecision.InferencePreservation.OpenQuestion : Type

Open questions for Inference Preservation.

• question : String

  The question

• difficulty : String

  Why it's open

def Phenomena.Imprecision.InferencePreservation.instReprOpenQuestion.repr : OpenQuestion → Nat → Std.Format

Equations

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

instance Phenomena.Imprecision.InferencePreservation.instReprOpenQuestion : Repr OpenQuestion

Equations

• Phenomena.Imprecision.InferencePreservation.instReprOpenQuestion = { reprPrec := Phenomena.Imprecision.InferencePreservation.instReprOpenQuestion.repr }

def Phenomena.Imprecision.InferencePreservation.question1 : OpenQuestion

Equations

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

def Phenomena.Imprecision.InferencePreservation.question2 : OpenQuestion

Equations

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

def Phenomena.Imprecision.InferencePreservation.question3 : OpenQuestion

Equations

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

structure Phenomena.Imprecision.InferencePreservation.InferencePreservationGeneralizations : Type

Core empirical generalizations about inference preservation.

• nonRoundExactDueToAlternatives : Bool

  Non-round numerals exact due to round alternatives

• conjunctionsResistDueToAlternatives : Bool

  Conjunctions resist non-max due to conjunct alternatives

• collectivesExceptional : Bool

  Collective predicates exceptional

• alternativesBased : Bool

  Constraint is about alternatives, not monotonicity

def Phenomena.Imprecision.InferencePreservation.instReprInferencePreservationGeneralizations.repr : InferencePreservationGeneralizations → Nat → Std.Format

Equations

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

instance Phenomena.Imprecision.InferencePreservation.instReprInferencePreservationGeneralizations : Repr InferencePreservationGeneralizations

Equations

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

def Phenomena.Imprecision.InferencePreservation.mainGeneralizations : InferencePreservationGeneralizations

Equations

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

def Phenomena.Imprecision.InferencePreservation.numeralBlockingExamples : List NumeralBlockingDatum

Equations

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

def Phenomena.Imprecision.InferencePreservation.conjunctionBlockingExamples : List ConjunctionBlockingDatum

Equations

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

def Phenomena.Imprecision.InferencePreservation.collectiveExceptions : List CollectiveCumulativeException

Equations

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

def Phenomena.Imprecision.InferencePreservation.predictions : List InferencePreservationPrediction

Equations

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

def Phenomena.Imprecision.InferencePreservation.openQuestions : List OpenQuestion

Equations

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