FM Thesis

So yesterday I polished off chapters 4 and 5 of Using Z and I finished chapter 6 tonight. With any luck, I'll get a good start on chapter 7 before bed. It's a much faster read than I would have expected, but that might just be because I haven't gotten into the really heavy stuff yet.

Chapter four discussed rules for equality of expressions and introduced the "one-point" rule for reasoning with existential quantifiers. It also included some interesting examples of predicates describing uniquness with quantifiers and introduced the mu notation for definite description. That was something I had not seen before. The notation is (μ x: a | p), which denotes the unique object x in set a which satisfies predicate p.

Chapter five was an overview of basic set theory, including things like the inference rules regarding set conprehension. It also included basics such as definitions of the union, intersection, and difference operations, and all that good stuff. It also included a brief definition of types in Z. It turns out that Z types are maximal sets, often defined in terms of power sets or Cartesian products.

Chapter six was an introduction to defining things in Z. This includes defining types, declaring objects, and introducing axioms. The basic syntax is fairly straight forward so far. The only problem I had was trying to figure out the relevance of power sets of power sets.

To take the example from page 82, the predicate "is a crowd" was formalized as:
crowds: P(P Person)
crowds = {s: P Person | #s >= 3}
This indicates that crowds is an element of the power set of the power set of all people and that crowds is the set of all members of the power set of people with three or more members. After thinking about this for a few minutes, it started to become clear what that means. The set of all crowds is a set of sets, so its elements obviously have to belong to the power set of all people. But since a type is a maximal set, what is the type of crowds? Obviously it must be P(P Person), since crowds must be an element of that. And since crowds contains elements of P Person, we end up with each element of crowds being a set of individual people.

It all makes perfect sense, really. It's just a different type and level of abstraction than I'm used to using. I just needed to stop for a few minutes and wrap my brain around.