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:

This indicates that *crowds*: **P**(**P** *Person*)*crowds* = {*s*: **P** *Person* | #*s* >= 3}*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.

You can reply to this entry by leaving a comment below. You can send TrackBack pings to this URL. This entry accepts Pingbacks from other blogs. You can follow comments on this entry by subscribing to the RSS feed.

## Add your comments #

A comment body is required. No HTML code allowed. URLs starting with http:// or ftp:// will be automatically converted to hyperlinks.