structure Phenomena.Presupposition.Diagnostics.DiagnosticResult : Type

A diagnostic test result: sentence + judgment.

• frame : String

  The diagnostic frame used

• trigger : String

  The trigger being tested

• content : String

  The content being probed

• sentence : String

  Full sentence

• judgment : Core.Empirical.Acceptability

  Native speaker judgment

• interpretation : String

  What the judgment indicates

def Phenomena.Presupposition.Diagnostics.instReprDiagnosticResult.repr : DiagnosticResult → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Diagnostics.instReprDiagnosticResult : Repr DiagnosticResult

Equations

• Phenomena.Presupposition.Diagnostics.instReprDiagnosticResult = { reprPrec := Phenomena.Presupposition.Diagnostics.instReprDiagnosticResult.repr }

def Phenomena.Presupposition.Diagnostics.allowsForFrame : String

The "allows for" test identifies preconditions (@cite{roberts-simons-2024} §2.1).

Frame: "ψ, which is part of what allows/allowed for φ"

If acceptable, ψ is an ontological precondition of the event in φ. Preconditions are states that must hold for the event to be possible.

Atelic caveat (@cite{roberts-simons-2024} p. 711–712): For atelic target verbs (e.g., know), the "allows for" frame can yield true readings for concomitants due to a "definitional" sense of possibility. Fix: substitute "come to V" to force a telic, inceptive interpretation. Example: use "come to know" rather than "know" in the frame.

Equations

• Phenomena.Presupposition.Diagnostics.allowsForFrame = "_, which is part of what allowed for _"

def Phenomena.Presupposition.Diagnostics.allowsFor_stop_priorState : DiagnosticResult

@cite{roberts-simons-2024} ex. 5a adapted to stop.

Equations

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

def Phenomena.Presupposition.Diagnostics.allowsFor_start_priorNonSmoker : DiagnosticResult

@cite{roberts-simons-2024} ex. 5a adapted to start.

Equations

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

def Phenomena.Presupposition.Diagnostics.allowsFor_kick_hasFeet : DiagnosticResult

@cite{roberts-simons-2024} ex. 13a: selectional restriction passes.

Equations

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

def Phenomena.Presupposition.Diagnostics.allowsFor_kick_touchedTree : DiagnosticResult

@cite{roberts-simons-2024} ex. 13b: concomitant fails.

Equations

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

def Phenomena.Presupposition.Diagnostics.allowsFor_stop_consequence : DiagnosticResult

@cite{roberts-simons-2024} ex. 5b adapted: consequence fails "allows for".

Equations

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

def Phenomena.Presupposition.Diagnostics.counterfactualFrame : String

The counterfactual test confirms preconditions (@cite{roberts-simons-2024} §2.1).

Frame: "If not-ψ, it would not have been possible for [agent] to VP"

If acceptable, ψ is an ontological precondition: without it, the event couldn't have occurred.

Equations

• Phenomena.Presupposition.Diagnostics.counterfactualFrame = "If not _, it would not have been possible for _ to _"

def Phenomena.Presupposition.Diagnostics.counterfactual_kick_hasFeet : DiagnosticResult

"If the robot did not have feet, it would not have been possible for the robot to kick the tree." (T)

Equations

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

def Phenomena.Presupposition.Diagnostics.counterfactual_discover_ignorance : DiagnosticResult

"If John hadn't been ignorant of whether the jewels had been stolen, he couldn't have discovered that the jewels had been stolen." (T)

Equations

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

def Phenomena.Presupposition.Diagnostics.counterfactual_continue_priorActivity : DiagnosticResult

"If Yasmin had not been smoking, it would not have been possible for Yasmin to continue to smoke." (T)

Equations

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

def Phenomena.Presupposition.Diagnostics.resultsInFrame : String

The "results in" test identifies consequences.

Frame: "S results in C"

If acceptable, C is a consequence of the event described by S. Consequences are states that follow from the event occurring.

Equations

• Phenomena.Presupposition.Diagnostics.resultsInFrame = "_ results in _"

def Phenomena.Presupposition.Diagnostics.resultsIn_stop_noLongerSmoking : DiagnosticResult

"John stopped smoking results in him no longer smoking"

Equations

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

def Phenomena.Presupposition.Diagnostics.resultsIn_start_nowSmoking : DiagnosticResult

"John started smoking results in him now being a smoker"

Equations

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

def Phenomena.Presupposition.Diagnostics.resultsIn_win_winner : DiagnosticResult

"John won the race results in him being the winner"

Equations

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

def Phenomena.Presupposition.Diagnostics.resultsIn_stop_priorState : DiagnosticResult

"John stopped smoking results in him having been a smoker" — ODD

Equations

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

def Phenomena.Presupposition.Diagnostics.resultsIn_start_priorState : DiagnosticResult

"John started smoking results in him having never smoked" — ODD

Equations

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

structure Phenomena.Presupposition.Diagnostics.PreconditionConsequencePattern : Type

The precondition/consequence diagnostic pattern.

Empirical observation: For change-of-state predicates,

• Prior states pass "allows for" but fail "results in"
• Result states pass "results in" but fail "allows for"

This pattern holds across CoS verbs (stop, start, continue, finish, etc.)

• predicate : String

  The predicate being tested

• priorPassesAllowsFor : Bool

  Prior state passes "allows for"

• priorFailsResultsIn : Bool

  Prior state fails "results in"

• resultPassesResultsIn : Bool

  Result state passes "results in"

• resultFailsAllowsFor : Bool

  Result state fails "allows for"

