order - note-math

Binary relation := Propositional function or a subset of

when it's called is independent

-ary relation is similar

[order]

Propositional function is an order :=

Transitive:
Acyclic:

Can also use the "equivalent" version

Transitivity:
Reflexivity
Antisymmetry

Equivalence means

If we first have the version of partial order, then define , we get the version of partial order, and it can be converted back to (converting back is not obvious and requires the properties of partial order to prove, same below)
If we first have the version of partial order, then define , we get the version of partial order, and it can be converted back to

Prop partial order ==> irreflexive Proof If , then acyclicity is broken

Note: "nonreflexive" is not not reflexive

Prop partial order ==> ( ) Proof If then

Def

Prop Assume is a partial order, then

Proof

But partial order ==> , so

Prop Assume is a partial order, then Proof

But partial order ==>

Proof <== is obvious. For ==>, assume . If then because , we have . If then

Prop (Proof does not require partial order properties of )

is reflexive
is irreflexive

Prop Acyclicity of ==> Antisymmetry of

Prop Antisymmetry of ==> Acyclicity of

Prop Transitivity of ==> Transitivity of

Prop Transitivity of + Antisymmetry ==> Transitivity of

These propositions together prove the equivalence of partial orders

Example

Subset "inclusion" or "inclusion and not equal to" is an order

image modified from wiki media about partial order
of
Tree diagram

[order-comparable] comparable :=

[comparable-component] is comparable-component :=

Partial order can be decomposed into comparable-components that are not comparable to each other. Imagine two tree diagrams that have no relation

[linear-order] linear order

Intuitively, a linear order has no branches, also called a "chain"

[maximal-linear-order] Maximal linear order chain

let with linear order. is maximal-linear-order := the following definitions are equivalent

It cannot be used to decompose partial orders. Two maximal linear order chains can have intersecting parts

Equivalently,

chain cannot be extended

The extension of chain means there exists and , such that for every , . After extension, is also a chain

[maximal-linear-order-exists] maximal-linear-order chain alaways exists

Also known as the Zorn Lemma

Requires Axiom of Choice: If it can be proven that some sets (of a certain type) have elements with a certain property, then a function can be defined that maps these sets to the corresponding elements.

Proof (ref-29) (ported from formal proof in zorn_lemma.ac in my github repo ac-math ref-30)

We can use the partial order of all intervals in as an intuitive example. An interval chain means that for every interval , either or

Assume there are no maximal chains, then every chain is extendable

According to the axiom of choice, an extension function can be constructed with domain and range , where is the extension element

Def The " " or "successor" of a chain is

Def Comparability between chains is defined as or

Def A set of comparable chains, or a linear set of chains .

Prop The union of elements of a linear chain set is a chain in , i.e.,

Proof

For each , there exist such that .

If , then are comparable

Def An inductive chain set and satisfies,

Contains the zero element or inductive initial element.
Contains "+1". For each , its successor also
The union of a linear chain set is also an inductive chain. If is a linear chain set , then

Seems similar to "strong induction" for : (for , is true ==> is true) ==> for all , is true

Prop Inductive chain sets exist. The set of all chains satisfies all properties required for

Def Minimal inductive chain set :=

Prop is an inductive chain set

Proof Prove that the properties of inductive chain sets are closed under intersection

Zero element.

belongs to every , and thus also to

For each chain

For each

Thus

Strong Induction

Let be a linear chain

For each

Thus

Def Comparable chains in the set of minimal inductive chains and satisfies

For each , they are chain-comparable

Prop is a set of inductive chains

Thus
Thus

Proof

Zero element

The empty chain is a comparable chain because other chains, so

. If is a comparable chain, then is also a comparable chain

Prop For , if , then

Proof is a comparable chain, so are comparable. . By contradiction, assume leads to a contradiction

Since is what we need to prove, we need to bypass it

Def Let be a comparable chain, is defined as and satisfies

Prop is an inductive set

Proof

Zero element
"+1"

Let

If , as stated before
If , then and thus
If , then

Thus or

Thus

Strong induction

Let

For , take such that

==>

Thus

Back to proving the property of , proving

For

If Then according to the definition of ,

Thus or

Thus

Strong induction

Let and

For

If for every , , then
If there exists a such that , then

Thus are comparable, hence

Prop is a set of linear chains

Proof Using

the properties of , and

Thus, the smallest inductive chain set is also a set of linear chains

Prop

Prop is a chain

Prop is a maximal chain

Proof

Define

Assume is not a maximal chain

By the properties of inductive chain sets,

, so

That is,

This contradicts , according to the definition of the chain extension function