# Re: [tlaplus] Understanding CHOOSE

You are correct, but this is a result of neither TLC nor even TLA+, but of how we describe things in mathematics. A CHOOSE _expression_ is equal to some value that satisfies the condition (I think SOME would have been a better name). In mathematics, A = A for any _expression_ A, and therefore it is always the case that (CHOOSE x ∈ S : P(x)) = (CHOOSE x ∈ S : P(x)); all occurrence of this _expression_ are equal to one another. ∃ x ∈ S : P(x) is also a mathematical _expression_, but one that can only be equal to either TRUE or FALSE. As with CHOOSE, always (∃ x ∈ S : P(x)) = (∃ x ∈ S : P(x)), but while the value (TRUE/FALSE) of these two expressions is equal, the x in both cases might not be the same; the expressions -- while equal -- can be talking about different xs.

-- Ron

On Thursday, January 21, 2021 at 10:21:41 AM UTC sadraskol (Thomas Bracher) wrote:
Hello John,

I think Alex answered your first point, but I'll try to express by my own words for you to see how it translates to a formal description.
Say your system is a simple increment/decrement of a global state :

/\ i' = i + 1
/\ i' = i - 1

As you mentioned, you can use CHOOSE :

Init == i = 0
Next == LET answer == CHOOSE code \in {"200", "400"}: TRUE

But as mentioned by Alex and yourself, this would not yield the expected behavior. CHOOSE having no guarantees, all possible outputs are not covered by TLC.
The existential quantifier is the correct way of exploring all possible behavior :

Init == i = 0

The operator \E corresponds to the correct way of introducing non-determinist behavior in your specifications. TLC will check all possible behaviors for you.

I hope it helped,

Thomas
Le mercredi 20 janvier 2021 à 15:40:58 UTC+1, John a écrit :
Hi Alex,