December 16, 2022

# Commissioning and Performance of the New ALICE Inner Tracking System in the
First Phase of LHC Run 3

Ivan Ravasenga1 for the ALICE Collaboration 1CERN1CERN Geneva Geneva
Switzerland Switzerland<EMAIL_ADDRESS>
###### Abstract

ALICE is one of the four experiments at the CERN Large Hadron Collider (LHC)
specifically designed to study nuclear matter at extreme conditions of
temperature and pressure. The LHC Run 3 started officially in July 2022 with
proton–proton (pp) collisions at a centre-of-mass energy $\sqrt{s}$ = 13.6 TeV
after a shutdown of more than two years to allow for the upgrade of both the
accelerator and the experiments. To fulfill the requirements of the ALICE
physics program for Run 3, new timing, tracking and multiplicity detectors
have been installed in the ALICE central barrel both at mid- and forward
rapidities, the readout electronics of the majority of the detectors has been
upgraded and the ALICE Offline and Online computing farm has been completely
renewed. A key detector of the apparatus is the new, ultra-light, high-
resolution Inner Tracking System (ITS2) that significantly enhances the
resolution on the determination of the distance of closest approach to the
primary vertex, the tracking efficiency at low transverse momenta, and the
read-out rate capabilities with respect to what was achieved in the LHC Run 2
with the older tracker. The new tracker consists of seven layers, azimuthally
segmented into Staves, equipped with silicon Monolithic Active Pixel Sensors
with a pixel size of 27$\times$29 $\mu$m2 covering a sensitive area of about
10 m2. A long effort allowed the construction, characterization, installation
and commissioning of the ITS2 before starting Run 3. The in-pixel
discriminator threshold calibration represents a challenging procedure due to
the huge number of channels and it is carried out by exploiting the power of
the ALICE Offline and Online farm. The detector took data for the full 2022
and its first performance results represent the second key part of this
article.

LHC, ALICE, tracker, track, cluster, pixel, silicon, run, calibration,
detector, alignment

##  1 The upgraded Inner Tracking System

To fullfil the requiments of the Run 3 physics program of the CERN Large
Hadron Collider (LHC), the Inner Tracking System (ITS) of the ALICE experiment
has been upgraded with seven cylindrical and concentric layers of silicon
Monolithic Active Pixel Sensors (MAPS) called ALPIDE covering a total active
area of about 10 m2 [1]. The detector is divided into three Inner Layers (IL),
two Middle Layers (ML) and two Outer Layers (OL) as shown in Fig. 1. The four
outermost layers constitute the Outer Barrel (OB) while the three innermost
layers form the Inner Barrel (IB). The main features of the upgraded ITS
(simply called ITS2 in the following) compared to the ones of the older
detector (called ITS1) are summarised in Table 1.

Figure 1: Schematic layout of the upgraded ITS.

The sensor, produced by TowerJazz in the 0.18 $\mu$m CMOS imaging process
technology, features a pixel size of $\sim$27$\times$29 $\mu$m2 with a total
of 512 $\times$ 1024 pixels. The main characteristics of ALPIDE are:

  1. 1.

a n-well diode about 100 times smaller than the pixel size, leading to a small
capacitance of few fF;

  2. 2.

a fast data driven encoder [2];

  3. 3.

a n-well of p-MOS transistors shielded by a deep p-well allowing a full CMOS
circuitry within the active volume [3, 4];

  4. 4.

a pixel analogue signal amplified and digitized at a pixel level leading to a
low power consumption of about 40 mW/cm2;

  5. 5.

the possibility to apply a moderate reverse bias voltage to the substrate
between $-$6 V and 0 V.

Table 1: Main technological features of updraded ITS (ITS2) compared to the older ITS (ITS1). The radial positions are the average between the minimum and maximum radii of the innermost layer. | ITS1 | ITS2
---|---|---
Readout rate | up to 1 kHz |  $>$ 100 kHz (Pb–Pb)
|  |  $>$ 400 kHz (pp)
Material budget | 1.1% X0 | 0.36% $X_{0}$ (Inner Barrel)
|  | 1.1% $X_{0}$ (Outer Barrel)
Pixel size | 50$\times$425 $\mu$m2 | 27$\times$29 $\mu$m2
Pointing resolution ($p_{\rm T}$ = 500 MeV/$c$) |  $\sim$240 $\mu$m ($z$) |  $\sim$50 $\mu$m ($z$)
|  $\sim$120 $\mu$m ($r\varphi$) |  $\sim$40 $\mu$m ($r\varphi$)
Standalone tracking efficiency ($p_{\rm T}$ = 200 MeV/$c$) |  $\sim$60% |  $\sim$90%
Radius (innermost layer) | 3.9 cm | 2.5 cm

In the ITS2, the ALPIDE chips are arranged in Hybrid Integrated Circuits (HIC)
featuring 14 (9) ALPIDE chips for the OB (IB). A Flexible Printed Circuit
(FPC) wire-bonded to the chips into a HIC is used for clock, control and data
transmission towards and from the outside electronics [1]. For IB chips, a
readout at 1.2 Gb/s per chip is achieved while for the OB a group of 7 chips
is readout with a single link at 400 Mb/s. The HICs are glued on a cold plate
for chip cooling. The IB cold plate is attached to a ultra-light space-frame
forming a Stave with a total length of 27 cm. In the OL(ML), 7(4) HICs are
glued on cold plate to build an Half-Stave (HS) with a total length of 147(84)
cm. Two HSs are then aligned on a carbon-fiber support structure (space frame)
with $\sim$100 $\mu$m precision to assemble the final Stave. The Stave
features also two power buses and two bias buses (one per HS) for chip
powering and chip reverse bias voltage supply, respectively. A schematic view
of the ITS2 Staves is given by Fig. 2. In summary, ITS2 is composed by 192
Staves on which 24120 sensors are mounted for a total of 12.5 billion pixels,
being the largest pixel tracker ever built.

Figure 2: View (not to scale) of an Inner Barrel Stave (left) and of an Outer
Barrel Stave (right) of upgraded ALICE ITS.

##  2 Data readout architecture

The huge amount of channels of ITS is readout by 192 identical Readout Units
(RU) which provide control and trigger, and read the high-speed data lines
from the ALPIDE chips with a total data rate of up to $\sim$40 GB/s. To
minimize the power consumption and achieve the maximum bit rate of 1.2 Gb/s,
the RUs and the ITS2 Power Boards (PB) are located within the ALICE L3 magnet,
in a magnetic field of 0.5 T, and are exposed to the radiation environment.
Both sytems were tested and validated under these conditions [5]. The RU
design thus makes use of two programmable logic devices, one of them a flash-
based FPGA, whereas the other is a Static RAM (SRAM)-based FPGA. The first is
responsible for auxiliary tasks, such as configuring the other FPGA and
periodically refreshing (“scrubbing”) its Configuration RAM (CRAM). The latter
is implementing the main functionality of the RU, being in charge of data
readout from the sensor, assembling sensor data into event frames and
communicating those to the ALICE Offline and Online (O2) computing system [6],
receiving triggers from the ALICE Central Trigger Processor [7], control,
configuration and monitoring of the ALPIDE sensors, as well as control and
monitoring of the PB, which provides the power to the ALPIDE.
The 192 RUs are connected through GigaBit Transceiver (GBT) links (up to 3 per
RU) to 22 Common Readout Units (CRU) which are mounted into 13 First Level
Processors (FLP, CPU servers) located about 200 m far from the detector, in a
non-radiation environment, which are part of the O2 DAQ farm. The CRUs are
custom-FPGA based boards with up to 24 bi-directional fiber-optic links and a
PCIe interface to the relative FLP. The FLPs communicate via a shared network
with the processors of the Detector Control System (DCS) and transfer DCS data
to and from the RUs via their associated CRUs. Trigger information is
communicated from the trigger system to both the RUs and the CRUs so that
event fragments from various RUs can be associated with the appropriate
triggers. As a backup, when the O2 system and its optical links are not
available (e.g. during system maintenance) the RU is equipped with a CAN bus
communication interface for control and monitoring.
The FLPs are connected to a farm of 250 Event Processing Nodes (EPN) shared
among all the ALICE detectors which feature 32-core AMD Rome CPUs and 8 AMD
MI50 graphics processing units (GPUs) each. By using the computing farm, the
data can be processed synchronously, for time frame building, online
reconstruction and calibration, or asynchronously, for final calibration and
full reconstruction.
Finally, the EPN farm is connected to a 100 PB disk buffer. A 100 GB/s link
connects the disk buffer to the permanent storage facility. Figure 3
summarizes the data readout chain of ITS2 up to the FLPs.

Figure 3: Summary scheme of the data readout achitecture of ITS2.

##  3 Detector Control System and Data Quality Control

As described in Sec. 2, the FLPs communicate via a shared network with the
machines of the Detector Control System and tranfer DCS data to and from the
RUs via their associated CRUs. The DCS functionalities are accessible through
a WinCC panel and they mainly include:

  * •

a Finite State Machine (FSM) allowing for detector operations: powering and
configuration. Different statuses of the detector are encoded by different
colors for the various components of the detector, from the barrels to the
single HICs;

  * •

a full color-encoded (status-dependent) map of the detector with access to
single stave functional parameters: power supply voltage and currents of the
stave and its electronics, status of the power supply, temperature, status of
the cooling lines;

  * •

widgets which allow to configure the detector for different kind of runs:
physics, calibration, simulated data patterns.

An independent ITS Safety System (ITS2S) interlocks the power channels based
on the stave temperatures and cooling loop statuses.
The DCS is used both by detector experts and central ALICE shifters for
everyday operations with the detector (powering, configuration, calibration,
etc.) and for the monitoring of all its functional parameters. Based on that,
a set of alarms pops up in case one or more operating parameters overcome the
limits of their optimal working ranges.
Another important branch in the context of the control systems is represented
by the Data Quality Control System (simply called QC in the following) which
is capable to synchronously monitor the following data:

  * •

detector fake-hit rate: monitoring of detector raw hits and noisy pixels;

  * •

front-end electronics: monitoring of the number of channels in error and of
the trigger flags;

  * •

decoding errors: monitoring of decoding errors for every chip;

  * •

clusters: monitoring of the cluster size and of the cluster occupancy in every
detector sensor;

  * •

tracks: monitoring of track multiplicty in every readout frame, angular
distributions ($\eta$ and $\varphi$), clusters per track, etc.;

  * •

calibration data: monitoring of calibration data during special calibration
runs. The main variables are the amount of problematic and dead pixels in the
detector and the in-pixel discriminator thresholds. This is extremely
important so to guarantee a stable and efficient data taking.

