[TYPES] Re: Reg Axioms of pure type systems

[Param Jyothi Reddy]

As Thorsten pointed out PTS does not impose such conditiosn but the
point being we might loose consistency. Any necessary and sufficient
conditions on A and R to ensure that PTS is consistent?

Also am i correct in assuming "consistency iff Strong normalization"?

Param


On Mon, 27 Dec 2004 08:34:28 +0530, Param Jyothi Reddy <paramr at gmail.com> wrote:
> Hi all,
> I have a doubt regarding the pure type systems.  Let it be (S, A, R)
> 
> In A we have sorting relation on the sorts (s_1:s_2 kind of data). Are
> there any conditions on these? (Not like functional or injective but
> more inherent for arbitrary PTS).
> 
> Like for example is circularity allowed (s_1:s_2 and s_2:s_1)?
> 
> Regards,
> Param
>