[TYPES] decidability vs completeness

Paul Levy P.B.Levy at cs.bham.ac.uk
Sat Aug 23 12:01:22 EDT 2014

```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

```