# Zulip Chat Archive

## Stream: general

### Topic: classical.em without funext / quot.sound

#### Mario Carneiro (Aug 19 2020 at 00:20):

After inlining and compression, I got this:

```
import tactic
theorem em' (p : Prop) : p ∨ ¬ p :=
begin
let subs := λ P Q, (P,Q) = (true,p) ∨ (P,Q) = (p,true),
have U : subs true p := or.inl rfl,
have V : subs p true := or.inr rfl,
have : ∀ P Q, subs P Q → ∃ b, cond b P Q,
{ rintros pt pf (⟨⟨⟩⟩|⟨⟨⟩⟩); [use tt, use ff] },
choose f hf,
suffices : p ∨ f _ _ U ≠ f _ _ V,
{ refine this.imp_right (mt $ λ pp, _),
cases eq_true_intro pp, refl },
have up := hf _ _ U,
cases f _ _ U,
{ exact or.inl up },
have vp := hf _ _ V,
cases f _ _ V,
{ right, trivial },
{ exact or.inl vp }
end
#print axioms em' -- classical.choice, propext
```

#### Junyan Xu (Aug 19 2020 at 01:33):

I made two essential adaptations to the original proof explained at https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#the-law-of-the-excluded-middle : using `bool`

instead of `Prop`

as the type to choose from (just like the {0,1} used in the Wikipedia proof; not sure why `Prop`

was chosen in Lean), and using `Prop × Prop`

instead of the function type `bool → Prop`

to get rid of function extensionality.

Not sure if this makes sense, but it seems that `nonempty_pi`

preserves computability, while `choice`

doesn't.

Obviously you can't prove `prop_decidable`

and `type_decidable`

this way; `choice`

follows from `type_decidable`

, which follows from `prop_decidable`

without choice. It makes me wonder what advantage decidability really has over excluded middle for the purpose of doing math? You can't exhibit a function using `ite`

or `dite`

without decidability, but can prove such functions exist using `em`

and `or.elim`

. When using tactics, the difference between em and decidability only matters when the goal is a `Type`

instead of a `Prop`

. Most likely in those cases you are able to carry out a computable/recursive construction or the goal is a function that you can apply `nonempty_pi`

show it exists. So maybe the `choose`

tactic should produce a existential statement in the context when the goal is a `Type`

using `nonempty_pi`

rather than invoking `choice`

, but when the goal is a `Prop`

then it's free to exhibit an element proven to exist.

I am currently thinking of proving `em`

with `quot.sound`

but without `propext`

. The rough idea is to quotient `Prop`

by the equivalence relation `iff`

.

#### Junyan Xu (Aug 19 2020 at 01:52):

Fun to see and digest the statement of `nonempty_choice`

, and nice observation that `nonempty_pi`

follows from it! (Edit: it should prove nonempty_pi, as nonempty_pi is a Prop, so for the purpose of proving it, nonempty (something) is the same as something.)

#### Mario Carneiro (Aug 19 2020 at 01:53):

Not sure if this makes sense, but it seems that nonempty_pi preserves computability, while choice doesn't.

There have been discussions about the `trunc`

version of `nonempty_pi`

, which looks like it should be computable but isn't:

```
import tactic.basic
universes u v
meta def trunc_pi.impl {α : Sort u} {β : α → Sort v} :
(∀ (a : α), trunc (β a)) → trunc (Π (a : α), β a) := unchecked_cast
@[vm_override trunc_pi.impl] -- this should be fine, right?
noncomputable def trunc_pi {α : Sort u} {β : α → Sort v} :
(∀ (a : α), trunc (β a)) → trunc (Π (a : α), β a) :=
λ h, trunc.mk $ λ a, (h a).out
meta def weird (α) : trunc (trunc α → α) := trunc_pi.impl id
def singl {α} (a : α) := {x // x = a}
instance singl.subsingleton {α} (a : α) : subsingleton (singl a) :=
⟨by rintro ⟨_, rfl⟩ ⟨_, rfl⟩; refl⟩
meta def lie : singl tt :=
trunc.rec_on_subsingleton (weird bool) $ λ f,
⟨_, to_bool_tt (by congr : f (trunc.mk ff) = f (trunc.mk tt))⟩
#eval lie.1 -- ff
```

