inductive Phenomena.Ellipsis.Gapping.WordOrder : Type

Basic word order types for transitive clauses.

S = Subject, V = Verb, O = Object

• SOV : WordOrder
• SVO : WordOrder
• VSO : WordOrder
• VOS : WordOrder
• OVS : WordOrder
• OSV : WordOrder

@[implicit_reducible]

instance Phenomena.Ellipsis.Gapping.instDecidableEqWordOrder : DecidableEq WordOrder

Equations

• Phenomena.Ellipsis.Gapping.instDecidableEqWordOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Ellipsis.Gapping.instReprWordOrder : Repr WordOrder

Equations

• Phenomena.Ellipsis.Gapping.instReprWordOrder = { reprPrec := Phenomena.Ellipsis.Gapping.instReprWordOrder.repr }

def Phenomena.Ellipsis.Gapping.instReprWordOrder.repr : WordOrder → Nat → Std.Format

Equations

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

structure Phenomena.Ellipsis.Gapping.WordOrderProfile : Type

Languages can have different orders in main vs subordinate clauses

• mainClause : WordOrder
• subClause : WordOrder

def Phenomena.Ellipsis.Gapping.instReprWordOrderProfile.repr : WordOrderProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Ellipsis.Gapping.instReprWordOrderProfile : Repr WordOrderProfile

Equations

• Phenomena.Ellipsis.Gapping.instReprWordOrderProfile = { reprPrec := Phenomena.Ellipsis.Gapping.instReprWordOrderProfile.repr }

inductive Phenomena.Ellipsis.Gapping.GappingDirection : Type

Direction of gapping in coordinate structures.

Forward: verb in first conjunct, gap in second "Dexter ate bread, and Warren, potatoes" ↑ ↑gap

Backward: gap in first conjunct, verb in second "Ken Naomi-o, Erika Sara-o tazuneta" ↑gap ↑verb

• forward : GappingDirection
• backward : GappingDirection

@[implicit_reducible]

instance Phenomena.Ellipsis.Gapping.instDecidableEqGappingDirection : DecidableEq GappingDirection

Equations

• Phenomena.Ellipsis.Gapping.instDecidableEqGappingDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Ellipsis.Gapping.instReprGappingDirection : Repr GappingDirection

Equations

• Phenomena.Ellipsis.Gapping.instReprGappingDirection = { reprPrec := Phenomena.Ellipsis.Gapping.instReprGappingDirection.repr }

def Phenomena.Ellipsis.Gapping.instReprGappingDirection.repr : GappingDirection → Nat → Std.Format

Equations

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

structure Phenomena.Ellipsis.Gapping.GappingPattern : Type

A gapping pattern describes what a language allows.

• allowsForward : Prop
• allowsBackward : Prop
• decAllowsForward : Decidable self.allowsForward
• decAllowsBackward : Decidable self.allowsBackward

def Phenomena.Ellipsis.Gapping.GappingPattern.forwardOnly : GappingPattern

Equations

• Phenomena.Ellipsis.Gapping.GappingPattern.forwardOnly = { allowsForward := True, allowsBackward := False, decAllowsForward := instDecidableTrue, decAllowsBackward := instDecidableFalse }

def Phenomena.Ellipsis.Gapping.GappingPattern.backwardOnly : GappingPattern

Equations

• Phenomena.Ellipsis.Gapping.GappingPattern.backwardOnly = { allowsForward := False, allowsBackward := True, decAllowsForward := instDecidableFalse, decAllowsBackward := instDecidableTrue }

def Phenomena.Ellipsis.Gapping.GappingPattern.both : GappingPattern

Equations

• Phenomena.Ellipsis.Gapping.GappingPattern.both = { allowsForward := True, allowsBackward := True, decAllowsForward := instDecidableTrue, decAllowsBackward := instDecidableTrue }

def Phenomena.Ellipsis.Gapping.GappingPattern.neither : GappingPattern

Equations

• Phenomena.Ellipsis.Gapping.GappingPattern.neither = { allowsForward := False, allowsBackward := False, decAllowsForward := instDecidableFalse, decAllowsBackward := instDecidableFalse }

def Phenomena.Ellipsis.Gapping.rossOriginal (order : WordOrder) : GappingPattern

Ross's original generalization about gapping and word order.

Equations