In addition, a set of post-processing tasks has been developed in order to
monitor the stability of the above parameters over time on a run-by-run basis
or during the run itself. As for the DCS, also the QC system is used on an
everyday basis for the online quality control of the data but also for the
offline reconstruction in order to ensure the preparation of a good data
sample for the subsequent physics analyses.
Finally, the quality control of the data happens also at Monte Carlo level to
check the tracking efficiency, the impact-parameter distributions and the raw
particle momentum distributions. Every QC task is developped in C++ and is
part of the ALICE O2 software [8].

##  4 Detector commissioning, installation and preparation for Run 3

The detector assembly was performed in a clean room, where staves have been
mounted in two IB and two OB half-barrels, connected to final services (power,
cooling, readout) installed in an adjacent room (Fig. 4). The on-surface
commissioning of the detector started in September 2019 and continued until
December 2020 to validate in sequence each of the four half-barrels after
assembly.

Figure 4: The ALICE ITS2 in the CERN clean room split in half-barrels during
the on-surface commissioning.

In the last phase of the on-surface commissioning the detector was continuosly
in operation with 24/7 shifts: several cosmic and calibration runs were
recorded and analysed with the aim of validating the detector stability. An
important result of this phase is shown in Fig. 5 where the average detection
efficiency of the outermost half-barrels is plotted. As can be seen, an
efficiency above 99.5% is obtained. This is well in line with the detector
requirements for Run 3. The bottom panel of the plot shows the number of
cosmic tracks taken into account for the measurements, different for top and
bottom barrels due to their separated position in the laboratory.

Figure 5: Detection efficienty of ITS2 outer half-barrels calculated with
cosmic muons during the on-surface commissioning. The bottom panel shows the
number of cosmic tracks considered for the analysis in each half-barrel.

The installation of the detector in the cavern has been performed in two
phases: first the outer barrel was installed inside the ALICE Time Projection
Chamber (TPC) and, successively, the inner barrel was positioned around the
beampipe. The installation of the full tracker represented a challenge mainly
because of a small clearance between adjacent staves of only 1.2 mm (when
approaching the two half-barrels) and of a clearance around the beam pipe of
only 2 mm. In addition, the manipulation of the barrels had to be performed
from a distance of about 4 m. Several cameras where mounted in different spots
to constantly monitor the position of the barrels during the insertion and the
final approach of the two halves. The installation of the full detector was
completed in May 2021. A basic verification of the detector followed after
installation including power tests, readout tests and resistance measurements
of the data lines to ensure the reliability of all cable connections.
The beginning of summer 2021, till July, was dedicated to the ITS2 standalone
commissioning with 24/7 shifts. In this phase the detector was fully
recommissioned with continuos cosmic data taking and calibration runs. In
addition, the full readout chain has been tested by simulating the data load
provided by high multiplicity pp collisions and central lead–lead collisions:
the hits extracted from the Monte Carlo simulation, were used to pulse the
pixels involved so to simulate the hit occupancy of real collisions.
In July 2021 the ALICE global commissioning started with the aim of validating
the full ALICE software for data taking and reconstruction in view of the very
first pp pilot collisions at LHC injection center-of-mass energy ($\sqrt{s}$ =
900 GeV) which happened at the end of October 2021. Figure 6 shows an event
display of that period with reconstructed tracks in ITS2 and in the external
TPC in one Time Frame (TF) corresponding to a time interval of 11.5 ms
containing about 6 collisions (due to the low interaction rate (IR) of the
bunches).

Figure 6: Event display of the very first pp pilot collisions at $\sqrt{s}$ =
900 GeV of October 2021.

##  5 Calibration of ITS2

The calibration of ITS2 mainly consists in the determination and tuning of its
in-pixel discriminator thresholds, and in the masking of its noisy pixels
based on the selected target threshold. The measurement of the in-pixel
threshold is based on the injection of an analogue pulse with amplitudes
ranging from 0 to 500 electrons. The pixel response is fit with an error
function to extract the 50% point (threshold) and the sigma (ENC noise).
Similarly, the tuning of the thresholds is obtained by injecting a fixed pulse
equal to the target threshold (typically 100 or 150 electrons at which the
ALPIDE is known to be fully efficient [4]), and by varying the registers which
are responsible for the variation of the threshold itself.
Once the threshold is fixed, a standard cosmic run is used to tag the most
noisy pixels in the detector and to prepare a detector configuration
containing the proper masking: every pixel in the IB(OB) with an occupancy
above 10-2(10-6) hits/event is tagged as noisy and masked. The looser
selection for the IB is chosen in order to maximize the detection efficiency.
With a typical average threshold of 100 electrons, the number of masked pixels
amounts to only $\sim$0.015% of the total. This leads to an overall fake-hit
rate of about 10-8 hits/event/pixel in average (stable over time), well below
the required 10-6 hits/event/pixel by design as shown in Fig. 7.

Figure 7: Average fake-hit rate for each layer of ITS2 as a function of time
after masking about 0.015% of the pixels of the full detector.

In order to run the calibration scans, the ITS2 RUs contain a sequencer to
trigger the pulses to the chips, which allows the scan execution to be
controlled entirely by the DCS software.
The main challenge resides in the decoding and the threshold extraction of the
12.5 billion channels. A threshold scan of the full detector with 50 charge
injection points and 50 hits per point results in about 3 $\times 10^{13}$
hits or approximately 100 TB of raw hit data. If the scan is performed as fast
as the on-detector bandwidth allows, this data is collected in slightly less
than 1 hour, resulting in a data rate of 20–30 GB/s. However, a full scan is
generally used as a reference and it is not needed on a daily basis. In fact,
to ensure a good threshold calibration of the detector it is sufficient to
pulse about 1–2% of the pixels with the advantage of completing the scan in
less than 5 minutes.
In order to cope with the amount of data the analysis is performed in a
distributed manner on the EPNs. A special configuration of the sub-timeframe
builder is used, since the requirements of the calibration are orthogonal to
standard data taking: whereas in data taking single events of the full
detector are assembled to one time-frame and shipped to available EPNs, in
calibration a number of consecutive events belonging to a group of chips (a
so-called “link”) must be analysed together on the same EPN. As a consequence,
the sub-timeframe builder sends all events of a detector link to the same
processing node, thus reducing significantly the bandwidth used for data
transfer between the processing nodes. Figure 8 shows the distribution of the
threshold for 2% of the pixels in all the 24120 sensors of ITS2 after a tuning
with a target threshold of 100 electrons. The typical ENC noise is of only 5
electrons and it is observed to be stable for all chips.

Figure 8: Bi-dimensional distribution of the threshold of 2% of the pixels in
all the 24120 sensors of ITS2 after a tuning with a target threshold of 100
electrons. About 2.1% of the pixels are considered for this measurement, which
is enough to evaluate the quality of the detector calibration.

In summary, every parameter related to calibration (addresses of the pixels to
be masked, ALPIDE register settings for threshold tuning) is used to prepare a
new detector configuration in the configuration database by using a dedicated
WinCC panel in the DCS sofware.

##  6 Start of LHC Run 3 and ITS2 performance

The LHC Run 3 started officially on July 5th, 2022 with pp collisions at the
unprecedented energy of $\sqrt{s}$ = 13.6 TeV. As of today, the ALICE detector
accumulated about 700h of data taking with pp collisions and 10.6 hours of
Pb–Pb pilot collisions at a center-of-mass energy per nucleon pairs of
$\sqrt{s_{\rm NN}}$ = 5.36 TeV. The nominal IR of the proton bunches in LHC is
about 500 kHz and the ITS2 is readout in continuos mode at a framing rate
nominally set to 202 kHz. High-rate rate scans have also been performed by
increasing the IR up to 4–5 MHz. For the first Pb–Pb test, the IR was about 42
Hz and the ITS2 took data in continuous mode at a framing rate of 67 kHz. The
loss of acceptance of ITS2 during the runs is generally below 1% which is in
agreement with the design requirements for Run 3. At every beam dump, a scan
of the pixel thresholds is performed to ensure that the detector remains fully
efficient in the subquent runs.
Figure 9 shows an event display with reconstructed ITS2-standalone tracks in
pp collisions at $\sqrt{s}$ = 13.6 TeV at an IR of the proton bunches of about
1 MHz.

Figure 9: Event display of 1 readout frame in pp collisions at $\sqrt{s}$ =
13.6 TeV with an average IR of the proton bunches of about 1 MHz. The ITS2
framing rate was 202 kHz which corresponds to a time-length of the frame of
about 5 $\mu$s.

###  6.1 Performance of ITS2

This section aims at illustrating the first performance results of ITS2 in Run
3 pp collisions at $\sqrt{s}$ = 13.6 TeV. The first piece of information which
is important for a pixel detector is the size of the clusters and their
occupancy. Studies with machine learning techniques are ongoing in order to
exploit the cluster size for the identification of pions, kaons and protons
down to an unprecedented low transverse momentum $p_{\rm T}$ $<$ 0.1 GeV/$c$.
Left panel of Fig. 10 shows the average cluster size for each half-layer of
the ITS2 in a pp run of Run 3 ($\sqrt{s}$ = 13.6 TeV) at an IR of the bunches
of about 1 MHz and at an ITS2 framing rate of 202 kHz. The minimum granularity
for layers 0, 1 and 2 is the single chip while for the outermost layers it is
given by the single HIC. As shown in Fig. 10, the cluster size ranges between
3 and 8 pixels depending on the pseudo-rapidity $\eta$. The dependence of the
cluster size on the bunch IR is shown in the right panel of Fig. 10 including
the results from a simulation based on 20000 events generated with Pythia 8
[9] and propagated with Geant 3 [10] through the detector material. Based on
what shown in Fig. 7, the noise in the simulation is set to 2 $\times$ 10-8 (3
$\times$ 10-9) hits/event/pixel for the IB(OB). In general a good agreement
between data and simulation is observed in average, within 5-6%. The main
source of discrepancy resides in the approximation of the noise simulation
where only an average per barrel is considered instead of a single-chip value.
The slight dependence of the cluster size on the IR can be explained by the
fact that at low IR, the noise hits (1-pixel clusters) become comparable to
the physics hits ($>$ 1-pixel clusters) lowering the cluster size as a
consequence.

Figure 10: Left figure shows the average cluster size for each half-layer of
the ITS2 in a pp run of Run 3 ($\sqrt{s}$ = 13.6 TeV) at an IR of the bunches
of about 1 MHz and at an ITS2 framing rate of 202 kHz. The minimum granularity
for the layers 0, 1 and 2 is the single chip while for the outermost later it
is given by the single HIC. Right figure shows the dependence of the cluster
size on the bunch IR including the results from a simulation based on Geant 3
and Pythia 8.

