coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] help with excluded middle at point vs. all

From: Vilhelm Sjoberg <vilhelm.sjoberg AT yale.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] help with excluded middle at point vs. all
Date: Sun, 3 Jul 2016 16:13:25 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vilhelm.sjoberg AT yale.edu; spf=Pass smtp.mailfrom=vilhelm.sjoberg AT yale.edu; spf=None smtp.helo=postmaster AT mail-vk0-f42.google.com
Ironport-phdr: 9a23:6TSM4h/nVWxYBv9uRHKM819IXTAuvvDOBiVQ1KB90OMcTK2v8tzYMVDF4r011RmSDN2dsasP0raK+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2WVTerzWI4CIIHV2nbEwud7yzQNeZ1pjrn8mJuLTrKz1SgzS8Zb4gZD6Xli728vcsvI15N6wqwQHIqHYbM85fxGdvOE7B102kvpT4r9Zf9HFbvOtk/MpdW437eb45RPpWFmcIKWcwsfPqsRnOSQ7H3XkbWGgMnVIcHQnB7Bz+W9HqsCzwu/By8DiTOcCwQLwpD2fxp5x3QQPl3X9UfwUy93va35R9

Indeed, I don't think it's provable for A:=nat. Consider the predicate (P n) := "the turing machine M does not halt within n steps". That is certainly "pointwise" decidable. So if this theorem was provable, you could use it to decide whether M halts.

Vilhelm

[Coq-Club] help with excluded middle at point vs. all, Jonathan Leivent, 07/03/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Vilhelm Sjoberg, 07/03/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Arnaud Spiwack, 07/03/2016
  - Re: [Coq-Club] help with excluded middle at point vs. all, Hugo Carvalho, 07/14/2016
    - Re: [Coq-Club] help with excluded middle at point vs. all, Arnaud Spiwack, 07/14/2016
      - Re: [Coq-Club] help with excluded middle at point vs. all, Hugo Carvalho, 07/15/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Clément Pit--Claudel, 07/03/2016
  - Re: [Coq-Club] help with excluded middle at point vs. all, Clément Pit--Claudel, 07/03/2016
- Re: [Coq-Club] help with excluded middle at point vs. all, Abhishek Anand, 07/03/2016
  - Re: [Coq-Club] help with excluded middle at point vs. all, Jonathan Leivent, 07/03/2016