[Agda] Positivity checker

[Peter Dybjer]

I agree that this example is analogous to Wouter's.

The question is: what is an "axiom" and what is a "theorem"? I would argue
(not very strongly) that Wouter's introduction rule (and Peter's negative
introduction rule below) is not natural as an axiom; it should  rather be
a theorem. The reason is that it is easy to reduce it to a more natural
axiom.

Ideally, we would like to have a clear collection of axioms, although I
agree that programming practice a la Agda suggests that it is good to have
a
rather generous notion of axiom. We have had this debate many times in
Gothenburg. It still goes on.

Peter

> 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
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>