decidability implies LEM

Stream: general

[Huỳnh Trần Khanh]

how does decidability imply LEM? this is something that I struggle to understand

[Yakov Pechersky]

Decidable means that given some true-false statement, there is a defined, executable algorithm to determine whether it is true or false. No in between. Decidability by definition means that the algorithm terminates, so you will get exactly one of either true or false. That's my understanding

[Eric Wieser]

Decidability of all propositions implies LEM

[Eric Wieser]

Obviously the fact that natural numbers are decidably equal does not imply LEM generally

[Yakov Pechersky]

Yes, I meant LEM for the class of propositions for which one has decidability

[Eric Wieser]

Sure, I was just making sure Huỳnh Trần Khanh was aware of the distinction

[Mario Carneiro]

syntactically, it's a triviality: psum p (~p) implies p \/ ~p by case split

[Eric Wieser]

What's the relevance of psum?

[Mario Carneiro]

that's what decidable p is

[Eric Wieser]

src#decidable says otherwise

[Mario Carneiro]

I would write sum but that doesn't typecheck in lean for silly reasons

[Mario Carneiro]

They are isomorphic types

[Eric Wieser]

If we're handwaving decidable as psum we may as well handwave it as or

[Mario Carneiro]

No, because psum is a type and or is a prop

[Mario Carneiro]

decidable p is not isomorphic to p \/ ~p

[Mac]

Mario Carneiro said:

I would write sum but that doesn't typecheck in lean for silly reasons

Isn't one key difference between decidable' (p : Prop) := psum p (~p) and the real decidable p that psum is a normal inductive and decidable is a class inductive?

[Kyle Miller]

@Mac This should be functionally equivalent:

def decidable' (p : Prop) := psum p ¬p
attribute [class] decidable'