I have the following code:

constant B:Type
constant A:Type
constant P:B → A → Prop
definition F:Type := B → A

axiom a1: ∀b:B, ∃a:A, P b a
theorem thrm1: ∀b:B, ∀a:A, (P b a) → ∃f:F, (f b = a) ∧ ∀bb:B, P bb (f bb) := 
    λ b:B, λ a:A, 
    assume h: P b a, 


It should be almost trivial to prove this, yet I'm not sure how to do it in type theory. Perhaps my intuition is implicitly based on some axiom from classical logic?

The informal argument is as follows: If for a particular $b$ and $a$ the property $P \; b\; a$ holds, then we can consider the equivalence class of functions $f:B \to A$ for which $f \; b= a$. Moreover, since for any $b\in B$, there is an $a\in A$ such that $P \; b \; a$ holds, we can simply pick from this the function $f$ which also assigns for every other $b$ some $a$ such that $P\; b\; a$ holds. Such a function must always exist, since we can freely adjust the output for each input independently.

But how do we formalize this argument in type theory?


If you used Type instead of Prop in the definition of P, then you could easily extract from axiom a1 a function f such that ∀b:B, P b (f b). However, there would be no guarantee that this function would satisfy f b = a for any given a and b that satisfy P b a. Given a decidable equality on B, you could turn the function that a1 gives you into your desired function via λ bb:B, if bb == b then a else fst (a1 bb). Without decidable equality, it's not clear how you would construct a function that you could prove would give a when given b.

As far as your informal argument, the problem is "picking" from the equivalence class. Constructive logic/type theory is compatible with everything being computable. (Formally, this is usually expressed via realizability.) To say that you can "pick" from an equivalence class subject to some constraints means you are providing an algorithm that can somehow "search" through (some representation of) the equivalence class and find an element that satisfies your constraints. However, you don't even know these types are computably enumerable. At any rate, "picking" is rarely "simple".

I'd have to look at the rules of LEAN to be sure, but with P going to Prop, you need the (real) Axiom of Choice to even get the function f at all before you ever got around to constraints. In fact, while I haven't thought about it too much, I believe the statement you give is equivalent to the (real) Axiom of Choice.

  • $\begingroup$ Why does it make sense to replace Prop by Type? It would no longer be a proposition then? $\endgroup$ – user56834 Oct 1 '18 at 20:32
  • $\begingroup$ @Programmer2134 I didn't say it would make sense. I'm just saying that if we used Type instead of Prop then we can proceed further but we still run into difficulties. As Gilles and I say, with P going into Prop you're dead in the water from the get-go, because your statement then requires the Axiom of Choice. $\endgroup$ – Derek Elkins Oct 1 '18 at 21:17
  • $\begingroup$ ok. Although I wouldn't say I'm "dead in the water", because I'm ok with using the axiom of choice (if I can find out how to do so) $\endgroup$ – user56834 Oct 2 '18 at 5:10
  • $\begingroup$ @Programmer2134 The Axiom of Choice implies classical logic. (This is known as Diaconescu's theorem.) LEAN's type theory is constructive by default, but you can certainly assert the Axiom of Choice and/or the Law of the Excluded Middle (LEM) if you want. LEM implies that all propositions are decidable and thus equality is decidable. The proof is then: Use the Axiom of Choice to get a function g satisfying ∀b:B, P b (g b) then make f as described in my answer using g in the else branch. $\endgroup$ – Derek Elkins Oct 2 '18 at 5:26

In a nutshell, you want to go from “forall b, exists a” to a function from that maps a to b. This is called the axiom of choice. The axiom of choice is not a given in type theory. Some theories have it, others don't but usually can use it as an additional axiom. This additional axiom is not always automatic because it's an additional burden on the logic which could add opportunities for contradictions. Also it may make proofs impossible to extract to code.

More precisely, suppose that $P$ is inhabited, i.e. that there exists $a_0$ and $b_0$ such that $P b_0 a_0$. Then thrm1 b0 a0 proof_of_B_b0_a0 is ∃f:F, (f b = a) ∧ ∀bb:B, P bb (f bb). By basic first-order logic, this implies ∃f:F, ∀bb:B, P bb (f bb). Getting this from ∀b:B, ∃a:A, P b a is the functional axiom of choice.

Lean offers choice as an axiom in the standard library. The introduction of this chapter gives some background as to why you'd need to invoke it and why you may not always want to. The Coq FAQ also has some more theoretical explanations on the topic (Coq, like Lean, is based on the calculus of inductive constructions).

  • $\begingroup$ I'm not sure I follow. Firstly, getting "∃f:F, ∀bb:B, P bb (f bb) from ∀b:B, ∃a:A, P b a". I don't see how this is equivalent to the axiom of choice as formally stated on wikipedia, and the axiom of choice as stated in the lean library is even more different. Secondly, I don't see how to use the axiom of choice to prove the complete statement, namely ∃f:F, (f b = a) ∧ ∀bb:B, P bb (f bb), because we need that (f b = a), but the axiom of choice only gives us some arbitrary example of a choice function, and I don't see how to use it with that equality restriction. $\endgroup$ – user56834 Oct 1 '18 at 20:31

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.