Del Pinal (2015): Dual Content Semantics

[DP15]

Dual-content reanalysis of privative adjectives: nouns have E-structure + qualia C-structure ([Pus95]); privatives operate on C-structure. Sibling to Partee2010.lean (same data, opposite mechanism: Partee re-types fake as subsective plus noun-coercion, DC keeps fake's Kamp-privative typing and pairs it with C-structure).

Main definitions

• Qualia, NounMeaning, DCAdjMeaning: dual-content lexical-entry types.
• DelPinalReanalysis: stand-alone operator-typed reanalysis structure.
• fakeDC, counterfeitDC, artificialDC: the privative trio (paper eqs. 16, 11, 12); fakeDelPinal, counterfeitDelPinal: constructive witnesses. artificialDC is not a DelPinalReanalysis (it admits no look-like-N inference) — see artificialDC_not_DelPinalReanalysis.
• AdjMeaning.toDCAdjMeaning: lift a classical AdjMeaning to a DCAdjMeaning by inheriting noun qualia.
• DelPinalReanalysis.no_LicensedCoercion: cross-framework divergence with [Par10] (any DC reanalysis projects to a Kamp-privative AdjMeaning, hence admits no NVP-licensed coercion).
• Kamp1975_fakeAdj_lift_not_DelPinalReanalysis: Kamp's classical typing of fake is genuinely impoverished — the lift to DCAdjMeaning fails to satisfy the look-like-N constraint that DC's fake enforces.

Implementation notes

Paper qualia values involve event quantifiers (λx.GEN e[SHOOTING(e) ∧ INSTRUMENT(e,x)], ∃e[MAKING(e) ∧ GOAL(e, Q_F(N)(x))]); these are flattened to characteristic predicates of type Property W E. The AGENTIVE clause of fakeDC is approximated as N.qualia.formal (the GOAL projects the formal quale), which loses the existential commitment about an event of making — a found object can look like a gun without being made-to-look-like one. This proxy is adequate at the predicate-level fidelity of the current substrate; faithful encoding would require an event substrate. Counterfeit's AGENTIVE goal is Q_F ∧ Q_T; artificial's is Q_T alone.

The dual FA_DC compositional rule (paper §3: E-side standard FA, C-side pointwise FA via qualia functions) is elided — operators here are flat NounMeaning → NounMeaning functions rather than structured pairs of E-functions and C-functions. The trade-off is exposed by artificialDC_not_DelPinalReanalysis: not every privative-like operator satisfies extension_implies_formal.

References

• [Pus95] (qualia roles).
• [Par10] (sibling reanalysis).

structure DelPinal2015.Qualia (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Pustejovsky-style four-role qualia profile.

• constitutive : Semantics.Gradability.Classification.Property W E
• formal : Semantics.Gradability.Classification.Property W E
• telic : Semantics.Gradability.Classification.Property W E
• agentive : Semantics.Gradability.Classification.Property W E

structure DelPinal2015.NounMeaning (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

DC lexical entry: extension plus qualia profile.

• extension : Semantics.Gradability.Classification.Property W E
• qualia : Qualia W E

@[reducible, inline]

abbrev DelPinal2015.DCAdjMeaning (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

Adjective as a DC operator on noun meanings.

Equations

• DelPinal2015.DCAdjMeaning W E = (DelPinal2015.NounMeaning W E → DelPinal2015.NounMeaning W E)

structure DelPinal2015.DelPinalReanalysis (W : Type u_3) (E : Type u_4) : Type (max u_3 u_4)

DC reanalysis: a DCAdjMeaning operator with privative E-structure and formal-quale entailment (the "looks like N" inference).

• operator : DCAdjMeaning W E
• extension_privative (N : NounMeaning W E) (w : W) (x : E) : (self.operator N).extension w x → ¬N.extension w x
• extension_implies_formal (N : NounMeaning W E) (w : W) (x : E) : (self.operator N).extension w x → N.qualia.formal w x

The privative trio: fake, counterfeit, artificial

def DelPinal2015.fakeDC {W : Type u_1} {E : Type u_2} : DCAdjMeaning W E

DC fake operator (paper eq. 16).

Equations

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

def DelPinal2015.counterfeitDC {W : Type u_1} {E : Type u_2} : DCAdjMeaning W E

DC counterfeit operator (paper eq. 11). The AGENTIVE goal is to look AND function like N (made-to-look-and-function). TELIC preserved (not negated).

Equations

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

def DelPinal2015.artificialDC {W : Type u_1} {E : Type u_2} : DCAdjMeaning W E

DC artificial operator (paper eq. 12). The AGENTIVE goal is to function like N (no look-like commitment). FORMAL is preserved in qualia but is not asserted in extension.

Equations

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

def DelPinal2015.fakeDelPinal {W : Type u_1} {E : Type u_2} : DelPinalReanalysis W E

fakeDC is a DelPinalReanalysis.

Equations

• DelPinal2015.fakeDelPinal = { operator := DelPinal2015.fakeDC, extension_privative := ⋯, extension_implies_formal := ⋯ }

def DelPinal2015.counterfeitDelPinal {W : Type u_1} {E : Type u_2} : DelPinalReanalysis W E

counterfeitDC is a DelPinalReanalysis.

Equations

• DelPinal2015.counterfeitDelPinal = { operator := DelPinal2015.counterfeitDC, extension_privative := ⋯, extension_implies_formal := ⋯ }

theorem DelPinal2015.artificialDC_not_DelPinalReanalysis : ¬∃ (r : DelPinalReanalysis Unit Unit), r.operator = artificialDC

artificialDC is not a DelPinalReanalysis: artificial N does not entail the look-like inference (paper §3: artificial heart need not look like a heart). Counterexample noun shows that the extension can be inhabited while the input formal quale is empty.

Cross-framework divergence with [Par10]

def DelPinal2015.DelPinalReanalysis.toAdjMeaning {W : Type u_1} {E : Type u_2} (r : DelPinalReanalysis W E) (Q : Semantics.Gradability.Classification.Property W E → Qualia W E) : Semantics.Gradability.Classification.AdjMeaning W E

Classical-AdjMeaning projection of a DC operator under a per-noun qualia assignment Q.

Equations

• r.toAdjMeaning Q N w x = (r.operator { extension := N, qualia := Q N }).extension w x

theorem DelPinal2015.DelPinalReanalysis.toAdjMeaning_isPrivative {W : Type u_1} {E : Type u_2} (r : DelPinalReanalysis W E) (Q : Semantics.Gradability.Classification.Property W E → Qualia W E) : Semantics.Gradability.Classification.isPrivative (r.toAdjMeaning Q)

theorem DelPinal2015.DelPinalReanalysis.no_LicensedCoercion {W : Type u_1} {E : Type u_2} (r : DelPinalReanalysis W E) (Q : Semantics.Gradability.Classification.Property W E → Qualia W E) (N : Semantics.Gradability.Classification.Property W E) (w : W) : IsEmpty (Semantics.Composition.Coercion.LicensedCoercion N (r.toAdjMeaning Q) w)

The classical projection of any DC reanalysis admits no LicensedCoercion. The two frameworks make incompatible type-level commitments about privatives.

Classical lift; impoverishment of Kamp-typed fake

def Semantics.Gradability.Classification.AdjMeaning.toDCAdjMeaning {W : Type u_1} {E : Type u_2} (adj : AdjMeaning W E) : DelPinal2015.DCAdjMeaning W E

Lift a classical AdjMeaning to a DCAdjMeaning by computing the extension via the classical adj and inheriting the input noun's qualia (the C-structure passes through unchanged).

Equations

• adj.toDCAdjMeaning N = { extension := adj N.extension, qualia := N.qualia }

theorem DelPinal2015.Kamp1975_fakeAdj_lift_not_DelPinalReanalysis : ¬∃ (r : DelPinalReanalysis Kamp1975.W2 Kamp1975.E3), r.operator = Kamp1975.fakeAdj.toDCAdjMeaning

Kamp1975.fakeAdj lifted to a DCAdjMeaning is not a DelPinalReanalysis: the classical typing preserves the Kamp- privative E-structure but cannot in general guarantee the look-like-N inference (the input noun's formal quale need not hold at the fake-witness entity). Formal counterpart to Del Pinal's argument that the classical analysis is incomplete.

RevisedClass classification: DC side

theorem DelPinal2015.Kamp1975_fakeAdj_RevisedClass_nonSubsective : Semantics.Gradability.Classification.RevisedClass.nonSubsective.satisfies Kamp1975.fakeAdj

Under Del Pinal's framework, Kamp1975.fakeAdj keeps its Kamp-privative typing and falls in RevisedClass.nonSubsective. Contrast with Partee2010.fakeReanalysis.is_subsective: Partee reclassifies the reanalyzed meaning into RevisedClass.subsective. The two frameworks attribute different RevisedClass values to the lexical item 'fake' because they posit different formal objects for it.

Output-qualia witness theorems

Per paper eqs. 11, 12, 16/17, the three operators produce distinct qualia outputs. The Iff.rfl theorems below verify the structural discrimination, justifying the 4-field Qualia shape.

theorem DelPinal2015.fakeDC_telic_negates {W : Type u_1} {E : Type u_2} (N : NounMeaning W E) (w : W) (x : E) : (fakeDC N).qualia.telic w x ↔ ¬N.qualia.telic w x

theorem DelPinal2015.counterfeitDC_telic_preserved {W : Type u_1} {E : Type u_2} (N : NounMeaning W E) (w : W) (x : E) : (counterfeitDC N).qualia.telic w x ↔ N.qualia.telic w x

theorem DelPinal2015.artificialDC_telic_preserved {W : Type u_1} {E : Type u_2} (N : NounMeaning W E) (w : W) (x : E) : (artificialDC N).qualia.telic w x ↔ N.qualia.telic w x

theorem DelPinal2015.fakeDC_agentive_is_formal {W : Type u_1} {E : Type u_2} (N : NounMeaning W E) (w : W) (x : E) : (fakeDC N).qualia.agentive w x ↔ N.qualia.formal w x

theorem DelPinal2015.counterfeitDC_agentive_is_formal_and_telic {W : Type u_1} {E : Type u_2} (N : NounMeaning W E) (w : W) (x : E) : (counterfeitDC N).qualia.agentive w x ↔ N.qualia.formal w x ∧ N.qualia.telic w x

theorem DelPinal2015.artificialDC_agentive_is_telic {W : Type u_1} {E : Type u_2} (N : NounMeaning W E) (w : W) (x : E) : (artificialDC N).qualia.agentive w x ↔ N.qualia.telic w x