• Phenomena.Ellipsis.Gapping.rossOriginal Phenomena.Ellipsis.Gapping.WordOrder.SOV = Phenomena.Ellipsis.Gapping.GappingPattern.backwardOnly
• Phenomena.Ellipsis.Gapping.rossOriginal Phenomena.Ellipsis.Gapping.WordOrder.VSO = Phenomena.Ellipsis.Gapping.GappingPattern.forwardOnly
• Phenomena.Ellipsis.Gapping.rossOriginal Phenomena.Ellipsis.Gapping.WordOrder.SVO = Phenomena.Ellipsis.Gapping.GappingPattern.forwardOnly
• Phenomena.Ellipsis.Gapping.rossOriginal Phenomena.Ellipsis.Gapping.WordOrder.VOS = Phenomena.Ellipsis.Gapping.GappingPattern.forwardOnly
• Phenomena.Ellipsis.Gapping.rossOriginal Phenomena.Ellipsis.Gapping.WordOrder.OVS = Phenomena.Ellipsis.Gapping.GappingPattern.backwardOnly
• Phenomena.Ellipsis.Gapping.rossOriginal Phenomena.Ellipsis.Gapping.WordOrder.OSV = Phenomena.Ellipsis.Gapping.GappingPattern.backwardOnly

def Phenomena.Ellipsis.Gapping.HasRightwardVerbs : WordOrder → Prop

Steedman's revised generalization: gapping depends on lexical availability of verb categories, not "underlying" word order.

A language allows forward gapping iff it has rightward-combining verbs. A language allows backward gapping iff it has leftward-combining verbs.

Equations

• Phenomena.Ellipsis.Gapping.HasRightwardVerbs Phenomena.Ellipsis.Gapping.WordOrder.VSO = True
• Phenomena.Ellipsis.Gapping.HasRightwardVerbs Phenomena.Ellipsis.Gapping.WordOrder.SVO = True
• Phenomena.Ellipsis.Gapping.HasRightwardVerbs Phenomena.Ellipsis.Gapping.WordOrder.VOS = True
• Phenomena.Ellipsis.Gapping.HasRightwardVerbs x✝ = False

@[implicit_reducible]

instance Phenomena.Ellipsis.Gapping.instDecidablePredWordOrderHasRightwardVerbs : DecidablePred HasRightwardVerbs

Equations

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

def Phenomena.Ellipsis.Gapping.HasLeftwardVerbs : WordOrder → Prop

Equations

• Phenomena.Ellipsis.Gapping.HasLeftwardVerbs Phenomena.Ellipsis.Gapping.WordOrder.SOV = True
• Phenomena.Ellipsis.Gapping.HasLeftwardVerbs Phenomena.Ellipsis.Gapping.WordOrder.OVS = True
• Phenomena.Ellipsis.Gapping.HasLeftwardVerbs Phenomena.Ellipsis.Gapping.WordOrder.OSV = True
• Phenomena.Ellipsis.Gapping.HasLeftwardVerbs x✝ = False

@[implicit_reducible]

instance Phenomena.Ellipsis.Gapping.instDecidablePredWordOrderHasLeftwardVerbs : DecidablePred HasLeftwardVerbs

Equations

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

def Phenomena.Ellipsis.Gapping.rossRevised (profile : WordOrderProfile) : GappingPattern

Equations

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

def Phenomena.Ellipsis.Gapping.japanese : WordOrderProfile

Japanese: pure SOV, backward gapping only

Equations

• Phenomena.Ellipsis.Gapping.japanese = { mainClause := Phenomena.Ellipsis.Gapping.WordOrder.SOV, subClause := Phenomena.Ellipsis.Gapping.WordOrder.SOV }

def Phenomena.Ellipsis.Gapping.irish : WordOrderProfile

Irish: pure VSO, forward gapping only

Equations

• Phenomena.Ellipsis.Gapping.irish = { mainClause := Phenomena.Ellipsis.Gapping.WordOrder.VSO, subClause := Phenomena.Ellipsis.Gapping.WordOrder.VSO }

def Phenomena.Ellipsis.Gapping.english : WordOrderProfile

English: pure SVO, forward gapping only

Equations

• Phenomena.Ellipsis.Gapping.english = { mainClause := Phenomena.Ellipsis.Gapping.WordOrder.SVO, subClause := Phenomena.Ellipsis.Gapping.WordOrder.SVO }

def Phenomena.Ellipsis.Gapping.dutch : WordOrderProfile

Dutch: VSO main clause, SOV subordinate clause - both directions

Equations

• Phenomena.Ellipsis.Gapping.dutch = { mainClause := Phenomena.Ellipsis.Gapping.WordOrder.SVO, subClause := Phenomena.Ellipsis.Gapping.WordOrder.SOV }

