468:
filter's dual ideal). (If the filter is cofinite (Fréchet), its dual is the set of finite sets of indices.) The agreement set of a negation is the complement of the agreement set of the original formula, and the negation in the constructed model has the opposite truth value of the formula in the source model. disjunctions, conjunctions, and implications are only slightly more complex. Henle and
Keinberg show the proof for disjunctions and existential quantifications, and challenge the reader to complete the proof for the other cases.
95:
85:
64:
31:
662:
By making these functions of the positive integers, and thus a subset of the ultraproduct model with all the first-order properties of the reals, it should be much easier to introduce students already familiar with the infinitesimal approach to calculus to the wider implications of nonstandard analysis. More advanced model theory including ultrafilters and the Axiom of Choice can be introduced afterward.
22:
844:
In science, it frequently takes powerful methods or tools to make important discoveries that lesser tools may confirm. I think my polynomial ratios are an example of more modest tools that merely confirm the discovery
Robinson made with model theory and ultraproducts, the most powerful tools at his
661:
The polynomial ratio functions of real numbers serve as a formal model and justification of
Leibnizian calculus even without the full transfer principle. (Why did no one between Weierstrass and Robinson point out this model, and show the formalists were too hasty in throwing out the infinitesimals?)
629:
You're correct that the property of being an integer is not first-order definable in the reals (with plus and times as the only nonlogical symbols). But I'm afraid the argument you give is not a correct way to prove that. Consider a similar case: Every real number is either negative or nonnegative,
936:
As one can see by some of my work on
Knowledge this year, I have some ideas about hyperreal numbers and nonstandard analysis that are still unpublished, and therefore are not yet ready for entry in this encyclopedia. They need some kicking around in an open forum. Does anyone know an internet
655:. Is it negative, or nonnegative? The smart-ass in me wants to answer, "Yes!" The correct answer is that this sequence does indeed require an ultrafilter to decide. But this sequence would never appear in a suitably limited subset of the set of all sequences like my polynomial ratio sequences.
560:, ...) is clearly a nonstandard integer, and all integers are either odd or even but not both. Is this sequence odd or even? One ultrafilter that includes to odd terms, say the sequence is odd. Another filter, with the even terms, says the sequence is even. Conclusion: Parity of integers is
467:
Hopeless? The case for negation of a simpler formula is the easiest part of the entire proof: The agreement set of indices for which the negation holds is the complement of the agreement set of the original formula. Complements of filter members are nonmembers of the filter (and members of the
902:
subsets of the naturals. It's an ultrafilter on a different
Boolean algebra; namely, all finite and cofinite subsets of the naturals. That choice does make the negation step trivial. The hard part now becomes proving that the set of all indices where the proposition holds, is actually an
434:, would also imply the truth of the theorem as applied to models using suitably limited subsets of the entire set of sequences. Yet, this section concludes that "the fact that U is an ultrafilter (and not just a filter) is used in the negation clause." What negation clause?
555:
Ultrafilters can define when higher order formulae hold, but may disagree with other ultrafilters. This shows that the formula cannot be rephrased in first order terms within the source model. Example: The natural sequence of positive integers (1, 2, ...,
551:
th terms of the sequences holds is cofinite when and only when φ holds in the source model, and its complement, the agreement set for ¬φ is cofinite iff φ does not hold in the source, and nonfinite sets of indices with nonfinite complements are never
823:, exponential sequences) that make infinitesimals and unlimited elements of what traditional calculus refers to as "higher order" (infinitely smaller or larger) than any polynomial ratio, but they are not essential to actual problems in analysis.
453:
On your more substantial question, I think what's being referred to is the proof of the theorem by induction on formulas. One case of the induction is when the formula being considered is the negation of a simpler formula. That case is trivial if
728:), and (2) it would fall apart as soon as you made the expressive power a little stronger. For example, as soon as you can define the trig functions, you'll have the same problem with the cosine of the element represented by <0,π,2π,3π...: -->
422:(1979, Massachusetts Institute of Technology, republished 2003 by Dover Publications) refers to this theorem as the "fundamental theorem of ultraproducts", and cites Robinson's transfer principle as an application to nonstandard analysis.
473:
I'll take your comment that you've always heard the theorem called "washes theorem" as an approval to change the possessive in the main article, and add a line crediting "fundamental theorem of ultraproducts" to Henle and
Kleinberg.
429:
filters,not just ultrafilters, implying that the use of a free ultrafilter is only needed so that the entire set of sequences can be used in the ultraproduct. Proper subsets of the ultrafilter, including the cofinite filter on
538:
is the source model (I use the "rational function" sequences of reals to construct a set of hyperreals), allows one to use the cofinite filter, the subset common to all free ultrafilters on the index set, the positive integers
519:
Just the phrase "fundamental theorem of ultraproducts." Is this single citation sufficient for
Knowledge, or should the phrase be removed as insufficiently cited? Are there any other citable uses of this phrase for Łoś's
630:
and the property of being negative is certainly first-order definable within the real numbers (with plus and times). So consider the element of the ultraproduct represented by the sequence <1, −1, 1, −1, 1, −1, ...: -->
509:
In fact, honestly, I don't even know how you interpret atomic formulas, if you don't have an ultrafilter. What if the set of indices on which the atomic formula is true is not in the filter, and neither is its complement?
816:). The advantage of using sequences rather than functions of real numbers for a nonstandard model is that it is easier to extend the meanings of standard formulae from the standard model to the nonstandard one.
886:, and there is no sequence induced by a rational function whose square gives you that sequence cofinitely often. You'll have to extend the possible sequences (say, to all functions first-order definable over <
523:
Paraphrasing Henle & Kleinberg, an atomic formula is relation of a finite number of terms, each of which is a particular element, a variable standing for such an element, or a function of a finite number of
874:
While (as you've alluded to) this isn't really the proper use of this talk page, it's so interesting that I'll indulge myself one more time and make a few more remarks. We should really quit here, though.
502:? All the induction hypothesis tells us, in that case, is that the set of indices for which φ holds is not in the filter. We can't conclude, just from that, that the set of indices for which ¬φ holds,
247:
bothers me. The square brackets suggest we're considering equivalence classes, that is, elements of the ultraproduct, but the text claims that they're elements of the product. I feel like probably
1047:
is proved using this one and the
Boolean Ulrafilter Axiom, which is weaker than AOC. It says the Compactness Theorem is equivalent to boolean Ultrafilter Axiom (over ZF) - both are weaker than AOC.
658:
I still do not see any "negation clause" that requires an ultrafilter. Ultrafilters are only needed for cases where nonfinite agreement sets have nonfinite complements, as in this sequence.
151:
967:"The hyperreal numbers are the ultraproduct of one copy of the real numbers for every natural number, with regard to an ultrafilter over the natural numbers containing all cofinite sets."
391:
1090:
245:
309:
679:
I should give credit to Eric
Schecter's page on defining the real numbers as my source for the "rational functions" as an example of a field with infinitesimals. Go to
1080:
687:. He told me by email that he was introduced to the idea by fellow mathematicians a few years earlier at a meeting, but he no longer had the names of his sources.
1095:
1034:
946:"the axiom of choice is needed at the existential quantifier step" The ultrafilter lemma suffices and is, in ZF, strictly weaker than the axiom of choice. ---
35:
885:
Rational functions aren't actually going to do it. For example, you need to be able to take the square root of the element represented by <0,1,2,...: -->
1105:
975:
then N\A=B and N\B=A, therefore A and B are not cofinite and therefore A and N\A are not in F and therefore F is not an ultrafilter but simply a filter.
437:
If "Łoś" is pronounced "wash", shouldn't the possessive be "Łoś's"? I propose that this section be renamed "Łoś's fundamental theorem of ultraproducts".
141:
878:"Rational function" is completely standard terminology and is not ambiguous. It's rarely a good idea to reinvent the wheel on nomenclature just because
796:) = √2 is a "rational function" even though it's an irrational number.) A "polynomial ratio sequence" is a sequence derived from such a function, say
1075:
447:
Hm, interesting point. I always hear it called "washes theorem" but it seems to me that I rarely see the apostrophe-ess in print. I don't know why. --
907:
of that
Boolean algebra. That will require a harder and more delicate argument than I think you've come to terms with (if, that is, it's even true).
1085:
721:
However: (1) the proof would be somewhat involved, as it would rely on the limited expressive power of first-order logic in that structure (e.g.
117:
1100:
916:
unlikely to work, it's not impossible that the mathematics as a whole will work, and it does sound like a fun question to investigate. --
494:
On to negations: Suppose we know the theorem holds for a formula φ and we want to show it holds for ¬φ. Your argument works fine if φ is
108:
69:
759:(Thanks for helping me clarify my ideas. A lot of this extended discussion will be reflected in the paper I am still working on.)
971:
let F={cofinite subsets of N}={A in N such that N\A is finite} when N is the set of natural numbers and N\A={n in N and not in A}
1070:
780:
I use "polynomial ratio" as an alternative name for "rational function" to avoid confusing these functions with functions from
696:
So I'm not too sure what you mean by "polynomial ratio sequences". Do you mean that the sequence can only be of the form <
44:
912:
Good luck with your research! While your hope of using this to simplify the introduction to calculus is in my opinion
1043:
I'm quite rusty, but, it seems to me AOC is not required. Only requires that U be a set closed for contain. The
314:
491:? Either way, I'm skeptical. If you just want to use them as a reference, then of course that should be fine.
176:
980:
1052:
894:
The reason you don't see any problem with the "negation" step of the induction is that you're effectively
50:
976:
94:
21:
1044:
938:
846:
688:
621:
569:
475:
438:
250:
116:
on Knowledge. If you would like to participate, please visit the project page, where you can join
100:
84:
63:
620:," which quantizes sets rather than real numbers, and is thus not first order within that set.
1048:
713:
is a rational function? That might possibly work, for the specific case of the structure <
680:
723:
the fact that all functions first-order definable over the structure are rational functions
1037:
999:
991:
There's nothing wrong with the statement. It does not state that the ultrafilter contains
951:
937:
discussion group on this topic that would be more suitable than these discussion pages?
726:
oops--that's not actually a "fact"; you can define the square-root function, for example
917:
733:
632:
511:
459:
448:
404:
394:
1019:
1064:
969:
But that is wrong, since a filter containing all cofinite sets is not an ultrafilter:
973:
let A be the subset of even natural numbers and B the subset of odd natural numbers,
898:
an ultrafilter -- it's just that it's not an ultrafilter on the Boolean algebra of
1036:
is an ultrafilter (and not just a filter) is used in the negation clause, and the
425:
They present an inductive proof on first order formulas that uses properties of
113:
995:
cofinite sets. The ultrafiter can (and indeed must) contain also other sets. —
1056:
996:
947:
90:
955:
941:
441:
1002:
984:
920:
849:
736:
691:
635:
624:
572:
514:
478:
462:
407:
397:
729:. So it seems rather limiting as a way of introducing the calculus.
564:
a first order property within the reals. (I'm not even sure that "
819:
Ultraproduct models of the hyperreals numbers contain sequences (
1013:
The following statement is in the proof, I think it is wrong:
15:
732:
Still, it does seem like an interesting avenue to explore. --
882:
can think of another possible meaning of the standard term.
681:
http://www.math.vanderbilt.edu/~schectex/courses/thereals/
568:
is an integer" is first order within the real numbers!)
527:
Limiting the set of sequences in the constructed model
458:
is an ultrafilter, but otherwise probably hopeless. --
1022:
718:. At least I don't immediately know a counterexample.
317:
253:
179:
112:, a collaborative effort to improve the coverage of
1028:
385:
303:
239:
1091:Knowledge level-5 vital articles in Mathematics
1040:is needed at the existential quantifier step.
654:The sequence <1, −1, 1, −1, 1, −1, ...: -->
1009:Wrong statement in the proof of Los's Theorem
8:
543:im my case. The agreement set of indices
483:Last things first: You mean crediting the
386:{\displaystyle ,\ldots ,\in \prod M_{i}/U}
58:
1021:
418:James M. Henle and Eugene M. Kleinberg's
375:
369:
350:
325:
316:
286:
261:
252:
231:
212:
187:
178:
965:In the examples section, this is stated:
240:{\displaystyle ,\ldots ,\in \prod M_{i}}
1081:Knowledge vital articles in Mathematics
60:
19:
547:for which the formula φ holds for the
498:in the ultraproduct. But what if it's
1096:C-Class vital articles in Mathematics
506:in the filter, which is what we need.
393:was meant instead. Can you verify? -
7:
631:. Is it negative, or nonnegative? --
106:This article is within the scope of
49:It is of interest to the following
961:Hyperreal example - bad statement?
581:is an integer" is equivalent to "∃
173:The notation used in the equation
14:
1106:Low-priority mathematics articles
126:Knowledge:WikiProject Mathematics
1076:Knowledge level-5 vital articles
129:Template:WikiProject Mathematics
93:
83:
62:
29:
20:
146:This article has been rated as
1086:C-Class level-5 vital articles
356:
343:
331:
318:
304:{\displaystyle ,\ldots ,\in M}
292:
279:
267:
254:
218:
205:
193:
180:
1:
120:and see a list of open tasks.
1101:C-Class mathematics articles
1122:
788:. (The constant function
408:17:26, 11 April 2006 (UTC)
403:Good catch. I fixed it. --
398:16:54, 11 April 2006 (UTC)
1003:16:00, 16 June 2009 (UTC)
985:15:54, 16 June 2009 (UTC)
515:20:30, 30 June 2007 (UTC)
479:20:12, 30 June 2007 (UTC)
463:06:04, 30 June 2007 (UTC)
442:05:23, 30 June 2007 (UTC)
145:
78:
57:
1057:02:58, 24 May 2020 (UTC)
942:02:10, 1 July 2007 (UTC)
921:01:27, 4 July 2007 (UTC)
850:18:16, 3 July 2007 (UTC)
737:17:44, 2 July 2007 (UTC)
692:09:49, 2 July 2007 (UTC)
683:and search the file for
636:10:35, 1 July 2007 (UTC)
625:08:19, 1 July 2007 (UTC)
573:00:13, 1 July 2007 (UTC)
152:project's priority scale
1008:
956:18:47, 2 May 2012 (UTC)
169:Product or ultraproduct
109:WikiProject Mathematics
1071:C-Class vital articles
1030:
420:Infinitesimal Calculus
413:
387:
305:
241:
1031:
487:to them, or just the
388:
306:
242:
36:level-5 vital article
1020:
315:
251:
177:
132:mathematics articles
1045:Compactness theorem
1026:
383:
301:
237:
101:Mathematics portal
45:content assessment
1029:{\displaystyle U}
727:
166:
165:
162:
161:
158:
157:
1113:
1035:
1033:
1032:
1027:
725:
392:
390:
389:
384:
379:
374:
373:
355:
354:
330:
329:
310:
308:
307:
302:
291:
290:
266:
265:
246:
244:
243:
238:
236:
235:
217:
216:
192:
191:
134:
133:
130:
127:
124:
103:
98:
97:
87:
80:
79:
74:
66:
59:
42:
33:
32:
25:
24:
16:
1121:
1120:
1116:
1115:
1114:
1112:
1111:
1110:
1061:
1060:
1038:axiom of choice
1018:
1017:
1011:
963:
532:
416:
365:
346:
321:
313:
312:
282:
257:
249:
248:
227:
208:
183:
175:
174:
171:
131:
128:
125:
122:
121:
99:
92:
72:
43:on Knowledge's
40:
30:
12:
11:
5:
1119:
1117:
1109:
1108:
1103:
1098:
1093:
1088:
1083:
1078:
1073:
1063:
1062:
1025:
1016:The fact that
1010:
1007:
1006:
1005:
987:
974:
972:
970:
968:
966:
962:
959:
939:Alan R. Fisher
934:
933:
932:
931:
930:
929:
928:
927:
926:
925:
924:
923:
910:
909:
908:
892:
883:
861:
860:
859:
858:
857:
856:
855:
854:
853:
852:
847:Alan R. Fisher
833:
832:
831:
830:
829:
828:
827:
826:
825:
824:
817:
808:th term being
769:
768:
767:
766:
765:
764:
763:
762:
761:
760:
748:
747:
746:
745:
744:
743:
742:
741:
740:
739:
730:
719:
689:Alan R. Fisher
685:infinitesimals
670:
669:
668:
667:
666:
665:
664:
663:
659:
656:
645:
644:
643:
642:
641:
640:
639:
638:
622:Alan R. Fisher
575:
570:Alan R. Fisher
553:
530:
525:
521:
507:
492:
476:Alan R. Fisher
470:
469:
465:
451:
439:Alan R. Fisher
415:
412:
411:
410:
382:
378:
372:
368:
364:
361:
358:
353:
349:
345:
342:
339:
336:
333:
328:
324:
320:
300:
297:
294:
289:
285:
281:
278:
275:
272:
269:
264:
260:
256:
234:
230:
226:
223:
220:
215:
211:
207:
204:
201:
198:
195:
190:
186:
182:
170:
167:
164:
163:
160:
159:
156:
155:
144:
138:
137:
135:
118:the discussion
105:
104:
88:
76:
75:
67:
55:
54:
48:
26:
13:
10:
9:
6:
4:
3:
2:
1118:
1107:
1104:
1102:
1099:
1097:
1094:
1092:
1089:
1087:
1084:
1082:
1079:
1077:
1074:
1072:
1069:
1068:
1066:
1059:
1058:
1054:
1050:
1046:
1041:
1039:
1023:
1014:
1004:
1001:
998:
994:
990:
989:
988:
986:
982:
978:
960:
958:
957:
953:
949:
944:
943:
940:
922:
919:
915:
911:
906:
901:
897:
893:
889:
884:
881:
877:
876:
873:
872:
871:
870:
869:
868:
867:
866:
865:
864:
863:
862:
851:
848:
843:
842:
841:
840:
839:
838:
837:
836:
835:
834:
822:
818:
815:
811:
807:
803:
799:
795:
791:
787:
783:
779:
778:
777:
776:
775:
774:
773:
772:
771:
770:
758:
757:
756:
755:
754:
753:
752:
751:
750:
749:
738:
735:
731:
724:
720:
717:,0,1,+,*: -->
716:
712:
707:
703:
699:
695:
694:
693:
690:
686:
682:
678:
677:
676:
675:
674:
673:
672:
671:
660:
657:
653:
652:
651:
650:
649:
648:
647:
646:
637:
634:
628:
627:
626:
623:
619:
615:
611:
607:
603:
599:
595:
591:
587:
584:
580:
576:
574:
571:
567:
563:
559:
554:
550:
546:
542:
537:
533:
526:
522:
518:
517:
516:
513:
508:
505:
501:
497:
493:
490:
486:
482:
481:
480:
477:
472:
471:
466:
464:
461:
457:
452:
450:
446:
445:
444:
443:
440:
435:
433:
428:
423:
421:
409:
406:
402:
401:
400:
399:
396:
380:
376:
370:
366:
362:
359:
351:
347:
340:
337:
334:
326:
322:
298:
295:
287:
283:
276:
273:
270:
262:
258:
232:
228:
224:
221:
213:
209:
202:
199:
196:
188:
184:
168:
153:
149:
143:
140:
139:
136:
119:
115:
111:
110:
102:
96:
91:
89:
86:
82:
81:
77:
71:
68:
65:
61:
56:
52:
46:
38:
37:
27:
23:
18:
17:
1049:Itaj Sherman
1042:
1015:
1012:
992:
977:Rockyrackoon
964:
945:
935:
913:
904:
899:
895:
887:
879:
820:
813:
809:
805:
804:), with the
801:
797:
793:
789:
785:
781:
722:
714:
710:
708:(2),...: -->
705:
701:
697:
684:
617:
613:
609:
605:
601:
597:
593:
589:
585:
582:
578:
565:
561:
557:
552:encountered.
548:
544:
540:
535:
528:
503:
499:
495:
488:
484:
455:
436:
431:
426:
424:
419:
417:
414:Łoś' theorem
172:
148:Low-priority
147:
107:
73:Low‑priority
51:WikiProjects
34:
123:Mathematics
114:mathematics
70:Mathematics
1065:Categories
918:Trovatore
914:extremely
890:,+,*: -->
845:command.
734:Trovatore
633:Trovatore
512:Trovatore
460:Trovatore
449:Trovatore
405:Trovatore
39:is rated
709:, where
534:, where
520:theorem?
905:element
612:≠1 → 1/
485:theorem
150:on the
41:C-class
524:terms.
489:phrase
47:scale.
948:Dagme
896:using
500:false
395:lethe
28:This
1053:talk
997:Emil
993:only
981:talk
952:talk
821:e.g.
704:(1),
700:(0),
496:true
900:all
880:you
784:to
600:∧ (
562:not
427:all
311:or
142:Low
1067::
1055:)
1000:J.
983:)
954:)
891:).
608:∧
592:∧
510:--
504:is
363:∏
360:∈
338:…
296:∈
274:…
225:∏
222:∈
200:…
1051:(
1024:U
979:(
950:(
888:R
814:n
812:(
810:f
806:n
802:x
800:(
798:f
794:x
792:(
790:f
786:Q
782:Q
715:R
711:r
706:r
702:r
698:r
618:Z
616:∉
614:y
610:y
606:Z
604:∈
602:y
598:Z
596:∈
594:x
590:R
588:⊂
586:Z
583:Z
579:x
577:"
566:x
558:n
549:i
545:i
541:N
536:M
531:i
529:M
456:U
432:I
381:U
377:/
371:i
367:M
357:]
352:n
348:a
344:[
341:,
335:,
332:]
327:1
323:a
319:[
299:M
293:]
288:n
284:a
280:[
277:,
271:,
268:]
263:1
259:a
255:[
233:i
229:M
219:]
214:n
210:a
206:[
203:,
197:,
194:]
189:1
185:a
181:[
154:.
53::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
