[TYPES] decidability vs completeness

[Paul Levy]

On 23 Aug 2014, at 00:42, Paul Levy wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list 
>  ]
>
> Dear colleagues,
>
> I would like to present a polemic for your consideration.
>
> Let T : (nat * nat) -> bool be the primitive recursive predicate  
> where T(m,n) means that Turing machine number m (with no arguments)  
> executes for at least n steps.
>
> Say that a number m is "terminating" if for some n, not T(m,n), and  
> "HA-divergent" if it is provable in Heyting arithmetic that for all  
> n, T(m,n).
>
> (This happens to coincide with provability in Peano arithmetic but I  
> am using a constructive system for the sake of the argument.)
>
> In a dependent type system with boolean type and natural number  
> type, for every number m let t_m be the term
>
>   lambda x:nat. if T(m,x) then true else 7
>
> Say that a system is "typing HA-complete" if |- t_m : nat -> bool is  
> provable for all HA-divergent m.
>
> Say that a system is "typing decidable" if the judgement |- t : A,  
> where t is a closed term and A a closed term

Sorry, that should be "where t is a closed term and A a closed type"

> , is decidable.
>
> A system cannot be both typing decidable and typing HA-complete,  
> because termination and HA-divergence are recursively inseparable  
> properties.  Martin-Löf's intensional type theory is typing  
> decidable by design and therefore not typing HA-complete.
>
> Now the polemic:
>
> In my opinion typing HA-completeness is a very minimal completeness  
> property to require of a dependently typed system (with nat), and I  
> cannot see the interest of a system that lacks it.  Advocates of  
> typing decidability will of course disagree.  A curious feature of  
> this disagreement is the contrast with traditional arguments over  
> the acceptability of individual judgements.  (Is the Axiom of Choice  
> valid?  Is excluded middle valid?  Is this large cardinal hypothesis  
> valid?  etc.)  Here, typing decidability advocates are apparently  
> comfortable with the judgement |- t_m : nat -> bool for any  
> *particular* HA-divergent m, but object to including it for *all* HA- 
> divergent m.
>
> If I am wrong, please enlighten me by providing a particular HA- 
> divergent m and a philosophical or mathematical case why t_m should  
> not have type nat -> bool.
>
> Best regards,
> Paul