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 , i.e. a quantity canโt be smaller than itself Proof If , then acyclicity is broken
Note: โnonreflexiveโ is not not reflexive
Prop partial order ==> () Proof If then , this contradicts to nonreflexive of partial order
Def
Prop Assume is a partial order, then
Proof
But partial order satisfy , so
so
Prop Assume is a partial order, then Proof
But partial order satisfy
Proof <== is obvious. For ==>, assume . If then because , we have . If then
so
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 := (lt form) or (lte form) :=
[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 zorn_lemma.ac in my github repo ac-math ref_30