L-Analyticity in Natural Language

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

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 NeoGricean.Analyticity.SemType : Type

Semantic types in the Montagovian sense.

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

instance NeoGricean.Analyticity.instDecidableEqSemType : DecidableEq SemType

Equations

• NeoGricean.Analyticity.instDecidableEqSemType = NeoGricean.Analyticity.instDecidableEqSemType.decEq

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

Equations

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

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

Equations

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

instance NeoGricean.Analyticity.instReprSemType : Repr SemType

Equations

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

instance NeoGricean.Analyticity.instBEqSemType : BEq SemType

Equations

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

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

Equations

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

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

Equations

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

def NeoGricean.Analyticity.et : SemType

Equations

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

def NeoGricean.Analyticity.ett : SemType

Equations

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

def NeoGricean.Analyticity.Det : SemType

Equations

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

@[reducible, inline]

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

A permutation on the entity domain.

Equations

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

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

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

Equations

• NeoGricean.Analyticity.liftPermT _π = id

def NeoGricean.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

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

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

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

Equations

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

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

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

Equations

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

def NeoGricean.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 NeoGricean.Analyticity.everyD (Entity : Type u_2) : (Entity → Prop) → (Entity → Prop) → Prop

Standard logical determiners (returning Prop for cleaner proofs).

Equations

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

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

Equations

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

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

Equations

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

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

"every" is permutation invariant

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

"some" is permutation invariant

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

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

Equations

• NeoGricean.Analyticity.thereP Entity x✝ = True

theorem NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.Analyticity.thereSome_not_LAnalytic {Entity : Type u_1} [Inhabited Entity] : ¬(thereSomeSkeleton Entity).isLAnalytic

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

def NeoGricean.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 NeoGricean.Analyticity.thereEvery_LTautology {Entity : Type u_1} : (thereEverySkeleton Entity).isLTautology

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

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

def NeoGricean.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 NeoGricean.Analyticity.everyXisY_not_LAnalytic {Entity : Type u_1} [Inhabited Entity] : ¬(everyXisYSkeleton Entity).isLAnalytic

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

def NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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).

inductive NeoGricean.Analyticity.GrammaticalStatus : Type

Grammatical status for L-analyticity predictions.

• grammatical : GrammaticalStatus
• ungrammatical : GrammaticalStatus

instance NeoGricean.Analyticity.instDecidableEqGrammaticalStatus : DecidableEq GrammaticalStatus

Equations

• NeoGricean.Analyticity.instDecidableEqGrammaticalStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance NeoGricean.Analyticity.instReprGrammaticalStatus : Repr GrammaticalStatus

Equations

• NeoGricean.Analyticity.instReprGrammaticalStatus = { reprPrec := NeoGricean.Analyticity.instReprGrammaticalStatus.repr }

def NeoGricean.Analyticity.instReprGrammaticalStatus.repr : GrammaticalStatus → ℕ → Std.Format

Equations

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

instance NeoGricean.Analyticity.instBEqGrammaticalStatus : BEq GrammaticalStatus

Equations

• NeoGricean.Analyticity.instBEqGrammaticalStatus = { beq := NeoGricean.Analyticity.instBEqGrammaticalStatus.beq }

def NeoGricean.Analyticity.instBEqGrammaticalStatus.beq : GrammaticalStatus → GrammaticalStatus → Bool

Equations

• NeoGricean.Analyticity.instBEqGrammaticalStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def NeoGricean.Analyticity.predictGrammaticality {Entity : Type u_1} (skel : LogicalSkeleton Entity) (hDec : Decidable skel.isLAnalytic) : GrammaticalStatus

Predict grammatical status from logical skeleton.

Equations

• NeoGricean.Analyticity.predictGrammaticality skel hDec = if skel.isLAnalytic then NeoGricean.Analyticity.GrammaticalStatus.ungrammatical else NeoGricean.Analyticity.GrammaticalStatus.grammatical

structure NeoGricean.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 : GrammaticalStatus

  Empirical grammaticality judgment

• predictionMatches : Bool

  Does prediction match?

• notes : String

  Notes

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

Equations

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

instance NeoGricean.Analyticity.instReprLAnalyticityExample : Repr LAnalyticityExample

Equations

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

def NeoGricean.Analyticity.thereEveryStudent : LAnalyticityExample

Equations

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

def NeoGricean.Analyticity.thereSomeStudents : LAnalyticityExample

Equations

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

def NeoGricean.Analyticity.someButBill : LAnalyticityExample

Equations

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

def NeoGricean.Analyticity.everyButBill : LAnalyticityExample

Equations

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

def NeoGricean.Analyticity.noOneButBill : LAnalyticityExample

Equations

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

def NeoGricean.Analyticity.everyWomanIsWoman : LAnalyticityExample

Equations

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

def NeoGricean.Analyticity.johnSmokesAndDoesnt : LAnalyticityExample

Equations

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

def NeoGricean.Analyticity.lAnalyticityExamples : List LAnalyticityExample

All examples

Equations

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