def Phenomena.Ellipsis.Gapping.german : WordOrderProfile

German: similar to Dutch

Equations

• Phenomena.Ellipsis.Gapping.german = { mainClause := Phenomena.Ellipsis.Gapping.WordOrder.SVO, subClause := Phenomena.Ellipsis.Gapping.WordOrder.SOV }

def Phenomena.Ellipsis.Gapping.zapotec : WordOrderProfile

Zapotec: VSO subordinate, but allows SOV main clause - both directions

Equations

• Phenomena.Ellipsis.Gapping.zapotec = { mainClause := Phenomena.Ellipsis.Gapping.WordOrder.VSO, subClause := Phenomena.Ellipsis.Gapping.WordOrder.VSO }

structure Phenomena.Ellipsis.Gapping.GappingExample : Type

A gapping example in a specific language.

• language : String
• surface : String
• gloss : String
• translation : String
• direction : GappingDirection
• isGrammatical : Bool

@[implicit_reducible]

instance Phenomena.Ellipsis.Gapping.instReprGappingExample : Repr GappingExample

Equations

• Phenomena.Ellipsis.Gapping.instReprGappingExample = { reprPrec := Phenomena.Ellipsis.Gapping.instReprGappingExample.repr }

def Phenomena.Ellipsis.Gapping.instReprGappingExample.repr : GappingExample → Nat → Std.Format

Equations

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

def Phenomena.Ellipsis.Gapping.japanese_backward : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.japanese_forward_bad : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.irish_forward : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.irish_backward_bad : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.english_forward : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.english_backward_bad : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.dutch_main_forward : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.dutch_sub_backward : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.allGappingExamples : List GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.grammaticalExamples : List GappingExample

Equations

• Phenomena.Ellipsis.Gapping.grammaticalExamples = List.filter (fun (x : Phenomena.Ellipsis.Gapping.GappingExample) => x.isGrammatical) Phenomena.Ellipsis.Gapping.allGappingExamples

def Phenomena.Ellipsis.Gapping.ungrammaticalExamples : List GappingExample

Equations

• Phenomena.Ellipsis.Gapping.ungrammaticalExamples = List.filter (fun (x : Phenomena.Ellipsis.Gapping.GappingExample) => !x.isGrammatical) Phenomena.Ellipsis.Gapping.allGappingExamples

inductive Phenomena.Ellipsis.Gapping.EllipsisType : Type

