L-Analyticity in Natural Language

@cite{barwise-cooper-1981} @cite{gajewski-2002} @cite{von-fintel-1993}

Formalization of @cite{gajewski-2002}. A sentence is L-analytic iff its logical skeleton (obtained by replacing non-logical items with variables) is true or false under all variable assignments. L-analytic sentences are ungrammatical.

inductive Implicature.Analyticity.SemType : Type

Semantic types in the Montagovian sense.

• e : SemType
• t : SemType
• fn : SemType → SemType → SemType

instance Implicature.Analyticity.instDecidableEqSemType : DecidableEq SemType

Equations

• Implicature.Analyticity.instDecidableEqSemType = Implicature.Analyticity.instDecidableEqSemType.decEq

def Implicature.Analyticity.instDecidableEqSemType.decEq (x✝ x✝¹ : SemType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Implicature.Analyticity.instDecidableEqSemType.decEq Implicature.Analyticity.SemType.e Implicature.Analyticity.SemType.e = isTrue ⋯
• Implicature.Analyticity.instDecidableEqSemType.decEq Implicature.Analyticity.SemType.e Implicature.Analyticity.SemType.t = isFalse Implicature.Analyticity.instDecidableEqSemType.decEq._proof_1
• Implicature.Analyticity.instDecidableEqSemType.decEq Implicature.Analyticity.SemType.e ⟨a, a_1⟩ = isFalse ⋯
• Implicature.Analyticity.instDecidableEqSemType.decEq Implicature.Analyticity.SemType.t Implicature.Analyticity.SemType.e = isFalse Implicature.Analyticity.instDecidableEqSemType.decEq._proof_3
• Implicature.Analyticity.instDecidableEqSemType.decEq Implicature.Analyticity.SemType.t Implicature.Analyticity.SemType.t = isTrue ⋯
• Implicature.Analyticity.instDecidableEqSemType.decEq Implicature.Analyticity.SemType.t ⟨a, a_1⟩ = isFalse ⋯
• Implicature.Analyticity.instDecidableEqSemType.decEq ⟨a, a_1⟩ Implicature.Analyticity.SemType.e = isFalse ⋯
• Implicature.Analyticity.instDecidableEqSemType.decEq ⟨a, a_1⟩ Implicature.Analyticity.SemType.t = isFalse ⋯

instance Implicature.Analyticity.instReprSemType : Repr SemType

Equations

• Implicature.Analyticity.instReprSemType = { reprPrec := Implicature.Analyticity.instReprSemType.repr }

def Implicature.Analyticity.instReprSemType.repr : SemType → ℕ → Std.Format

Equations

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

def Implicature.Analyticity.instBEqSemType.beq : SemType → SemType → Bool

Equations

• Implicature.Analyticity.instBEqSemType.beq Implicature.Analyticity.SemType.e Implicature.Analyticity.SemType.e = true
• Implicature.Analyticity.instBEqSemType.beq Implicature.Analyticity.SemType.t Implicature.Analyticity.SemType.t = true
• Implicature.Analyticity.instBEqSemType.beq ⟨a, a_1⟩ ⟨b, b_1⟩ = (Implicature.Analyticity.instBEqSemType.beq a b && Implicature.Analyticity.instBEqSemType.beq a_1 b_1)
• Implicature.Analyticity.instBEqSemType.beq x✝¹ x✝ = false

instance Implicature.Analyticity.instBEqSemType : BEq SemType

Equations

• Implicature.Analyticity.instBEqSemType = { beq := Implicature.Analyticity.instBEqSemType.beq }

def Implicature.Analyticity.«term⟨_,_⟩» : Lean.ParserDescr

Equations

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

def Implicature.Analyticity.et : SemType

Equations

• Implicature.Analyticity.et = ⟨Implicature.Analyticity.SemType.e, Implicature.Analyticity.SemType.t⟩

def Implicature.Analyticity.ett : SemType

Equations

• Implicature.Analyticity.ett = ⟨Implicature.Analyticity.et, Implicature.Analyticity.SemType.t⟩

def Implicature.Analyticity.Det : SemType

Equations

• Implicature.Analyticity.Det = ⟨Implicature.Analyticity.et, Implicature.Analyticity.ett⟩

@[reducible, inline]

abbrev Implicature.Analyticity.EntityPerm (Entity : Type u_2) : Type u_2

A permutation on the entity domain.

Equations

• Implicature.Analyticity.EntityPerm Entity = Equiv.Perm Entity

def Implicature.Analyticity.liftPermT {Entity : Type u_1} (_π : EntityPerm Entity) : Bool → Bool

Lift a permutation on entities to truth values (identity).

Equations

• Implicature.Analyticity.liftPermT _π = id

def Implicature.Analyticity.liftPermFn {A : Type u_2} {B : Type u_3} (_πA : A → A) (πB : B → B) (πAinv : A → A) (f : A → B) : A → B

Lift a permutation to functions: π⟨a,b⟩(f) = πb ∘ f ∘ πa⁻¹.

Equations

• Implicature.Analyticity.liftPermFn _πA πB πAinv f a = πB (f (πAinv a))

def Implicature.Analyticity.isPermInvariant_et {Entity : Type u_1} (P : Entity → Prop) : Prop

A property is permutation invariant iff preserved under all domain permutations.

Equations

• Implicature.Analyticity.isPermInvariant_et P = ∀ (π : Implicature.Analyticity.EntityPerm Entity) (x : Entity), P (π x) ↔ P x

def Implicature.Analyticity.isPermInvariant_ett {Entity : Type u_1} (Q : (Entity → Prop) → Prop) : Prop

A GQ is permutation invariant iff π(Q) = Q for all permutations π.

Equations

• Implicature.Analyticity.isPermInvariant_ett Q = ∀ (π : Implicature.Analyticity.EntityPerm Entity) (P : Entity → Prop), (Q fun (x : Entity) => P ((Equiv.symm π) x)) ↔ Q P

def Implicature.Analyticity.isPermInvariant_Det {Entity : Type u_1} (D : (Entity → Prop) → (Entity → Prop) → Prop) : Prop

A determiner is permutation invariant iff π(D) = D for all permutations π.

Equations

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

def Implicature.Analyticity.everyD (Entity : Type u_2) : (Entity → Prop) → (Entity → Prop) → Prop

Standard logical determiners (returning Prop for cleaner proofs).

Equations

• Implicature.Analyticity.everyD Entity P Q = ∀ (x : Entity), P x → Q x

def Implicature.Analyticity.someD (Entity : Type u_2) : (Entity → Prop) → (Entity → Prop) → Prop

Equations

• Implicature.Analyticity.someD Entity P Q = ∃ (x : Entity), P x ∧ Q x

def Implicature.Analyticity.noD (Entity : Type u_2) : (Entity → Prop) → (Entity → Prop) → Prop

Equations

• Implicature.Analyticity.noD Entity P Q = ¬∃ (x : Entity), P x ∧ Q x

theorem Implicature.Analyticity.every_permInvariant {Entity : Type u_1} : isPermInvariant_Det (everyD Entity)

"every" is permutation invariant

theorem Implicature.Analyticity.some_permInvariant {Entity : Type u_1} : isPermInvariant_Det (someD Entity)

"some" is permutation invariant

def Implicature.Analyticity.thereP (Entity : Type u_2) : Entity → Prop

Expletive "there" denotes the full domain (always true predicate)

Equations

• Implicature.Analyticity.thereP Entity x✝ = True

theorem Implicature.Analyticity.there_permInvariant_prop {Entity : Type u_1} (π : EntityPerm Entity) (x : Entity) : thereP Entity (π x) ↔ thereP Entity x

"there" is permutation invariant (proof for Prop version)

structure Implicature.Analyticity.LogicalSkeleton (Entity : Type u_2) : Type u_2

A logical skeleton parameterized by assignments to non-logical slots.

• numSlots : ℕ

  Number of non-logical slots (variables)

• slotTypes : Fin self.numSlots → SemType

  Types of each slot (simplified: all are properties for now)

• interpret : (Fin self.numSlots → Entity → Prop) → Prop

  Interpretation given an assignment to slots

def Implicature.Analyticity.LogicalSkeleton.isLTautology {Entity : Type u_1} (skel : LogicalSkeleton Entity) : Prop

A logical skeleton is L-tautologous if true under all assignments.

Equations

• skel.isLTautology = ∀ (assignment : Fin skel.numSlots → Entity → Prop), skel.interpret assignment

def Implicature.Analyticity.LogicalSkeleton.isLContradiction {Entity : Type u_1} (skel : LogicalSkeleton Entity) : Prop

A logical skeleton is L-contradictory if false under all assignments.

Equations

• skel.isLContradiction = ∀ (assignment : Fin skel.numSlots → Entity → Prop), ¬skel.interpret assignment

def Implicature.Analyticity.LogicalSkeleton.isLAnalytic {Entity : Type u_1} (skel : LogicalSkeleton Entity) : Prop

A logical skeleton is L-analytic if either L-tautologous or L-contradictory.

Equations

• skel.isLAnalytic = (skel.isLTautology ∨ skel.isLContradiction)

def Implicature.Analyticity.thereSomeSkeleton (Entity : Type u_2) [Inhabited Entity] : LogicalSkeleton Entity

Skeleton for "There are some Xs".

Equations

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

theorem Implicature.Analyticity.thereSome_not_LAnalytic {Entity : Type u_1} [Inhabited Entity] : ¬(thereSomeSkeleton Entity).isLAnalytic

"There are some Xs" is NOT L-analytic (contingent)

def Implicature.Analyticity.thereEverySkeleton (Entity : Type u_2) : LogicalSkeleton Entity

Skeleton for "*There is every X".

Equations

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

theorem Implicature.Analyticity.thereEvery_LTautology {Entity : Type u_1} : (thereEverySkeleton Entity).isLTautology

"*There is every X" is L-tautologous (hence ungrammatical)

theorem Implicature.Analyticity.thereEvery_LAnalytic {Entity : Type u_1} : (thereEverySkeleton Entity).isLAnalytic

def Implicature.Analyticity.everyXisYSkeleton (Entity : Type u_2) [Inhabited Entity] : LogicalSkeleton Entity

Skeleton for "Every X is a Y" with distinct variables.

Equations

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

theorem Implicature.Analyticity.everyXisY_not_LAnalytic {Entity : Type u_1} [Inhabited Entity] : ¬(everyXisYSkeleton Entity).isLAnalytic

"Every X is a Y" is NOT L-analytic

def Implicature.Analyticity.butExceptive {Entity : Type u_1} (D : (Entity → Prop) → (Entity → Prop) → Prop) (A C P : Entity → Prop) : Prop

Von Fintel's but-exceptive semantics. The first conjunct is the presupposition that the exception set C is nonempty (@cite{von-fintel-1993}: "but X" presupposes X is non-vacuous).

Equations

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

def Implicature.Analyticity.someButSkeleton (Entity : Type u_2) : LogicalSkeleton Entity

Skeleton for "*Some X but Y Zs"

Equations

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

theorem Implicature.Analyticity.someBut_LContradiction {Entity : Type u_1} : (someButSkeleton Entity).isLContradiction

"*Some X but Y Zs" is L-contradictory (hence ungrammatical).

Proof: assume the but-exceptive holds with nonempty C. The first conjunct gives a witness x ∈ A ∩ P. Instantiate minimality with S = ∅: since some(A ∩ E)(P) holds (via x), all of C must be in ∅. But C is nonempty by presupposition — contradiction.

def Implicature.Analyticity.everyButSkeleton (Entity : Type u_2) : LogicalSkeleton Entity

Skeleton for "Every X but Y Zs"

Equations

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

theorem Implicature.Analyticity.everyBut_not_LAnalytic {Entity : Type u_1} [Inhabited Entity] [DecidableEq Entity] (h2 : ∃ (a : Entity), ∃ (b : Entity), a ≠ b) : ¬(everyButSkeleton Entity).isLAnalytic

"Every X but Y Zs" is NOT L-analytic (hence grammatical).

def Implicature.Analyticity.predictGrammaticality {Entity : Type u_1} (skel : LogicalSkeleton Entity) (hDec : Decidable skel.isLAnalytic) : Core.Empirical.Acceptability

Predict acceptability from logical skeleton: L-analytic → unacceptable.

Equations

• Implicature.Analyticity.predictGrammaticality skel hDec = if skel.isLAnalytic then Core.Empirical.Acceptability.unacceptable else Core.Empirical.Acceptability.ok

structure Implicature.Analyticity.LAnalyticityExample : Type

An L-analyticity example with empirical judgment.

• sentence : String

  The sentence

• isLAnalytic : Bool

  Is it L-analytic?

• analyticityType : String

  Why (tautology, contradiction, or neither)

• empiricalJudgment : Core.Empirical.Acceptability

  Empirical acceptability judgment

• predictionMatches : Bool

  Does prediction match?

• notes : String

  Notes

instance Implicature.Analyticity.instReprLAnalyticityExample : Repr LAnalyticityExample

Equations

• Implicature.Analyticity.instReprLAnalyticityExample = { reprPrec := Implicature.Analyticity.instReprLAnalyticityExample.repr }

def Implicature.Analyticity.instReprLAnalyticityExample.repr : LAnalyticityExample → ℕ → Std.Format

Equations

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

def Implicature.Analyticity.thereEveryStudent : LAnalyticityExample

Equations

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

def Implicature.Analyticity.thereSomeStudents : LAnalyticityExample

Equations

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

def Implicature.Analyticity.someButBill : LAnalyticityExample

Equations

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

def Implicature.Analyticity.everyButBill : LAnalyticityExample

Equations

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

def Implicature.Analyticity.noOneButBill : LAnalyticityExample

Equations

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

def Implicature.Analyticity.everyWomanIsWoman : LAnalyticityExample

Equations

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

def Implicature.Analyticity.johnSmokesAndDoesnt : LAnalyticityExample

Equations

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

def Implicature.Analyticity.lAnalyticityExamples : List LAnalyticityExample

All examples

Equations

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