# [tlaplus] Re: [Newbie Question] Engineer trying to get maths meaning

It's just syntax. It happens to be syntax that's based on century-old mathematical notation, but at the end of the day, it's still just syntax.

The trouble you’re having is caused by your assumption that Q is defined on the left side of the colon ("\E Q \in Quorum"), and then used on the right side.

But, in fact, Q is actually defined on the right side of the colon and then used on the left. In other words, we define Q and then ask “is there any element in the set Quorum that meets the definition of Q?”

On Friday, October 2, 2020 at 12:44:13 PM UTC-5 franke...@xxxxxxxxx wrote:
Hi,

I'm trying to understand this part of the paxos specification. I'm not trying to understand how paxos works, I get that, I'm just trying to understand how to read and understand this part of the specification.

01  /\ \E Q \in Quorum :
02        LET Q1b == {m \in msgs : /\ m.type = "1b"
03                                 /\ m.acc \in Q
04                                 /\ m.bal = b}
05            Q1bv == {m \in Q1b : m.mbal \geq 0}
06        IN  /\ \A a \in Q : \E m \in Q1b : m.acc = a
07            /\ \/ Q1bv = {}
08               \/ \E m \in Q1bv :
09                    /\ m.mval = v
10                    /\ \A mm \in Q1bv : m.mbal \geq mm.mbal

On line 01 you define that Q is in set of Quorum and then lines 02-10 define what Q will be. My confusion is on Line 03 Q is referenced. How can you reference something that hasn't been assigned a value yet.

I may very well be suffering from "... brain washing done by years of C programming".

Any help that I could get in understanding this would be greatly appreciated. Also, is there a place on the web were I can better familiarize my self with such concepts.

Thanks,

-Frank

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.