Wiki

Fundamental Property on PartialOrder

In this section, we prove the following theorem.

Theorem: Let (S,R) be a finite non empty partially ordered set.

Then, there exist an element x∈S such that ∀y∈S・¬(y R x) ###

The claim of this theorem can be represented as follows:

Theorem1 on Partial Order

Let S be an arbitrary partial order on Elt. Then, for all S : Set, if S is not empty, the proposition S [R] S holds.

#!python
module CLAIM1/PARTIALORDER
(
  X :: TRIV,
  S :: SET(X),
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  T :: TRANSITIVE(X,R),
  P :: PARTIALORDER(X,R,I,A,T),
  C :: COMPLEMENT(X,R)
)
{
  imports
  {
    pr(LEMMA1/COMPLEMENT(X,S,R,I,C))
    pr(EXTEND(X,S,R))
  }
  signature
  {
    op r : -> PartialOrder
    op claim : Set -> Prop
  }
  axioms
  {
    vars S : Set
    eq claim(S) = deducible(nil |- (S = nil),(S [r] S)) .
  }
}

Let X, S and R be arbitrary elements such that X : Elt, S : Set and R : PartialOrder. Then, the expression X [R] S means that forall Y containd in S, (Y R X) does not hold, i.e., the sequent ((X [R] S),(Y @ S),(Y R X) |- nil) is deducible. Moreover, let T be also an arbitrary set. Then, T [R] S means that some elements Z exists in T such that Z [R] S. The claim can be represented that the proposition S [R] S is true for any non-empty partially ordered set (S,R).

The chaim in the above module can be shown to be true with structural induction on S.

#!python
-- [initial case]
open CLAIM1/PARTIALORDER .
ops x : -> Elt .
red claim(x) .
close

In the nitial case, claim is trivially true.

#!python
%CLAIM1/PARTIALORDER(X, S, R, I, A, T, P)> 
-- reduce in %CLAIM1/PARTIALORDER(X, S, R, I, A, T, P) : 
    (claim(x)):Prop
(true):Bool
(0.000 sec for parse, 5 rewrites(0.000 sec), 64 matches)

In the nitial case, claim is trivially true.

#!python
%CLAIM1/PARTIALORDER(X, S, R, I, A, T, P)> 
-- reduce in %CLAIM1/PARTIALORDER(X, S, R, I, A, T, P) : 
    (claim(nil)):Prop
(true):Bool
(0.000 sec for parse, 6 rewrites(0.000 sec), 49 matches)

The following proof score shows that the claim is reduced to true even in the induction step.

#!python
-- [induction step]
open CLAIM1/PARTIALORDER .
ops s n : -> Set .
ops x : -> Elt .
eq n = (s,x) .
eq deducible((s = nil) |- nil) = true .
-- hypothisis of induction
eq deducible(nil |- (s = nil),(s [r] s)) = true .

ops q1 q2 q3 q4 q5 q6 : -> Sequent .
-- hypothesis of the case
eq q1 = ((s = nil) |- nil) .
-- lemma on irreflexive relation
eq q2 = (nil |- (x [r] x)) .
-- hypothesis of the induction
eq q3 = (nil |- (s = nil),(s [r] s)) .
-- definitions of extension
eq q4 = ((s [r] s) |- (n [r] s)) .
eq q5 = ((x [r] x) |- (n [r] x)) .
eq q6 = ((n [r] s),(n [r] x) |- (n [r] n)) .
ops i1 i2 i3 i4 : -> Inference .
eq antecedent(i1) = (q1,q3) .
trans (nil |- (s [r] s)) => consequent(i1) .
trans consequent(i1) => (nil |- (s [r] s)) .
eq antecedent(i2) = (consequent(i1),q4) .
trans (nil |- (s,x) [r] s) => consequent(i2) .
trans consequent(i2) => (nil |- (s,x) [r] s) .
eq antecedent(i3) = (q2,q5) .
trans (nil |- (s,x) [r] x) => consequent(i3) .
trans consequent(i3) => (nil |- (s,x) [r] x) .
eq antecedent(i4) = (consequent(i2),consequent(i3),q6) .
eq (nil |- ((s,x) [r] (s,x))) = consequent(i4) . 
red claim(n) .
close

Indeed, the claim is ruduced to true in the following result.

#!python
%CLAIM1/PARTIALORDER(X, S, R, I, A, T, P)> *
-- reduce in %CLAIM1/PARTIALORDER(X, S, R, I, A, T, P) : 
    (claim(n)):Prop

** Found [state 222] (consequent(i4)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 13] (consequent(i3)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 21] (consequent(i2)):Set/Sequent
   {}
-- found required number of solutions 1.

** Found [state 13] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 1721 rewrites(0.710 sec), 119023 matches, 887 memo hits)

Due to this result, we can declare the theorem as the following module:

#!python
module THEOREM1/PARTIALORDER
(
  X :: TRIV,
  S :: SET(X),
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  T :: TRANSITIVE(X,R),
  P :: PARTIALORDER(X,R,I,A,T),
  C :: COMPLEMENT(X,R),
  E :: EXTEND(X,S,R)
)
{
  imports
  {
    pr(LK)
  }
  axioms
  {
    vars S : Set
    vars R : PartialOrder
    eq deducible(nil |- (S = nil),(S [R] S)) = true .
  }
}

Let (S,R) be an arbitrary non-empty partially ordered set. When an element x contained in S satisfies (x [R] S), we call x a root in S concerning on R.

The above theorem says that a non-empty partially ordered set (S,R) has at least one root. So we can declare the operation to extract the set of root element from (S,R).

#!python
module ROOT
(
  X :: TRIV,
  S :: SET(X),
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  T :: TRANSITIVE(X,R),
  P :: PARTIALORDER(X,R,I,A,T)
)
{
  signature
  {
    op  root : Set PartialOrder -> Set
  }
  axioms
  {
    vars X Y : Elt
    vars S : Set
    vars R : PartialOrder
    eq root(nil,R) = nil .
    eq deducible((root(S,R) = nil) |- (S = nil)) = true .
    eq deducible((X @ root(S,R)) |- (X @ S)) =  true .
    eq deducible(((X @ root(S,R)),(Y @ S),(Y R X)) |- nil) =  true .
  }
}