The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi.

I would answer that it depends. Guillaume provides an example of looping 
function in False. Then, of course, you can build a proof of False. But 
what if f is in nat? Then problems may arise if you can prove that 0=1. 
Define for instance f by  f x = S (f x). So, I am not sure that 
non-termination always leads to inconsistency, especially if you 
restrict type dependencies to terminating terms (but it is not 
decidable...). See for instance the works of Constable et al on partial 
functions in constructive type theory, and the NuPRL proof assistant.

Best regards,

Frédéric.

Le 08/02/2014 12:19, Guillaume Melquiond a écrit :
> On 08/02/2014 12:05, Kirill Taran wrote:
>
> > Is it true that if we had possibility to write non-terminating programs
> > (suppose we don't use non-terminating term in types, so type check
> > terminates) then we would have possibility to prove everything?
>
> Fixpoint f (x : unit) : False := f x.
> Goal False. exact (f tt). Qed.
>
> Best regards,
>
> Guillaume