The average amount of clusters per readout frame and per chip in the full
detector is instead shown in the left part of Fig. 11 for a pp run of Run 3
($\sqrt{s}$ = 13.6 TeV) at an IR of the bunches of about 1 MHz and at an ITS2
framing rate of 202 kHz. With these parameters, the cluster occupancy ranges
between 0.1 and 10 clusters per readout frame per chip depending on $\eta$. As
opposed to the cluster size, the cluster occupancy is strongly dependent on
the IR as shown on the right panel of Fig. 11 together with the very same
simulation results explained at the beginning of this paragraph. In general a
good agreement between data and simulation is observed considering the
limitations previously explained.

Figure 11: Left figure shows the average cluster occupancy (number of clusters
per readout frame per chip) for each half-layer of the ITS2 in a pp run of Run
3 ($\sqrt{s}$ = 13.6 TeV) at an IR of the bunches of about 1 MHz and at an
ITS2 framing rate of 202 kHz. The minimum granularity for the layers 0, 1 and
2 is the single chip while for the outermost later it is given by the single
HIC. Right figure shows the dependence of the cluster occupancy on the bunch
IR including the results from a simulation based on Geant 3 and Pythia 8. See
text for further details.

The tracks in the ITS2 are recontructed by using a Cellular Automaton (CA)
algorithm synchronously running on the EPNs. After a preliminary vertex
position estimation, needed as seed, the tracking phase is constituted by
three macro steps: tracklet finding, cell finding and track finding [1]. In a
subsquent phase, the ITS-standalone tracks are matched with the TPC tracks as
explained in detail in Ref. [11]. The tracking algorithm performance is
strongly influenced by the detector alignment (obtained with the Millepede
software [12]) which is currently in its close-to-final version. At the
moment, at $p_{\rm T}$ $>$ 3 GeV/$c$ a pointing resolution of about 10 $\mu$m
is measured (residual misalignment contributions are not negligible here) in
$r\varphi$ direction while at lower momenta the resolution agrees with design
specifications (see Table 1). In addition, the signal of the K${}^{0}_{S}$ can
be already extracted as shown in Fig. 12 with a preliminary study using ITS-
standalone tracks in Run 3 pp collisions at $\sqrt{s}$ = 13.6 TeV. Further
studies are ongoing to fine tune the detector alignment parameters and to
study the performance of the detector in different conditions.

Figure 12: $p_{T}$-integrated invariant mass peak of the K${}^{0}_{S}$
obtained with the ITS-standalone tracking in pp collisions at $\sqrt{s}$ =
13.6 TeV.

Finally, the angular distribution (correlation between the azimuthal angle
$\varphi$ and the pseudo-rapidity $\eta$) of the reconstructed ITS2 tracks is
shown in Fig. 13 for pp collisions at $\sqrt{s}$ = 13.6 TeV at an IR of about
1 MHz.

Figure 13: Correlation between the azimuthal angle $\varphi$ and the pseudo-
rapidity $\eta$ of the reconstructed ITS2 tracks in pp collisions at
$\sqrt{s}$ = 13.6 TeV at an IR of about 1 MHz.

##  7 Summary

The upgraded Inner Tracking System (ITS2) of the ALICE experiment is composed
by seven layers of silicon Monolithic Active Pixel Sensors with a total number
of 12.5 billion pixels, being the largest pixel tracker ever built. It has
been successfully installed in the ALICE cavern in May 2021 after about 1.5
years of commissioning on surface. The detector is readout by 192 identical
FPGA-based readout units which communicate with the ALICE Offline and Online
farm made of 13 First Level Processors (for ITS2 only) and 250 Event
Processing Nodes for the synchronous and asynchronous calibration and
reconstruction of the data. The Detector and Data Quality Control Systems are
available to monitor the detector and its services, to operate the detector
for data taking and to synchronously check the quality of the data.
The calibration of the detector mainly consists in the tuning of the in-pixel
discriminator thresholds, in their measurement and in the monitoring of their
stability over time. The calibration of the detector channels is challenging
due to its large number channels. As a consequence, the procedure fully
exploits the parallel processing on the powerful Event Processing Nodes.
The commissioning in the cavern, completed in June 2022, allowed the
resolution of various hardware issues related to services and the full
validation of the software for data taking and reconstruction. Since the start
of the LHC Run 3 in July 2022, ALICE accumulated about 700h of data taking and
the ITS2 main functional parameters were observed to be stable over time:
average fake-hit rate at a level of 10-8 hits/event/pixel by masking only
$\sim$0.015% of the total number of pixels, an average cluster size between 3
and 8 pixels and a realiable track reconstruction and detector alignment in
software. ITS2 will continue to record data for the full Run 3 and it is ready
for the first lead–lead collisions at top energy foreseen in October 2023.

## References

  * [1] ALICE Collaboration, Technical Design Report for the Upgrade of the ALICE Inner Tracking System, J. Phys. G41 2014 087002.
  * [2] Yang P. et al., Low-power priority Address-Encoder and Reset-Decoder data-driven readout for Monolithic Active Pixel Sensors for tracker system, Nucl. Instrum. Meth. A 785 2015 61.
  * [3] Aglieri Rinella G. et al., The ALPIDE pixel sensor chip for the upgrade of the ALICE Inner Tracking System, NIM A 845 2017 583-587.
  * [4] $\check{S}$ulji$\acute{c}$ M. et al., ALPIDE: the Monolithic Active Pixel Sensor for the ALICE ITS upgrade, JINST 11 2016 C11025.
  * [5] Schambach J. et al., A Radiation-Tolerant Readout System for the ALICE Inner Tracking System Upgrade, 10.1109/NSSMIC.2018.8824419.
  * [6] ALICE Collaboration, Technical Design Report for the Upgrade of the Online-Offline Computing System, CERN-LHCC-2015-006, ALICE-TDR-019 2015.
  * [7] Kvapil J. et al., ALICE Central Trigger System for LHC Run 3, arXiv2106.08353, 10.1051/epjconf/202125104022, EPJ Web Conf. 251 04022, 2021.
  * [8] Quality Control project in the ALICE O2: https://github.com/AliceO2Group/QualityControl.
  * [9] Sjöstrand T. et al., An introduction to PYTHIA 8.2, 10.1016/j.cpc.2015.01.024, Comput. Phys. Commun., 191 159–177, 2015.
  * [10] Brun R. et al., GEANT3, CERN-DD-EE-84-1, 1987.
  * [11] Rohr D. et al., GPU-accelerated track reconstruction in the ALICE High Level Trigger, 2017 J. Phys.: Conf. Ser. 898 032030.
  * [12] https://www.desy.de/ kleinwrt/MP2/doc/html/index.html.


$\mathbb{P}_{n}^{\alpha}=\mathbb{P}_{n}^{J}\cap X_{\alpha}$ for all
$n<\omega$, and $S_{\alpha}$ codes $X_{\alpha}$. Let $M_{\alpha}$ be the
transitive collapse of $X_{\alpha}$. Then $\mathbb{P}_{n}^{\alpha}$ is the
image of $\mathbb{P}_{n}^{J}$ under the collapse and $\alpha$ is the image of
$\omega_{1}$. Let $\bar{\mathcal{A}}=\mathcal{A}\cap X_{\alpha}$ be the image
of $\mathcal{A}$. So at stage $\alpha$ in the construction of $\vec{P}^{J}$,
we chose a forcing extension $M_{\alpha}[G]$ of $M_{\alpha}$ by
$\mathbb{Q}(\vec{P}_{\alpha},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ and
let $\mathbb{P}^{\alpha+1}_{n}=(\mathbb{P}_{n}^{\alpha})^{*}$ be constructed
in $M_{\alpha}[G]$. By Lemma 6.13, $\bar{\mathcal{A}}$ remains maximal in all
further $\mathbb{P}(\vec{P}_{\beta},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ for
$\beta>\alpha$, and hence $\bar{\mathcal{A}}$ remains maximal in
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$. It
follows that $\bar{\mathcal{A}}=\mathcal{A}$ is countable. ∎

##  7\. The generalized Kanovei-Lyubetsky Theorem

Now that we have constructed the $\omega$-iteration
$\vec{P}^{J}=\langle\mathbb{P}_{n}^{J}\mid n<\omega\rangle$ and the
corresponding tree iteration
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ of
Jensen’s forcing, we would like to generalize the Kanovei-Lyubetsky argument
of Section 3 to prove the analogue of the “uniqueness of generics” property
for tree iterations. Namely, we will show that in a forcing extension $L[G]$
by $\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega})$ the only
$L$-generic filters for $\mathbb{P}_{n}^{J}$ are the restrictions of $G$ to a
level $n$ node.

