# Zulip Chat Archive

## Stream: new members

### Topic: fintype + decidability

#### 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?

#### 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

#### 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?

#### 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.

#### Reid Barton (Mar 17 2020 at 15:00):

Well, maybe not if `X`

is empty but otherwise yes

#### 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.

#### 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.

#### 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: Dec 20 2023 at 11:08 UTC