The king of France

Stream: new members

[Bjørn Kjos-Hanssen]

I can't find this in the documentation. How would I define c below?

constant U: Type
constant F : U → Prop -- F x says that x is king of France

axiom only_one : ∃ x, (F x ∧ ∀ y, F y → x = y)

definition c := "the x such that F x"

[Kyle Miller]

You can use the axiom of choice to get a witness for there-exists:

constant U: Type
constant F : U → Prop -- F x says that x is king of France

axiom only_one : ∃ x, (F x ∧ ∀ y, F y → x = y)

noncomputable
definition c := only_one.some  -- short for Exists.some only_one

lemma c_property : F c ∧ ∀ y, F y → c = y := only_one.some_spec

[Kyle Miller]

You need to write noncomputable to tell Lean that it's not something it's able to actually compute -- the reason you need it is a technical non-classical-math thing you can ignore if you want.

[Bjørn Kjos-Hanssen]

Thanks @Kyle Miller! Is there a way without Choice? (I am not against Choice but logically it shouldn't be needed here...)

[Kyle Miller]

If I tell you there exists a unique King of France, how would you tell me who it is? This is the issue.

[Kyle Miller]

This is an alternative:

constant U: Type
constant F : U → Prop -- F x says that x is king of France
constant c : U

axiom only_one : F c ∧ ∀ y, F y → c = y

[Kyle Miller]

There exists a King of France, and it's c. This avoids the axiom of choice.

There are also ways to deal with this by using sigma types instead of existentials.

[Kyle Miller]

Here's the kind of example that helped me understand why choice was needed:

lemma ex1 : ∃ x, x > 0 := ⟨1, by simp⟩
lemma ex2 : ∃ x, x > 0 := ⟨2, by simp⟩

example : ex1 = ex2 := rfl

[Bjørn Kjos-Hanssen]

I don't know if this is a type theory thing, but in regular first-order logic we would just expand the language with a new constant... or agree that any reference to c is officially supposed to be an abbreviation for a more elaborate statement. For instance, c is bald officially means: there is one and only one king of France, and he is bald.

[Kyle Miller]

Both ex1 and ex2 are proofs that there is a positive natural number. For the first, I use 1, and for the second, I use 2. You'd think you could just get that witness from a proof when you want to have a positive natural number. However, in Lean all proofs of the same proposition are equal by definition (that's proof irrelevance).

So, if we could extract the number from the proof, we'd get the contradictory result that 1 = 2.

[David Wärn]

