Docs / Logic / Natural / ProjectivitySignature

Projectivity signatures

import Linglib.Logic.Natural.ProjectivitySignature · namespace NaturalLogic

This file defines the function classes of natural logic and the nine projectivity signatures of Icard that name them. A map between bounded lattices may be monotone or antitone, and additive, multiplicative, anti-additive or anti-multiplicative with the unit conditions of Icard's complete properties; a signature asserts some of these properties and holds of a map that has them all. Signatures are ordered by refinement, and composing maps composes their signatures in a monoid whose invertible elements are the two polarities and whose sign, the marking of the Monotonicity Calculus, is multiplicative. Signatures act on the relations of natural logic by projection (Logic/Natural/Projection.lean).

References

Icard 2012, Inclusion and Exclusion in Natural Language formalized

Projectivity signatures

Composition

Signs and polarities

The function class of a signature

L225–232

A function has signature σ — is a "σ-function" — when it has every property σ asserts.

def ProjectivitySignature.HoldsFor L234–237

{α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] (σ : ProjectivitySignature) (f : α → β) :

Prop

σ.HoldsFor f = ∀ p ∈ σ.properties, p.HoldsFor f

Built from , ,

Used in Logic/Natural/Completeness, Logic/Natural/Composition, Logic/Natural/Projection, Semantics/PolarityItem/Environment, Semantics/PolarityItem/Licenser and 1 more

A ψ-function after a φ-function is a ψ * φ-function, over any bounded lattices: the function classes compose as compose says (Icard 2012 Definition 2.6 and Lemma 2.7).

theorem ProjectivitySignature.HoldsFor.comp L300–306

{α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {γ : Type u_3} [Lattice γ] [BoundedOrder γ] {ψ φ : ProjectivitySignature} {f : β → γ} {g : α → β} (hf : ψ.HoldsFor f) (hg : φ.HoldsFor g) :

(ψ * φ).HoldsFor (f ∘ g)

Built from ,