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

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