Suppose that $\vec{P}=\langle\mathbb{P}_{n}\mid n<\omega\rangle$ is an
$\omega$-iteration of perfect posets and $H$ is a generic filter for
$\mathbb{P}(\vec{P},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$.
Given a node $s$ on level $n$ of ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega$, let
$x_{s}$ be the $n$-length sequence of generic reals added by $H$ on node $s$
and let $\dot{x}_{s}$ be the canonical name for $x_{s}$.

For the next lemma, suppose that $\vec{P}=\langle\mathbb{P}_{n}\mid
n<\omega\rangle$ is an $\omega$-iteration of perfect posets that is an element
of a suitable model $M$. We should think of $\vec{P}$ as one of the
$\omega$-iterations $\vec{P}_{\alpha}$ arising at stage $\alpha$ in the
construction of the $\omega$-iteration $\vec{P}^{J}$ and we should think of
$M$ as the model $M_{\alpha}$ from that stage.

######  Lemma 7.1.

In $M$, suppose that $\dot{r}$ is a
$\mathbb{P}(\vec{P},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$-name
for an $n$-length sequence of reals such that for all nodes $s$ on level $n$
of ${}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega$,

$\mathop{1\hskip-2.5pt{\rm
l}}\Vdash_{\mathbb{P}(\vec{P},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)}\dot{r}\neq\dot{x}_{s}.$

Then in a forcing extension $M[G]$ by
$\mathbb{Q}(\vec{P},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$, for
every node $s$ on level $n$ of ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega$, the
set of conditions forcing the statement

$\Phi(s):=$“If $\dot{r}$ is $M[G]$-generic for $\mathbb{P}^{*}_{n}$, then
$\langle\mathcal{T}^{0}_{s(0)},\dot{\mathcal{T}}^{1}_{s(1)},\ldots,\dot{\mathcal{T}}^{n-1}_{s(n-1)}\rangle$
is not in the filter determined by $\dot{r}$.”

is dense in $\mathbb{P}(\vec{P}^{*},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$.

###### Proof.

Fix a condition
$f_{X}\in\mathbb{P}(\vec{P}^{*},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ and a
node $d$ on level $n$ of ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega$. We
need to find a condition $f^{\prime}_{X^{\prime}}\leq f_{X}$ such that
$f^{\prime}_{X^{\prime}}\Vdash\Phi(d)$. Since $\mathbb{U}$ is dense in
$\mathbb{P}(\vec{P}^{*},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$, we
can assume without loss that $f_{X}\in\mathbb{U}$. For a node $s$ on level $m$
of $X$, let

$f_{X}(s)=(\mathcal{T}_{j_{0,s}}^{0}\wedge
S_{0,s},\ldots,\dot{\mathcal{T}}_{j_{m-1,s}}^{m-1}\wedge\dot{S}_{m-1,s}).$

Let $\langle j_{0,s},\ldots,j_{m-1,s}\rangle=\vec{j}_{s}$, and note that we
can have $\vec{j}_{s}=\vec{j}_{s^{\prime}}$. By strengthening if necessary, we
can assume that there is a node $s\in X$ with $\vec{j}_{s}=d$. Repeatedly
using the construction in the proof of Lemma 6.7 on terminal nodes, we can
find a determined condition $g_{Y}\in G$ with
$g_{Y}(\vec{j}_{s})=(q_{\vec{j}_{s}},F_{\vec{j}_{s}})$ such that for every
node $s\in X$, some $\tau_{s}:m\to{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}2$ lies on
$(q_{\vec{j}_{s}},F_{\vec{j}_{s}})$ with

$q_{\vec{j}_{s}}(0)_{\tau_{s}(0)}\leq S_{0,s}$, and for all $1\leq i<m$,
$(q_{\vec{j}_{s}}\upharpoonright i)\mid(\tau_{s}\upharpoonright i)\Vdash
q_{\vec{j}_{s}}(i)_{\tau_{s}(i)}\leq\dot{S}_{i,s}$.

The construction gives $\tau_{s}$ satisfying that if $s^{\prime}$ extends $s$,
then $\tau_{s^{\prime}}$ extends $\tau_{s}$.

Now we are going to construct a condition
$a_{A}^{g}\in\mathbb{P}(\vec{P},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ with
$a_{A}^{g}(s)=q_{s}$ associated to $g_{Y}$, satisfying the following
properties:

  1. (1)

$X\subseteq A$ and for every node $s\in X$, $q_{s}\leq
q_{\vec{j}_{s}}\mid\tau_{s}$.
There is $X\subseteq\bar{A}\subseteq A$ such that:

  2. (2)

For every $\sigma$ which lies on $(q_{d},F_{d})$, there is a node
$s_{\sigma}\in\bar{A}$ such that $q_{s_{\sigma}}\leq q_{d}\mid\sigma$.

  3. (3)

For every node $s$ on level $n$ of $\bar{A}$, $a_{A}^{g}$ forces over
$\mathbb{P}(\vec{P},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ the
statement:

“There is $i<n-1$ such that $\dot{r}\upharpoonright i$ is (ground model)
generic for $\mathbb{P}_{i}$ and
$\dot{r}(i)\notin[(a_{A}^{g}(s)(i))_{\dot{r}\upharpoonright i}]$.”

Let $a_{\bar{A}}$ be a condition in
$\mathbb{P}(\vec{P},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ with
$X\subseteq\bar{A}$ be such that $a_{\bar{A}}(s)=q_{\vec{j}_{s}}\mid\tau_{s}$
for every node $s\in X$, and for every $\sigma$ which lies on $(q_{d},F_{d})$,
there is a node $s_{\sigma}\in\bar{A}$ such that
$a_{\bar{A}}(s_{\sigma})=q_{d}\mid\sigma$. Fix a node $s$ on level $n$ of
$\bar{A}$ and consider a forcing extension $M[H]$ by
$\mathbb{P}(\vec{P},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$. By
assumption, we have $r=\dot{r}_{H}\neq x_{s}$. So there is $i<n-1$ such that
$r\upharpoonright i=x_{s}\upharpoonright i$ and $r(i)\neq x_{s}(i)$. So we can
strengthen $a_{\bar{A}}$ to a condition $a_{A^{\prime}}$ forcing that there is
$i<n-1$ such that $\dot{r}\upharpoonright i$ is $M$-generic and
$\dot{r}(i)\notin[(a_{A^{\prime}}(s)(i))_{\dot{r}(i)}]$. By repeating this for
all the finitely many nodes on level $n$, we obtain the required condition
$a_{A}^{g}$.

Next, we can carry out the construction in the proof of Proposition 4.8,
moving up the tree instead of up the iteration, to obtain a condition
$\bar{g}_{Y}\leq g_{Y}$ with
$\bar{g}_{Y}(\vec{j}_{s})=(\bar{q}_{\vec{j}_{s}},\bar{F}_{\vec{j}_{s}})$ such
that for every $s\in X$, some $\sigma$ lies on
$(\bar{q}_{\vec{j}_{s}},\bar{F}_{\vec{j}_{s}})$ having
$\bar{q}_{\vec{j}_{s}}\mid\sigma\leq a_{A}^{g}(s)$. We can also ensure that
for every $\tau$ which lies on $(\bar{q}_{d},\bar{F}_{d})$, if $\tau$ extends
$\sigma$ which lies on $(q_{d},F_{d})$, then $\bar{q}_{d}\mid\tau\leq
a^{g}_{A}(s_{\sigma})$. By density, some such $\bar{g}_{Y}$ must be in $G$.

By construction, $\bar{g}_{Y}$ forces that $f_{X}$ is compatible with
$a_{A}^{g}$. So let $\bar{f}_{\bar{X}}\leq f_{X},a_{A}^{g}$. We will be done
if we can show that $a^{g}_{A}$ forces the statement $\Phi(d)$ over
$\mathbb{P}(\vec{P}^{*},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$.

Suppose $H^{*}\subseteq\mathbb{P}(\vec{P}^{*},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ is a
$V$-generic filter containing $a^{g}_{A}$ ($V=M[G]$). Now let’s suppose
towards a contradiction that
$p=\langle\mathcal{T}^{0}_{d(0)},\dot{\mathcal{T}}^{1}_{d(1)},\ldots,\dot{\mathcal{T}}^{n-1}_{d(n-1)}\rangle$
is in the filter determined by $r$. Thus, there is some $\sigma$ which lies on
$p$ such for for all $i<n$, $r(i)$ is a branch through
$(p\mid\sigma(i))_{r\upharpoonright i}$. By construction, we have that
$p\mid\sigma\leq a^{g}_{A}(s)$ for some $s$ on level $n$ of
${}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega$. Let
$H$ be the restriction of $H^{*}$ to an $M$-generic filter for
$\mathbb{P}(\vec{P},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$, and
note that $a^{g}_{A}\in H$. Thus, there is some $i<n-1$ such that $r(i)$ is
not a branch through $(a^{g}_{A}(s)(i))_{r\upharpoonright i}$, which is the
desired contradiction. ∎

######  Theorem 7.2.

Suppose $H\subseteq\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ is
$L$-generic. If an $n$-length sequence of reals $r\in L[H]$ is $L$-generic for
$\mathbb{P}_{n}$, then $r=x_{s}$ for some node $s$ on level $n$ of
${}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega$.

###### Proof.

Let’s suppose that $r$ is not one of the $x_{s}$ for $s$ on level $n$ of
${}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega$. Let
$\dot{r}$ be a nice $\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$-name
for $r$ such that for all nodes $s$ on level $n$ of
${}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega$,
$\mathop{1\hskip-2.5pt{\rm
l}}\Vdash_{\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)}\dot{r}\neq\dot{x}_{s}$.

Choose some transitive $M\prec L_{\omega_{2}}$ of size $\omega_{1}$ with
$\dot{r}\in M$. We can decompose $M$ as the union of a continuous elementary
chain of countable substructures

$X_{0}\prec X_{1}\prec\cdots\prec X_{\alpha}\prec\cdots\prec M$

with $\dot{r}\in X_{0}$. By the properties of $\diamondsuit$, there is some
$\alpha$ such that $\alpha=\omega_{1}\cap{X_{\alpha}}$,
$\mathbb{P}_{n}^{\alpha}=\mathbb{P}_{n}^{J}\cap X_{\alpha}$ for all
$n<\omega$, and $S_{\alpha}$ codes $X_{\alpha}$. Let $M_{\alpha}$ be the
transitive collapse of $X_{\alpha}$. Then, for every $n<\omega$,
$\mathbb{P}_{n}^{\alpha}$ is the image of $\mathbb{P}_{n}^{J}$ under the
collapse, and $\alpha$ is the image of $\omega_{1}$. The name $\dot{r}$ is
fixed by the collapse by our assumption that we can always code conditions in
$\mathbb{P}(\vec{\mathbb{P}}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ by
subsets of $\omega$ and because all antichains of
$\mathbb{P}(\vec{\mathbb{P}}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ are
countable. So at stage $\alpha$ in the construction of $\vec{P}^{J}$, we chose
a forcing extension $M_{\alpha}[G]$ of $M_{\alpha}$ by
$\mathbb{Q}(\vec{P}^{\alpha},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ and
let $\vec{P}_{\alpha+1}=\vec{P}_{\alpha}^{*}$ be constructed in
$M_{\alpha}[G]$.

By elementarity, $M_{\alpha}$ satisfies that $\mathop{1\hskip-2.5pt{\rm
l}}_{\mathbb{P}(\vec{P}_{\alpha},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)}\Vdash\dot{r}\neq\dot{x}_{s}$
for all $s$ on level $n$ of ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega$. Thus,
by Lemma 7.1, for every $s$ on level $n$ of ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega$,
$\mathbb{P}(\vec{\mathbb{P}}_{\alpha+1},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ has a
maximal antichain $\mathcal{A}_{s}$ consisting of conditions $f_{X}$ forcing
the statement:

$\Phi(s):=$“If $\dot{r}$ is $M_{\alpha}[G]$-generic for $\mathbb{P}^{*}_{n}$,
then
$\langle\mathcal{T}^{0}_{s(0)},\dot{\mathcal{T}}^{1}_{s(1)},\ldots,\dot{\mathcal{T}}^{n-1}_{s(n-1)}\rangle$
is not in the filter determined by $\dot{r}$.”

It follows, by an argument analogous to the proof of Proposition 2.7, that
every $\mathcal{A}_{s}$ remains maximal in
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$. So
let’s argue that if $f_{X}\in\mathcal{A}_{s}$, then $f_{X}$ forces in
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ that
if $\dot{r}$ is $L$-generic, then
$\langle\mathcal{T}^{0}_{s(0)},\dot{\mathcal{T}}^{1}_{s(1)},\ldots,\dot{\mathcal{T}}^{n-1}_{s(n-1)}\rangle$
is not in the filter determined by $\dot{r}$.

Let
$\bar{H}^{*}\subseteq\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$ be an
$L$-generic filter containing $f_{X}$ and let $\bar{H}$ be the restriction of
$\bar{H}^{*}$ to
$\mathbb{P}(\vec{P}_{\alpha+1},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$. Let
$r=\dot{r}_{\bar{H}^{*}}$ and suppose that it is $L$-generic for
$\mathbb{P}_{n}^{*}$. Since $f_{X}\in\bar{H}$, it follows that
$M_{\alpha}[G][\bar{H}]$ satisfies that
$\langle\mathcal{T}^{0}_{s(0)},\dot{\mathcal{T}}^{1}_{s(1)},\ldots,\dot{\mathcal{T}}^{n-1}_{s(n-1)}\rangle$
is not in the filter determined by $r$. But then this is true in $L$ as well.

Since $H$ must meet every $\mathcal{A}_{s}$, it holds in $L[H]$ that if $r$ is
$L$-generic for $\mathbb{P}_{n}^{J}$, then it does not meet the maximal
antichain consisting of conditions
$\langle\mathcal{T}^{0}_{s(0)},\dot{\mathcal{T}}^{1}_{s(1)},\ldots,\dot{\mathcal{T}}^{n-1}_{s(n-1)}\rangle$
for nodes $s$ on level $n$ of ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega$ (from
level $\alpha$ of the construction), and so $r$, in fact, cannot be
$L$-generic. ∎

##  8\. Iterating $\vec{P}^{J}$ along the tree
${}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$

We will now argue that the tree iteration
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$,
where we iterate along the uncountable tree ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$,
shares all the key properties of the tree iteration
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$,
namely it has the ccc and Theorem 7.2, concerning the uniqueness of generic
filters for $\mathbb{P}_{n}^{J}$, continues to holds.

######  Theorem 8.1.

The poset $\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
has the ccc.

###### Proof.

Let’s suppose to the contrary that there is an uncountable antichain
$\mathcal{A}$ in $\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$.
By a $\Delta$-system argument, there must be some finite subtree
$X\subseteq{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$
and an uncountable subset $\mathcal{A}^{\prime}\subseteq\mathcal{A}$ such that
for any $f_{Y}$ and $g_{Z}$ in $\mathcal{A}^{\prime}$, $Y\cap Z=X$. Given
$f_{Y}\in\mathcal{A}^{\prime}$, let $f_{X}$ be the restriction of $f_{Y}$ to
$X$. Clearly the collection of all such $f_{X}$ is an uncountable antichain in
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$.
But then since $X$ is finite, there must be a corresponding uncountable
antichain in $\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$,
which is impossible by Theorem 6.14. ∎

######  Theorem 8.2.

Suppose $H\subseteq\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
is $L$-generic. If an $n$-length sequence of reals $r\in L[H]$ is $L$-generic
for $\mathbb{P}_{n}^{J}$, then $r=x_{s}$ for some node $s$ on level $n$ of
${}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$.

###### Proof.

Suppose that $r$ is an $n$-length sequence of reals in $L[H]$ that is
$L$-generic for $\mathbb{P}_{n}^{J}$. Let $\dot{r}$ be a nice
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$-name
for $r$. Since $\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
has the ccc by Theorem 8.2, it follows that conditions in the name $\dot{r}$
use only countably many nodes of ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$.
Thus, $\dot{r}$ is a $\mathbb{P}(\vec{P},\mathscr{T})$-name, where
$\mathscr{T}$ is a countable subtree of ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$.
We may assume that $\mathscr{T}$ is isomorphic to
${}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega$, and
so $\mathbb{P}(\vec{P},\mathscr{T})$ is isomorphic to
$\mathbb{P}(\vec{P},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$. Let
$\bar{H}$ be the restriction of $H$ to $\mathbb{P}(\vec{P},\mathscr{T})$,
which is $L$-generic for it. Thus, $r\in L[\bar{H}]$, from which it follows,
by Theorem 7.2, that $r=x_{s}$ for some $s\in\mathscr{T}$. ∎

##  9\. Symmetric models of ${\rm ZF}+{\rm AC}_{\omega}+\neg{\rm DC}$

We will construct a symmetric submodel of a forcing extension $L[G]$ by
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
in which ${\rm ZF}+{\rm AC}_{\omega}$ holds, but ${\rm DC}$ fails. The reals
of this model will be a model of second-order arithmetic in which ${\rm
Z}_{2}+\Sigma^{1}_{\infty}$-${\rm AC}$ holds, but $\Pi^{1}_{2}$-${\rm DC}$
fails. Let’s start with a brief discussion of the method of constructing
symmetric submodels of a forcing extension, which goes all the way back to
Cohen’s pioneering work on forcing.

Suppose that $\mathbb{P}$ is a forcing notion. Recall that if $\pi$ is an
automorphism of $\mathbb{P}$, then we can apply $\pi$ recursively to
conditions in a $\mathbb{P}$-name $\sigma$ to obtain the $\mathbb{P}$-name
$\pi(\sigma)$. It is not difficult to see by induction on complexity of
formulas, that for every formula $\varphi$ and condition $p\in\mathbb{P}$,
$p\Vdash\varphi(\sigma)$ if and only if $\pi(p)\Vdash\varphi(\pi(\sigma))$.
Fix some group $\mathcal{G}$ of automorphisms of $\mathbb{P}$. Recall that a
filter $\mathscr{F}$ on subgroups of a group $\mathcal{G}$ is _normal_ if
whenever $g\in\mathcal{G}$ and $\mathcal{K}\in\mathscr{F}$, then
$g\mathcal{K}g^{-1}\in\mathscr{F}$. Let’s fix a normal filter $\mathscr{F}$ on
the subgroups of $\mathcal{G}$. The subgroup of $\mathcal{G}$ fixing a
particular $\mathbb{P}$-name $\sigma$, consisting of automorphisms $\pi$ such
that $\pi(\sigma)=\sigma$, is called $\text{sym}(\sigma)$. If
$\text{sym}(\sigma)$ is in $\mathscr{F}$, then we say that $\sigma$ is a
_symmetric_ $\mathbb{P}$-name. We recursively define that a $\mathbb{P}$-name
is _hereditarily symmetric_ when it is symmetric and all names inside it are
hereditarily symmetric. Let ${\rm HS}$ be the collection of all hereditarily
symmetric $\mathbb{P}$-names. Let $G\subseteq\mathbb{P}$ be $V$-generic. The
_symmetric model_

$N=\\{\sigma_{G}\mid\sigma\in{\rm HS}\\}$

associated to the group of autmorphisms $\mathcal{G}$ and the normal filter
$\mathscr{F}$ consists of the interpretations of all hereditarily symmetric
$\mathbb{P}$-names. It is a standard result that $N\models{\rm ZF}$.

We would like to review now a classical construction of a symmetric model in
which countable choice holds but dependent choice fails, which is due to
Jensen [Jen67]. Let $\mathbb{P}$ be the forcing adding a set of Cohen subsets
of $\omega_{1}$, indexed by the tree ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$,
with countable conditions. We will call the poset adding a Cohen subset to
$\omega_{1}$ with countable conditions ${\rm Add}(\omega_{1},1)$. So, more
precisely, conditions in $\mathbb{P}$ are functions $f_{X}:X\to{\rm
Add}(\omega_{1},1)$, where $X$ is some countable subtree of
${}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$,
ordered so that $g_{Y}\leq f_{X}$ whenever $X\subseteq Y$ and for all $t\in
X$, $g_{Y}(t)\leq f_{X}(t)$ in ${\rm Add}(\omega_{1},1)$. Note that
$\mathbb{P}$ is countably closed. Next, we need to select an appropriate group
of automorphisms of $\mathbb{P}$.

Let ${\rm Aut}({}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
be the automorphism group of the tree ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$.
Every automorphism $\pi\in{\rm Aut}({}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
induces an automorphism $\pi^{*}$ of $\mathbb{P}$, so that
$\pi^{*}(f_{X})=f_{\pi\mathbin{\hbox{\tt\char 34\relax}}X}$ with
$f_{\pi\mathbin{\hbox{\tt\char 34\relax}}X}(t)=f_{X}(\pi^{-1}(t))$. Let

$\mathcal{G}=\\{\pi^{*}\mid\pi\in{\rm Aut}({}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})\\}.$

Next, we need to select an appropriate filter on the subroups of
$\mathcal{G}$. Let’s call a subtree $T$ of the tree
${}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$
_useful_ if it is countable and doesn’t have an infinite branch. Given a
useful tree $T$, let $H_{T}$ be the subgroup of $\mathcal{G}$ consisting of
all automorphisms $\pi^{*}$ such that $\pi$ point-wise fixes $T$. Let
$\mathscr{F}$ be the filter on the subgroups of $\mathcal{G}$ generated by all
such subgroups $H_{T}$ with $T$ a useful tree. To see that $\mathscr{F}$ is
normal, observe that if $T$ is a useful tree and $H_{T}\subseteq
K\in\mathscr{F}$, then $\pi\mathbin{\hbox{\tt\char 34\relax}}T$ is useful and
$H_{\pi\mathbin{\hbox{\tt\char 34\relax}}T}\subseteq\pi^{*}K\pi^{*-1}$.

Now, let $G\subseteq\mathbb{P}$ be $V$-generic and let
$N=\\{\sigma_{G}\mid\sigma\in{\rm HS}\\}$ be the symmetric model associated to
$\mathcal{G}$ and $\mathscr{F}$. In $V[G]$, let $\mathcal{T}$ be the tree
isomorphic to ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$
whose nodes are the Cohen subsets of $\omega_{1}$ added by $G$. Given a node
$t\in{}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$,
let $\sigma_{t}$ be the canonical name for the Cohen subset of $\omega_{1}$
added on node $t$ by $G$. Let $\dot{\mathcal{T}}=\\{({\rm
op}(\sigma_{s},\sigma_{t}),\mathop{1\hskip-2.5pt{\rm l}}_{\mathbb{P}})\mid
s\leq t\text{ in }{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}\\}$,
where ${\rm op}(\sigma_{s},\sigma_{t})$ is the canonical $\mathbb{P}$-name for
the ordered pair of $\sigma_{s}$ and $\sigma_{t}$. Clearly
$\dot{\mathcal{T}}_{G}=\mathcal{T}$. Fix any $\pi^{*}\in\mathcal{G}$, and
observe that $\pi^{*}(\dot{\mathcal{T}})=\\{({\rm
op}(\sigma_{\pi(s)},\sigma_{\pi(t)}),\mathop{1\hskip-2.5pt{\rm
l}}_{\mathbb{P}})\mid s\leq t\text{ in }{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}\\}=\dot{\mathcal{T}}$.
Also, any automorphism $\pi^{*}$ with $\pi(s)=s$ fixes $\sigma_{s}$. This
shows that $\dot{\mathcal{T}}\in{\rm HS}$, and hence $\mathcal{T}$ is in the
symmetric model $N$. Using that a symmetric name must be fixed by a group of
automorphisms point-wise fixing a tree without an infinite branch, we can show
that no infinite branch through $\mathcal{T}$ can have a symmetric name, and
so ${\rm DC}$ fails in $N$. Using that $\mathbb{P}$ is countably closed, we
can show that ${\rm AC}_{\omega}$ holds in $N$.

We are now ready to construct a symmetric model $N$ of a forcing extension
$L[G]$ by $\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
with the same properties. First, observe that every $\pi\in{\rm
Aut}({}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
induces an automorphism $\pi^{*}$ of
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
so that $\pi^{*}(f_{X})=f_{\pi\mathbin{\hbox{\tt\char 34\relax}}X}$ with
$f_{\pi\mathbin{\hbox{\tt\char 34\relax}}X}(t)=f_{X}(\pi^{-1}(t))$. As above,
let $\mathcal{G}$ be the group of automorphisms $\pi^{*}$ for $\pi\in{\rm
Aut}({}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
and let $\mathscr{F}$ be the normal filter generated by the subgroups $H_{T}$
of $\mathcal{G}$, consisting of all automorphisms point-wise fixing some
useful subtree $T$ of $\omega_{1}{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}$. Note that
in the present situation the domains of conditions $f_{X}$ are finite subtrees
$X$, while we use countable trees $T$ to determine which names are symmetric.
Let $N\subseteq L[G]$ be the symmetric model determined by the group of
automorphisms $\mathcal{G}$ and the filter $\mathscr{F}$. In $L[G]$, consider
the tree $\mathcal{T}$, isomorphic to ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$
whose nodes are the generic sequences of reals added by $G$. The argument we
gave above generalizes in a straightforward way to show that
$\dot{\mathcal{T}}$, the canonical name for $\mathcal{T}$, is hereditarily
symmetric, and hence $\mathcal{T}\in N$.

Suppose $T$ is any subtree of $\omega_{1}{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}$. If $f_{X}$
is a condition in $\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$,
we will denote by $f_{X\cap T}$, the restriction of $f_{X}$ to nodes in $T$,
i.e. $f_{X\cap T}$ has domain $X\cap T$ and $f_{X\cap T}(t)=f_{X}(t)$. We let

$G_{T}=\\{f_{X}\in G\mid X\subseteq T\\}.$

Note that if $T$ is useful, then the canonical name for $G_{T}$ is fixed by
all elements of the subgroup $H_{T}$, and therefore $G_{T}\in N$. Thus, each
$L[G_{T}]\subseteq N$.

If $\sigma$ is a $\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$-name
and $H_{T}\subseteq\text{sym}(\sigma)$ for a useful tree $T$, we will say that
$T$ _witnesses_ that $\sigma$ is symmetric.

######  Proposition 9.1.

Suppose that $\sigma$ is a symmetric
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$-name,
as witnessed by a useful tree $T$, and $f_{X}\Vdash\varphi(\sigma,\check{a})$.
Then $f_{X\cap T}\Vdash\varphi(\sigma,\check{a})$.

###### Proof.

Suppose it is not the case that $f_{X\cap T}\Vdash\varphi(\sigma,\check{a})$.
Then there is a condition $g_{Y}\leq f_{X\cap T}$ which forces
$\neg\varphi(\sigma,\check{a})$. So $g_{Y}$ is incompatible with $f_{X}$ and
the incompatibility must occur on nodes outside of $T$. Let $\pi\in{\rm
Aut}({}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
be an automorphism which switches these nodes in $Y\setminus T$ with some
nodes outside both $T$ and $X$. Clearly $\pi^{*}\in H_{T}$, and so
$\pi^{*}(\sigma)=\sigma$. It follows that
$\pi^{*}(g_{Y})\Vdash\neg\varphi(\sigma,\check{a})$. But, by construction,
$\pi^{*}(g_{Y})$ is compatible with $f_{X}$, which is the desired
contradiction. Thus, we have shown that $f_{X\cap
T}\Vdash\varphi(\sigma,\check{a})$. ∎

######  Proposition 9.2.

Suppose that $\sigma$ is a symmetric
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$-name,
as witnessed by a useful tree $T$, and $A=\sigma_{G}$ is a set of ordinals.
Then $A\in L[G_{T}]$.

###### Proof.

Let $f_{X}$ be some condition in $G$ forcing that $\sigma$ is a set of
ordinals. Define a name

$\sigma^{*}=\\{(\xi,g_{Y\cap T})\mid g_{Y}\leq
f_{X},g_{Y}\Vdash\xi\in\sigma\\}.$

We will argue that $f_{X}\Vdash\sigma=\sigma^{*}$. Let
$H\subseteq\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
be some $L$-generic filter containing $f_{X}$. Suppose $\xi\in\sigma_{H}$.
Then there is $g_{Y}\in H$ such that $g_{Y}\leq f_{X}$ and
$g_{Y}\Vdash\xi\in\sigma$, from which it follows that $(\xi,g_{Y\cap
T})\in\sigma^{*}$ and $g_{Y\cap T}\in H$. So we have $\xi\in\sigma^{*}_{H}$.
Next, suppose that $\xi\in\sigma^{*}_{H}$. Then there is a condition
$g_{Y}\Vdash\xi\in\sigma$ such that $(\xi,g_{Y\cap T})\in\sigma^{*}$ and
$g_{Y\cap T}\in H$. But by Proposition 9.1, it follows that $g_{Y\cap
T}\Vdash\xi\in\sigma$, and so $\xi\in\sigma_{H}$. ∎

######  Lemma 9.3.

${\rm DC}$ fails in $N$.

###### Proof.

We will argue that $\mathcal{T}$ does not have a infinite branch in $N$, and
hence ${\rm DC}$ fails. Suppose to the contrary that $N$ has an infinite
branch $b$ through $\mathcal{T}$, which we can view via coding as a subset of
natural numbers (since it is an $\omega$-length sequence of reals). Fix a
symmetric name $\dot{b}$ for $b$, as witnessed by a useful tree $T$. By
Proposition 9.2, we can assume that the name $\dot{b}$ mentions only
conditions with domains contained in $T$. Recall that for a node
$s\in{}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$,
$x_{s}$ is the $L$-generic sequence of reals for
$\mathbb{P}_{\text{len}(s)}^{J}$ added by $G$ on node $s$ and $\dot{x}_{s}$ is
the canonical $\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$-name
for $x_{s}$. Let $\bar{b}$ be the branch through the tree
${}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$
which corresponds to $b$ via the obvious isomoprhism. Since $T$ doesn’t have
infinite branches by assumption, $\bar{b}$ cannot be a branch through $T$.
Thus, there is some natural number $n$ such that $\bar{b}\upharpoonright
n\subseteq T$ and $\bar{b}(n)=s$ is outside $T$.

Fix a condition

$f_{X}\Vdash\dot{b}(n)=\dot{x}_{s},$

and assume without loss that $s\in X$. It is easy to see that conditions
$g_{Y}$ having some $t\in Y\setminus(X\cup T)$ with $g_{Y}(t)=f_{X}(s)$ are
dense below $f_{X}$. So fix a condition $g_{Y}\in G$ with $X\subseteq Y$ and
$t\in Y\setminus(X\cup T)$ with $g_{Y}(t)=f_{X}(s)$. Let $\pi$ be the
automorphism of the tree ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$
which swaps $s$ with $t$. Let $H=\pi\mathbin{\hbox{\tt\char 34\relax}}G$,
which is also $L$-generic for
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$.
Observe that $\dot{b}_{H}=b$ since the name $\dot{b}$ only mentioned
conditions with domain in $T$. Observe also that $f_{X}\in H$ since it is
above $\pi(g_{Y})=g_{\pi\mathbin{\hbox{\tt\char 34\relax}}Y}$. So it must be
the case that $b(n)=(\dot{x}_{s})_{H}$. But this is impossible because
$(\dot{x}_{s})_{H}=x_{t}$ and $(\dot{x}_{s})_{G}=x_{s}$ and, by genericity,
$x_{s}\neq x_{t}$.

∎

The proof of the next lemma relies mainly on the fact that
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
has the ccc and uses very little else about what the conditions in
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
look like. So to make the notation nicer, we will switch away from the
previous convention and call conditions in
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
standard names like $p$ and $q$.

######  Lemma 9.4.

${\rm AC}_{\omega}$ holds in $N$.

###### Proof.

Suppose $F\in N$ is a countable family of non-empty sets. Let $\dot{F}$ be a
hereditarily symmetric name for $F$ with the useful tree $S$ witnessing that
$\dot{F}$ is symmetric, and let $q\in G$ force that $\dot{F}$ is a countable
family of non-empty sets. We would like to build a name $\dot{C}\in{\rm HS}$
such that $q$ forces that $\dot{C}$ is a choice function for $\dot{F}$. We
will adapt the following strategy. First, we will build a mixed name
$\dot{C}_{0}\in{\rm HS}$ (over an antichain below $q$) and a useful tree
$T_{0}$ extending $S$, witnessing that $\dot{C}_{0}$ is symmetric, such that
$q\Vdash\dot{C}_{0}\in\dot{F}(0)$. Next, we will build a mixed name
$\dot{C}_{1}\in{\rm HS}$ and a useful tree $T_{1}$ extending $T_{0}$,
witnessing that $\dot{C}_{1}$ is symmetric, such that
$q\Vdash\dot{C}_{1}\in\dot{F}(1)$. Proceeding in this fashion, we will build
names $\dot{C}_{n}\in{\rm HS}$ and an increasing sequence of useful trees
$T_{n}$ such that $q\Vdash\dot{C}_{n}\in\dot{F}(n)$. Provided we can ensure in
the course of the construction that $T=\bigcup_{n\in\omega}T_{n}$ does not
have an infinite branch, we will be able to build from the names $\dot{C}_{n}$
a hereditarily symmetric name $\dot{C}$, witnessed by $T$ to be symmetric,
that is forced by $q$ to be a choice function for $\dot{F}$.

Let $D_{0}$ be the dense set below $q$ of conditions $p$ such that for some
name $\dot{c}_{p}\in{\rm HS}$, $p\Vdash\dot{c}_{p}\in\dot{F}(0)$. We will thin
out $D_{0}$ to a maximal antichain over which we can mix the names
$\dot{c}_{p}$ to get the desired name $\dot{C}_{0}\in{\rm HS}$. At the
beginning, we choose some condition $p_{0}\in D_{0}$ and a name
$\dot{c}_{p_{0}}\in{\rm HS}$, witnessed by a useful tree $S_{0}^{\prime}$ to
be symmetric, such that $p_{0}\Vdash\dot{c}_{p_{0}}\in\dot{F}(0)$. By
extending $S_{0}^{\prime}$, if necessary, we can assume that
$\text{dom}(p_{0})\subseteq S_{0}^{\prime}$. Let $S_{0}$ be the union of $S$
and $S_{0}^{\prime}$. Next, we choose some $p_{1}^{\prime}\in D_{0}$,
incompatible to $p_{0}$, and a name $\dot{c}_{p_{1}^{\prime}}\in{\rm HS}$,
witnessed by a useful tree $S_{1}^{\prime}$, with
$\text{dom}(p_{1}^{\prime})\subseteq S_{1}^{\prime}$, to be symmetric, such
that $p_{1}^{\prime}\Vdash\dot{c}_{p_{1}^{\prime}}\in\dot{F}(0)$. At this
point, it is not a good idea to union up $S_{0}$ and $S^{\prime}_{1}$ because
if we keep doing this we might end up with an infinite branch in the final
tree. So instead, we first consider those nodes in $S_{0}\setminus S$ which
have some new node of $S_{1}^{\prime}$ sitting directly above them, meaning
that we are extending an old branch that was already extended once from
$S_{0}$. Call these nodes in $S_{0}\setminus S$ _bad_ and the nodes of
$S_{1}^{\prime}$ sitting directly above them _bad successors_. Let $\pi$ be an
automorphism of the tree ${}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$
which moves every bad node $t$ (and its bad successors along with it) to some
node outside $S_{0}$. Since $S_{0}$ is countable and each node in
${}^{{\mathrel{\mathchoice{\raise 2.0pt\hbox{$\scriptstyle<$}}{\raise
1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1}$
has $\omega_{1}$-many successors, there are many nodes to which the nodes $t$
can move. Since $\pi$ fixes $S$, we have $\pi^{*}\in H_{S}$. So we have
$\pi^{*}(p_{1}^{\prime})\Vdash\pi^{*}(\dot{c}_{p_{1}^{\prime}})\in\dot{F}(0)$.
We can safely union up $S_{0}$ and $\pi\mathbin{\hbox{\tt\char
34\relax}}S_{1}^{\prime}$ without growing any branches in $S_{0}$ that have
extended beyond $S$. But the problem now is that $\pi^{*}(p_{1}^{\prime})$ may
no longer be incompatible with $p_{0}$, since the incompatibility could have
come from some node $t$ that got moved. This, however, can be easily remedied
by adding back to $\pi^{*}(p_{1}^{\prime})$ one of the nodes from $S_{0}$
which caused the incompatibility. Let $p_{1}$ be the condition
$\pi^{*}(p_{1}^{\prime})$ together with possibly one extra node from
$S_{1}^{\prime}\cap S_{0}$, let
$\dot{c}_{p_{1}}=\pi^{*}(\dot{c}_{p_{1}^{\prime}})$, and let $S_{1}$ be the
union of $S_{0}$ and $\pi\mathbin{\hbox{\tt\char 34\relax}}S_{1}^{\prime}$.
Using that the filter $\mathscr{F}$ is normal, it is not difficult to see that
the image of a name $\sigma$ in ${\rm HS}$ under an automorphism $\pi^{*}$
from $\mathcal{G}$ is also a name in ${\rm HS}$, and moreover if some useful
tree $T$ witnesses that $\sigma$ is symmetric, then
$\pi\mathbin{\hbox{\tt\char 34\relax}}T$ witnesses that $\pi^{*}(\sigma)$ is
symmetric. So $\dot{c}_{p_{1}}\in{\rm HS}$ and $S_{1}$ witnesses that it is
symmetric. Finally, note that $\text{dom}(p_{1})\subseteq S_{1}$. In the next
step, we choose some condition in $D_{0}$ incompatible with both $p_{0}$ and
$p_{1}$ together with some name in ${\rm HS}$ it forces to be in $\dot{F}(0)$.
We use an automorphism from $H_{S}$ to transform the witnessing tree into a
tree that can be unioned up with $S_{1}$ without growing any branches by
moving over nodes (outside $S$) that have new nodes sitting directly above
them. We continue this process transfinitely for as long as we can find a
condition in $D_{0}$ that is incompatible to all previously chosen conditions.
At limit stages, we simply take the union of the increasing sequence of trees
constructed up to that stage. The process must terminate by some countable
ordinal stage $\alpha$ since
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
has the ccc. Thus, the final union tree $T_{0}=\bigcup_{\xi<\alpha}S_{\xi}$
must be countable and by construction, since we never allow any branch to grow
more than once, $T_{0}$ cannot have an infinite branch.

Let’s argue that the tree $T_{0}$, because it contains
$\bigcup_{\xi<\alpha}\text{dom}(p_{\xi})$, witnesses that the mixed name
$\dot{C}_{0}$ of the names $\dot{c}_{p_{\xi}}$ for $\xi<\alpha$ over the
antichain $\langle p_{\xi}\mid\xi<\alpha\rangle$ is symmetric. Recall that

$\dot{C}_{0}=\bigcup_{\xi<\alpha}\\{(\tau,r)\mid r\leq
p_{\xi},\,r\Vdash\tau\in\dot{c}_{p_{\xi}},\tau\in\text{\text{dom}}(\dot{c}_{p_{\xi}})\\}.$

Fix an automorphism $\pi$ point-wise fixing $T_{0}$. It suffices to argue that
whenever $(\tau,r)\in\dot{C}_{0}$, then
$(\pi^{*}(\tau),\pi^{*}(r))\in\dot{C}_{0}$. So suppose
$(\tau,r)\in\dot{C}_{0}$ and fix $p_{\xi}$ witnessing this. Since $r\leq
p_{\xi}$, it follows that $\pi^{*}(r)\leq p_{\xi}$; since
$r\Vdash\tau\in\dot{c}_{p_{\xi}}$, it follows that
$\pi^{*}(r)\Vdash\pi^{*}(\tau)\in\dot{c}_{p_{\xi}}$; and finally, since
$\dot{c}_{p_{\xi}}$ is symmetric and $\tau\in\text{dom}(\dot{c}_{p_{\xi}})$,
it follows that $\pi^{*}(\tau)\in\text{dom}(\dot{c}_{p_{\xi}})$. Now observe
that, since each $\dot{c}_{p_{\xi}}\in{\rm HS}$, we have $\dot{C}_{0}\in{\rm
HS}$.

Next, we let $D_{1}$ be the dense set below $q$ of conditions $p$ such that
for some name $\dot{c}_{p}\in{\rm HS}$, $p\Vdash\dot{c}_{p}\in\dot{F}(1)$. We
thin out $D_{1}$ to a maximal antichain over which we can mix to obtain the
desired symmetric name $\dot{C}_{1}$ by the same process as above building the
new trees as extensions of $T_{0}$, where branches that have extended beyond
$S$ are no longer allowed to grow. Once, $\dot{C}_{1}$ and $T_{1}$ have been
obtained, we proceed to obtain $\dot{C}_{2}$ and $T_{2}$ extending $T_{1}$,
and continue in this manner for $\omega$-many steps. The final tree
$T=\bigcup_{n<\omega}T_{n}$ is still countable, cannot have an infinite branch
by construction, and witnesses that the canonical name for the sequence of the
$\dot{C}_{n}$ is symmetric. ∎

##  10\. A second-order arithmetic model of $\Sigma^{1}_{\infty}$-${\rm
AC}$+$\neg\Pi^{1}_{2}$-${\rm DC}$

We will now argue that the reals of the symmetric submodel $N$ of the forcing
extension $L[G]$ by $\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega)$,
constructed in Section 9, is a second-order arithmetic model of ${\rm Z}_{2}$
together with $\Sigma^{1}_{\infty}$-${\rm AC}$ in which $\Pi^{1}_{2}$-${\rm
DC}$ fails.

######  Theorem 10.1.

There is a $\beta$-model of second-order arithmetic ${\rm Z}_{2}$ together
with $\Sigma^{1}_{\infty}$-${\rm AC}$ in which $\Pi^{1}_{2}$-${\rm DC}$ fails.

###### Proof.

Let $G\subseteq\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
be $L$-generic and let $N\subseteq L[G]$ be the symmetric submodel of ${\rm
ZF}+{\rm AC}_{\omega}+\neg{\rm DC}$ constructed in Section 9. Let
$\mathcal{M}$ be the model of ${\rm Z}_{2}$ whose collection of sets is
$P(\omega)^{N}$. Since ${\rm AC}_{\omega}$ holds in $N$, it immediately
follows that $\Sigma^{1}_{\infty}$-${\rm AC}$ holds in $\mathcal{M}$. Thus, it
remains to show that $\Pi^{1}_{2}$-${\rm DC}$ fails in $\mathcal{M}$. The
result will follow if we can show that the tree $\mathcal{T}$ is
$\Pi^{1}_{2}$-definable in $\mathcal{M}$. By Theorem 8.2, a sequence $\langle
r_{0},\ldots,r_{n-1}\rangle$ of reals is in the domain of $\mathcal{T}$ if and
only if it is $L$-generic for $\mathbb{P}_{n}^{J}$. So we need to see that the
statement $\langle r_{0},\ldots,r_{n-1}\rangle$ is $L$-generic for
$\mathbb{P}_{n}^{J}$ is $\Pi^{1}_{2}$-expressible in $\mathcal{M}$. This will
suffice because the sequences in $\mathcal{T}$ are ordered simply by
extension.

What we would like to say is that all $L_{\alpha}$, with $\alpha$ a limit
ordinal, should satisfy the following. Given an ordinal $\beta$ we check
whether stage $\beta$ was nontrivial in the construction of
$\vec{P}^{J}=\langle\mathbb{P}_{n}^{J}\mid n<\omega\rangle$. In this case, we
check whether $\langle r_{0},\ldots,r_{n-1}\rangle$ generates an
$M_{\beta}$-generic filter for $\mathbb{P}_{n}^{\beta}$. Let $H_{0}$ consist
of all trees in $\mathbb{P}_{1}^{\beta}$ which have the branch $r_{0}$. If
$H_{0}$ is not $M_{\beta}$-generic, we are done. Otherwise, let $H_{1}$
consist of all conditions $p\in\mathbb{P}_{2}$ such that $p(0)\in H_{0}$ and
$r_{1}$ is a branch through $p(1)_{H_{0}}$. If $H_{1}$ is not
$M_{\beta}$-generic, we are done. Otherwise, we continue. So $\langle
r_{0},\ldots,r_{n-1}\rangle$ is $\mathbb{P}_{n}^{J}$-generic if whenever
$\alpha$ is a limit ordinal, then $L_{\alpha}$ satisfies that for every
nontrivial stage $\beta$ in the construction of $\mathbb{P}_{n}^{J}$, $\langle
r_{0},\ldots,r_{n-1}\rangle$ generates an $M_{\beta}$-generic filter. Now it
is not difficult to check that the complexity of this statement is
$\Pi^{1}_{2}$, because it says that for every set $X$, if $X$ codes a limit
ordinal $\alpha$, then there is another set $Y$ coding $L_{\alpha}$ and a set
coding the filters $H^{\beta}$ needed to verify for every nontrivial stage
$\beta\in L_{\alpha}$ that $H^{\beta}$ is $M_{\beta}$-generic. The statement
that $X$ codes an ordinal is $\Pi^{1}_{1}$ and the remaining statements are
$\Sigma^{1}_{1}$. ∎

##  11\. Reflection can fail in models of ${\rm ZFC}$ without powerset

Let’s call the _Reflection Principle_ the statement that for every set $a$ and
formula $\varphi(\bar{x},a)$, there is a transitive set model $M$ containing
$a$ such that $\varphi(\bar{x},a)$ is absolute between $M$ and the universe.
By the Lévy-Montague reflection, ${\rm ZFC}$ implies the Reflection Principle,
namely every formula is reflected by some $V_{\alpha}$. It is natural to
wonder whether the Reflection Principle holds in models of ${\rm ZFC}^{-}$,
which may not have the $V_{\alpha}$-hierarchy.555In the absence of powerset,
the axiom of choice, defined as the existence of choice functions, is not
equivalent the assertion that every set can be well-ordered [Zar82]. Here the
theory ${\rm ZFC}^{-}$ is assumed to include the assertion that every set can
be well-ordered. It has been suspected for a long time that the Reflection
Principle can fail in such models. The question was first asked by Zarach in
[Zar96], and considered again in [GHJ]. We will show that the Reflection
Principle fails in the model $H_{\omega_{1}}^{N}$, where $N$ is the symmetric
submodel of the forcing extension $L[G]$ by
$\mathbb{P}(\vec{P}^{J},{}^{{\mathrel{\mathchoice{\raise
2.0pt\hbox{$\scriptstyle<$}}{\raise 1.0pt\hbox{$\scriptstyle<$}}{\raise
0.0pt\hbox{$\scriptscriptstyle<$}}{\scriptscriptstyle<}}}\omega}\omega_{1})$
that we constructed in Section 9.

The argument requires first seeing that the Reflection Principle is equivalent
to a version of ${\rm DC}$ for definable relations. Following [GHJ], let’s
define that the _Dependent Choice Scheme_ , abbreviated ${\rm DC}$-scheme,
asserts for every formula $\varphi(x,y,z)$ and parameter $a$ that if for every
$x$, there is $y$ such that $\varphi(x,y,a)$ holds, then there is an
$\omega$-sequence $\langle x_{n}\mid n<\omega\rangle$ such that for all $n$,
$\varphi(x_{n},x_{n+1},a)$ holds; in other words, if a definable relation has
no terminal nodes, then we can make $\omega$-many dependent choices according
to it.

######  Lemma 11.1 ([GHJ]).

The Reflection Principle is equivalent over ${\rm ZFC}^{-}$ to the ${\rm
DC}$-scheme.666This equivalence holds regardless of whether we include the
existence of choice functions or well-orderings as the choice axiom in our
theory.

###### Proof.

First, let’s assume that the Reflection Principle holds. Fix a relation
$\varphi(x,y,a)$ without terminal nodes. Let $M$ be a transitive set which
reflects $\varphi(x,y,a)$ and let $R$ be the set relation on $M$ derived from
$\varphi(x,y,a)$. Now fix a well-ordering $W$ of $M$ and use it to define an
$\omega$-sequence of choices according to $R$.

Next, suppose that the ${\rm DC}$-scheme holds. Fix a formula
$\varphi(\bar{x},a)$. Observe that given any set $A$, using collection, we can
argue that there is a set $\bar{A}\supseteq A$ which is closed under
existential witnesses for subformulas of $\varphi(\bar{x},a)$ with parameters
from $A$. By taking the transitive closure we can assume that $\bar{A}$ is
transitive. So consider the definable relation $R$ which says that $A$ is
related to $\bar{A}$, whenever $A\subseteq\bar{A}$, $\bar{A}$ is transitive,
and $\bar{A}$ is closed under existential witnesses for subformulas of
$\varphi(\bar{x},a)$ with parameters from $A$. We just argued that $R$ has no
terminal nodes. Thus, we can make a sequence $\langle M_{n}\mid
n<\omega\rangle$ of dependent choices in $R$. But then clearly
$M=\bigcup_{n<\omega}M_{n}$ reflects $\varphi(\bar{x},a)$. ∎

######  Theorem 11.2.

The theory ${\rm ZFC}^{-}$ does not imply the Reflection Principle.

###### Proof.

Let $M=H_{\omega_{1}}^{N}$, where $N$ is the ${\rm ZF}$-model constructed in
Section 9. Clearly $M\models{\rm ZF}^{-}$ and since $N\models{\rm
AC}_{\omega}$, choice holds in $M$, so $M\models{\rm ZFC}^{-}$. Since
$\mathcal{T}$ is definable in $M$ (by the argument given in the proof of
Theorem 10.1), it follows that the ${\rm DC}$-scheme fails in $M$. Thus, by
Lemma 11.1, the Reflection Principle fails as well. ∎

##  12\. Open Questions

We end with some open questions related to the results of this article.

To produce our $\beta$-model of ${\rm Z}_{2}+\Sigma^{1}_{\infty}$-${\rm AC}$
in which $\Pi^{1}_{2}$-${\rm DC}$ fails we used the consistency of (a fragment
of) ${\rm ZFC}$.

######  Question 12.1.

Does the consistency of ${\rm Z}_{2}+\Sigma^{1}_{\infty}\text{-}{\rm
AC}+\neg\Pi^{1}_{2}\text{-}{\rm DC}$ follow just from the consistency of ${\rm
Z}_{2}$? Does this implication hold with ”consistency” replaced by ”existence
of a $\beta$-model”?

The third author showed in [Kan79] that it is consistent to have a model of
${\rm Z}_{2}+\Sigma^{1}_{\infty}$-${\rm AC}+\Pi^{1}_{n}$-${\rm DC}$ in which
$\Pi^{1}_{n+1}$-${\rm DC}$ fails. The construction used countable-support
iterations of Jensen’s forcing.

######  Question 12.2.

Can we obtain a new proof of the result using techniques of this article
involving finite iterations?

Finally, we showed that the Reflection Principle can fail in a model of ${\rm
ZFC}^{-}$ in which every set is hereditarily countable.

######  Question 12.3.

Can the Reflection Principle fail in a model of ${\rm ZFC}^{-}$ with a largest
cardinal $\kappa$ that is inaccessible in the model?

The theory ${\rm ZFC}^{-}$ together with the assertion that there is a largest
cardinal $\kappa$ that is inaccessible is bi-interpretable with the second-
order set theory Kelley-Morse together with an appropriate version of the
choice scheme. Kelley-Morse is the set-theoretic analogue of ${\rm Z}_{2}$ in
that it contains the comprehension scheme for all second-order assertions. The
strategy for answering Question 12.3 involves defining a version of Jensen’s
forcing for an inaccessible cardinal $\kappa$ and carrying out the rest of the
construction to produce a symmetric model $N$ such that
$(V_{\kappa}^{N},V_{\kappa+1}^{N})$ is a model of Kelley-Morse together with
the choice scheme in which the dependent choice scheme fails. We will
undertake this project in an upcoming article.

## References

  * [Abr84] Uri Abraham.  A minimal model for $\neg{\rm CH}$: iteration of Jensen’s reals.  Trans. Amer. Math. Soc., 281(2):657–674, 1984.
  * [GHJ] Victoria Gitman, Joel David Hamkins, and Thomas A. Johnstone.  What is the theory ZFC without power set?  To appear in Mathematical Logic Quarterly.
  * [Jen67] Ronald B. Jensen.  Consistency results for models of ZF.  Notices Am. Math. Soc., 14:137, 1967.
  * [Jen70] Ronald Jensen.  Definable sets of minimal degree.  In Mathematical logic and foundations of set theory (Proc. Internat. Colloq., Jerusalem, 1968), pages 122–128. North-Holland, Amsterdam, 1970.
  * [Kan79] V. G. Kanovei.  On descriptive forms of the countable axiom of choice.  Investigations on nonclassical logics and set theory, Work Collect., Moscow, 3-136, 1979.
  * [KL17] V. G. Kanovei and V. A. Lyubetsky.  A definable countable set containing no definable elements.  Mat. Zametki, 102(3):369–382, 2017.
  * [Lév70] Azriel Lévy.  Definability in axiomatic set theory. II.  In Mathematical Logic and Foundations of Set Theory (Proc. Internat. Colloq., Jerusalem, 1968), pages 129–145. North-Holland, Amsterdam, 1970.
  * [Sim73] Stephen G. Simpson.  Choice schemata in second-order arithmetic (abstract).  Notices Am. Math. Soc., 20:A449, 1973.
  * [Sim09] Stephen G. Simpson.  Subsystems of second order arithmetic.  Perspectives in Logic. Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, second edition, 2009.
  * [Zar82] Andrzej Zarach.  Unions of ${\rm ZF}^{-}$-models which are themselves ${\rm ZF}^{-}$-models.  In Logic Colloquium ’80 (Prague, 1980), volume 108 of Stud. Logic Foundations Math., pages 315–342. North-Holland, Amsterdam, 1982\.
  * [Zar96] Andrzej M. Zarach.  Replacement $\nrightarrow$ collection.  In Gödel ’96 (Brno, 1996), volume 6 of Lecture Notes Logic, pages 307–322. Springer, Berlin, 1996.