Types of elliptical constructions (Steedman's taxonomy).

Gapping and Stripping are syntactically mediated via CCG. VP Ellipsis and Sluicing are purely anaphoric.

• gapping : EllipsisType
• stripping : EllipsisType
• vpEllipsis : EllipsisType
• sluicing : EllipsisType

@[implicit_reducible]

instance Phenomena.Ellipsis.Gapping.instDecidableEqEllipsisType : DecidableEq EllipsisType

Equations

• Phenomena.Ellipsis.Gapping.instDecidableEqEllipsisType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Ellipsis.Gapping.instReprEllipsisType : Repr EllipsisType

Equations

• Phenomena.Ellipsis.Gapping.instReprEllipsisType = { reprPrec := Phenomena.Ellipsis.Gapping.instReprEllipsisType.repr }

def Phenomena.Ellipsis.Gapping.instReprEllipsisType.repr : EllipsisType → Nat → Std.Format

Equations

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

def Phenomena.Ellipsis.Gapping.isSyntacticallyMediated : EllipsisType → Prop

Is the ellipsis type syntactically mediated (vs purely anaphoric)?

Equations

• Phenomena.Ellipsis.Gapping.isSyntacticallyMediated Phenomena.Ellipsis.Gapping.EllipsisType.gapping = True
• Phenomena.Ellipsis.Gapping.isSyntacticallyMediated Phenomena.Ellipsis.Gapping.EllipsisType.stripping = True
• Phenomena.Ellipsis.Gapping.isSyntacticallyMediated Phenomena.Ellipsis.Gapping.EllipsisType.vpEllipsis = False
• Phenomena.Ellipsis.Gapping.isSyntacticallyMediated Phenomena.Ellipsis.Gapping.EllipsisType.sluicing = False

@[implicit_reducible]

instance Phenomena.Ellipsis.Gapping.instDecidablePredEllipsisTypeIsSyntacticallyMediated : DecidablePred isSyntacticallyMediated

Equations

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

def Phenomena.Ellipsis.Gapping.HasWordOrderConstraints : EllipsisType → Prop

Does the ellipsis type exhibit word-order constraints?

Equations

• Phenomena.Ellipsis.Gapping.HasWordOrderConstraints Phenomena.Ellipsis.Gapping.EllipsisType.gapping = True
• Phenomena.Ellipsis.Gapping.HasWordOrderConstraints Phenomena.Ellipsis.Gapping.EllipsisType.stripping = True
• Phenomena.Ellipsis.Gapping.HasWordOrderConstraints Phenomena.Ellipsis.Gapping.EllipsisType.vpEllipsis = False
• Phenomena.Ellipsis.Gapping.HasWordOrderConstraints Phenomena.Ellipsis.Gapping.EllipsisType.sluicing = False

@[implicit_reducible]

instance Phenomena.Ellipsis.Gapping.instDecidablePredEllipsisTypeHasWordOrderConstraints : DecidablePred HasWordOrderConstraints

Equations

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

theorem Phenomena.Ellipsis.Gapping.sov_backward_only : ¬(rossRevised japanese).allowsForward ∧ (rossRevised japanese).allowsBackward

Pure SOV language has backward gapping only

theorem Phenomena.Ellipsis.Gapping.vso_forward_only : (rossRevised irish).allowsForward ∧ ¬(rossRevised irish).allowsBackward

Pure VSO language has forward gapping only

theorem Phenomena.Ellipsis.Gapping.svo_forward_only : (rossRevised english).allowsForward ∧ ¬(rossRevised english).allowsBackward

Pure SVO language has forward gapping only

theorem Phenomena.Ellipsis.Gapping.mixed_allows_both : (rossRevised dutch).allowsForward ∧ (rossRevised dutch).allowsBackward

Mixed order language (Dutch) allows both

def Phenomena.Ellipsis.Gapping.RequiresSyntacticIdentity : EllipsisType → Prop

Does this ellipsis type require syntactic identity (SIC)? @cite{anand-hardt-mccloskey-2021}: sluicing and gapping require structural matching; VP ellipsis does not.

Equations

• Phenomena.Ellipsis.Gapping.RequiresSyntacticIdentity Phenomena.Ellipsis.Gapping.EllipsisType.sluicing = True
• Phenomena.Ellipsis.Gapping.RequiresSyntacticIdentity Phenomena.Ellipsis.Gapping.EllipsisType.gapping = True
• Phenomena.Ellipsis.Gapping.RequiresSyntacticIdentity Phenomena.Ellipsis.Gapping.EllipsisType.stripping = True
• Phenomena.Ellipsis.Gapping.RequiresSyntacticIdentity Phenomena.Ellipsis.Gapping.EllipsisType.vpEllipsis = False

@[implicit_reducible]

instance Phenomena.Ellipsis.Gapping.instDecidablePredEllipsisTypeRequiresSyntacticIdentity : DecidablePred RequiresSyntacticIdentity

Equations

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

def Phenomena.Ellipsis.Gapping.RequiresSemanticIdentity : EllipsisType → Prop

Does this ellipsis type require semantic identity (e-GIVENness)? @cite{anand-hardt-mccloskey-2021}: all ellipsis types require e-GIVENness.

Equations

• Phenomena.Ellipsis.Gapping.RequiresSemanticIdentity x✝ = True

@[implicit_reducible]

instance Phenomena.Ellipsis.Gapping.instDecidablePredEllipsisTypeRequiresSemanticIdentity : DecidablePred RequiresSemanticIdentity

Equations

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

theorem Phenomena.Ellipsis.Gapping.sluicing_requires_both : RequiresSemanticIdentity EllipsisType.sluicing ∧ RequiresSyntacticIdentity EllipsisType.sluicing

Sluicing requires both semantic and syntactic identity.

theorem Phenomena.Ellipsis.Gapping.vpe_semantic_only : RequiresSemanticIdentity EllipsisType.vpEllipsis ∧ ¬RequiresSyntacticIdentity EllipsisType.vpEllipsis

VP ellipsis requires semantic identity but not syntactic identity.

theorem Phenomena.Ellipsis.Gapping.vpe_voice_mismatch_explained : ¬RequiresSyntacticIdentity EllipsisType.vpEllipsis

VP ellipsis tolerates voice mismatches because it lacks the SIC. Since VPE has no syntactic identity requirement, voice flavor differences (agentive vs nonThematic) are irrelevant — only e-GIVENness (semantic identity) must hold.