classical.em without funext / quot.sound

Stream: general

[Mario Carneiro]

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]

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]

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]

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]

@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]

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]

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]

@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]

does that mean that we still write noncomputable but it's not actually noncomputable?

[Simon Hudon]

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]

maybe noncomputable should be an attribute

[Simon Hudon]

We would face a similar problem. I think we might need vm_override to be a keyword like using_well_founded

[Mario Carneiro]

maybe we should call it computable :D

[Junyan Xu]

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]

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]

yes, proof irrelevance is a no axioms axiom

[Junyan Xu]

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]

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]

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]

@Kevin Buzzard has a blog post on no_confusion: https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

[Junyan Xu]

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]

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]

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]

the refl is a proof that f true true U = f true true V

[Junyan Xu]

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]

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]

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]

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]

Update: choice + proof irrelevance => decidable equality for any type
https://gist.github.com/alreadydone/7474d5000c912194d794d06192e84f1e#file-choice_and_excluded_middle-lean-L29

[Junyan Xu]

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]

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]

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]

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]

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]

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]

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

[Eric Rodriguez]

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]

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