Zulip Chat Archive

Stream: new members

Topic: fintype + decidability


view this post on Zulip Vaibhav Karve (Mar 17 2020 at 14:17):

I am trying to figure out how decidability works. I have an incomplete picture of this and so am writing various functions to see if I can figure it out.

My instinct is that any predicate on a fintype should be decidable + computable. Is that correct? For example I wrote:

  example (α : Type*) [f : fintype α] (p : α  Prop) : decidable_pred p :=
  by refine @set.decidable_set_of α p _

Lean informs me that this is noncomputable because it depends on classical.prop_decidable. But I don't want to give up computability. How can I make this computable?

view this post on Zulip Patrick Massot (Mar 17 2020 at 14:20):

I'm don't care at all about computability so read this with caution, but I don't think knowing finiteness is enough

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 14:44):

My understanding is probably even worse than Patrick's but if I have two real numbers a and b for which a=b is undecidable then can't I just make a fintype from a and b and now equality is not decidable on this fintype?

view this post on Zulip Chris Hughes (Mar 17 2020 at 14:45):

It's not true. This would imply decidability of every Proposition, since for any Proposition P, and a fintype X, λ x : X, P is a predicate on a finite type.

view this post on Zulip Reid Barton (Mar 17 2020 at 15:00):

Well, maybe not if X is empty but otherwise yes

view this post on Zulip Vaibhav Karve (Mar 17 2020 at 15:09):

Kevin Buzzard said:

My understanding is probably even worse than Patrick's but if I have two real numbers a and b for which a=b is undecidable then can't I just make a fintype from a and b and now equality is not decidable on this fintype?

But the code I included in my question does type-check! So Lean is telling me that any predicate on a fintype is decidable. My question is why is it not computable.

view this post on Zulip Chris Hughes (Mar 17 2020 at 15:14):

With classical logic every proposition is decidable. You can't computable decide every predicate on a fintype because then you'd be able to computably decide every proposition.

view this post on Zulip Vaibhav Karve (Mar 17 2020 at 15:18):

Okay. I didn't realize that. I commented out open classical and local attribute prop_decidable from my file. Now the example above does not type-check.


Last updated: May 15 2021 at 00:39 UTC