#### Mario Carneiro (Aug 19 2020 at 01:55):

@Simon Hudon unfortunately my demonstration doesn't quite work with `vm_override`

as I was hoping, because `trunc_pi`

is still considered `noncomputable`

and hence functions based on it don't get any VM implementation

#### Mario Carneiro (Aug 19 2020 at 02:02):

It makes me wonder what advantage decidability really has over excluded middle for the purpose of doing math?

You are omitting the most important part: ease of use. Yes, mathematicians like to prove theorems and as long as it's a Prop you can use `nonempty_choice`

instead of `choice`

, but the problem is that you have to be always working with respect to some choice function, and this is really inconvenient for things like choicy definitions (of which there are many in mathlib), like "the limit of the filter". You could probably cobble something together using a typeclass `[choicy.{u}]`

to get a choice function, but we already have problems with typeclass unification when the class is a subsingleton, and the `choicy`

typeclass is as non-unique as they come (that's sort of it's shtick)

#### Mario Carneiro (Aug 19 2020 at 02:03):

The rough idea is to quotient Prop by the equivalence relation iff.

I will be interested to see if this is successful. I tried and failed to do exactly this a few years ago

#### Simon Hudon (Aug 19 2020 at 02:08):

@Mario Carneiro I think what it needs is for the `vm_override`

attribute to remove the `noncomputable`

mark when it is set. I didn't think of it before

#### Mario Carneiro (Aug 19 2020 at 02:09):

does that mean that we still write `noncomputable`

but it's not actually noncomputable?

#### Simon Hudon (Aug 19 2020 at 02:11):

Yeah, I know that's weird. The trouble is that the definition and its attribute are not added to the environment at the same time. First you add the definition and in all regards, it is `noncomputable`

and that's only invalidated when the attribute is added

#### Mario Carneiro (Aug 19 2020 at 02:13):

maybe `noncomputable`

should be an attribute

#### Simon Hudon (Aug 19 2020 at 02:19):

We would face a similar problem. I think we might need `vm_override`

to be a keyword like `using_well_founded`

#### Mario Carneiro (Aug 19 2020 at 02:23):

maybe we should call it `computable`

:D

#### Junyan Xu (Aug 19 2020 at 03:00):

Hmm, I thought `subtype.ext_val`

must depend on `propext`

(`true`

has one constructor so any proven `Prop`

has only one element), but it turns out it doesn't. Does the principle of proof irrelevance not need to be stated anywhere and is just directly applied by the kernel?

`theorem pf_irrel (p : Prop) (a b : p) : a = b`

#### Junyan Xu (Aug 19 2020 at 03:02):

I have only learned Lean for three weeks (not counting natural number game or min/max game) so pardon my curiosity about many foundational issues.

#### Mario Carneiro (Aug 19 2020 at 03:03):

yes, proof irrelevance is a no axioms axiom

#### Junyan Xu (Aug 19 2020 at 03:04):

I think I now have a good grasp of type theory by playing with Lean and it's maybe time to learn some HoTT.

#### Mario Carneiro (Aug 19 2020 at 03:04):

if you have the stomach for some type theory, https://github.com/digama0/lean-type-theory/releases/tag/v1.0 has the description of the basic rules of lean in chapter 2

#### Junyan Xu (Aug 19 2020 at 03:04):

Earlier today I was drawn to the problem what's the shortest proof from first principles of `tt≠ff`

; it was used in the `em`

proof above, but `trivial`

solved it. Then I found `no_confusion`

and `no_confusion_type`

associated to every inductive type (just like `rec`

, `rec_on`

and `cases_on`

), but am unable to find any documentation except brief mention in "Theorem Proving in Lean". Anyway, here is a relatively minimal proof of the fact:

