Projection through projectivity signatures

The constraint between the values of a function with property p that a constraint a between its arguments guarantees, when there is one (ProjectivitySignature.Property.HoldsFor.project): a monotone function keeps ≤ and ≥ and an antitone one swaps them, an additive function keeps codisjointness and a multiplicative one disjointness, an anti-additive function turns codisjointness into disjointness and an anti-multiplicative one the reverse.

The projection of a relation through a function of the given signature is the strongest relation guaranteed between f x and f y when x R y and f has signature σ (Icard 2012 Definition 2.3, computed by his Lemma 2.4): ≡, since every function preserves equality, and otherwise the relation asserting what the property rule gives for each property of σ and constraint of R (ProjectivitySignature.mem_constraints_project). Each row is sound (ProjectivitySignature.soundFor_of_holdsFor) and least (ProjectivitySignature.isLeast_project in Logic/Natural/Completeness.lean). Icard 2012 remarks under the table that [R]^• = # for all R (p. 715), which is what the property rule alone gives for ≡ too.

A signature σ is sound for f when f projects every relation as σ's row of the projection table says (Icard 2012 Lemma 2.5: every φ-function projects R to [R]^φ).

A per-position signature profile for a two-place operator. For determiners the positions are restrictor and scope; under the restrictor analysis of conditionals, antecedent and consequent.

A profile is sound for a two-place operator when each component signature is sound for the corresponding section (the other argument held constant).