wp@iddth.id.dk (Wiesiek Pawlowski (900415#)) (01/25/91)
Maybe somebody could give me some references to the literature or give
me some advise. I have problems in proving decidability of a sequent
calculus formalizing subtype-relation. The system looks as follows:
Type ::= Nat | Type-set | T + T | N
N - type name (an identifier)
Subtype Calculus
formulae are of the form: T1 < T2
sequents are of the form: A |- f ,where f is a formula and A is a set of
formulae.
inference rules:
A |- T < T
T1 < T2,A |- T1 < T2
A |- T1 < T2 ==> A |- T1-set < T2-set
A |- T < T1 ==> A |- T < T1+T2
A |- T < T2 ==> A |- T < T1+T2
A |- T1 < T & A |- T2 < T ==> A |- T1+T2 < T
n < T2,A |- T1 < T2 ==> A |- n < T2 ,where n=T1 is a type definition
A |- T1 < T2 & A |- T2 < T3 ==> A |- T1 < T3
It is the last rule - the rule of transitivity which causes problems.
In a sence some form of "transitivity-elimination" theorem should be
proved. In a reacher type system with more constants and some specific
axioms it would mean that for a given proof tree we are able to "push-down"
all the occurrences of the transitivity rule up to the axioms. But I do not
know how to prove it. Perhaps there exists some well-known strategy
of proving decidability of similar systems? Maybe the system as stated
is undecidable?!
Wiesiek Pawlowski
my e-mail address is wp@id.dth.dk