Is this a formal definition of the maximal element of partially ordered set?

EDITED (Version 4)

In mathematics, especially in order theory, a maximal element of a subset S of some partially ordered set (poset) is an element of S that is not smaller than [?] any other element in S. https://en.wikipedia.org/wiki/Maximal_and_minimal_elements

Is this a formal definition of a maximal element of a partially ordered set $$S$$?

$$\forall S:[\forall a\in S: a\leq a \\ \land \forall a,b\in S:[a\leq b ~\land~ b\leq a \implies a=b]\\ \land \forall a,b,c\in S:[a\leq b ~\land ~b\leq c \implies a\leq c]$$

$$\implies \forall m\in S: [Maximal(S,m) \iff\forall a\in S:[m=a \lor \neg [m\le a]]]]$$

where $$Maximal(S,m)$$ means a maximal element of $$S$$ is $$m$$.

• $\forall a\in S \, : \, a\le m$ is sufficient in the last line. BTW in some topics (e.g. set-theoretic Forcing) a poset may have $b\ne a\le b\le a$ for some $a,b.$ Jun 20, 2021 at 5:13
• There can be several maximal elements. Jun 20, 2021 at 6:36
• @DanielWainfleet: That's rather odd! I'd have called a relation with that sort of property a preorder, rather than a partial order. Jun 20, 2021 at 15:20
• @CameronBuie. Texts on Forcing invariably say Poset. Jun 21, 2021 at 0:28

What you have is instead a formal definition of a maximum or greatest element of $$S.$$
Instead, you want $$m\in S\wedge\neg(\exists a\in S:m\neq a\wedge m\leq a),$$ or equivalently, $$m\in S\wedge\bigl[\forall a\in S, m=a\vee\neg(m\leq a)\bigr].$$
Consider any set $$S$$ with more than one element, and the relation $$R$$ given by $$R=\bigl\{\langle a,a\rangle\mid a\in S\bigr\}.$$ Then $$S$$ is partially-ordered by $$R,$$ and has no greatest element, but all of its elements are maximal.
• So, my last line now should be "$\implies \forall m\in S: [Maximal(S,m) \iff \forall a\in S: [m=a \lor \neg [m\le a]]]$"? Jun 20, 2021 at 15:15
• Can you not write "$a\le m$" instead of "$m=a\vee\neg(m\leq a)$"? Jun 20, 2021 at 15:36
• No, because it is possible in a partial order that $a\not\leq m$ and $m\not\leq a$ are both true, as in the example schema I mentioned in my answer. In a total order, though, $a=m$ or $m\not\leq a$ is equivalent to $a\leq m.$ Jun 20, 2021 at 15:53
• For any partial ordering $\le$, can we define $a\le b \iff a\lt b \lor a=b$ and $a\lt b \iff a\le b ~\land ~ a\neq b$? Jun 20, 2021 at 17:43