494:'s algebraic approach). There are interesting theorems that concern a set of deductive systems being a directed-complete partial ordering. Also, a set of deductive systems can be chosen to have a least element in a natural way (so that it can be also a pointed dcpo), because the set of all consequences of the empty set (i.e. “the set of the logically provable/logically valid sentences”) is (1) a deductive system (2) contained by all deductive systems.
223:
709:
631:
735:
657:
878:
1149:
135:
918:
898:
843:
560:
536:
507:
has a supremum. As a corollary, an ordered set is a pointed dcpo if and only if every (possibly empty) chain has a supremum, i.e., if and only if it is
266:
of the respective (approximative) computations. This intuition, in the context of denotational semantics, was the motivation behind the development of
262:
Requiring the existence of directed suprema can be motivated by viewing directed sets as generalized approximation sequences and suprema as
1041:
Tarski, Alfred: BizonyĂtás Ă©s igazság / Válogatott tanulmányok. Gondolat, Budapest, 1990. (Title means: Proof and truth / Selected papers.)
421:.) This order is a pointed dcpo, where the least element is the nowhere-defined partial function (with empty domain). In fact, ≤ is also
1293:
285:
1303:
1186:
1026:
928:
Directed completeness alone is quite a basic property that occurs often in other order-theoretic investigations, using for instance
1157:
94:
and every pair of elements has an upper bound in the subset.) In the literature, dcpos sometimes also appear under the label
1144:
920:
has a fixed point. This theorem, in turn, can be used to prove that Zorn's lemma is a consequence of the axiom of choice.
487:
281:. However, this concept occurs far less frequently in practice, since one usually can work on the dual order explicitly.
508:
44:
163:
940:
40:
1170:
1189:, where the Knaster–Tarski theorem, formulated over pointed dcpo's, is given to prove as exercise 4.3-5 on page 90.
815:
1250:
773:
1083:
330:
can be turned into a pointed dcpo by adding a least element ⊥ and introducing a flat order with ⊥ ≤
776:
746:
575:
443:
312:
274:
48:
664:
1322:
822:
36:
1066:
601:
504:
472:
429:
374:
308:
288:
of a partially ordered set, every partially ordered set can be extended uniquely to a minimal dcpo.
418:
146:
714:
636:
1227:
993:
465:
848:
1299:
1182:
1022:
795:
742:
1289:
1259:
1211:
1199:
977:
591:
539:
483:
422:
350:
320:
301:
256:
233:
17:
1271:
1223:
989:
120:
1267:
1219:
1153:
1140:
1054:
1010:
985:
929:
512:
450:
425:. This example also demonstrates why it is not always natural to have a greatest element.
315:, is a dcpo. Together with the empty filter it is also pointed. If the order has binary
145:
is also used, because of the characterization of pointed dcpos as posets in which every
968:
Markowsky, George (1976), "Chain-complete posets and directed sets with applications",
944:
933:
903:
883:
828:
750:
545:
521:
1316:
1231:
491:
316:
267:
237:
225:) has a supremum that belongs to the poset. The same notion can be extended to other
114:
52:
1050:
997:
240:
is also a dcpo (with the same basis). An ω-cpo (dcpo) with a basis is also called a
436:
83:
1120:
476:
461:
226:
28:
1173:
sometimes referred to as "Pataraia’s theorem". For example, see
Section 4.1 of
772:
is pointed. Thus the complete partial orders with Scott-continuous maps form a
35:
is variously used to refer to at least three similar, but distinct, classes of
1245:
1174:
1014:
490:
closed under consequence (for defining notion of consequence, let us use e.g.
1263:
1181:(1987), 2nd edition, Jacques Loeckx and Kurt Sieber, John Wiley & Sons,
765:
454:
137:). Formulated differently, a pointed dcpo has a supremum for every directed
91:
1175:"Realizability at Work: Separating Two Constructive Notions of Finiteness"
595:
if it maps directed sets to directed sets while preserving their suprema:
563:
87:
319:, then this construction (including the empty filter) actually yields a
1215:
981:
232:
Every dcpo is an ω-cpo, since every ω-chain is a directed set, but the
432:
794:
is continuous then this fixed-point is equal to the supremum of the
393:
agree on all inputs for which they are both defined. (Equivalently,
845:
is a function from a dcpo to itself with the property that
503:
An ordered set is a dcpo if and only if every non-empty
277:
notion of a directed-complete partial order is called a
939:
Directed completeness relates in various ways to other
741:
Note that every continuous function between dcpos is a
756:
The set of all continuous functions between two dcpos
71:, has several possible meanings depending on context.
906:
886:
851:
831:
717:
667:
639:
604:
548:
524:
166:
123:
90:. (A subset of a partial order is directed if it is
1084:"Iwamura's Lemma, Markowsky's Theorem and ordinals"
912:
892:
872:
837:
745:. This notion of continuity is equivalent to the
729:
703:
651:
625:
554:
530:
217:
129:
218:{\displaystyle x_{1}\leq x_{2}\leq x_{3}\leq ...}
43:. Complete partial orders play a central role in
1021:. Oxford: Clarendon Press. Prop 2.2.14, pp. 20.
963:
961:
959:
686:
674:
1298:(Second ed.). Cambridge University Press.
1019:Handbook of Logic in Computer Science, volume 3
1248:(1951), "Beweisstudien zum Satz von M. Zorn",
1177:(2016) by Bezem et al. See also Chapter 4 of
1146:The lambda calculus, its syntax and semantics
768:, this is again a dcpo, and pointed whenever
8:
1082:Goubault-Larrecq, Jean (February 23, 2015).
160:). These are posets in which every ω-chain (
1119:Goubault-Larrecq, Jean (January 28, 2018).
1065:See online in p. 24 exercises 5–6 of §5 in
905:
885:
850:
830:
716:
666:
638:
603:
547:
523:
236:is not true. However, every ω-cpo with a
197:
184:
171:
165:
122:
307:For any poset, the set of all non-empty
297:Every finite poset is directed complete.
1179:The foundations of program verification
955:
538:is a pointed dcpo if and only if every
251:is never used to mean a poset in which
103:pointed directed-complete partial order
255:subsets have suprema; the terminology
570:Continuous functions and fixed-points
417:are identified with their respective
7:
1069:
1202:(1949), "Sur le théorème de Zorn",
821:Another fixed point theorem is the
704:{\displaystyle f(\sup D)=\sup f(D)}
1295:Introduction to Lattices and Order
124:
25:
790:, ⊥) has a least fixed-point. If
782:Every order-preserving self-map
1169:This is a strengthening of the
764:is denoted . Equipped with the
633:is directed for every directed
626:{\displaystyle f(D)\subseteq Q}
279:filtered-complete partial order
76:directed-complete partial order
861:
855:
698:
692:
680:
671:
614:
608:
518:Alternatively, an ordered set
39:, characterized by particular
1:
1108:. Harper and Row. p. 33.
1055:A Course in Universal Algebra
457:sets, ordered by restriction.
381:is a subset of the domain of
346:and no other order relations.
286:Dedekind–MacNeille completion
74:A partially ordered set is a
730:{\displaystyle D\subseteq P}
652:{\displaystyle D\subseteq P}
244:ω-cpo (or continuous dcpo).
152:A related notion is that of
143:chain-complete partial order
45:theoretical computer science
18:Chain-complete partial order
814:(⊥), …) of ⊥ (see also the
357:can be ordered by defining
304:are also directed complete.
1339:
873:{\displaystyle f(x)\geq x}
816:Kleene fixed-point theorem
259:is used for this concept.
1251:Mathematische Nachrichten
1053:and H.P. Sankappanavar:
154:ω-complete partial order
109:, sometimes abbreviated
1264:10.1002/mana.3210040138
468:, ordered by inclusion.
449:The set of all partial
41:completeness properties
1171:Knaster–Tarski theorem
914:
894:
874:
839:
747:topological continuity
731:
705:
653:
627:
556:
532:
249:complete partial order
219:
131:
65:complete partial order
49:denotational semantics
37:partially ordered sets
33:complete partial order
1210:(6): 434–437 (1951),
1204:Archiv der Mathematik
1017:, Maibaum TS (1994).
915:
895:
875:
840:
823:Bourbaki-Witt theorem
732:
706:
654:
628:
557:
533:
511:. Proofs rely on the
482:Let us use the term “
220:
132:
130:{\displaystyle \bot }
1121:"Markowsky or Cohn?"
1068:. Or, on paper, see
904:
884:
849:
829:
715:
665:
637:
602:
546:
522:
473:specialization order
430:linearly independent
284:By analogy with the
164:
121:
113:), is a dcpo with a
1104:Cohn, Paul Moritz.
970:Algebra Universalis
786:of a pointed dcpo (
711:for every directed
453:on a collection of
1216:10.1007/bf02036949
1152:2004-08-23 at the
982:10.1007/bf02485815
945:chain completeness
910:
890:
870:
835:
825:, stating that if
727:
701:
649:
623:
592:(Scott) continuous
581:between two dcpos
552:
528:
385:and the values of
353:on some given set
334:and s ≤
215:
127:
1200:Bourbaki, Nicolas
1106:Universal Algebra
1051:Stanley N. Burris
913:{\displaystyle f}
893:{\displaystyle x}
838:{\displaystyle f}
743:monotone function
555:{\displaystyle P}
531:{\displaystyle P}
499:Characterizations
351:partial functions
302:complete lattices
141:subset. The term
117:(usually denoted
96:up-complete poset
82:) if each of its
16:(Redirected from
1330:
1309:
1290:Priestley, H. A.
1276:
1274:
1242:
1236:
1234:
1196:
1190:
1167:
1161:
1141:Barendregt, Henk
1138:
1132:
1131:
1129:
1127:
1116:
1110:
1109:
1101:
1095:
1094:
1092:
1090:
1079:
1073:
1063:
1057:
1048:
1042:
1039:
1033:
1032:
1007:
1001:
1000:
965:
943:notions such as
930:algebraic posets
919:
917:
916:
911:
899:
897:
896:
891:
879:
877:
876:
871:
844:
842:
841:
836:
774:cartesian closed
736:
734:
733:
728:
710:
708:
707:
702:
658:
656:
655:
650:
632:
630:
629:
624:
561:
559:
558:
553:
540:order-preserving
537:
535:
534:
529:
484:deductive system
451:choice functions
423:bounded complete
321:complete lattice
313:subset inclusion
257:complete lattice
224:
222:
221:
216:
202:
201:
189:
188:
176:
175:
149:has a supremum.
136:
134:
133:
128:
84:directed subsets
21:
1338:
1337:
1333:
1332:
1331:
1329:
1328:
1327:
1313:
1312:
1306:
1287:
1284:
1279:
1244:
1243:
1239:
1198:
1197:
1193:
1168:
1164:
1154:Wayback Machine
1139:
1135:
1125:
1123:
1118:
1117:
1113:
1103:
1102:
1098:
1088:
1086:
1081:
1080:
1076:
1064:
1060:
1049:
1045:
1040:
1036:
1029:
1009:
1008:
1004:
967:
966:
957:
953:
926:
902:
901:
882:
881:
847:
846:
827:
826:
810: (⊥)), …
766:pointwise order
749:induced by the
713:
712:
663:
662:
635:
634:
600:
599:
572:
544:
543:
520:
519:
513:axiom of choice
501:
460:The set of all
428:The set of all
401:if and only if
365:if and only if
349:The set of all
294:
193:
180:
167:
162:
161:
119:
118:
61:
23:
22:
15:
12:
11:
5:
1336:
1334:
1326:
1325:
1315:
1314:
1311:
1310:
1304:
1283:
1280:
1278:
1277:
1237:
1191:
1162:
1133:
1111:
1096:
1074:
1058:
1043:
1034:
1027:
1002:
954:
952:
949:
934:Scott topology
925:
922:
909:
889:
869:
866:
863:
860:
857:
854:
834:
751:Scott topology
739:
738:
726:
723:
720:
700:
697:
694:
691:
688:
685:
682:
679:
676:
673:
670:
660:
648:
645:
642:
622:
619:
616:
613:
610:
607:
571:
568:
551:
527:
509:chain-complete
500:
497:
496:
495:
486:” as a set of
480:
469:
458:
447:
426:
373:, i.e. if the
347:
324:
305:
298:
293:
290:
214:
211:
208:
205:
200:
196:
192:
187:
183:
179:
174:
170:
126:
67:, abbreviated
60:
57:
24:
14:
13:
10:
9:
6:
4:
3:
2:
1335:
1324:
1321:
1320:
1318:
1307:
1305:0-521-78451-4
1301:
1297:
1296:
1291:
1288:Davey, B.A.;
1286:
1285:
1281:
1273:
1269:
1265:
1261:
1257:
1253:
1252:
1247:
1241:
1238:
1233:
1229:
1225:
1221:
1217:
1213:
1209:
1205:
1201:
1195:
1192:
1188:
1187:0-471-91282-4
1184:
1180:
1176:
1172:
1166:
1163:
1159:
1158:North-Holland
1155:
1151:
1148:
1147:
1142:
1137:
1134:
1122:
1115:
1112:
1107:
1100:
1097:
1085:
1078:
1075:
1071:
1067:
1062:
1059:
1056:
1052:
1047:
1044:
1038:
1035:
1030:
1028:9780198537625
1024:
1020:
1016:
1012:
1006:
1003:
999:
995:
991:
987:
983:
979:
975:
971:
964:
962:
960:
956:
950:
948:
946:
942:
937:
935:
931:
923:
921:
907:
887:
867:
864:
858:
852:
832:
824:
819:
817:
813:
809:
805:
801:
797:
793:
789:
785:
780:
778:
775:
771:
767:
763:
759:
754:
752:
748:
744:
724:
721:
718:
695:
689:
683:
677:
668:
661:
646:
643:
640:
620:
617:
611:
605:
598:
597:
596:
594:
593:
588:
584:
580:
577:
569:
567:
565:
549:
541:
525:
516:
514:
510:
506:
498:
493:
492:Alfred Tarski
489:
485:
481:
478:
474:
470:
467:
463:
459:
456:
452:
448:
445:
442:, ordered by
441:
438:
434:
431:
427:
424:
420:
416:
412:
408:
405: ⊆
404:
400:
397: ≤
396:
392:
388:
384:
380:
376:
372:
368:
364:
361: ≤
360:
356:
352:
348:
345:
341:
337:
333:
329:
325:
322:
318:
314:
311:, ordered by
310:
306:
303:
299:
296:
295:
291:
289:
287:
282:
280:
276:
271:
269:
268:domain theory
265:
260:
258:
254:
250:
245:
243:
239:
235:
230:
228:
227:cardinalities
212:
209:
206:
203:
198:
194:
190:
185:
181:
177:
172:
168:
159:
155:
150:
148:
144:
140:
116:
115:least element
112:
108:
104:
99:
97:
93:
89:
85:
81:
77:
72:
70:
66:
58:
56:
54:
53:domain theory
50:
46:
42:
38:
34:
31:, the phrase
30:
19:
1323:Order theory
1294:
1255:
1249:
1240:
1207:
1203:
1194:
1178:
1165:
1145:
1136:
1124:. Retrieved
1114:
1105:
1099:
1087:. Retrieved
1077:
1061:
1046:
1037:
1018:
1005:
976:(1): 53–68,
973:
969:
941:completeness
938:
927:
820:
811:
807:
803:
802: (⊥),
799:
791:
787:
783:
781:
769:
761:
757:
755:
740:
590:
586:
582:
578:
573:
562:has a least
542:self-map of
517:
502:
462:prime ideals
439:
437:vector space
414:
410:
406:
402:
398:
394:
390:
386:
382:
378:
370:
366:
362:
358:
354:
343:
339:
335:
331:
327:
283:
278:
272:
263:
261:
252:
248:
246:
241:
231:
229:of chains.
157:
153:
151:
142:
138:
110:
107:pointed dcpo
106:
102:
100:
95:
79:
75:
73:
68:
64:
62:
32:
26:
1258:: 434–438,
1246:Witt, Ernst
477:sober space
59:Definitions
29:mathematics
1282:References
1126:January 6,
1089:January 6,
1011:Abramsky S
589:is called
479:is a dcpo.
338:for every
326:Every set
247:Note that
242:continuous
1232:117826806
1070:Tar:BizIg
1015:Gabbay DM
865:≥
722:⊆
644:⊆
618:⊆
488:sentences
455:non-empty
444:inclusion
204:≤
191:≤
178:≤
125:⊥
92:non-empty
63:The term
1317:Category
1292:(2002).
1150:Archived
998:16718857
932:and the
924:See also
880:for all
806: (
796:iterates
777:category
576:function
564:fixpoint
369:extends
292:Examples
234:converse
139:or empty
88:supremum
1272:0039776
1224:0047739
990:0398913
900:, then
475:of any
433:subsets
309:filters
1302:
1270:
1230:
1222:
1185:
1160:(1984)
1025:
996:
988:
419:graphs
409:where
375:domain
264:limits
86:has a
1228:S2CID
994:S2CID
951:Notes
505:chain
464:of a
435:of a
317:meets
238:basis
158:ω-cpo
147:chain
47:: in
1300:ISBN
1183:ISBN
1128:2024
1091:2024
1023:ISBN
798:(⊥,
760:and
585:and
471:The
466:ring
413:and
389:and
300:All
275:dual
273:The
111:cppo
80:dcpo
51:and
1260:doi
1212:doi
978:doi
947:.
818:).
687:sup
675:sup
377:of
342:in
253:all
69:cpo
27:In
1319::
1268:MR
1266:,
1254:,
1226:,
1220:MR
1218:,
1206:,
1156:,
1143:,
1013:,
992:,
986:MR
984:,
972:,
958:^
936:.
779:.
753:.
574:A
566:.
515:.
270:.
101:A
98:.
55:.
1308:.
1275:.
1262::
1256:4
1235:.
1214::
1208:2
1130:.
1093:.
1072:.
1031:.
980::
974:6
908:f
888:x
868:x
862:)
859:x
856:(
853:f
833:f
812:f
808:f
804:f
800:f
792:f
788:P
784:f
770:Q
762:Q
758:P
737:.
725:P
719:D
699:)
696:D
693:(
690:f
684:=
681:)
678:D
672:(
669:f
659:.
647:P
641:D
621:Q
615:)
612:D
609:(
606:f
587:Q
583:P
579:f
550:P
526:P
446:.
440:V
415:g
411:f
407:g
403:f
399:g
395:f
391:g
387:f
383:g
379:f
371:f
367:g
363:g
359:f
355:S
344:S
340:s
336:s
332:s
328:S
323:.
213:.
210:.
207:.
199:3
195:x
186:2
182:x
173:1
169:x
156:(
105:(
78:(
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.