2865:. Using those axioms, one can show that the points on a line form a real closed field R, and one can introduce coordinates so that the Euclidean plane is identified with R . Employing the decidability of the theory of real closed fields, Tarski then proved that the elementary theory of Euclidean geometry is complete and decidable.
1326:-tuple of the components corresponding to the subset of variables. The projection theorem asserts that a projection of a semialgebraic set is a semialgebraic set, and that there is an algorithm that, given a quantifier-free formula defining a semialgebraic set, produces a quantifier-free formula for its projection.
1411:
The decidability of a first-order theory of the real numbers depends dramatically on the primitive operations and functions that are considered (here addition and multiplication). Adding other functions symbols, for example, the
784:
3208:"On the computational complexity and geometry of the first-order theory of the reals. Part I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals"
2386:
2090:
These three cardinal numbers tell us much about the order properties of any real closed field, though it may be difficult to discover what they are, especially if we are not willing to invoke the
1552:
1439:'s results about the incompleteness and undecidability of the first-order theory of the natural numbers (using addition and multiplication). There is no contradiction, since the statement "
913:
520:
1472:
1238:
1195:
1164:
1129:
1092:
991:
956:
1425:
854:
819:
720:
1958:
is real closed and non-Archimedean. These fields contain infinitely large (larger than any integer) and infinitesimal (positive but smaller than any positive rational) elements.
1768:
2674:
a hyperreal field, and hence a suitable field for the usages of nonstandard analysis. It can be seen to be the higher-dimensional analogue of the real numbers; with cardinality
1722:
1395:
2309:
2276:
2207:
268:
2486:
2447:
2534:
2412:
1613:
876:
2834:
2807:
2780:
2753:
2726:
2699:
2664:
2633:
2588:
2046:
1822:, and therefore in double exponential time, but their argument (in the case of more than one variable) is generally held as flawed; see Renegar (1992) for a discussion.
1797:
1256:. Since the truth of quantifier-free formulas without free variables can be easily checked, this yields the desired decision procedure. These results were obtained
1947:. Note that this statement is not expressible in the first-order language of ordered fields, since it is not possible to quantify over integers in that language.
1049:
1029:
2422:, and its uniqueness is equivalent to the continuum hypothesis. (Even without the continuum hypothesis we have that if the cardinality of the continuum is
728:
1431:
Furthermore, the completeness and decidability of the first-order theory of the real numbers (using addition and multiplication) contrasts sharply with
1329:
In fact, the projection theorem is equivalent to quantifier elimination, as the projection of a semialgebraic set defined by the formula
1562:
295:
is formally real. (In other words, the field is maximal in an algebraic closure with respect to the property of being formally real.)
962:(as well as equality, if this is not considered a logical symbol). In this language, the (first-order) theory of real closed fields,
3188:
3169:
3132:
3042:
3014:
2917:
3344:
2350:
2017:
of the smallest cofinal set, which is to say, the size of the smallest cardinality giving an unbounded sequence. For example,
3265:
1267:
1252:
means that the two formulas are true for exactly the same values of the variables. Tarski's proof uses a generalization of
3124:
1951:
1502:
92:
3339:
2329:
3334:
3180:
881:
488:
321:
303:
958:
includes symbols for the operations of addition and multiplication, the constants 0 and 1, and the order relation
31:
1446:
1212:
1169:
1138:
1103:
1066:
965:
930:
1914:(1996) provided a well-behaved algorithm to decide the truth of such an existential formula with complexity of
1803:. This shows that both the time complexity and the space complexity of quantifier elimination are intrinsically
1672:
quantifiers, and involving polynomials of constant degree, such that any quantifier-free formula equivalent to
1493:
824:
789:
690:
3246:
1804:
1421:
88:
3002:
1911:
1486:
1315:
1206:
137:
1727:
3051:
3018:
2541:
1684:
1645:
1490:
1350:
3317:
2287:
2254:
2185:
236:
2464:
2425:
2419:
2325:
2091:
1417:
1198:
213:
134:
2537:
2502:
2139:
1241:
278:
163:
46:
2395:
1575:
859:
3285:
3077:
3073:
2998:
2862:
2812:
2785:
2758:
2731:
2704:
2677:
2642:
2611:
2566:
2496:
2024:
1800:
1060:
723:
535:
149:
2858:
1773:
1253:
675:
is a field (no ordering compatible with the field operations is assumed, nor is it assumed that
3184:
3165:
3128:
3038:
3010:
2324:
The characteristics of real closed fields become much simpler if we are willing to assume the
1936:
1566:
1291:
1056:
454:
450:
394:
366:
341:
335:
217:
91:
to the real numbers. In other words, it has the same first-order properties as the reals: any
53:
17:
3277:
3219:
3194:
3138:
3103:
3093:
3047:
2977:
2936:
2415:
2312:
1955:
1094:
is just the set of all first-order sentences that are true about the field of real numbers.
684:
554:
379:
372:
347:
221:
65:
61:
3297:
3157:
2991:
3293:
3237:
3198:
3142:
3107:
3026:
2987:
2547:
2242:
2238:
2131:
1132:
924:
578:
482:
231:
562:
3062:
2164:
2018:
1944:
1638:
1408:
represent respectively the set of eliminated variables, and the set of kept variables.
1034:
1014:
386:
359:
99:
3224:
3207:
3098:
3081:
2982:
2051:
We have therefore the following invariants defining the nature of a real closed field
3328:
3253:
2544:
1432:
1245:
1097:
1002:
531:
114:
2941:
1818:(1986) claimed to have proved that the theory of real closed fields is decidable in
2600:
however is not a complete field; if we take its completion, we end up with a field
2344:
1811:
1248:, produces an equivalent quantifier-free formula in the same free variables, where
779:{\displaystyle \mathbb {R} _{\mathrm {alg} }\!\times \mathbb {R} _{\mathrm {alg} }}
390:
27:
Non algebraically closed field whose extension by sqrt(â1) is algebraically closed
1205:
to determine the truth or falsity of any such sentence. This was done by showing
1166:-sentence can be proven either true or false from the above axioms. Furthermore,
3233:
2850:
property (which merely means between any two real numbers we can find another).
2014:
1939:, meaning it has the Archimedean property that for any real number, there is an
1436:
442:
353:
141:
122:
106:
57:
38:
1626:
is the product of the degrees of the polynomials occurring in the formula, and
433:
is a real closed field whose ordering is an extension of the given ordering on
30:"ArtinâSchreier theorem" redirects here. For the branch of Galois theory, see
3030:, Journal of Computer and Systems Sciences 32 (1986), no. 2, pp. 251â264.
1962:
527:
130:
1443:
is an integer" cannot be formulated as a first-order formula in the language
2960:
Alling, Norman L. (1962), "On the existence of real-closed fields that are η
1815:
1290:, the set of the points that satisfy the formula. Such a subset is called a
1202:
3310:
2495:, we can do so much more constructively as the subfield of series with a
1819:
3239:
Combined
Decision Procedures for Nonlinear Arithmetics, Real and Complex
3289:
2554:
2450:
2154:
2021:
are cofinal in the reals, and the cofinality of the reals is therefore
1940:
683:
still has a real closure, which may not be a field anymore, but just a
523:
3123:. Mathematical Surveys and Monographs. Vol. 124. Providence, RI:
1924:
3281:
1935:
A crucially important property of the real numbers is that it is an
291:
is a formally real field such that no proper algebraic extension of
1825:
For purely existential formulas, that is for formulas of the form
1648:
is nearly optimal for quantifier elimination by producing a family
993:, consists of all sentences that follow from the following axioms:
3179:. London Mathematical Society Lecture Note Series. Vol. 171.
2861:
are an axiom system for the first-order ("elementary") portion of
998:
438:
2328:. If the continuum hypothesis holds, all real closed fields with
2094:. There are also particular properties that may or may not hold:
1008:
the axiom asserting that every positive number has a square root;
60:. Some examples are the field of real numbers, the field of real
1413:
3035:
Quantifier elimination and cylindrical algebraic decomposition
2392:
is a maximal ideal not leading to a field order-isomorphic to
166:
such that every polynomial of odd degree with coefficients in
2608:
has the cardinality of the continuum, which by hypothesis is
80:
in which any of the following equivalent conditions is true:
3153:, Trans. of the American Math. Soc., Vol. 352, No. 12, 1998.
1569:, provides a much more practicable algorithm of complexity
1453:
1219:
1176:
1145:
1110:
1073:
972:
937:
302:
making it an ordered field such that, in this ordering, the
481:). For example, the real closure of the ordered field of
2381:{\displaystyle \mathbb {R} ^{\mathbb {N} }/\mathbf {M} }
1426:
Decidability of first-order theories of the real numbers
117:
such that, in this ordering, every positive element of
1961:
3258:
A Decision Method for
Elementary Algebra and Geometry
2920:
A decision method for elementary algebra and geometry
2815:
2788:
2761:
2734:
2707:
2680:
2645:
2614:
2569:
2505:
2467:
2428:
2398:
2353:
2290:
2257:
2188:
2027:
1776:
1730:
1687:
1578:
1505:
1449:
1353:
1215:
1172:
1141:
1106:
1069:
1037:
1031:, the axiom asserting that all polynomials of degree
1017:
968:
933:
884:
862:
827:
792:
731:
693:
491:
239:
3312:
Real
Algebraic and Analytic Geometry Preprint Server
2670:
as a dense subfield. It is not an ultrapower but it
1547:{\displaystyle 2^{2^{\cdot ^{\cdot ^{\cdot ^{n}}}}}}
3082:"Real quantifier elimination is doubly exponential"
1622:is the total number of variables (free and bound),
1063:ranges only over elements of the field). Note that
786:(the two copies correspond to the two orderings of
3151:Weakly o-minimal structures and real closed fields
3033:Caviness, B F, and Jeremy R. Johnson, eds. (1998)
3005:(2003) "Algorithms in real algebraic geometry" in
2828:
2801:
2774:
2747:
2720:
2693:
2658:
2627:
2582:
2528:
2491:Moreover, we do not need ultrapowers to construct
2480:
2441:
2406:
2380:
2303:
2270:
2201:
2040:
1791:
1762:
1716:
1607:
1546:
1466:
1389:
1232:
1189:
1158:
1123:
1086:
1043:
1023:
985:
950:
907:
870:
848:
813:
778:
714:
514:
277:that does not extend to an ordering on any proper
262:
3027:The complexity of elementary algebra and geometry
2339:property are order isomorphic. This unique field
2082:, which is the minimum size of a dense subset of
1557:can bound the execution time of the algorithm if
752:
95:in the first-order language of fields is true in
3266:"An isomorphism theorem for real-closed fields"
3162:Handbook of Discrete and Computational Geometry
3264:Erdös, P.; Gillman, L.; Henriksen, M. (1955),
3149:Macpherson, D., Marker, D. and Steinhorn, C.,
3024:Michael Ben-Or, Dexter Kozen, and John Reif,
1644:Davenport and Heintz (1988) proved that this
908:{\displaystyle \mathbb {R} _{\mathrm {alg} }}
687:. For example, the real closure of the field
515:{\displaystyle \mathbb {R} _{\mathrm {alg} }}
8:
565:there is a maximal ordered field extension (
453:between real closed fields automatically is
1467:{\displaystyle {\mathcal {L}}_{\text{rcf}}}
1233:{\displaystyle {\mathcal {L}}_{\text{rcf}}}
1190:{\displaystyle {\mathcal {T}}_{\text{rcf}}}
1159:{\displaystyle {\mathcal {L}}_{\text{rcf}}}
1124:{\displaystyle {\mathcal {T}}_{\text{rcf}}}
1087:{\displaystyle {\mathcal {T}}_{\text{rcf}}}
986:{\displaystyle {\mathcal {T}}_{\text{rcf}}}
951:{\displaystyle {\mathcal {L}}_{\text{rcf}}}
3223:
3097:
3007:Algorithms and computation in mathematics
2981:
2940:
2820:
2814:
2793:
2787:
2766:
2760:
2739:
2733:
2712:
2706:
2685:
2679:
2650:
2644:
2619:
2613:
2574:
2568:
2507:
2506:
2504:
2472:
2466:
2433:
2427:
2400:
2399:
2397:
2373:
2368:
2362:
2361:
2360:
2356:
2355:
2352:
2295:
2289:
2262:
2256:
2193:
2187:
2032:
2026:
1775:
1740:
1735:
1729:
1697:
1692:
1686:
1588:
1583:
1577:
1530:
1525:
1520:
1515:
1510:
1504:
1458:
1452:
1451:
1448:
1352:
1224:
1218:
1217:
1214:
1181:
1175:
1174:
1171:
1150:
1144:
1143:
1140:
1115:
1109:
1108:
1105:
1078:
1072:
1071:
1068:
1036:
1016:
977:
971:
970:
967:
942:
936:
935:
932:
892:
891:
887:
886:
883:
864:
863:
861:
856:is considered as an ordered subfield of
849:{\displaystyle \mathbb {Q} ({\sqrt {2}})}
836:
829:
828:
826:
814:{\displaystyle \mathbb {Q} ({\sqrt {2}})}
801:
794:
793:
791:
763:
762:
758:
757:
739:
738:
734:
733:
730:
715:{\displaystyle \mathbb {Q} ({\sqrt {2}})}
702:
695:
694:
692:
499:
498:
494:
493:
490:
256:
246:
238:
3164:. CRC Press. 2004 edition, p. 743.
1420:, can provide undecidable theories; see
1209:: there is an algorithm that, given any
1055:All of these axioms can be expressed in
2874:
2284:real closed fields both of cardinality
1280:is a real closed field, a formula with
919:Decidability and quantifier elimination
418:has an algebraic extension, called the
2591:
1950:There are real-closed fields that are
1561:is the size of the input formula. The
878:, its real closure is again the field
3158:Computational Real Algebraic Geometry
2499:number of nonzero terms of the field
1270:extends this result to the following
7:
2911:
2909:
2320:The generalized continuum hypothesis
1910:, the complexity is lower. Basu and
230:is not algebraically closed but the
1763:{\displaystyle 2^{2^{\Omega (n)}},}
1681:must involve polynomials of degree
1563:cylindrical algebraic decomposition
1284:free variables defines a subset of
3117:Valuations, orderings, and Milnor
2817:
2790:
2763:
2736:
2709:
2682:
2647:
2616:
2571:
2469:
2430:
2292:
2259:
2245:; any two real closed fields are η
2233:and smaller than every element of
2190:
2029:
1810:For the decision problem, Ben-Or,
1777:
1741:
1717:{\displaystyle 2^{2^{\Omega (n)}}}
1698:
1390:{\displaystyle (\exists x)P(x,y),}
1357:
899:
896:
893:
770:
767:
764:
746:
743:
740:
506:
503:
500:
25:
2983:10.1090/S0002-9947-1962-0146089-X
2414:. This is the most commonly used
2304:{\displaystyle \aleph _{\alpha }}
2271:{\displaystyle \aleph _{\alpha }}
2237:. This is closely related to the
2202:{\displaystyle \aleph _{\alpha }}
263:{\displaystyle F({\sqrt {-1}}\,)}
2481:{\displaystyle \aleph _{\beta }}
2442:{\displaystyle \aleph _{\beta }}
2374:
2326:generalized continuum hypothesis
2092:generalized continuum hypothesis
1485:Tarski's original algorithm for
3212:Journal of Symbolic Computation
2942:10.1090/s0002-9904-1953-09664-1
2894:Rajwade (1993) pp. 222â223
2130:, this is equivalent to saying
522:of real algebraic numbers. The
306:holds for all polynomials over
76:A real closed field is a field
2523:
2520:
2514:
2511:
2343:can be defined by means of an
2278:-saturated, and moreover two η
2213:is less than every element of
1786:
1780:
1750:
1744:
1707:
1701:
1598:
1592:
1381:
1369:
1363:
1354:
843:
833:
808:
798:
709:
699:
329:Examples of real closed fields
257:
243:
18:Elementary theory of the reals
1:
3225:10.1016/S0747-7171(10)80003-3
3125:American Mathematical Society
3099:10.1016/s0747-7171(88)80004-x
2854:Elementary Euclidean geometry
2529:{\displaystyle \mathbb {R} ]}
2229:larger than every element of
2106:if there is no ordered field
1257:
652:the relative real closure of
601:, together with its ordering
3319:Model Theory preprint server
3260:. Univ. of California Press.
3156:Mishra, Bhubaneswar (1997) "
2407:{\displaystyle \mathbb {R} }
2330:cardinality of the continuum
2005:is an unbounded sequence in
1969:contained in an ordered set
1954:; for example, any field of
1608:{\displaystyle d^{2^{O(n)}}}
871:{\displaystyle \mathbb {R} }
648:is the algebraic closure of
2916:McNaughton, Robert (1953).
2829:{\displaystyle \aleph _{0}}
2802:{\displaystyle \aleph _{1}}
2775:{\displaystyle \aleph _{0}}
2748:{\displaystyle \aleph _{1}}
2721:{\displaystyle \aleph _{1}}
2694:{\displaystyle \aleph _{2}}
2659:{\displaystyle \aleph _{2}}
2628:{\displaystyle \aleph _{1}}
2583:{\displaystyle \aleph _{1}}
2209:such that every element of
2041:{\displaystyle \aleph _{0}}
1201:, meaning that there is an
549:) is an ordered field, and
56:properties as the field of
3361:
3181:Cambridge University Press
1923:arithmetic operations and
1792:{\displaystyle \Omega (n)}
304:intermediate value theorem
29:
2843:property in place of the
2182:of cardinality less than
2170:, if for any two subsets
1478:Complexity of deciding đ
1268:TarskiâSeidenberg theorem
821:). On the other hand, if
410:is an ordered field, the
170:has at least one root in
2903:Efrat (2006) p. 177
2251:if and only if they are
1496:, meaning that no tower
1494:computational complexity
298:There is an ordering on
273:There is an ordering on
270:is algebraically closed.
174:, and for every element
102:it is true in the reals.
3345:Real algebraic geometry
3247:University of Edinburgh
3206:Renegar, James (1992).
3175:Rajwade, A. R. (1993).
2970:Trans. Amer. Math. Soc.
2604:of larger cardinality.
2122:. If the cofinality of
1263:and published in 1948.
1051:have at least one root.
631:real closed relative to
445:of fields identical on
89:elementarily equivalent
2830:
2803:
2776:
2749:
2722:
2695:
2660:
2629:
2584:
2530:
2482:
2449:then we have a unique
2443:
2416:hyperreal number field
2408:
2382:
2305:
2272:
2217:, there is an element
2203:
2042:
1793:
1764:
1718:
1657:of formulas of length
1609:
1548:
1487:quantifier elimination
1468:
1391:
1234:
1207:quantifier elimination
1191:
1160:
1125:
1088:
1045:
1025:
987:
952:
927:of real closed fields
909:
872:
850:
815:
780:
716:
516:
412:ArtinâSchreier theorem
362:with real coefficients
264:
3069:. Oxford Univ. Press.
3052:Howard Jerome Keisler
2929:Bull. Amer. Math. Soc
2831:
2804:
2777:
2750:
2723:
2696:
2661:
2630:
2585:
2531:
2483:
2444:
2409:
2383:
2306:
2273:
2204:
2043:
1794:
1765:
1719:
1646:worst-case complexity
1610:
1549:
1469:
1392:
1235:
1192:
1161:
1126:
1089:
1046:
1026:
1011:for every odd number
988:
953:
910:
873:
851:
816:
781:
717:
607:relative real closure
517:
265:
32:ArtinâSchreier theory
2813:
2786:
2759:
2732:
2705:
2678:
2643:
2612:
2567:
2503:
2465:
2426:
2420:nonstandard analysis
2396:
2351:
2288:
2255:
2241:property of being a
2186:
2110:properly containing
2025:
2009:. The cofinality of
1774:
1728:
1685:
1576:
1503:
1447:
1422:Richardson's theorem
1418:exponential function
1351:
1294:. Given a subset of
1244:, which may contain
1213:
1170:
1139:
1104:
1067:
1035:
1015:
966:
931:
882:
860:
825:
790:
729:
691:
489:
237:
214:algebraically closed
3340:Field (mathematics)
3115:Efrat, Ido (2006).
3074:Davenport, James H.
3003:Marie-Françoise Roy
2538:formal power series
2074:To this we may add
2059:The cardinality of
1135:, meaning that any
679:is orderable) then
668:described earlier.
279:algebraic extension
164:formally real field
64:, and the field of
3061:Dales, H. G., and
2863:Euclidean geometry
2826:
2799:
2772:
2745:
2718:
2691:
2656:
2625:
2580:
2526:
2478:
2439:
2404:
2378:
2301:
2268:
2199:
2066:The cofinality of
2038:
2001:. In other words,
1943:larger than it in
1902:stands for either
1805:double exponential
1801:big Omega notation
1789:
1760:
1714:
1605:
1544:
1464:
1387:
1272:projection theorem
1230:
1187:
1156:
1121:
1084:
1041:
1021:
983:
948:
905:
868:
846:
811:
776:
712:
512:
342:computable numbers
334:the field of real
260:
52:that has the same
3335:Real closed field
3067:Super-Real Fields
2149:An ordered field
1956:hyperreal numbers
1937:Archimedean field
1820:exponential space
1567:George E. Collins
1461:
1292:semialgebraic set
1227:
1184:
1153:
1118:
1081:
1057:first-order logic
1044:{\displaystyle d}
1024:{\displaystyle d}
980:
945:
841:
806:
707:
589:and the order on
451:ring homomorphism
449:(note that every
367:Levi-Civita field
348:definable numbers
336:algebraic numbers
254:
218:algebraic closure
148:has at least one
66:hyperreal numbers
62:algebraic numbers
43:real closed field
16:(Redirected from
3352:
3300:
3250:
3244:
3229:
3227:
3202:
3146:
3111:
3101:
3058:. North-Holland.
3048:Chen Chung Chang
2994:
2985:
2964:-sets of power â”
2947:
2946:
2944:
2926:
2913:
2904:
2901:
2895:
2892:
2886:
2879:
2835:
2833:
2832:
2827:
2825:
2824:
2808:
2806:
2805:
2800:
2798:
2797:
2781:
2779:
2778:
2773:
2771:
2770:
2754:
2752:
2751:
2746:
2744:
2743:
2727:
2725:
2724:
2719:
2717:
2716:
2700:
2698:
2697:
2692:
2690:
2689:
2665:
2663:
2662:
2657:
2655:
2654:
2639:has cardinality
2634:
2632:
2631:
2626:
2624:
2623:
2589:
2587:
2586:
2581:
2579:
2578:
2535:
2533:
2532:
2527:
2510:
2487:
2485:
2484:
2479:
2477:
2476:
2448:
2446:
2445:
2440:
2438:
2437:
2413:
2411:
2410:
2405:
2403:
2387:
2385:
2384:
2379:
2377:
2372:
2367:
2366:
2365:
2359:
2313:order isomorphic
2310:
2308:
2307:
2302:
2300:
2299:
2277:
2275:
2274:
2269:
2267:
2266:
2208:
2206:
2205:
2200:
2198:
2197:
2132:Cauchy sequences
2047:
2045:
2044:
2039:
2037:
2036:
1931:Order properties
1925:polynomial space
1922:
1909:
1905:
1901:
1894:
1798:
1796:
1795:
1790:
1769:
1767:
1766:
1761:
1756:
1755:
1754:
1753:
1723:
1721:
1720:
1715:
1713:
1712:
1711:
1710:
1680:
1671:
1667:
1656:
1636:
1625:
1621:
1614:
1612:
1611:
1606:
1604:
1603:
1602:
1601:
1565:, introduced by
1560:
1553:
1551:
1550:
1545:
1543:
1542:
1541:
1540:
1539:
1538:
1537:
1536:
1535:
1534:
1473:
1471:
1470:
1465:
1463:
1462:
1459:
1457:
1456:
1407:
1403:
1396:
1394:
1393:
1388:
1343:
1325:
1321:
1318:that maps every
1313:
1307:
1297:
1289:
1283:
1279:
1262:
1259:
1239:
1237:
1236:
1231:
1229:
1228:
1225:
1223:
1222:
1196:
1194:
1193:
1188:
1186:
1185:
1182:
1180:
1179:
1165:
1163:
1162:
1157:
1155:
1154:
1151:
1149:
1148:
1130:
1128:
1127:
1122:
1120:
1119:
1116:
1114:
1113:
1093:
1091:
1090:
1085:
1083:
1082:
1079:
1077:
1076:
1050:
1048:
1047:
1042:
1030:
1028:
1027:
1022:
992:
990:
989:
984:
982:
981:
978:
976:
975:
961:
957:
955:
954:
949:
947:
946:
943:
941:
940:
914:
912:
911:
906:
904:
903:
902:
890:
877:
875:
874:
869:
867:
855:
853:
852:
847:
842:
837:
832:
820:
818:
817:
812:
807:
802:
797:
785:
783:
782:
777:
775:
774:
773:
761:
751:
750:
749:
737:
721:
719:
718:
713:
708:
703:
698:
685:real closed ring
660:is actually the
605:, is called the
555:Galois extension
521:
519:
518:
513:
511:
510:
509:
497:
483:rational numbers
465:if and only if â
455:order preserving
437:, and is unique
380:superreal number
373:hyperreal number
322:weakly o-minimal
269:
267:
266:
261:
255:
247:
222:finite extension
21:
3360:
3359:
3355:
3354:
3353:
3351:
3350:
3349:
3325:
3324:
3307:
3282:10.2307/1969812
3263:
3242:
3234:Passmore, Grant
3232:
3205:
3191:
3174:
3135:
3114:
3086:J. Symb. Comput
3072:
2999:Richard Pollack
2997:Basu, Saugata,
2967:
2963:
2959:
2956:
2951:
2950:
2924:
2915:
2914:
2907:
2902:
2898:
2893:
2889:
2880:
2876:
2871:
2859:Tarski's axioms
2856:
2849:
2842:
2836:, and with the
2816:
2811:
2810:
2789:
2784:
2783:
2762:
2757:
2756:
2735:
2730:
2729:
2708:
2703:
2702:
2681:
2676:
2675:
2666:, and contains
2646:
2641:
2640:
2615:
2610:
2609:
2570:
2565:
2564:
2563:of cardinality
2560:
2548:divisible group
2542:totally ordered
2501:
2500:
2468:
2463:
2462:
2458:
2429:
2424:
2423:
2394:
2393:
2354:
2349:
2348:
2338:
2332:and having the
2322:
2291:
2286:
2285:
2283:
2258:
2253:
2252:
2250:
2243:saturated model
2239:model-theoretic
2189:
2184:
2183:
2162:
2028:
2023:
2022:
2019:natural numbers
1952:non-Archimedean
1933:
1915:
1907:
1903:
1899:
1892:
1883:
1876:
1867:
1858:
1851:
1845:
1836:
1829:
1772:
1771:
1736:
1731:
1726:
1725:
1693:
1688:
1683:
1682:
1679:
1673:
1669:
1658:
1655:
1649:
1627:
1623:
1619:
1584:
1579:
1574:
1573:
1558:
1526:
1521:
1516:
1511:
1506:
1501:
1500:
1483:
1481:
1450:
1445:
1444:
1405:
1401:
1349:
1348:
1330:
1323:
1319:
1309:
1303:
1298:variables, the
1295:
1285:
1281:
1275:
1260:
1254:Sturm's theorem
1216:
1211:
1210:
1173:
1168:
1167:
1142:
1137:
1136:
1107:
1102:
1101:
1070:
1065:
1064:
1033:
1032:
1013:
1012:
969:
964:
963:
959:
934:
929:
928:
921:
885:
880:
879:
858:
857:
823:
822:
788:
787:
756:
732:
727:
726:
689:
688:
492:
487:
486:
404:
387:surreal numbers
331:
235:
234:
232:field extension
74:
35:
28:
23:
22:
15:
12:
11:
5:
3358:
3356:
3348:
3347:
3342:
3337:
3327:
3326:
3323:
3322:
3315:
3306:
3305:External links
3303:
3302:
3301:
3276:(3): 542â554,
3261:
3251:
3230:
3218:(3): 255â299.
3203:
3189:
3172:
3154:
3147:
3133:
3112:
3092:(1â2): 29â35.
3070:
3063:W. Hugh Woodin
3059:
3045:
3031:
3022:
3019:online version
2995:
2965:
2961:
2955:
2952:
2949:
2948:
2905:
2896:
2887:
2881:D. Macpherson
2873:
2872:
2870:
2867:
2855:
2852:
2847:
2840:
2823:
2819:
2796:
2792:
2769:
2765:
2742:
2738:
2715:
2711:
2688:
2684:
2653:
2649:
2622:
2618:
2577:
2573:
2558:
2525:
2522:
2519:
2516:
2513:
2509:
2475:
2471:
2454:
2436:
2432:
2402:
2376:
2371:
2364:
2358:
2336:
2321:
2318:
2317:
2316:
2298:
2294:
2279:
2265:
2261:
2246:
2196:
2192:
2165:ordinal number
2158:
2147:
2088:
2087:
2078:The weight of
2072:
2071:
2064:
2035:
2031:
1973:is cofinal in
1945:absolute value
1932:
1929:
1896:
1895:
1888:
1881:
1872:
1868:) â 0 ⧠... â§
1863:
1856:
1849:
1841:
1834:
1788:
1785:
1782:
1779:
1759:
1752:
1749:
1746:
1743:
1739:
1734:
1709:
1706:
1703:
1700:
1696:
1691:
1675:
1651:
1639:big O notation
1616:
1615:
1600:
1597:
1594:
1591:
1587:
1582:
1555:
1554:
1533:
1529:
1524:
1519:
1514:
1509:
1482:
1479:
1476:
1455:
1398:
1397:
1386:
1383:
1380:
1377:
1374:
1371:
1368:
1365:
1362:
1359:
1356:
1344:is defined by
1322:-tuple to the
1246:free variables
1221:
1178:
1147:
1112:
1075:
1061:quantification
1053:
1052:
1040:
1020:
1009:
1006:
1003:ordered fields
974:
939:
920:
917:
901:
898:
895:
889:
866:
845:
840:
835:
831:
810:
805:
800:
796:
772:
769:
766:
760:
755:
748:
745:
742:
736:
711:
706:
701:
697:
508:
505:
502:
496:
403:
400:
399:
398:
383:
376:
369:
363:
360:Puiseux series
356:
350:
344:
338:
330:
327:
326:
325:
324:ordered field.
315:
296:
286:
271:
259:
253:
250:
245:
242:
225:
207:
202: = â
157:
103:
100:if and only if
73:
70:
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
3357:
3346:
3343:
3341:
3338:
3336:
3333:
3332:
3330:
3321:
3320:
3316:
3314:
3313:
3309:
3308:
3304:
3299:
3295:
3291:
3287:
3283:
3279:
3275:
3271:
3270:Ann. of Math.
3267:
3262:
3259:
3255:
3254:Alfred Tarski
3252:
3248:
3241:
3240:
3235:
3231:
3226:
3221:
3217:
3213:
3209:
3204:
3200:
3196:
3192:
3190:0-521-42668-5
3186:
3182:
3178:
3173:
3171:
3170:1-58488-301-4
3167:
3163:
3159:
3155:
3152:
3148:
3144:
3140:
3136:
3134:0-8218-4041-X
3130:
3126:
3122:
3118:
3113:
3109:
3105:
3100:
3095:
3091:
3087:
3083:
3079:
3075:
3071:
3068:
3064:
3060:
3057:
3053:
3049:
3046:
3044:
3043:3-211-82794-3
3040:
3036:
3032:
3029:
3028:
3023:
3020:
3016:
3015:3-540-33098-4
3012:
3008:
3004:
3000:
2996:
2993:
2989:
2984:
2979:
2975:
2971:
2958:
2957:
2953:
2943:
2938:
2934:
2930:
2923:
2922:by A. Tarski"
2921:
2912:
2910:
2906:
2900:
2897:
2891:
2888:
2884:
2878:
2875:
2868:
2866:
2864:
2860:
2853:
2851:
2846:
2839:
2821:
2794:
2782:, and weight
2767:
2740:
2728:, cofinality
2713:
2686:
2673:
2669:
2651:
2638:
2620:
2607:
2603:
2599:
2595:
2593:
2575:
2562:
2557:
2552:
2549:
2546:
2543:
2539:
2517:
2498:
2494:
2489:
2473:
2460:
2457:
2453:
2434:
2421:
2417:
2391:
2369:
2346:
2342:
2335:
2331:
2327:
2319:
2314:
2296:
2282:
2263:
2249:
2244:
2240:
2236:
2232:
2228:
2224:
2220:
2216:
2212:
2194:
2181:
2177:
2173:
2169:
2166:
2161:
2156:
2152:
2148:
2145:
2141:
2137:
2133:
2129:
2125:
2121:
2117:
2113:
2109:
2105:
2101:
2097:
2096:
2095:
2093:
2085:
2081:
2077:
2076:
2075:
2069:
2065:
2062:
2058:
2057:
2056:
2054:
2049:
2033:
2020:
2016:
2012:
2008:
2004:
2000:
1996:
1992:
1988:
1984:
1980:
1977:if for every
1976:
1972:
1968:
1964:
1959:
1957:
1953:
1948:
1946:
1942:
1938:
1930:
1928:
1926:
1921:
1918:
1913:
1891:
1887:
1880:
1875:
1871:
1866:
1862:
1855:
1848:
1844:
1840:
1833:
1828:
1827:
1826:
1823:
1821:
1817:
1813:
1808:
1806:
1802:
1783:
1757:
1747:
1737:
1732:
1704:
1694:
1689:
1678:
1665:
1661:
1654:
1647:
1642:
1640:
1634:
1630:
1595:
1589:
1585:
1580:
1572:
1571:
1570:
1568:
1564:
1531:
1527:
1522:
1517:
1512:
1507:
1499:
1498:
1497:
1495:
1492:
1491:nonelementary
1488:
1477:
1475:
1442:
1438:
1434:
1429:
1427:
1423:
1419:
1415:
1409:
1384:
1378:
1375:
1372:
1366:
1360:
1347:
1346:
1345:
1341:
1337:
1333:
1327:
1317:
1312:
1306:
1301:
1293:
1288:
1278:
1273:
1269:
1264:
1255:
1251:
1247:
1243:
1208:
1204:
1200:
1134:
1099:
1095:
1062:
1058:
1038:
1018:
1010:
1007:
1004:
1000:
996:
995:
994:
926:
918:
916:
838:
803:
753:
725:
704:
686:
682:
678:
674:
669:
667:
663:
659:
655:
651:
647:
643:
639:
635:
632:
628:
624:
620:
616:
612:
608:
604:
600:
596:
592:
588:
584:
580:
576:
572:
568:
564:
560:
556:
552:
548:
544:
539:
537:
533:
532:Otto Schreier
529:
526:is named for
525:
485:is the field
484:
480:
477: +
476:
473: =
472:
468:
464:
461: â€
460:
456:
452:
448:
444:
440:
436:
432:
428:
424:
421:
417:
413:
409:
401:
396:
392:
388:
385:the field of
384:
381:
377:
374:
370:
368:
364:
361:
358:the field of
357:
355:
352:the field of
351:
349:
346:the field of
345:
343:
340:the field of
339:
337:
333:
332:
328:
323:
319:
316:
313:
309:
305:
301:
297:
294:
290:
287:
284:
280:
276:
272:
251:
248:
240:
233:
229:
226:
223:
219:
215:
211:
208:
205:
201:
197:
194: =
193:
189:
185:
181:
177:
173:
169:
165:
161:
158:
155:
151:
147:
143:
139:
136:
132:
128:
124:
120:
116:
115:ordered field
113:making it an
112:
108:
104:
101:
98:
94:
90:
86:
83:
82:
81:
79:
71:
69:
67:
63:
59:
55:
51:
48:
44:
40:
33:
19:
3318:
3311:
3273:
3269:
3257:
3238:
3215:
3211:
3176:
3161:
3150:
3120:
3116:
3089:
3085:
3078:Heintz, Joos
3066:
3056:Model Theory
3055:
3037:. Springer.
3034:
3025:
3009:. Springer.
3006:
2973:
2969:
2935:(1): 91â93.
2932:
2928:
2919:
2899:
2890:
2882:
2877:
2857:
2844:
2837:
2671:
2667:
2636:
2605:
2601:
2597:
2596:
2555:
2550:
2492:
2490:
2455:
2451:
2389:
2340:
2333:
2323:
2280:
2247:
2234:
2230:
2226:
2222:
2218:
2214:
2210:
2179:
2175:
2171:
2167:
2159:
2150:
2143:
2135:
2127:
2123:
2119:
2118:is dense in
2115:
2111:
2107:
2103:
2099:
2089:
2083:
2079:
2073:
2067:
2060:
2052:
2050:
2010:
2006:
2002:
1998:
1994:
1990:
1986:
1985:there is an
1982:
1978:
1974:
1970:
1966:
1960:
1949:
1934:
1919:
1916:
1897:
1889:
1885:
1878:
1873:
1869:
1864:
1860:
1853:
1846:
1842:
1838:
1831:
1824:
1809:
1676:
1663:
1659:
1652:
1643:
1632:
1628:
1617:
1556:
1484:
1440:
1430:
1410:
1399:
1339:
1335:
1331:
1328:
1310:
1304:
1299:
1286:
1276:
1271:
1265:
1249:
1100:showed that
1096:
1054:
922:
680:
676:
672:
670:
665:
662:real closure
661:
657:
653:
649:
645:
641:
637:
633:
630:
626:
622:
621:. We call (
618:
614:
610:
606:
602:
598:
594:
590:
586:
582:
574:
570:
566:
563:Zorn's lemma
558:
550:
546:
542:
540:
538:it in 1926.
478:
474:
470:
466:
462:
458:
446:
434:
430:
429:, such that
426:
422:
420:real closure
419:
415:
414:states that
411:
407:
405:
402:Real closure
391:proper class
354:real numbers
317:
311:
310:with degree
307:
299:
292:
288:
282:
274:
227:
209:
203:
199:
195:
191:
187:
183:
179:
175:
171:
167:
159:
153:
145:
142:coefficients
126:
118:
110:
96:
84:
77:
75:
58:real numbers
49:
42:
36:
2976:: 341â352,
2809:instead of
2755:instead of
2701:instead of
2592:Alling 1962
2553:that is an
2134:indexed by
2015:cardinality
1724:and length
1261: 1930
585:containing
443:isomorphism
389:(this is a
123:square root
107:total order
105:There is a
54:first-order
39:mathematics
3329:Categories
3199:0785.11022
3143:1103.12002
3108:0663.03015
2954:References
2345:ultrapower
2163:, for the
2157:property η
2140:convergent
2114:such that
1993:such that
1963:cofinality
1904:<, >
1300:projection
1250:equivalent
593:extending
561:, then by
528:Emil Artin
457:, because
216:, but its
190:such that
131:polynomial
72:Definition
2918:"Review:
2818:ℵ
2791:ℵ
2764:ℵ
2737:ℵ
2710:ℵ
2683:ℵ
2648:ℵ
2617:ℵ
2572:ℵ
2497:countable
2474:β
2470:ℵ
2435:β
2431:ℵ
2297:α
2293:ℵ
2264:α
2260:ℵ
2195:α
2191:ℵ
2030:ℵ
1778:Ω
1742:Ω
1699:Ω
1528:⋅
1523:⋅
1518:⋅
1358:∃
1203:algorithm
1199:decidable
754:×
441:a unique
249:−
182:there is
3236:(2011).
3080:(1988).
2461:of size
2388:, where
2153:has the
2104:complete
2098:A field
1965:. A set
1906:or
1837:, ..., â
1316:function
1133:complete
925:language
644:. When
640:is just
579:subfield
469: :
393:, not a
129:and any
93:sentence
3298:0069161
3290:1969812
3256:(1951)
3245:(PhD).
3177:Squares
3121:-theory
3065:(1996)
3054:(1989)
2992:0146089
2545:abelian
2155:eta set
2013:is the
1941:integer
1884:, ...,
1859:, ...,
1668:, with
1435:'s and
1416:or the
1314:is the
1242:formula
722:is the
597:. This
573:) with
524:theorem
212:is not
3296:
3288:
3197:
3187:
3168:
3160:," in
3141:
3131:
3106:
3041:
3013:
3001:, and
2990:
2885:(1998)
2883:et al.
1898:where
1893:) â 0,
1814:, and
1770:where
1618:where
1437:Turing
1400:where
1098:Tarski
1059:(i.e.
999:axioms
536:proved
534:, who
382:fields
375:fields
138:degree
121:has a
3286:JSTOR
3272:, 2,
3243:(PDF)
2925:(PDF)
2869:Notes
2561:group
2540:on a
2459:field
2347:, as
2225:with
1997:<
1812:Kozen
1433:Gödel
1302:from
1274:. If
617:) in
553:is a
439:up to
320:is a
220:is a
162:is a
140:with
47:field
45:is a
3185:ISBN
3166:ISBN
3129:ISBN
3050:and
3039:ISBN
3011:ISBN
2968:.",
2311:are
2174:and
2138:are
1816:Reif
1489:has
1424:and
1414:sine
1404:and
1266:The
997:the
923:The
724:ring
609:of (
541:If (
530:and
378:the
371:the
365:the
150:root
41:, a
3278:doi
3220:doi
3195:Zbl
3139:Zbl
3104:Zbl
3094:doi
2978:doi
2974:103
2937:doi
2594:).
2536:of
2488:.)
2418:in
2221:in
2178:of
2142:in
2126:is
2102:is
1989:in
1981:in
1912:Roy
1799:is
1637:is
1480:rcf
1460:rcf
1308:to
1226:rcf
1197:is
1183:rcf
1152:rcf
1131:is
1117:rcf
1080:rcf
1001:of
979:rcf
944:rcf
671:If
664:of
656:in
636:if
581:of
557:of
425:of
406:If
395:set
281:of
198:or
186:in
178:of
152:in
144:in
135:odd
133:of
125:in
109:on
87:is
37:In
3331::
3294:MR
3292:,
3284:,
3274:61
3268:,
3216:13
3214:.
3210:.
3193:.
3183:.
3137:.
3127:.
3102:.
3088:.
3084:.
3076:;
2988:MR
2986:,
2972:,
2933:59
2931:.
2927:.
2908:^
2672:is
2635:,
2055::
2048:.
1927:.
1807:.
1641:.
1474:.
1428:.
1338:,
1258:c.
915:.
629:)
625:,
613:,
577:a
569:,
545:,
314:0.
68:.
3280::
3249:.
3228:.
3222::
3201:.
3145:.
3119:K
3110:.
3096::
3090:5
3021:)
3017:(
2980::
2966:α
2962:α
2945:.
2939::
2848:0
2845:η
2841:1
2838:η
2822:0
2795:1
2768:0
2741:1
2714:1
2687:2
2668:Ï
2652:2
2637:Î
2621:1
2606:Ï
2602:Î
2598:Ï
2590:(
2576:1
2559:1
2556:η
2551:G
2524:]
2521:]
2518:G
2515:[
2512:[
2508:R
2493:Ï
2456:ÎČ
2452:η
2401:R
2390:M
2375:M
2370:/
2363:N
2357:R
2341:Ï
2337:1
2334:η
2315:.
2281:α
2248:α
2235:U
2231:L
2227:x
2223:F
2219:x
2215:U
2211:L
2180:F
2176:U
2172:L
2168:α
2160:α
2151:F
2146:.
2144:F
2136:Îș
2128:Îș
2124:F
2120:K
2116:F
2112:F
2108:K
2100:F
2086:.
2084:F
2080:F
2070:.
2068:F
2063:.
2061:F
2053:F
2034:0
2011:F
2007:F
2003:X
1999:x
1995:y
1991:X
1987:x
1983:F
1979:y
1975:F
1971:F
1967:X
1920:d
1917:s
1908:=
1900:â
1890:k
1886:x
1882:1
1879:x
1877:(
1874:s
1870:P
1865:k
1861:x
1857:1
1854:x
1852:(
1850:1
1847:P
1843:k
1839:x
1835:1
1832:x
1830:â
1787:)
1784:n
1781:(
1758:,
1751:)
1748:n
1745:(
1738:2
1733:2
1708:)
1705:n
1702:(
1695:2
1690:2
1677:n
1674:Ί
1670:n
1666:)
1664:n
1662:(
1660:O
1653:n
1650:Ί
1635:)
1633:n
1631:(
1629:O
1624:d
1620:n
1599:)
1596:n
1593:(
1590:O
1586:2
1581:d
1559:n
1532:n
1513:2
1508:2
1454:L
1441:x
1406:y
1402:x
1385:,
1382:)
1379:y
1376:,
1373:x
1370:(
1367:P
1364:)
1361:x
1355:(
1342:)
1340:y
1336:x
1334:(
1332:p
1324:k
1320:n
1311:R
1305:R
1296:k
1287:R
1282:n
1277:R
1240:-
1220:L
1177:T
1146:L
1111:T
1074:T
1039:d
1019:d
1005:;
973:T
960:â€
938:L
900:g
897:l
894:a
888:R
865:R
844:)
839:2
834:(
830:Q
809:)
804:2
799:(
795:Q
771:g
768:l
765:a
759:R
747:g
744:l
741:a
735:R
710:)
705:2
700:(
696:Q
681:F
677:F
673:F
666:F
658:E
654:F
650:F
646:E
642:F
638:M
634:E
627:P
623:F
619:E
615:P
611:F
603:Q
599:M
595:P
591:M
587:F
583:E
575:M
571:Q
567:M
559:F
551:E
547:P
543:F
507:g
504:l
501:a
495:R
479:z
475:x
471:y
467:z
463:y
459:x
447:F
435:F
431:K
427:F
423:K
416:F
408:F
397:)
318:F
312:â„
308:F
300:F
293:F
289:F
285:.
283:F
275:F
258:)
252:1
244:(
241:F
228:F
224:.
210:F
206:.
204:b
200:a
196:b
192:a
188:F
184:b
180:F
176:a
172:F
168:F
160:F
156:.
154:F
146:F
127:F
119:F
111:F
97:F
85:F
78:F
50:F
34:.
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.