```
theorem tt_ne_ff : bool.tt ≠ bool.ff :=
begin
set f := @bool.rec (λ_, Prop) false true with hf,
intro h, have : f tt = f ff, rw h,
rw hf at this, dsimp at this,
have t := true.intro, rwa this at t,
end
#print axioms tt_ne_ff -- no axioms
```

#### Bryan Gin-ge Chen (Aug 19 2020 at 03:06):

@Kevin Buzzard has a blog post on `no_confusion`

: https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

#### Junyan Xu (Aug 19 2020 at 03:07):

Thanks for pointing to that!

Indeed

```
theorem pf_irrel (p : Prop) (a b : p) : a = b := by trivial
#print axioms pf_irrel -- no axioms
```

requires no axioms

#### Mario Carneiro (Aug 19 2020 at 03:12):

it's more even than that. Two proofs are not just the same but *definitionally* the same - you can prove the equality using `rfl`

, the proof that `a = a`

#### Mario Carneiro (Aug 19 2020 at 03:13):

In fact, we exploit proof irrelevance in the proof of `em'`

, in the `cases eq_true_intro pp, refl`

part of my version of the proof

#### Mario Carneiro (Aug 19 2020 at 03:14):

the `refl`

is a proof that `f true true U = f true true V`

#### Junyan Xu (Aug 31 2020 at 21:34):

I observed that the drinker paradox implies excluded middle in Lean, using a variation of the Diaconescu argument. However, Coq documentation https://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html (Section "Weak classical axioms") says the former is weaker. What could be the reason?

```
import tactic
universe u
-- [Bell] John L. Bell, Choice principles in intuitionistic set theory, http://publish.uwo.ca/~jbell/Choice%20Principles.pdf
def sid {α : Sort u} [nonempty α] (p : α → Prop) := ∃a, (∃b, p b) → p a
-- [Lean] noncomputable theorem strong_indefinite_description {α : Sort u} (p : α → Prop) (h : nonempty α) : {x : α // (∃ y : α, p y) → p x}
#print axioms classical.strong_indefinite_description -- all three (uses EM)
-- [Bell] Un = [Coq] Drinker = drinker's paradox (small form) (called Ex in Bell [Bell])
-- This is the Prop form, and the strong (Type) form is [Coq] D_epsilon = (weakly classical) indefinite description principle
-- ∃a, p a → ∀b, p b ([Bell] Ex) is also called drinker paradox (e.g. on codewars); sid implies only ∃a, p a → ∀b, ¬¬p b
def sid' {α : Sort u} [nonempty α] (p : α → Prop) (r : Prop) :=
(r → ∃a, p a) → ∃a, r → p a
-- [Coq] IGP = independence of general premises (an unconstrained generalisation of the constructive principle of independence of premises)
-- implies LC : (φ→ψ∨χ)→(φ→ψ)∨(φ→χ) immediately
-- Trivially interderivable:
example {α : Sort u} [nonempty α] (p : α → Prop) :
sid' p (∃a, p a) → sid p := λs, s id
example {α : Sort u} [nonempty α] (p : α → Prop) (r : Prop) :
sid p → sid' p r := λ⟨a,ha⟩ h, ⟨a,ha∘h⟩
theorem em_of_sid' {p : Prop} :
@sid' {u:bool // p ∨ u=tt} ⟨⟨tt,or.inr rfl⟩⟩ (λu, ↑u=ff) p → p ∨ ¬p :=
λs, let ⟨⟨u,h1⟩,h2⟩ := s (λh, ⟨⟨ff,or.inl h⟩,rfl⟩) in
h1.elim or.inl (λh, or.inr (by {dsimp, rw h, triv} ∘ h2))
#print axioms em_of_sid' -- no axioms, not even proof irrelevance
```

#### Junyan Xu (Aug 31 2020 at 21:45):

This is part of my write-up of my investigation into proving em without propext. The attempt was unsuccessful, but I make connections between em, quotient exactness and choice principles.

I also introduced the function extension principle saying that you can extend a function from a subtype to a nonempty sort can be extended to the whole type, which I don't see discussed anywhere else. I showed that it's equivalent to the drinker paradox under nonempty_pi/choice.

