fintype + decidability

Stream: new members

[Vaibhav Karve]

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?

[Patrick Massot]

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

[Kevin Buzzard]

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?

[Chris Hughes]

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.

[Reid Barton]

Well, maybe not if X is empty but otherwise yes

[Vaibhav Karve]

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.

[Chris Hughes]

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.

[Vaibhav Karve]

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.