Core concepts

A core concept is a conceptual primitive that is universally available to every language's grammar, regardless of whether any lexical item in that language realizes it.

The notion comes from @cite{chemla-2007}, who introduced it to explain the anti-duality of French tous despite French lacking a lexical counterpart of both. @cite{buccola-kriz-chemla-2018} generalize the notion to "conceptual alternatives" feeding pragmatic competition, and @cite{jeretic-bassi-gonzalez-yatsushiro-meyer-sauerland-2025} refine it: core concepts feed competition only when an indirect alternative — a pronounceable expression equivalent in meaning to the unpronounceable core-concept structure — is available (Indirect Alternatives, Theories/Semantics/Alternatives/Indirect.lean).

This module is a small registry. The actual denotation of each core concept lives where its semantic content does (e.g. dualPredOnLattice in Features/Number.lean for dual). Use Lexicalizes to express the typological claim "language L lexicalizes core concept c", which is the formal content of "L has a word for c".

inductive Core.CoreConcept.Id : Type

The currently registered core concepts. New entries should correspond to conceptual primitives independently motivated in the literature, with a denotation defined elsewhere in linglib.

• dual : Id

  Number-feature dual: predicate-modifier "and has exactly 2 atomic parts"; denotation in Features.Number.dualPredOnLattice.

• trial : Id

  Number-feature trial. Mentioned in @cite{harbour-2014} as morphologically stable but rare. Denotation TBD.

• universal : Id

  Universal quantifier core concept. Lexicalized as all/tous cross-linguistically.

• existential : Id

  Existential quantifier core concept. Lexicalized as some/ quelques.

@[implicit_reducible]

instance Core.CoreConcept.instDecidableEqId : DecidableEq Id

Equations

• Core.CoreConcept.instDecidableEqId x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.CoreConcept.instReprId.repr : Id → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.CoreConcept.instReprId.repr Core.CoreConcept.Id.dual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.CoreConcept.Id.dual")).group prec✝
• Core.CoreConcept.instReprId.repr Core.CoreConcept.Id.trial prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.CoreConcept.Id.trial")).group prec✝

@[implicit_reducible]

instance Core.CoreConcept.instReprId : Repr Id

Equations

• Core.CoreConcept.instReprId = { reprPrec := Core.CoreConcept.instReprId.repr }

def Core.CoreConcept.Lexicalizes {Tok : Type} (lex : List Tok) (realizes : Tok → Id → Prop) (c : Id) : Prop

A lexicon (any list of lexical tokens of type Tok) lexicalizes a core concept iff some entry realizes it. The realization relation realizes is supplied by the caller — typically a per-language predicate that inspects the lexical entry's denotation.

Example: in Phenomena/Presupposition/Studies/JereticEtAl2025.lean, English realizes both Id.dual = True, French realizes _ Id.dual = False.

Equations

• Core.CoreConcept.Lexicalizes lex realizes c = ∃ (tok : Tok), tok ∈ lex ∧ realizes tok c

@[reducible, inline]

abbrev Core.CoreConcept.LexicalizesDual {Tok : Type} (lex : List Tok) (realizes : Tok → Id → Prop) : Prop

The dual classifier: Lexicalizes for Id.dual.

Equations

• Core.CoreConcept.LexicalizesDual lex realizes = Core.CoreConcept.Lexicalizes lex realizes Core.CoreConcept.Id.dual