This project will have two parts. The first week of June we'll see how to construct symmetric models of ZF. These are submodels of generic forcing extensions that don't necessarily satisfy the axiom of choice. We'll see what are good properties for a symmetric model to satisfy and how we can ensure such properties. One can read about this technique in Jech's books "Set theory" and "The axiom of choice". There forcing is done with Boolean valued models. We'll see the method when forcing with partial orders. The second part of the project will take place during the last two weeks of June. Then we'll see how to construct a set version of the first Gitik model, from his paper "All uncountable cardinals can be singular". This will be a model of ZF in which for any desired ordinal alpha, the first aleph_alpha-many uncountable cardinals are singular. To construct such a model we'll start from a model of ZFC + "there is a sequence of alpha-many strongly compact cardinals that has no regular limits". Experience with strongly compact cardinals or other large cardinals is not necessary. If time permits we'll see how to do class forcing (forcing with a class sized partial order) and take a look at the full version of the first Gitik model, where all uncountable cardinals are singular. We won't really follow Gitik's paper, we'll actually see a simpler version of his construction that does the same job. It is therefore not necessary (perhaps even unhelpful) to read Gitik's paper in advance, but it might be interesting to have it around when reviewing the notes from our meetings.