Quantifier-free formulas of ordered rings as sign conditions

A quantifier-free formula of the language of ordered rings Language.ring.sum Language.order is a Boolean combination of equations t₁ = t₂ and inequalities t₁ ≤ t₂ between terms, and a term is an integer polynomial (FirstOrder.Language.Term.toMvPolynomial). This file proves that such formulas are exactly the sign conditions on finitely many integer polynomials: conditions that depend only on the signs of the values of the polynomials.

• FirstOrder.Language.BoundedFormula.IsQF.exists_realize_iff_sign: a quantifier-free formula holds exactly when a fixed condition Φ holds of the signs of finitely many fixed integer polynomials p i in its free and bound variables.
• FirstOrder.Language.BoundedFormula.exists_isQF_realize_iff_sign: conversely, every condition on the signs of finitely many integer polynomials is expressed by a quantifier-free formula, built from the atomic formulas FirstOrder.Language.Term.signFormula saying that a term has a given sign.

The polynomials, the sign condition and the formula do not depend on the structure in which the formula is interpreted: the equivalences hold in every commutative ring with a compatible linear order, with the ring symbols and ≤ interpreted as usual. The first statement needs the order to be compatible with addition, since t₁ ≤ t₂ becomes the condition that t₁ - t₂ is not positive. The second needs no such compatibility, since a sign condition on p compares p with 0.

These are the formula-level translation laws between formulas of ordered rings and polynomial sign conditions. Over a fixed ring they identify semialgebraic sets with quantifier-free definable sets, as in TauCeti.Geometry.RealAlgebraic.Semialgebraic.Formula.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Section 2.3, for quantifier-free formulas and sign conditions.

noncomputable def FirstOrder.Language.Term.signFormula {α : Type u_1} {n : ℕ} (t : (ring.sum Language.order).Term (α ⊕ Fin n)) : SignType → (ring.sum Language.order).BoundedFormula α n

The quantifier-free formula saying that the value of the term t has sign s.

theorem FirstOrder.Language.Term.isQF_signFormula {α : Type u_1} {n : ℕ} (t : (ring.sum Language.order).Term (α ⊕ Fin n)) (s : SignType) : (t.signFormula s).IsQF

The formula t.signFormula s is quantifier-free.

@[simp]

theorem FirstOrder.Language.Term.realize_signFormula {α : Type u_1} {n : ℕ} {R : Type u_2} [CommRing R] [Ring.CompatibleRing R] [Language.order.Structure R] [LinearOrder R] [(ring.sum Language.order).OrderedStructure R] (t : (ring.sum Language.order).Term (α ⊕ Fin n)) (s : SignType) (v : α → R) (xs : Fin n → R) : (t.signFormula s).Realize v xs ↔ SignType.sign (realize (Sum.elim v xs) t) = s

The formula t.signFormula s holds exactly when the value of t has sign s.

theorem FirstOrder.Language.BoundedFormula.IsQF.exists_realize_iff_sign {α : Type u_1} {n : ℕ} {φ : (ring.sum Language.order).BoundedFormula α n} (hφ : φ.IsQF) : ∃ (m : ℕ) (p : Fin m → MvPolynomial (α ⊕ Fin n) ℤ) (Φ : (Fin m → SignType) → Prop), ∀ (R : Type u) [inst : CommRing R] [inst_1 : Ring.CompatibleRing R] [inst_2 : Language.order.Structure R] [inst_3 : LinearOrder R] [IsOrderedAddMonoid R] [(ring.sum Language.order).OrderedStructure R] (v : α → R) (xs : Fin n → R), φ.Realize v xs ↔ Φ fun (i : Fin m) => SignType.sign ((MvPolynomial.aeval (Sum.elim v xs)) (p i))

A quantifier-free formula is a sign condition. For a quantifier-free formula φ of ordered rings there are finitely many integer polynomials p i in the free and bound variables of φ, and a condition Φ on their signs, such that in every commutative ring with a compatible linear order φ holds exactly when Φ holds of the signs of the values of the p i.

theorem FirstOrder.Language.BoundedFormula.exists_isQF_realize_iff_sign {α : Type u_1} {n : ℕ} {ι : Type u_2} [Finite ι] (p : ι → MvPolynomial (α ⊕ Fin n) ℤ) (Φ : (ι → SignType) → Prop) : ∃ (φ : (ring.sum Language.order).BoundedFormula α n), φ.IsQF ∧ ∀ (R : Type u) [inst : CommRing R] [inst_1 : Ring.CompatibleRing R] [inst_2 : Language.order.Structure R] [inst_3 : LinearOrder R] [(ring.sum Language.order).OrderedStructure R] (v : α → R) (xs : Fin n → R), φ.Realize v xs ↔ Φ fun (i : ι) => SignType.sign ((MvPolynomial.aeval (Sum.elim v xs)) (p i))

A sign condition is a quantifier-free formula. For finitely many integer polynomials p i and a condition Φ on their signs there is a quantifier-free formula of ordered rings which, in every commutative ring with a compatible linear order, holds exactly when Φ holds of the signs of the values of the p i.