#### Mario Carneiro (Sep 01 2020 at 02:07):

This is very interesting. You should try replaying your proof in Coq to see if there are any non obvious foundational differences, but it seems like this proof would also go through in Coq, and if so it looks like it would be news

#### Junyan Xu (Sep 26 2020 at 02:41):

Releasing this "formal" write-up and wrapping up this expedition :)

https://gist.github.com/alreadydone/7474d5000c912194d794d06192e84f1e

I didn't end up porting the implication `sid→em`

to Coq; I found the same argument in [Bell] (relativized ε-scheme), so it's not new. According to [Bell], the version of `sid`

that only quantifies over the whole universe (called `Ex`

in [Bell]) is weaker than LEM, but if quantification over arbitrary set (or type, in type theory) is allowed (e.g. with the relativized ε-scheme), then it's equivalent to LEM. The Coq people might have missed this point and went on to claim that `sid`

(their `IGP`

) is weaker than LEM.

#### Junyan Xu (Sep 28 2020 at 05:14):

Update: choice + proof irrelevance => decidable equality for any type

https://gist.github.com/alreadydone/7474d5000c912194d794d06192e84f1e#file-choice_and_excluded_middle-lean-L29

#### Junyan Xu (Sep 29 2020 at 04:29):

Update: I managed to prove weak excluded middle `∀p, ¬p ∨ ¬¬p`

using choice, quot.sound (and PI) only:

https://gist.github.com/alreadydone/7474d5000c912194d794d06192e84f1e#file-choice_and_excluded_middle-lean-L52

In fact the argument implies `∀p q, (¬¬p ∧ ¬¬q) ∨ (¬p ∧ ¬q) ∨ ¬(p → q) ∨ ¬(q → p)`

which seems to be stronger.

#### Scott Morrison (Sep 29 2020 at 06:22):

You should write these things down / contribute them to mathlib / etc. Thoughts published only as gists are not going to last long in this world. :-)

#### Junyan Xu (Sep 29 2020 at 13:44):

These aren't just thoughts, but formalized thoughts, so should last a bit longer :) I also specified the Lean version and mathlib commits in leanpkg format so they won't bitrot unless someone deletes the commit history.

I agree that I need to add a list of contents that includes the line number of each section, state main results/highlights in an introduction section, and explain ideas of nontrivial proofs in more detail.

Regarding mathlib, would you like to see the current proof of classical.em be replaced by one that doesn't use quot.sound?

#### Junyan Xu (Sep 29 2020 at 13:49):

I seem to be able to prove we have a homomorphism from the Heyting algebra on `Prop`

to {0,1} respecting true,false,or,and,imp,neg (all logical connectives) mapping p to 1 iff `⟦ff⟧=⟦tt⟧`

in the quotient of `bool`

by `λ_ _,p`

. What strongest consequence does this have? It implies the Heyting algebra is a Stone algebra (satisfies weak excluded middle), for example.

#### Scott Morrison (Sep 29 2020 at 23:20):

Formalized thoughts rot even faster, because they are dependent on a big software stack. We have seen many examples now of work that was not updated being lost quickly.

#### Scott Morrison (Sep 29 2020 at 23:20):

Making PRs into mathlib is one good option. Another is @Rob Lewis's recent efforts to provide continuous integration for outside-of-mathlib projects, although I now can't find any links to it...

#### Rob Lewis (Sep 30 2020 at 07:51):

https://leanprover-community.github.io/lean_projects.html

#### Eric Rodriguez (Jul 14 2022 at 20:20):

Mario Carneiro said:

The rough idea is to quotient Prop by the equivalence relation iff.

I will be interested to see if this is successful. I tried and failed to do exactly this a few years ago

any success?

#### Junyan Xu (Jul 14 2022 at 20:22):

I think it's probably not impossible, and the best I could get is at this gist. (PI stands for proof irrelevance)

Last updated: Aug 03 2023 at 10:10 UTC