Pantcheva 2011: syncretism in directional expressions

[Pan11] [Bob12] [Cah09]

The directional containment object Place ⊂ Goal ⊂ Source ⊂ Route lives in Syntax/Case/Order.lean (Case.PathDir); this study tests its syncretism prediction. Of the logically possible syncretism patterns over the four path roles, only a few are attested, under two constraints ([Pan11] §9.2):

• *ABA (contiguity): a syncretism targets only adjacent heads on the containment chain — the framework-neutral Morphology.Containment object, the same used for nominal case allomorphy ([Cah09], [Bob12]).
• *A&¬A: Goal and Source never share a marker. Source is the semantic reversal of Goal ([Pan11] §9.2.2), so a Goal=Source marker would be contradictory — a pragmatic constraint, not a structural one.

Together they cut the 15 set-partitions of {Place, Goal, Source, Route} to four possible patterns (possible_syncretisms), Pantcheva's Types 1–4. (Her Tables 9.2/9.3 enumerate 14, omitting one *ABA-excluded pattern — Goal=Route skipping Source; the enumeration here is over all 15.) Attested instantiations (her Table 9.4): English at/to/from (all distinct, Type 1); Estonian -l/-l-le/-l-t and Imbabura Quechua -pi/-man/-man-da, where the Source marker morphologically contains the Goal marker — the shell containment made visible; Georgian Location=Goal (Type 3, her Table 9.1).

Main declarations

• Pantcheva2011.possible — the two-constraint filter (*ABA via Containment, *A&¬A via GoalSourceMerged)
• Pantcheva2011.possible_syncretisms — exactly the four attested patterns; four_possible, aba_excluded, ana_excluded
• Pantcheva2011.source_contains_goal — the morphological-containment fact, read off the shared PathDir shell decomposition

@[reducible, inline]

abbrev Pantcheva2011.Pattern : Type

A syncretism pattern over the four path roles, in containment order [Place, Goal, Source, Route], as form-class indices: the n = 4 instance of Morphology.Containment.Pattern.

Equations

• Pantcheva2011.Pattern = Morphology.Containment.Pattern 4 ℕ

def Pantcheva2011.allPatterns : List Pattern

The 15 canonical syncretism patterns — restricted-growth strings over four positions, i.e. the set-partitions of {Place, Goal, Source, Route} up to relabeling.

Equations

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

def Pantcheva2011.GoalSourceMerged (p : Pattern) : Prop

*A&¬A: Goal (position 1) and Source (position 2) share a form class. Forbidden — Source is the reversal of Goal, so a Goal=Source marker is contradictory ([Pan11] §9.2.2).

Equations

• Pantcheva2011.GoalSourceMerged p = (p 1 = p 2)

@[implicit_reducible]

instance Pantcheva2011.instDecidableGoalSourceMerged (p : Pattern) : Decidable (GoalSourceMerged p)

Equations

• Pantcheva2011.instDecidableGoalSourceMerged p = Pantcheva2011.instDecidableGoalSourceMerged._aux_1 p

def Pantcheva2011.Possible (p : Pattern) : Prop

A syncretism pattern is possible iff it is contiguous (*ABA, via the shared Morphology.Containment object) and keeps Goal distinct from Source (*A&¬A).

Equations

• Pantcheva2011.Possible p = (Morphology.Containment.IsContiguous p ∧ ¬Pantcheva2011.GoalSourceMerged p)

@[implicit_reducible]

instance Pantcheva2011.instDecidablePossible (p : Pattern) : Decidable (Possible p)

Equations

• Pantcheva2011.instDecidablePossible p = Pantcheva2011.instDecidablePossible._aux_1 p

theorem Pantcheva2011.possible_syncretisms : List.filter (fun (p : Pattern) => decide (Possible p)) allPatterns = [![0, 0, 1, 1], ![0, 0, 1, 2], ![0, 1, 2, 2], ![0, 1, 2, 3]]

The syncretism typology ([Pan11] Tables 9.2/9.3): of the 15 logically possible patterns, exactly four are attested — the contiguous ones keeping Goal and Source distinct. These are her Types 1–4: all-distinct (Type 1, English), Place=Goal (Type 3, Georgian), Source=Route (Type 2), and Place=Goal with Source=Route (Type 4).

theorem Pantcheva2011.four_possible : (List.filter (fun (p : Pattern) => decide (Possible p)) allPatterns).length = 4

Exactly four syncretism patterns are possible.

theorem Pantcheva2011.aba_excluded : (List.filter (fun (p : Morphology.Containment.Pattern 4 ℕ) => decide ¬Morphology.Containment.IsContiguous p) allPatterns).length = 7

Seven of the eleven excluded patterns violate *ABA (non-contiguous — a syncretism spanning non-adjacent path roles).

theorem Pantcheva2011.ana_excluded : (List.filter (fun (p : Morphology.Containment.Pattern 4 ℕ) => decide (Morphology.Containment.IsContiguous p ∧ GoalSourceMerged p)) allPatterns).length = 4

The remaining four excluded patterns are contiguous but merge Goal with Source — the *A&¬A constraint, unique to the directional domain (the nominal Caha containment has no analogue).

Morphological containment (Table 4.2)

The Source structure contains the Goal structure, visible where the Source marker contains the Goal marker (Quechua -man ⊂ -man-da). This is the shell containment of the shared PathDir object — not a fact re-stipulated here, but read off Case.PathDir.shells.

theorem Pantcheva2011.source_contains_goal : Case.PathDir.place.shells ⊂ Case.PathDir.goal.shells ∧ Case.PathDir.goal.shells ⊂ Case.PathDir.source.shells ∧ Case.PathDir.source.shells ⊂ Case.PathDir.route.shells

Source contains Goal contains Place, as shell-stack inclusion — the morphological-containment fact, from the substrate decomposition.

theorem Pantcheva2011.georgian_loc_goal_possible : Possible ![0, 0, 1, 2]

Georgian's Location=Goal syncretism ([Pan11] Table 9.1) is one of the four possible patterns (Type 3).

The *A&¬A constraint, grounded in the denotation (Ch. 5)

The Goal=Source exclusion (GoalSourceMerged) is not a stipulation: it follows from the directional interpretation. Source denotes the reversal of Goal (PathDir.source_denote_eq_goal_reverse, §5.4), so Goal and Source have distinct, in fact opposite, denotations — a single marker for both would be semantically contradictory.

theorem Pantcheva2011.goalSource_distinct_denotation : Case.PathDir.goal.denote ≠ Case.PathDir.source.denote

Goal and Source have distinct denotations (Source reverses Goal), so a Goal=Source marker would be contradictory — the semantic ground of the *A&¬A constraint that excludes GoalSourceMerged patterns.