Notes

Description: Definitions from constructive order theory

Content:

Definitions from constructive order theory} (for forms [0 AT], [0 AU], [1 DH], [1 DI], [1 DJ], [67 AB], [67 AC], [144 B] through [144 M] and Form 413 through Form 416.

Definition: A subset selection \(\cal Z\) is a (class) function defined on the class of all partial orderings such that if \((P,\le)\) is a partial ordering then \(\cal Z (P,\le)\) (or \(\cal Z P\) for short) is a subset of \()\cal P(P)\).  The subset selection \(\cal Z\) is a subset system if for any two partial orderings \((P_1,\le_1)\) and \((P_2,\le_2)\) if \(f:P_1\to P_2\) is order preserving then for all \(Z\in \cal Z P_1\), \(f[Z]\in \cal Z P_2\).

In Ern\'e [2001] the following subset selectors are considered

  1. \(\cal A P = \cal P(P)\) (arbitrary subsets of \(P\))
  2. \(\cal B P = \) one or two element subsets of \(P\)
  3. \(\cal C P = \) all non-empty chains in \((P,\le)\)
  4. \(\cal D P = \) all directed subsets in \((P,\le)\)
    5. (\(Z\subseteq P\) is directed by \(\le\) if any two elements of \(Z\) have a common upper bound.)
  5. \(\cal E P = \) all one element subsets of \(P\)
  6. \(\cal F P = \) all finite subsets of \(P\)
  7. \(\cal W P = \) all non-empty subsets of \(P\) well ordered by \(\le\).
  8. \(\cal U P = \) all \(U\subseteq P\) such that \(\forall x,y\in U\), \(x\lor y\) exists in \(P\) and is in \(U = \) all \(\bigvee\)-subsemilattices of \(P\).

Note that all of the above except \(\cal U\) are subset systems.

Definition: Assume \((P\le)\) is a partially ordered set and \(\cal Z\) is a subset selection.

  1. \((P,\le)\) is \(\cal Z\)-complete (or \(\cal Z\)-\(\bigvee\)-complete) if every element \(Z\) of \(\cal Z\) has a \(\sup\) (denoted \(\bigvee Z\) or \(\bigvee_P Z\)).
  2. A subset \(X\) of \(P\) is \(\cal Z\)-subcomplete if each \(Z\in \cal Z\cap \cal P(X)\) has a supremum \(s\) in \(P\) that is contained in \(X\)
  3. If \(Y\subset P\) then \(s\) is a constructive supremum of \(Y\) if either \(Y = \emptyset\) and \(s\) is the least element of \(P\) (if it exists) or \(s\) is an upper bound of \(Y\) and there is a function \(\psi:P\to Y\) such that \((\forall x\in P)(s \nleq x \leftrightarrow \psi(x) \nleq x)\).
  4. \((P,\le)\) is constructively \(\cal Z\)-complete if each \(Z\in \cal Z P\) has a constructive supremum.
  5. A constructively complete lattice is a complete lattice in which every supremum is constructive.
  6. \(\cal Z^\lor\) is the class function whose domain is the class of all partial orderings and which is defined by \[ \cal Z^\lor P = \{ Y\subseteq P : (\forall x\in Y)(\forall z\in P)(z\le x\to z\in Y)\mathrm{\; and \;}\\ (\forall Z\in \cal P(Y)\cap \cal Z P)(\mathrm{\; If \;}x =\bigvee_P Y \mathrm{ \; then \;} x\in Y \} \]
  7. \((P,\le)\) is constructively directed if there is a function assigning an upper bound to each non-empty finite subset of \(P\).
  8. If \(S\) is a set and \(\cal X \subseteq \cal P(S)\) then \(\cal X\) is \(\cal Z\)-inductive (or \(\cal Z\)-union complete if for each \(\cal Y\in \cal Z\cal X\), \(\bigcup \cal Y \in \cal X\).
  9. \(^c\cal D P\) (or \(^c\cal D (P,\le)\)) is the system of all constructively directed subsets of \(P\).
  10. If \(S\) is a set and \(\cal X\subseteq \cal P(S)\) then \(\cal X\) is a closure system (on \(S\)) if \(\cal X\) is closed under arbitrary intersections (with \(\bigcap\emptyset = S\)).
  11. An element \(x\) of a \(\cal Z\)-complete poset \(P\) is \(\cal Z\)-compact if for all \(Z\in\cal Z P\), if \(x\le \bigvee Z\), then \(x\in \downarrow Z\). (\(\downarrow Z = \{t\in P : (\exists y\in Z)(t\le y)\}\). The \()\cal D\)-compact elements are called the compact elements.
  12. A \(\cal Z\)-complete poset is \(\cal Z\)-compactly generated if each of its elements is a supremum of \(\cal Z\)-compact elements.
  13. An algebraic lattice is a \(\cal D\)-compactly generated complete lattice.
  14. If \(S\) is a set and \(\cal X\subseteq \cal P(S)\) then \(\cal X\) is a system of finite character for all \(X\), \(X\in \cal X \Leftrightarrow \cal F X\subseteq \cal X\)
  15. A Scott closed subset of \(P\) is an element of \(\cal D^\lor P\).
  16. A map \(\phi:P\to Q\) between posets preserves \(\cal Z\)-suprema if for each \(Z\in \cal Z P\) having a supremum \(s\), the image \(\phi(s)\) is the supremum of \(\phi[Z]\).
  17. A \(\cal Z\)-frame is a complete lattice in which the distributive law \(x\land \bigvee Z = \bigvee(x\land Z)\) holds for all \(x\in P\) and all \(Z\in\cal Z P\).

Howard-Rubin number: 154

Type: Definitions

Back