Branan and Erlewine 2023: Anti-pied-piping

[BE23] documents anti-pied-piping — focus morphosyntax (particle placement, focus movement) targeting a proper subpart of the logical focus — in over sixty languages from over forty language groups, and proposes that focus particles are morphosyntactic flags for abstract operators, severing the particle's pronounced position from the position of its semantic contribution. This file formalizes the introductory paradigm (their (1)–(8)): Japanese mo placement and Hungarian focus movement each attest exact targeting, pied-piping, and anti-pied-piping, stated over the host–focus containment relations of Morphology/Reflex.lean.

Main declarations

• BrananErlewine2023.Node: the clause skeleton of the paradigm.
• mo_attests_all_relations / movement_attests_all_relations: particle placement and focus movement each realize all three host–focus relations.
• msf_tolerates_mismatches: neither process strictly targets the F-marked constituent — the shape of the paper's argument that focus morphosyntax targets a particle phrase rather than F itself.

TODO

• The leftmost-targeting generalization of their §3 (requires linear order on constituents).
• The particle-phrase theory of their §4 and the cross-linguistic appendix as Data/Examples rows.

The clause skeleton

inductive BrananErlewine2023.Node : Type

Clause skeleton for the introductory paradigm: an attributive adjective within the object DP; verb and object within VP; subject and VP within S.

• s : Node
• sbj : Node
• vp : Node
• v : Node
• obj : Node
• att : Node

@[implicit_reducible]

instance BrananErlewine2023.instDecidableEqNode : DecidableEq Node

Equations

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

def BrananErlewine2023.instReprNode.repr : Node → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BrananErlewine2023.instReprNode : Repr Node

Equations

• BrananErlewine2023.instReprNode = { reprPrec := BrananErlewine2023.instReprNode.repr }

@[implicit_reducible]

instance BrananErlewine2023.instFintypeNode : Fintype Node

Equations

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

def BrananErlewine2023.nle : Node → Node → Bool

Constituent containment.

Equations

• BrananErlewine2023.nle x✝ BrananErlewine2023.Node.s = true
• BrananErlewine2023.nle BrananErlewine2023.Node.v BrananErlewine2023.Node.vp = true
• BrananErlewine2023.nle BrananErlewine2023.Node.obj BrananErlewine2023.Node.vp = true
• BrananErlewine2023.nle BrananErlewine2023.Node.att BrananErlewine2023.Node.vp = true
• BrananErlewine2023.nle BrananErlewine2023.Node.vp BrananErlewine2023.Node.vp = true
• BrananErlewine2023.nle BrananErlewine2023.Node.att BrananErlewine2023.Node.obj = true
• BrananErlewine2023.nle BrananErlewine2023.Node.obj BrananErlewine2023.Node.obj = true
• BrananErlewine2023.nle BrananErlewine2023.Node.sbj BrananErlewine2023.Node.sbj = true
• BrananErlewine2023.nle BrananErlewine2023.Node.v BrananErlewine2023.Node.v = true
• BrananErlewine2023.nle BrananErlewine2023.Node.att BrananErlewine2023.Node.att = true
• BrananErlewine2023.nle x✝¹ x✝ = false

@[implicit_reducible]

instance BrananErlewine2023.instPartialOrderNode : PartialOrder Node

Equations

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

@[implicit_reducible]

instance BrananErlewine2023.instDecidableLENode : DecidableLE Node

Equations

• BrananErlewine2023.instDecidableLENode x✝¹ x✝ = instDecidableEqBool (BrananErlewine2023.nle x✝¹ x✝) true

@[implicit_reducible]

instance BrananErlewine2023.instDecidableLTNode : DecidableLT Node

Equations

• BrananErlewine2023.instDecidableLTNode a b = instDecidableAnd

The introductory paradigm

Their (1)–(8): Japanese additive mo and Hungarian focus movement in all three host–focus configurations.

def BrananErlewine2023.moExact : Features.Marking Node

Their (2): Hanako-wa [hon]F*-mo* katta — mo on the focused object itself.

Equations

• BrananErlewine2023.moExact = { target := BrananErlewine2023.Node.obj, reflexes := [Features.Reflex.morpheme BrananErlewine2023.Node.obj] }

def BrananErlewine2023.moPiedPiped : Features.Marking Node

Their (4): Hanako-wa [[hon]F-o kai]-mo — mo on the VP properly containing the focused object (Kuroda's pied-piping datum).

Equations

• BrananErlewine2023.moPiedPiped = { target := BrananErlewine2023.Node.obj, reflexes := [Features.Reflex.morpheme BrananErlewine2023.Node.vp] }

def BrananErlewine2023.moAntiPiedPiped : Features.Marking Node

Their (8): [[Ame]-mo furu]F — sentence focus with mo on the subject properly contained in it (Nagano's anti-pied-piping datum).

Equations

• BrananErlewine2023.moAntiPiedPiped = { target := BrananErlewine2023.Node.s, reflexes := [Features.Reflex.morpheme BrananErlewine2023.Node.sbj] }

def BrananErlewine2023.movementExact : Features.Marking Node

Their (1): Hungarian movement of exactly the focused argument to the immediately preverbal focus position.

Equations

• BrananErlewine2023.movementExact = { target := BrananErlewine2023.Node.obj, reflexes := [Features.Reflex.displacement BrananErlewine2023.Node.obj] }

def BrananErlewine2023.movementPiedPiped : Features.Marking Node

Their (3): [a [használt]F autót] adta el — the whole object DP moves for a focus on the attributive adjective (Kenesei's pied-piping datum).

Equations

• BrananErlewine2023.movementPiedPiped = { target := BrananErlewine2023.Node.att, reflexes := [Features.Reflex.displacement BrananErlewine2023.Node.obj] }

def BrananErlewine2023.movementAntiPiedPiped : Features.Marking Node

Their (7): Péter [a Hamletet] [olvasta fel _ a kertben]F — predicate focus with movement of the object properly contained in it (Kenesei's anti-pied-piping datum).

Equations

• BrananErlewine2023.movementAntiPiedPiped = { target := BrananErlewine2023.Node.vp, reflexes := [Features.Reflex.displacement BrananErlewine2023.Node.obj] }

All three relations, in both processes

theorem BrananErlewine2023.mo_attests_all_relations : moExact.ExactlyTargets ∧ moPiedPiped.PiedPipes ∧ moAntiPiedPiped.AntiPiedPipes

Japanese mo placement attests all three host–focus relations (their (2)/(4)/(8)).

theorem BrananErlewine2023.movement_attests_all_relations : movementExact.ExactlyTargets ∧ movementPiedPiped.PiedPipes ∧ movementAntiPiedPiped.AntiPiedPipes

Hungarian focus movement attests all three host–focus relations (their (1)/(3)/(7)).

theorem BrananErlewine2023.msf_tolerates_mismatches : ¬moPiedPiped.ExactlyTargets ∧ ¬moAntiPiedPiped.ExactlyTargets ∧ ¬movementPiedPiped.ExactlyTargets ∧ ¬movementAntiPiedPiped.ExactlyTargets

Neither particle placement nor focus movement strictly targets the F-marked constituent: each tolerates mismatches in both directions.