instance Phenomena.Presupposition.Diagnostics.instReprPreconditionConsequencePattern : Repr PreconditionConsequencePattern

Equations

• Phenomena.Presupposition.Diagnostics.instReprPreconditionConsequencePattern = { reprPrec := Phenomena.Presupposition.Diagnostics.instReprPreconditionConsequencePattern.repr }

def Phenomena.Presupposition.Diagnostics.instReprPreconditionConsequencePattern.repr : PreconditionConsequencePattern → ℕ → Std.Format

Equations

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

def Phenomena.Presupposition.Diagnostics.stopPattern : PreconditionConsequencePattern

Pattern for "stop"

Equations

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

def Phenomena.Presupposition.Diagnostics.startPattern : PreconditionConsequencePattern

Pattern for "start"

Equations

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

def Phenomena.Presupposition.Diagnostics.winPattern : PreconditionConsequencePattern

Pattern for "win"

Equations

• Phenomena.Presupposition.Diagnostics.winPattern = { predicate := "win", priorPassesAllowsFor := true, priorFailsResultsIn := true, resultPassesResultsIn := true, resultFailsAllowsFor := true }

theorem Phenomena.Presupposition.Diagnostics.patternIsUniform : stopPattern.priorPassesAllowsFor = startPattern.priorPassesAllowsFor ∧ stopPattern.priorPassesAllowsFor = winPattern.priorPassesAllowsFor ∧ stopPattern.resultPassesResultsIn = startPattern.resultPassesResultsIn ∧ stopPattern.resultPassesResultsIn = winPattern.resultPassesResultsIn

The diagnostic pattern is uniform across predicates.

This suggests a systematic distinction between preconditions and consequences, not an idiosyncratic property of individual lexical items.

structure Phenomena.Presupposition.Diagnostics.ProjectionPrediction : Type

Content that passes "allows for" projects.

The precondition/consequence tests predict projection behavior:

• Preconditions (pass "allows for") → project through negation
• Consequences (pass "results in") → do not project through negation

Example:

• "John didn't stop smoking" still implies he was smoking (precondition projects)
• "John didn't stop smoking" does not imply he's not smoking (consequence doesn't project)

• contentType : String

  Content type

• passesAllowsFor : Bool

  Passes "allows for" test

• projectsThroughNegation : Bool

  Projects through negation

• correlation : Bool

  The two properties correlate

def Phenomena.Presupposition.Diagnostics.instReprProjectionPrediction.repr : ProjectionPrediction → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Diagnostics.instReprProjectionPrediction : Repr ProjectionPrediction

Equations

• Phenomena.Presupposition.Diagnostics.instReprProjectionPrediction = { reprPrec := Phenomena.Presupposition.Diagnostics.instReprProjectionPrediction.repr }

def Phenomena.Presupposition.Diagnostics.priorStateProjection : ProjectionPrediction

Prior state of "stop": passes "allows for", projects

Equations

• Phenomena.Presupposition.Diagnostics.priorStateProjection = { contentType := "prior state (was smoking)", passesAllowsFor := true, projectsThroughNegation := true }

def Phenomena.Presupposition.Diagnostics.resultStateProjection : ProjectionPrediction

Result state of "stop": fails "allows for", doesn't project

Equations

• Phenomena.Presupposition.Diagnostics.resultStateProjection = { contentType := "result state (no longer smoking)", passesAllowsFor := false, projectsThroughNegation := false }

def Phenomena.Presupposition.Diagnostics.negationTestFrame : String

The negation test for presupposition.

Frame: "It's not the case that S"

If content C survives (is still implied), C is presupposed by S.

Equations

• Phenomena.Presupposition.Diagnostics.negationTestFrame = "It's not the case that _"

def Phenomena.Presupposition.Diagnostics.negationTest_stop : DiagnosticResult

"It's not the case that John stopped smoking"

Equations

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

def Phenomena.Presupposition.Diagnostics.questionTestFrame : String

The question test for presupposition.

Frame: "Is it the case that S?"

If content C survives (is still implied), C is presupposed by S.

Equations

• Phenomena.Presupposition.Diagnostics.questionTestFrame = "Is it the case that _?"

def Phenomena.Presupposition.Diagnostics.questionTest_stop : DiagnosticResult

"Did John stop smoking?"

Equations

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

def Phenomena.Presupposition.Diagnostics.conditionalFilterFrame : String

The conditional test for presupposition filtering.

Frame: "If P, then S" where P entails the presupposition

If the presupposition is filtered (not globally projected), it shows local satisfaction by the antecedent.

Equations

• Phenomena.Presupposition.Diagnostics.conditionalFilterFrame = "If _, then _"

def Phenomena.Presupposition.Diagnostics.conditionalTest_stop_filter : DiagnosticResult

"If John was smoking, he stopped"

Equations

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

structure Phenomena.Presupposition.Diagnostics.DiagnosticSummary : Type

The diagnostic tests and what they reveal.

• name : String

  Name of diagnostic

• testsFor : String

  What it tests for

• positiveIndicates : String

  Positive result indicates...

instance Phenomena.Presupposition.Diagnostics.instReprDiagnosticSummary : Repr DiagnosticSummary

Equations

• Phenomena.Presupposition.Diagnostics.instReprDiagnosticSummary = { reprPrec := Phenomena.Presupposition.Diagnostics.instReprDiagnosticSummary.repr }

def Phenomena.Presupposition.Diagnostics.instReprDiagnosticSummary.repr : DiagnosticSummary → ℕ → Std.Format

Equations

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

def Phenomena.Presupposition.Diagnostics.diagnosticTests : List DiagnosticSummary

Equations

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