So I am wondering what the reasons are that to design `Ballot` in this way. Why not just setting it something like `Ballot == 0..10` in the first place?
say that ballot has to be in 0..10. The paper also doesn't say that it has to be Nat, but Nat is
(1) a totally ordered set (therefore any pair of elements are comparable---something that Paxos wants),
(2) infinite (so, more general than 0..10). This is the main reason. If the authors had written 0..10 to begin with,
I would assume that this specification/algorithm does not handle ballot 11 and may therefore be useless to me.
(3) defined in Naturals along with operators like >, <, etc and their arithmetic. So, we do not have to specify that.
So Nat serves the purpose as a high level abstraction of Ballots (but not as a practical executable one because
if Ballots is Nat, then the first conjunct of Phase2a would itself require consensus). Note that 0..10 satisfies (1) and (3)
but not (2).
Also, while with Nat we cannot do model checking, we can do theorem proving.
But that requires much more human effort than model checking.
Hope this helps,
Saksham