There's basically no interesting way to eliminate Props into Types without choice, since the proof of a Prop doesn't contain any data (it's represented by nothing at all). If you want computable "unique choice", then you should use trunc instead of Prop (and trunc-ated sigma types instead of existentials).

[Kyle Miller]

Bjørn Kjos-Hanssen said:

I don't know if this is a type theory thing, but in regular first-order logic we would just expand the language with a new constant...

This is more or less what Lean's version of the axiom of choice is. It introduces a whole family of constants, one for every existential. (Technically, one for every nonempty type.)

[Kevin Buzzard]

Yeah, I think this is a type theory thing (my understanding is that the analogous construction in ZFC would be unproblematic). It's because Prop forgets its proofs, but Type is data, so moving from Prop to Type requires magic.

[Kyle Miller]

The Axiom:

axiom classical.choice {α : Sort u} : nonempty α → α

The Exists.some function uses this indirectly, but it really is effectively giving a new constant for each existential. The name of this constant (given your first example) is Exists.some only_one.

[Chris B]

David Wärn said:

There's basically no interesting way to eliminate Props into Types without choice

It's all a matter of taste, but I think subsingletons are interesting.

[Kyle Miller]

As Kevin says, every definition that involves a non-Prop type has some obligation to be computable in some way (I'm not sure if this is a type theory thing, or a CS-people-like-computing-things thing). Using the definitions from my example, Exists.some ex1 does not promise to be able to actually provide a natural number.

[Kyle Miller]

However, on a case-by-case basis you can get a bona-fide computed thing. The natural numbers have their own version of docs#Exists.some called docs#nat.find, which will give the first number satisfying the predicate.

lemma ex2 : ∃ x, x > 0 := ⟨2, by simp⟩
def num := nat.find ex2

#eval num
-- 1

This depends on the structure of the natural numbers (induction). In contrast, the type U of people in your example doesn't have any sort of structure that could be used to obtain the King.

[David Wärn]

Chris B said:

It's all a matter of taste, but I think subsingletons are interesting.

Subsingletons are interesting but the point here is that in Lean you can't eliminate into the from Props without choice. What you can do is eliminate h : a = b using eq.rec, which is a little more limited.

[David Wärn]

Basically Lean without choice makes a distinction which is absent in ZFC, roughly speaking between "constructions" and "properties of constructions". In ZFC all you do is prove things about the universe of sets, so you are only working in the latter world. In Lean without choice you have access to both worlds, but going from the latter to the former is mostly verboten.

[Chris B]

I think there's a typo in there, so I don't know exactly what you mean. My point was that subsingletons can eliminate from Prop to an arbitrary Sort without invoking choice.

[Reid Barton]

I think maybe there is some confusion between subsingleton elimination and subsingleton.

[Chris B]

There's a joke about them being equal in there somewhere.

[David Wärn]

Ah right, you can eliminate from Props that are syntactic subsingletons, but basically this is the least interesting case.

[Kyle Miller]

David Wärn said:

the proof of a Prop doesn't contain any data (it's represented by nothing at all)

I learned a while back (to my surprise -- the only real reason I'm sharing) that Lean actually does represent proofs by data(*). Lean actually will reduce proof terms, and there are examples of proofs that don't normalize https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Defeq.20is.20algorithmic.20in.20HoTT/near/243115821

(*) I believe it erases proofs when evaluating with the VM, though. That and proof irrelevance mean the situation's that proofs effectively have no data.

(Another place that proof representation apparently can matter is with simp, again a bit of a surprise, though this doesn't count since it's operating syntactically.)

[Reid Barton]

Now I think there is some confusion between "proofs" (as in the things that supposedly inhabit propositions) and proof terms. :upside_down:

[Reid Barton]

It would be nice if we had a better name for the first one.

[Kyle Miller]

I guess my main surprise wasn't that there were proof terms, but that they mattered in any way.

[Reid Barton]

I think @David Wärn's description in terms of two worlds is a good one. But more generally, while Lean-with-choice corresponds to ZFC plus some universes, Lean-without-choice definitely doesn't correspond to anything like ZF. For example, Lean-without-choice doesn't prove LEM (as far as we know??)

[Reid Barton]

You could cook up some system of axioms to replace choice (like LEM and "unique choice") to get something that looks approximately like ZF, but there is not that much practical reason to do so.

[Kyle Miller]

(If a "proof" is a proof term, maybe an "oath" is a proof-modulo-irrelevance. Lean solemnly swears it's seen the proof.)

[Mario Carneiro]

Reid Barton said:

I think David Wärn's description in terms of two worlds is a good one. But more generally, while Lean-with-choice corresponds to ZFC plus some universes,

I would say it is closer to ZF+GC ("global choice"), in which there is a class function that selects elements from every nonempty set, or alternatively a well ordering of the universe

[Mario Carneiro]

In ZFC, you usually can't construct definable functions that make use of a choice witness; it all has to be behind an existential

[Mario Carneiro]

It would be possible to get something more like ZFC in lean if the axiom was instead docs#classical.axiom_of_choice

[Reid Barton]

If we interpret each Type n as a universe $U_n$ then choice.{n} only needs choice over $U_n$, which is a set. But then ZFC + some universes is maybe too much rather than too little. Anyways, it wasn't really the point but I should have said something less precise there.

[Mario Carneiro]

Kyle Miller said:

(If a "proof" is a proof term, maybe an "oath" is a proof-modulo-irrelevance. Lean solemnly swears it's seen the proof.)

I think this is still too syntactic. An element of a proposition is more of a hypothetical than an actual proof - Lean hasn't seen the proof, it's just assuming the proposition to be true. These elements are elements in the same way that real has uncountably many elements even though there are only countably many terms of type real

[Mario Carneiro]

Reid Barton said:

If we interpret each Type n as a universe $U_n$ then choice.{n} only needs choice over $U_n$, which is a set. But then ZFC + some universes is maybe too much rather than too little. Anyways, it wasn't really the point but I should have said something less precise there.

Even though it's a set (and thus amenable to the axiom of choice), you still don't get an explicit witness, except behind an existential, so it doesn't let you construct definable functions, unless you fix a set of choice functions "at the outset", which is messy because the choice of choice function becomes a parameter on every theorem

[Reid Barton]

Jacques Carette suggested the term "omniscient" to describe, as I understand it, the non-constructive aspect of classical mathematics that doesn't distinguish between knowing that there is exactly one king of France and knowing who the king of France is. (Or for a more practical example, not distinguishing between knowing that a given element $a$ of $(\mathbb{Z}/p)^\times$ can be expressed as $g^e$ for a unique $e$ mod $p-1$, and being able to compute $e$ from $a$.)

[Reid Barton]

Mario Carneiro said:

unless you fix a set of choice functions "at the outset", which is messy because the choice of choice function becomes a parameter on every theorem

Oh right, this part is indeed a bit weird.

[Kyle Miller]

I didn't mean to suggest that Lean actually has seen a proof -- we're taking Lean at its word. That's its oath. (At least as far as asserting the proposition is true.)

Point taken about using language that makes it seem like there actually are proof terms for every true proposition.

[Ania Misiorek]

Has anyone successfully downloaded lean3 on a macOS with an M1 chip? Seems to be a lot of issues.

[Johan Commelin]

@Ania Misiorek Welcome! Please start a new thread for your question. (You can edit your message and change the title.)

[Kevin Buzzard]

you might want to ask this in a more appropriate thread? We're talking about the King of France here. Search for M1 before you do though (use the search bar at the top of the app), because this has come up before.

[Kyle Miller]

(I apologize immensely for the following name idea in advance... A term of a proposition could be called a "troof.")

[Eric Rodriguez]

Kyle, you're now the one in the wrong thread ;b

[Kyle Miller]

(fixed -- and apparently took you with me)

[Bjørn Kjos-Hanssen]

Kyle Miller said:

You can use the axiom of choice to get a witness for there-exists:

constant U: Type
constant F : U → Prop -- F x says that x is king of France

axiom only_one : ∃ x, (F x ∧ ∀ y, F y → x = y)

noncomputable
definition c := only_one.some  -- short for Exists.some only_one

lemma c_property : F c ∧ ∀ y, F y → c = y := only_one.some_spec

Unfortunately I get this cryptic error message:
"invalid field notation, 'some' is not a valid "field" because environment does not contain 'Exists.some'
only_one"

[Kyle Miller]

Ah, right, you need a mathlib theorem for that. If you add

import logic.basic

it will work. (I had import tactic at the top of my file, which imports it transitively.)

[Kyle Miller]

(That error message means "I see only_one is an Exists. I see you are asking for .some. I looked for Exists.some, but I don't know what that is." This usually shows up if either (1) Lean guessed the types wrong, (2) you're missing some imports, or (3) you mistyped the stuff after the dot.)

[Bjørn Kjos-Hanssen]

Thanks again @Kyle Miller now I got it to work, even with "every country has a unique king":

import logic.basic
open classical

constant U: Type
constant F : U → U → Prop -- F a x says that x is king of a

definition is_only_one (a x:U) : Prop := (F a x ∧ ∀ y, F a y → x = y)

axiom only_one : ∀a : U, ∃ x : U, is_only_one a x

noncomputable definition c (a : U) : U := (only_one a).some  -- short for Exists.some only_one

lemma c_property : ∀ a : U,  F a (c a) ∧ ∀ y, F a y → c a = y := assume a, (only_one a).some_spec

[Mario Carneiro]

is_only_one is called docs#exists_unique btw

[Kyle Miller]

Terminology attempt number three: proof term vs truth term, or a proof vs a truth. We syntactically construct proof terms for a proposition, but these just witness the singular truth term whose type is the given proposition.

(I've heard a model theorist use truth term as thing that evaluates the truth of a proposition with respect to a model, so there's mild overloading.)