[Agda] Positivity checker

[Peter Hancock]

Sorry to be late replying,  I think I can say a bit better what I mean.

Suppose

   O : Set
   (<) : O -> O -> Set

is some system of ordinal notations (it doesn't matter what exactly).

Then I define

   Omega : O -> Set

by induction.  There are 3 constructors:

   0 : (a : O)-> Omega a
   S : (a : O)-> Omega a -> Omega a
   Sup : (a : O)-> (b : O)->  a < b  ->
         (Omega a -> Omega b) -> Omega b

I claim that

(i) this is, unless I'm confused, evidently OK.  Friedman
    and Feferman show there are quite weak subsystems of classical
    2nd order logic that can build models of a similar
    principle when the order type of (O,<) is w^w and epsilon0.
    (My copy of the paper is in Edinburgh, and I'm in Nottingham,
    so I could be wrong).
(ii) it has a very similar "negativity" to Wouter's data type.
    In some ways even worse.

I don't claim that the soundness of the definition can be
explained without iterating some W-type-like operation along
(O,<) (which requires a universe to iterate into, or
large-elimination, if that is any different).

BTW, I think the principle is a little cleaner if one takes the
ordinal notion system to be given by a (wellfounded) coalgebra:

   O : Set
   T : O -> Set
   n : (a : O)-> T a -> O

when the constructors have type

   0 : (a : O)-> Omega a
   S : (a : O)-> Omega a -> Omega a
   Sup : (a : O)-> (t : T a)->
         (Omega (n a t) -> Omega a) -> Omega a

Peter(H)

^^^^^^^^^^ top posting ^^^^^^^^^^^^^
Peter Dybjer wrote:
> So T is the operation which takes the type of ordinals of the nth number
> class to the type of ordinals of the n+1st number class. And then this
> operation is iterated transfinitely along some well-ordering.
> Type-theoretically, we would probably need to have a T which goes from
> all predecessors, what about
> 
> T : ((x : A) -> B x -> Set) -> Set
> O : W A B-> Set
> 
> O (sup a b) = T(\x y -> O(b y))?
> 
> But wouldn't this still be within the world of strictly postiive data
> types? (Actually how would T be defined?)
> 
> Peter
> 
> 
> 
> On Dec 10, 2008, at 12:33 PM, Peter Hancock wrote:
> 
>> It occurred to me there *is* an inductive definition a bit like
>> Wouter's which has been rather well studied, and exhibits what
>> may be a similar kind of "negativity".
>>
>> In the 60's logicians began to study systems they called ID_{< alpha},
>> where principle that takes you from A to T_A = mu X. 1 -> (A -> X)
>> is iterated a transfinite number of times, along a given wellordering
>> <, typically of order type w^w, or epsilon0.  So you would get a
>> predicate O : (a:Nat) -> (b:Nat) -> Set, where the first argument a
>> is really over the wellordering (here, coded in Nat), and the second b
>> is for things that satisfy the predicate O(a,_).  The crucial
>> thing is that the predicate O(a) is closed under some operation
>> whose operand has type \all n : Nat. O(a',n) -> O(a,{f}n), where a' < a.
>> -- in that case one would have O(a,2^a*3^a'*5^f). [{f}(_) is Kleene
>> application.]  Or something like that.
>>
>> Now this is a bit messy and old-fashioned, and it would need some effort
>> to present it in a manner palatable to you youngsters.  But I mention
>> it in case someone (Peter?) will know what I am referring to, and can
>> make that effort more quickly than me. (The papers I am
>> thinking of straight off are by Feferman, Friedman, and are in the 1968
>> "Buffalo volume".)
>>
>> In those (pre-universe) days, people didn't have much problem in
>> thinking of models of such (transfinitely iterated) g.i.d's.  But
>> perhaps the justification for them was really in terms of a recursive
>> definition along {<} into Set.
>>
>> Hank
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>