Wiki

THEOREM1/PARTIALORDER

For any non-empty arbitrary partially ordered set (S,R), the proposition (S [R] S) holds.

The following module describes this claim.

#!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)) .
  }
}

This claim is proved with structural induction on S using LEMMA1/COMPLEMENT. The proof score is:

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

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

The result of the execution of the above score is:

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

-- opening module CLAIM1/PARTIALORDER(X, S, R, I, A, T, P, C).. done.
___*
-- reduce in %CLAIM1/PARTIALORDER(X, S, R, I, A, T, P, C) : 
    (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(1.300 sec), 119023 matches, 887 memo hits)

So, we obtain the following theorem.

#!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 .
  }
}

EXISTENCE of ROOT ELEMENTS

Let (S,R) be an arbitrary partially ordered set. We call x is a root element of (S,R) if:

x∈S
∀y∈S・¬(y R x)

The latter contition can be described as (x R S).

This claim represents that the existence of a root element of (S,R).

#!python
module CLAIM/EXISTENCE/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),
  C :: COMPLEMENT(X,R),
  E :: EXTEND(X,S,R)
)
{
  imports
  {
--  pr(THEOREM1/PARTIALORDER(X,S,R,I,A,T,P,C,E))
    pr(LEMMA1/COMPLEMENT(X,S,R,I,C))
    pr(LEMMA2/COMPLEMENT(X,S,R,A,C))
    pr(LEMMA3/COMPLEMENT(X,S,R,T,C,E))
  }
  signature
  {
    ops w s : -> Set
    op r : -> PartialOrder
    op x : -> Elt
    op exist : Set Set PartialOrder -> Prop
    op claim : Set -> Prop
  }
  axioms
  {
    vars X : Elt
    vars S C : Set
    vars R : PartialOrder
    cq deducible((X [R] S) |- exist(X,S,R)) = true
       if ((X @ S) = true) .
    eq deducible((X @ S) |- (X @ (S,C))) = true .
    eq deducible(exist(C,S,R) |- exist((C,X),S,R)) = true .
    eq claim(S) = deducible(nil |- exist(w,S,r)) .
  }
}

This claim is proved with structural induction on S.

#!python
-- [base case]
-- s is a singleton, i.e., s = {x} for some x.
open CLAIM/EXISTENCE/ROOT .
eq s = x .
ops i : -> Inference .
ops q1 q2 : -> Sequent .
eq q1 = (nil |- (x [r] s)) .
eq q2 = ((x [r] s) |- exist(x,s,r)) .
eq antecedent(i) = (q1,q2) .
eq (nil |- exist(x,x,r)) = consequent(i) .
eq w = s .
red claim(s) .
close

-- [induction step]
-- Let (s,r) be an arbitrary partially ordered set.
-- Then, s has an element x such that x is a root of (s,r).
open CLAIM/EXISTENCE/ROOT .
eq (x @ s) = true .
eq deducible(nil |- (x [r] s)) = true .
ops y : -> Elt .
ops n : -> Set .
eq n = (s,y) .
eq (y @ s) = false .
eq (x = y) = false .

ops q0 q1 q2 q3 q4 q5 q6 q7 q8 q9 : -> Sequent .
-- hypothesis of induction
eq q0 = (nil |- x [r] s) .
-- lemma1/complement
eq q1 = (nil |- y [r] y) .
-- lemma2/complement
eq q2 = (nil |- (x [r] y),(y r x)) .
-- lemma3/complement
eq q3 = ((y r x), (x [r] s) |- (y [r] s)) .
-- definition in the module EXTEND
eq q4 = ((x [r] y), (x [r] s) |- (x [r] n)) .
eq q5 = ((y [r] y), (y [r] s) |- (y [r] n)) .
-- axioms on existence of a root of (n,r)
eq q6 = ((x [r] n) |- exist(x,n,r)) .
eq q7 = ((y [r] n) |- exist(y,n,r)) .
-- if x is a root of (n,r), then a root of (n,r) exists in w
eq q8 = (exist(x,n,r) |- exist(w,n,r)) .
-- if y is a root of (n,r), then a root of (n,r) exists in w
eq q9 = (exist(y,n,r) |- exist(w,n,r)) .
ops i1 i2 : -> Inference .
eq antecedent(i1) = (q0,q4) .
trans ((x [r] y) |- (x [r] (s,y))) => consequent(i1) .
trans consequent(i1) => ((x [r] y) |- (x [r] (s,y))) .
eq antecedent(i2) = (consequent(i1),q6,q8) .
trans ((x [r] y) |- exist((x,y),(s,y),r)) => consequent(i2) .
trans consequent(i2) => ((x [r] y) |- exist((x,y),(s,y),r)) .
ops i3 i4 i5 : -> Inference .
eq antecedent(i3) = (q0,q3) .
trans ((y r x) |- (y [r] s)) => consequent(i3) .
trans consequent(i3) => ((y r x) |- (y [r] s)) .
eq antecedent(i4) = (consequent(i3),q1,q5) .
trans ((y r x) |- (y [r] (s,y))) => consequent(i4) .
trans consequent(i4) => ((y r x) |- (y [r] (s,y))) .
eq antecedent(i5) = (consequent(i4),q7,q9) .
trans ((y r x) |- exist((x,y),(s,y),r)) => consequent(i5) .
trans consequent(i5) => ((y r x) |- exist((x,y),(s,y),r)) .
ops i6 : -> Inference .
eq antecedent(i6) = (q2,consequent(i2),consequent(i5)) .
eq (nil |- exist((x,y),(s,y),r)) = consequent(i6) .

-- w is a set including x and y
eq w = (x,y) .
red claim(n) .
close

The result of the execution of the above score is:

#!python
-- opening module CLAIM/EXISTENCE/ROOT(E, X, S, R, I, A, T, P, C, E).. done.
_*
-- reduce in %CLAIM/EXISTENCE/ROOT(E, X, S, R, I, A, T, P, C, E) : 
    (claim(s)):Prop

** Found [state 3] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 44 rewrites(0.000 sec), 314 matches, 1 memo hits)

-- opening module CLAIM/EXISTENCE/ROOT(E, X, S, R, I, A, T, P, C, E).. done.
_____*
-- reduce in %CLAIM/EXISTENCE/ROOT(E, X, S, R, I, A, T, P, C, E) : 
    (claim(n)):Prop

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

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

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

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

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

** Found [state 28] (consequent(i1)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 14126 rewrites(9.670 sec), 987707 matches, 7142 memo hits)

ROOT

So, we obtain the following module where an operation which returns a set of root elements of given non-empty partially ordered set.

#!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 .
  }
}