User grant olney passmore - MathOverflow

Answer by Grant Olney Passmore for How to show an ideal is Zero-dimensional

2013-05-04T11:29:02Z

Your question is better suited for math.stackexchange.com and will probably be closed here quickly (don't get discouraged by this -- MathOverflow is exclusively for research level mathematics, while math.stackexchange.com is a great resource for questions of any level).

But, in the mean time: Do you know how to form a Groebner basis? This is an easy way to prove that a finitely presented ideal is zero-dimensional (and is easy to do by hand in this example with a lexicographic monomial ordering $\prec$ s.t. $z \prec y \prec x$).

Think about what it means for $J$ to be zero-dimensional: $J$ is zero-dimensional iff $V_{\mathbb{C}}(J)$ contains only finitely many points. For this to happen, a (monic) Groebner basis for $J$ must contain polynomials $p_1, p_2, p_3$ s.t. $LM(p_1)$ = $x^{k_1}$, $LM(p_2)$ = $y^{k_2}$, and $LM(p_3)$ = $z^{k_3}$, where $LM(p_i)$ is the leading monomial of $p_i$, and $k_i \in \mathbb{N}^{+}$.

In general, to decide whether or not an ideal $I \subset \mathbb{Q}[x_1, \ldots, x_n]$ is zero-dimensional, it suffices to compute a (monic) Groebner basis for $I$ and verify that it contains, for each indeterminate $x_i$, a polynomial $p_i$ s.t. $LM(p_i) = x_i^{k_i}$ for some $k_i \in \mathbb{N}^{+}$.

Answer by Grant Olney Passmore for Practical applications of algebraic number theory?

2010-05-17T16:02:34Z

Algorithms for computing with real algebraic numbers (in particular, (i) computing the sign of an algebraic real A presented, for instance, as a pair of a minimal polynomial P $\in \mathbb{Z}[x]$ for A and an interval with rational endpoints containing A and no other real roots of P, and (ii) computing the sign of a polynomial evaluated at algebraic real numbers presented in form (i)) are critical components of some modern quantifier elimination based decision procedures for real algebra such as cylindrical algebraic decomposition. These procedures are used in a number of areas: formal verification of hardware, software and bioware (including control systems and other `hybrid' systems with both discrete and continuous dynamics), robot motion planning, correctly displaying algebraic curves on computers, testing the stability of initial and initial-boundary value problems, and formalised mathematics.

[Some references on cylindrical algebraic decomposition (CAD)]

Caviness, B. F. and Johnson, J. R. (Eds.). Quantifier Elimination and Cylindrical Algebraic Decomposition. New York: Springer-Verlag, 1998. (The `CAD bible' - Collins's festschrift.)

Collins, G. E. "Quantifier Elimination for the Elementary Theory of Real Closed Fields by Cylindrical Algebraic Decomposition." Lect. Notes Comput. Sci. 33, 134-183, 1975.

Collins, G. E. "Quantifier Elimination by Cylindrical Algebraic Decomposition--Twenty Years of Progress." In Quantifier Elimination and Cylindrical Algebraic Decomposition (Ed. B. F. Caviness and J. R. Johnson). New York: Springer-Verlag, pp. 8-23, 1998.

[Some references on applications of CAD: there are many, I only post a few]

(robot motion planning)

S. Lindemann and S. LaValle. "Computing Smooth Feedback Plans Over Cylindrical Algebraic Decompositions." In Proceedings of Robotics: Science and Systems, 2006.

(formal verification of systems)

M. Adlaide and O. Roux. "Using Cylindrical Algebraic Decomposition for the Analysis of Slope Parametric Hybrid Automata." In Proceedings of the 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, 2000.

(formalised mathematics)

A. Mahboubi, "Programming and certifying the CAD algorithm inside the Coq system." In Mathematics: Algorithms, Proofs. Volume 05021 of Dagstuhl Seminar Proceedings, Schloss Dagstuhl, 2005.

(display of algebraic curves)

D.S. Arnon. "Topologically reliable display of algebraic curves." SIGGRAPH Comput. Graph. 17, 3 (Jul. 1983), 219-227.

Also, many open problems in metric geometry actually fall within the theory of real closed fields (RCF), and thus can in principle be decided by the CAD algorithm. The issue is one of complexity. Due to Davenport-Heintz, it is known that real quantifier elimination is inherently doubly exponential in the dimension (number of variables) of the input formula. Thus, for the case of RCF, decidable in principle does not mean decidable in practice. Nevertheless, it is a fascinating state of affairs. Complexity aside, here are some examples:

All kissing problems for n-dimensional hyperspheres are in principle decidable by CAD and other real algebra decision methods.

Due to L. Fejes Toth, Kepler's conjecture is known to be equivalent to a single RCF sentence, and thus could be decided by CAD as well. In the formalisation of his proof of the Kepler conjecture, Thomas Hales has isolated a large collection of RCF sentences which appear as lemmata in his proof and which he believes should be amenable to specialised RCF decision methods. See T. Hales's ``A Collection of Problems in Elementary Geometry'' ( flyspeck.googlecode.com/files/collection_geom.pdf ).

Answer by Grant Olney Passmore for German mathematical terms like "Nullstellensatz"

2011-04-19T11:03:30Z

Gentzen's Hauptsatz (cut elimination theorem) : This is a fundamental result in structural proof theory, and is at the heart of Gentzen's consistency proof of elementary number theory. It is very funny that the word literally means "main theorem," with no reference to the subject domain, yet it is standard in logic in English to use just the word "Hauptsatz" to refer to this (family of) theorem(s) in proof theory.

Answer by Grant Olney Passmore for Nonstandard monomial orders?

2011-04-06T20:06:11Z

Yes. An important concept involving non-standard monomial orderings is that of a universal Gr\"obner basis:

Let $k$ be a field and $I \subset k[x_1, ..., x_n]$ an ideal. Then, a finite subset $U \subset I$ is called a universal Groebner basis if $U$ is a Groebner basis of $I$ w.r.t. all monomial orders over $x_1, ..., x_n$.

Every such ideal $I$ has a universal Groebner basis: $I$ has only finitely many reduced Groebner bases, and the union of these is a universal Groebner basis for $I$.

There is a global "combinatorial space" for studying the transformation of Groebner bases of I under changes of the underlying monomial order: the state polytope of I, or the Groebner Fan of I. This gives rise to deep connections between the theory of convex polytopes and Groebner basis theory. These objects become very useful in algebraic geometry (in particular, in tropical geometry and in the theory of toric ideals and toric varieties).

Sturmfels's "Groebner Bases and Convex Polytopes" is a great resource for this and covers applications to toric varieties, regular triangulations, and many other problems. See also, for instance, "Groebner bases and triangulations of the second hypersimplex" by De Loera, Sturmfels, and Thomas, Combinatorica, 15, 409-424 (1995).

There is a very nice recent piece of software called GFan by Jensen for computing Groebner fans (from which universal Groebner bases may be extracted). [ http://www.math.tu-berlin.de/~jensen/software/gfan/gfan.html ]

Also, in decision methods for the theory of real closed fields, non-standard monomial orderings are used in some proof construction methods. For instance, a method due to Tiwari for computing Positivstellensatz witnesses certifying the emptiness of a semialgebraic set defined by a purely conjunctive Tarski formula involves constructing non-standard monomial orders. These non-standard orders are constructed, one after the other, so that in each successive one, a Positivstellensatz witness is made "lower" in the active monomial order and will eventually be forced to appear in a Groebner basis. See [ http://www.csl.sri.com/users/tiwari/html/csl05b.html ].

Answer by Grant Olney Passmore for Elementary+Short+Useful

2011-04-03T19:11:47Z

Compactness of First Order Logic (using ultraproducts, not as a corollary of completeness; they get Łoś's Theorem for ultraproducts as a freebie.)

Answer by Grant Olney Passmore for What are the most fundamental classes of mathematical algorithms?

2010-06-09T12:51:06Z

An important class of algorithms which both make use of many fundamental algorithms already appearing in your list and contain significant ideas not reflected yet in your list are algorithms for computation with semialgebraic sets (i.e., algorithms in real algebraic geometry). These algorithms have a very different* flavour than their `counterparts' over algebraically closed fields such as Buchberger's algorithm and related techniques used for Groebner basis computation, Wu's method and other techniques in elimination theory, etc.

Quantifier elimination (effective semialgebraic projection) has always been a central concern in algorithmic real algebraic geometry, so there is perhaps some feeling that these algorithms should be placed under your bullet point (9). But, the wealth of techniques developed in the context of real quantifier elimination are independently interesting and useful outside of the goal of automated proof.

Important algorithms include those which compute:

Cylindrical Algebraic Decompositions (Collins et al),
Signed subresultants (Collins et al),
Betti numbers and Euler-Poincar\'e Characteristic (Basu, Basu-Pollack-Roy),
Connected component sampling (Basu-Pollack-Roy),
Roadmaps and Connectedness (Canny, Grigor'ev-Vorobjov, Heintz-Roy-Solerno, Gournay-Risler),
Positivstellensatz witnesses via Semidefinite programming (Parrilo, Choi, Harrison, Lam, Powers, Woermann et al) [perhaps this is partially covered by your bullet point (4)].

In a certain sense, the properties Collins exploited in defining cylindrical algebraic decompositions have been generalised to what are now called `o-minimal structures,' which has led to a rich and very active research area at the intersection of model theory and semialgebraic and subanalytic geometry (see L. van den Dries' ``Tame Topology and O-minimal Structures'').

(* Though it should be mentioned that fundamental algorithms in real algebraic geometry often make use of fundamental algorithms in classical algebraic geometry. )

Answer by Grant Olney Passmore for Reasons for success in automated theorem proving

2010-06-07T12:04:29Z

You may be interested in the wonderful little book ``The Efficiency of Theorem Proving Strategies: A Comparative and Asymptotic Analysis'' by David A. Plaisted and Yunshan Zhu. I have the 2nd edition which is paperback and was quite cheap. I'll paste the (accurate) blurb:

``This book is unique in that it gives asymptotic bounds on the sizes of the search spaces generated by many common theorem-proving strategies. Thus it permits one to gain a theoretical understanding of the efficiencies of many different theorem-proving methods. This is a fundamental new tool in the comparative study of theorem proving strategies.''

Now, from a critical perspective: There is no doubt that sophisticated asymptotic analyses such as these are very important (and to me, the ideas underlying them are beautiful and profound). But, from the perspective of the practitioner actually using automated theorem provers, these analyses are often too coarse to be of practical use. A related phenomenon occurs with decision procedures for real closed fields. Since Davenport-Heinz, it's been known that general quantifier elimination over real closed fields is inherently doubly-exponential w.r.t. the number of variables in an input Tarski formula. One full RCF quantifier-elimination method having this doubly-exponential complexity is CAD of Collins. But, many (Renegar, Grigor'ev/Vorobjov, Canny, ...) have given singly exponential procedures for the purely existential fragment. Hoon Hong has performed an interesting analysis of this situation. The asymptotic complexities of three decision procedures considered by Hong in ``Comparison of Several Decision Algorithms for the Existential Theory of the Reals'' are as follows:

(Let $n$ be the number of variables, $m$ the number of polynomials, $d$ their total degree, and $L$ the bit-width of the coefficients)

CAD: $L^3(md)^{2^{O(n)}}$

Grigor'ev/Vorobjov: $L(md)^{n^2}$

Renegar: $L(log L)(log log L)(md)^{O(n)}$

Thus, for purely existential formulae, one would expect the G/V and R algorithms to vastly out-perform CAD. But, in practice, this is not so. In the paper cited, Hong presents reasons why, with the main point being that the asymptotic analyses ignore huge lurking constant factors which make the singly-exponential algorithms non-applicable in practice. In the examples he gives ($n=m=d=L=2$), CAD would decide an input sentence in a fraction of a second, whereas the singly-exponential procedures would take more than a million years. The moral seems to be a reminder of the fact that a complexity-theoretic speed-up w.r.t. sufficiently large input problems should not be confused with a speed-up w.r.t. practical input problems.

In any case, I think the situation with asymptotic analyses in automated theorem proving is similar. Such analyses are important theoretical advances, but often are too coarse to influence the day-to-day practitioner who is using automated theorem proving tools in practice.

(* One should mention Galen Huntington's beautiful 2008 PhD thesis at Berkeley under Branden Fitelson in which he shows that Canny's singly-exponential procedure can be made to work on the small examples considered by Hong in the above paper. This is significant progress. It still does not compare in practice to the doubly-exponential CAD, though.)

Ultrafilters arising from Keisler-Shelah ultrapower characterisation of elementary equivalence

2010-05-13T13:43:41Z

In model theory, two structures $\mathfrak{A}, \mathfrak{B}$ of identical signature $\Sigma$ are said to be elementarily equivalent ($\mathfrak{A} \equiv \mathfrak{B}$) if they satisfy exactly the same first-order sentences w.r.t. $\Sigma$. An astounding theorem giving an algebraic characterisation of this notion is the so-called Keisler-Shelah isomorphism theorem, proved originally by Keisler (assuming GCH) and then by Shelah (avoiding GCH), which we state in its modern strengthening (saying that only a single ultrafilter is needed):

$\mathfrak{A} \equiv \mathfrak{B} \ \iff \ \exists \mathcal{U} \text{ s.t. } (\Pi_{i\in\mathcal{I}} \ \mathfrak{A})/\mathcal{U} \cong (\Pi_{i\in\mathcal{I}} \ \mathfrak{B})/\mathcal{U},$

where $\mathcal{U}$ is a non-principal ultrafilter on, say, $\mathcal{I} = \mathbb{N}$. That is, two structures are elementarily equivalent iff they have isomorphic ultrapowers.

My question is the following (admittedly rather vague): Does anyone know of constructions in which an ultrafilter is chosen by an appeal to this characterisation and then used for other means? An example of what I have in mind would be something like this (using the fact that any two real closed fields are elementarily equivalent w.r.t. the language of ordered rings): In order to perform some construction $C$ I ``choose'' a non-principal ultrafilter $\mathcal{U}$ on $\mathbb{N}$ by specifying it as a witness to the following isomorphism induced by Keisler-Shelah:

$\mathbb{R}^\mathbb{N}/\mathcal{U} \cong \mathbb{R}_{alg}^\mathbb{N}/\mathcal{U},$

where $\mathbb{R}_{alg}$ is the field of real algebraic numbers. So the construction $C$ should be dependent upon the fact that $\mathcal{U}$ is a non-principal ultrafilter bearing witness to the Keisler-Shelah isomorphism between some ultrapower of the reals and the algebraic reals, resp.

Also, a follow-up question: Let's say I'd like to ``solve'' the above isomorphism for $\mathcal{U}$. Are there interesting things in general known about the solution space, e.g., the set of all non-principal ultrafilters bearing witness to the Keisler-Shelah isomorphism for two fixed elementarily equivalent structures such as $\mathbb{R}$ and $\mathbb{R}_{alg}$? What machinery is useful in investigating this?

Answer by Grant Olney Passmore for Examples of inequality implied by equality.

2010-04-26T14:57:23Z

Over real-closed fields such as $\langle \mathbb{R}, +, *, -, <, 0, 1 \rangle$, there is an interesting simple answer: every polynomial inequality is equivalent to a projected equation. E.g., Given $p_1, p_2 \in \mathbb{Q}[\vec{x}]$ we have $\left( p_1 > p_2 \ \iff \ \exists z \text{ s.t. } z^2(p_1 - p_2) - 1 = 0 \right),$ and $\left( p_1 \geq p_2 \ \iff \ \exists z \text{ s.t. } p_1 - p_2 - z^2 = 0 \right).$

Geometrically, this is the simple observation that every semialgebraic set defined as the set of $n-$dimensional real vectors satisfying an inequality is the projection of an $n+1$-dimensional real-algebraic variety defined by a single equation. Semialgebraic sets defined by boolean combinations of equations and inequalities can be similarly encoded as the set of satisfying real vectors of (an) equation(s) by using the Rabinowitsch encoding $(p_1 = 0 \vee p_2 = 0 \ \iff p_1p_2 = 0)$ and $(p_1 = 0 \wedge p_2 = 0 \ \iff p_1^2 + p_2^2 = 0).$

Combining the above two observations, one obtains the fact that every semi-algebraic set $S \subseteq \mathbb{R}^n$ is the projection of a real algebraic variety $V \subseteq \mathbb{R}^{n+k}$, where $k$ is the number of inequality symbols appearing in the defining Tarski formula for $S$. In fact, due to a construction of Motzkin [``The Real Solution Set of a System of Algebraic Inequalities is the Projection of a Hypersurface in One More Dimension,'' Inequalities II, O. Shisha, ed., 251-254, Academic Press (1970)], it is known that every such $S$ is in fact the projection of a real-algebraic variety in $\mathbb{R}^{n+1}$.

Answer by Grant Olney Passmore for Has decidability got something to do with primes?

2010-03-30T20:06:55Z

In response to your statement: "It appears that the condition that primes are definable in the theory will implies incompleteness."

The primes being definable in an arithmetic theory does not necessarily lead to incompleteness. The theory of Skolem arithmetic ($Th(\langle\mathbb{N},*\rangle)$) is decidable and admits quantifier elimination (it is the elementary true theory of the weak-direct power of the standard model of Presburger arithmetic, so Feferman-Vaught quantifier-elimination lifting applies). A predicate for primality can easily be expressed in the language of this theory. This is due to Skolem and Mostowski initially, and to Feferman-Vaught when obtained in terms of weak-direct powers.

Moreover, Skolem arithmetic extended with the usual order restricted to primes is decidable, admits quantifier elimination, and in fact $Th(\langle\mathbb{N},*,<_p\rangle)$ and $Th(\langle\omega^\omega,+\rangle)$ are reducible to each other in linear time. This is due to Francoise Maurin (see "The Theory of Integer Multiplication with Order Restricted to Primes in Decidable" - J. Symbolic Logic, Volume 62, Issue 1 (1997), 123-130).

Note that in this latter case, the ordering cannot be the full ordering on the natural numbers, as this would allow one to define a successor predicate, and Julia Robinson showed successor and multiplication are sufficient for defining addition.

Answer by Grant Olney Passmore for What is the definition of "canonical" ?

2010-03-28T22:03:30Z

Not a definition, but an example of use in logic:

In model theory, "canonical" is often used in the phrase "the canonical model" to mean "intended structure." For instance, in first-order logic, one may speak of "the canonical model of Peano Arithmetic" to mean the structure of the natural numbers, or "the canonical model of the theory of real-closed fields" to mean the field of real numbers. Intuitively, "the canonical model" of a theory is the structure one was trying to pin down when the axiomatisation of the theory was written. It's just that in first-order logic, it is hard to pin down (infinite) structures! No first-order theories admitting infinite models are categorical (they admit non-isomorphic models; indeed, they admit models of every infinite cardinality), and compactness/ultraproduct/(many other) constructions can often be used to build "non-standard" models of theories. "Non-standard" models of Peano Arithmetic or the theory of real-closed fields would in this context be called "non-canonical" (even though there are many canonically studied "non-standard" models of those theories!).

But, many commonly studied theories do not have a notion of "canonical model." For instance, one would not say "the canonical model of group theory."

Comment by Grant Olney Passmore

2013-01-15T15:25:21Z

Also, Wikipedia has a nice short summary: en.wikipedia.org/wiki/…

Comment by Grant Olney Passmore

2013-01-15T15:23:45Z

Todd: Shoenfield Absoluteness. See, e.g., this MO question which contains a short summary of the result: mathoverflow.net/questions/71965/…

Comment by Grant Olney Passmore

2012-12-08T21:23:56Z

"Suppose G is a simple group of odd order. ... They were seeking, of course, to demonstrate a contradiction." But, there is no contradiction here, unless G is also specified to not be cyclic of prime order, right?

Comment by Grant Olney Passmore

2011-04-06T20:14:41Z

Ah, I see that this may not be what you are after, as you wanted "explicit" non-standard monomial orders. Sorry. I hope it is at least helpful in some way!

Comment by Grant Olney Passmore

2011-04-05T18:12:05Z

@Pete: You make a great point - One has to be very careful. But, with careful planning, I do think the ``big idea'' of compactness and an impactful impression of the power it gives one in constructing models of first-order theories can be communicated in 30 minutes. I believe this general setting of considering an arbitrary first-order theory and its models can be quite a revelation to undergraduates, as long as they have experience with reasoning about specific theories and models in the past, say after one or two abstract algebra courses. If nothing else,it leaves an inspiring impression.

Comment by Grant Olney Passmore

2010-10-06T20:11:50Z

a very nice question!

Comment by Grant Olney Passmore

2010-10-05T23:38:05Z

Shankar's proof of Goedel's First Incompleteness Theorem which he formalised within the Boyer-Moore theorem prover, (Nq)thm, is essentially a proof in PRA. Once one eliminates some conveniences (having direct access to ordered pairs instead of coding them as natural numbers, etc.), one sees that the Boyer-Moore logic used in that work is essentially PRA+TI(epsilon-0). But, Shankar does not use TI(epsilon-0) in his proof. So, his proof is formalised essentially in PRA. See Shankar's CUP book "Metamathematics, Machines and Goedel's Proof" for the gory details.

Comment by Grant Olney Passmore

2010-10-05T15:41:57Z

@Kevin: By design, one need worry only if changes were made to the (small, stable) type-checking kernel. The other machinery (which may be incompatible in various versions) can be seen as an evolving set of tools for making the construction of kernel-checkable proofs easier.

Comment by Grant Olney Passmore

2010-10-05T15:36:32Z

An example Coq changelog: lix.polytechnique.fr/coq/distrib/V8.3-beta0/…

Comment by Grant Olney Passmore

2010-10-05T14:43:06Z

@André: +1. This is very interesting to hear! I will ask Georges about this. If true, fixing this (or as much as is feasible in the available time-frame) might make for a nice MSc project.

Comment by Grant Olney Passmore

2010-06-09T14:37:13Z

Though I agree it'd be nice for IPMs to have a separate bullet, in his defense, bullet point 4 does say `and other algorithms using convexity properties.'

Comment by Grant Olney Passmore

2010-06-09T14:05:17Z

Thankfully, yes! The monumental tome `Algorithms in Real Algebraic Geometry' by Basu-Pollack-Roy is invaluable. A review is here ( math.tamu.edu/~rojas/bpr.pdf ) and with the 2nd edition, they've made it freely available online ( perso.univ-rennes1.fr/marie-francoise.roy/… ). I refer to it daily!

Comment by Grant Olney Passmore

2010-06-09T13:45:50Z

Fixed (should have been Vorobjov, and updated Poincar\'e with correct accent). Thank you!

Comment by Grant Olney Passmore

2010-06-08T21:57:06Z

You're welcome. I hope it helps!

Comment by Grant Olney Passmore

2010-05-28T00:03:40Z

A beautiful reply, thank you for this!