Re: [tlaplus] Regarding the SingletonCardinality Axiom in Consensus.tla

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello Christian,

and welcome to the TLA+ forum.

If I understand correctly, the axiom was necessary because the prover didn't know anything about finite sets and cardinalities at the time when the proof was done. It simply asserts that any singleton set is finite and has cardinality one.

In particular, considering

 \A e \in SUBSET {"a", "b", "c"} : IsFiniteSet({e}) /\ (Cardinality({e}) = 1)

this formula asserts that sets such as { {"a", "c"} } or { {} } are finite sets of cardinality one. Note that these sets are singletons whose only element is a set.

If I understand correctly, you are proposing to write

  \A e : IsFiniteSet(e) /\ Cardinality(e) = 1

But this would assert that any set is finite and has cardinality one, it would for example imply

  IsFiniteSet(Nat) /\ Cardinality(Nat) = 1

which is clearly false. (An axiom is a formula that is asserted to be true, all its instances had indeed better evaluate to TRUE.)

Since version 1.2.1, released last week, the standard TLAPS library contains a module FiniteSetTheorems that contains a collection of theorems about finite sets, including

THEOREM FS_Singleton ==
  /\ \A x : IsFiniteSet({x}) /\ Cardinality({x}) = 1
  /\ \A S : IsFiniteSet(S) => (Cardinality(S) = 1 <=> \E x: S = {x})

which supersedes the above axiom.

Hope this helps,

Stephan


On Sep 18, 2013, at 3:28 PM, Christian Spann <cspanns....@xxxxxxxxx> wrote:

> Hello,
> 
> Whilst playing around with tlaplus and trying to learn how to specify consensus algorithms I stepped across the refinement example by Leslie Lamport ("Mechanically Checked Safety Proof of a Byzantine Paxos Algorithm") found here: http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html
> 
> In the very basic Consensus.tla I stepped over an Axiom regarding the SingletonCardinality of sets (i guess). As I am very inadept with tla / pluscal I address my question to this group instead of adressing it directly to Mr. Lamport.
> 
> As far as I understand it, the axiom:
> 
> AXIOM SingletonCardinality == 
>          \A e : IsFiniteSet({e}) /\ (Cardinality({e}) = 1)
> 
> always evaluates to true, as {e} is always a set with a single entry, "e".
> 
> I guess the axiom would be correct if one would spare the {} brackets in both cases. Obviously the following test would then fail:
> 
> SingleCardinalityTest == 
>  \A e \in SUBSET {"a", "b", "c"} : IsFiniteSet({e}) /\ (Cardinality({e}) = 1)
> 
> as the SUBSET operator also produces {"a","b"} and alike.
> 
> So did I find a typo here or is the behaviour intended?
> 
> Best regards,
> Christian Spann
> 
> -- 
> 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+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/groups/opt_out.