The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

As Stephane said; consider an encoding $phi$ of Turing machines in nat,
then the predicate $P: nat -> nat$; $P m n$ stating that $phi n$ and $phi  
m$
recognize the same language, then how can you hope to be able to prove for  
a given $n$ that
there is no $m$ such that $m<n$ and $P n m$, that is given a Turing  
Machine, to prove that
there is (or there is no) other Turing Machine, recognizing the same  
language, but with
a shorter code.

I think it would be embarrassing if you were able to do such a thing for  
any $n$.

Le Tue, 12 Oct 2010 11:11:02 +0200, Stéphane Lescuyer  
<stephane.lescuyer AT inria.fr> a écrit:

> > I need to use a theorem like this:
> > Lemma nat_well_ordered: forall (P:nat -> Prop),
> >  (exists n:nat, P n) -> (exists m:nat, P m /\
> >    forall k:nat, P k -> k >= m).
>
> Consider the fact that Coq's logic is intuitionistic, and try to think
> of this theorem of yours in a constructive manner. If you're given an
> n for which P is true, then how are you gonna compute the smallest k
> for which P is true?
> Indeed, you need to be able to decide if P is true on a given m to
> write such a function.  This is why you need the decidability of P to
> prove this theorem.
>
> If you're not interested in constructive logic, just assume the
> excluded middle and using it you can use prove your theorem by a
> simple induction on n.
>
> HTH,
> Stéphane


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay