# Re: [TYPES] decidability vs completeness

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

hi paul,

this sort of example well exemplifies the fundamental conceptual difference
between nuprl and coq.  the core of coq is martin-lof's itt.  the system ett
is, by definition, itt extended with equality reflection and uniqueness of
identity proofs.  it is often misrepresented that nuprl is ett, usually on
passage to a "critique" of nuprl on the grounds that the typing judgment in
nuprl is not decidable, and supposedly this is a cardinal principle that ought
to hold for all type theories.

but nuprl is not ett.  say what you want about ett, but it has no bearing on
nuprl.  the reason is that the nuprl typing relation (written "in" in ascii,
written "\in" in print) is not at all intended to be, and never was intended to
be, the coq typing relation (written ":" in both ascii and in print).
comparing the two to each other is not really sensible; each is trying to
express a different thing.

in nuprl it would be the case that t_m in (nat->bool), but as you mention it
would not be the case that in coq t_m : (nat->bool).  the reason is that the
typing judgment in nuprl represents a statement about the a priori given
execution behavior of a program, whereas in coq the analogous statement is
about the grammar of programs themselves, before they ever get to be thought of
as having execution behavior.

put in other terms, nuprl is a theory of TRUTH, and is based on the semantic
propositions-as-types principle; it can be seen as an attempt to formulate
brouwer's notion of truth in intuitionistic mathematics.  coq, on the other
hand, is a theory of FORMAL PROOF, and is based on the syntactic
propositions-as-types principle; it is an account of proof, not an account of
truth.  it can be seen as a full development of heyting's formalization of
intuitionistic mathematics, which brouwer in fact rejected, but that's neither
here nor there.

you are saying, if i understood correctly, that certain facts are true, and
these facts can be independent of a particular proof theory.  eg, the goedel
sentence is true, but is not provable in HA.  (all the axioms of HA are true,
and that fact cannot be doubted without simply doubting everything in
mathematics.)

if one starts with a partial structural (syntactic) type theory with general
recursive types, then one can consider nuprl's types as relations over the
terms of a particular recursive type, essentially mu t.(t->t) or elaborations
thereof.  but the syntactic type theory cannot be construed as a logic, or
rather only as an inconsistent logic.  in nuprl partiality is handled using
"bar types", which predate the lifting monad, but which are essentially that
concept phrased in an operational setting.  there is a type of unevaluated
computations of a type, so that partial functions A - B are total functions A
-> [B] (written \overline{B} in nuprl).

hope this helps, and i hope i haven't misconstrued your question.

bob

-----------------------------
Prof Robert Harper
Carnegie Mellon CSD
r...@cs.cmu.edu
-----------------------------

On Aug 23, 2014, at 12:01, Paul Levy <p.b.l...@cs.bham.ac.uk> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>
> 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

`