11institutetext: Shenzhen International Graduate School, Tsinghua University,
Beijing, China 11email<EMAIL_ADDRESS>
22institutetext: College of Electronics and Information Engineering, Shenzhen
University, Shenzhen, China
https://github.com/tljxyys/Perspective-Unet

# Perspective$+$ Unet: Enhancing Segmentation with Bi-Path Fusion and
Efficient Non-Local Attention for Superior Receptive Fields

Jintong Hu 11 Siyan Chen 22 Zhiyi Pan 11 Sen Zeng 11 Wenming Yang 1(✉)1(✉)

###### Abstract

Precise segmentation of medical images is fundamental for extracting critical
clinical information, which plays a pivotal role in enhancing the accuracy of
diagnoses, formulating effective treatment plans, and improving patient
outcomes. Although Convolutional Neural Networks (CNNs) and non-local
attention methods have achieved notable success in medical image segmentation,
they either struggle to capture long-range spatial dependencies due to their
reliance on local features, or face significant computational and feature
integration challenges when attempting to address this issue with global
attention mechanisms. To overcome existing limitations in medical image
segmentation, we propose a novel architecture, Perspective$+$ Unet. This
framework is characterized by three major innovations: (i) It introduces a
dual-pathway strategy at the encoder stage that combines the outcomes of
traditional and dilated convolutions. This not only maintains the local
receptive field but also significantly expands it, enabling better
comprehension of the global structure of images while retaining detail
sensitivity. (ii) The framework incorporates an efficient non-local
transformer block, named ENLTB, which utilizes kernel function approximation
for effective long-range dependency capture with linear computational and
spatial complexity. (iii) A Spatial Cross-Scale Integrator strategy is
employed to merge global dependencies and local contextual cues across model
stages, meticulously refining features from various levels to harmonize global
and local information. Experimental results on the ACDC and Synapse datasets
demonstrate the effectiveness of our proposed Perspective$+$ Unet. The code is
available in the supplementary material.

###### Keywords:

Segmentation Dual-pathway strategy Efficient Non-local Transformer.

##  1 Introduction

3D Medical image segmentation plays a crucial role in the realm of diagnostic
radiology and surgical planning. Accurate segmentation of anatomical
structures from volumetric datasets, such as magnetic resonance imaging (MRI)
or CT, enables the extraction of critical clinical information, facilitating
precise interventions, monitoring of disease progression and personalization
of treatment strategies [2, 4].

Recently, Convolutional Neural Networks (CNNs) have achieved tremendous
success across various domains [19, 18, 3]. Their 3D-focused variants, like
V-Net [11] and 3D U-Net [13], play a prominent role in local feature
extraction for 3D medical image segmentation. These models, including enhanced
versions such as Res-UNet [20] with its residual connections, and U-Net$++$
[24] along with UNet3$+$ [5], with their advanced skip pathways and nested
designs, excel in detecting detailed local patterns. Despite their
proficiency, the inherent limitation of CNNs’ local receptive fields restricts
their ability to capture broader spatial relationships essential for a
comprehensive understanding of images. To compensate for this, multiple layers
are required to expand the coverage, potentially leading to increased model
complexity without effectively integrating global context.

Contrastingly, non-local methods expand the receptive fields of segmentation
models, harnessing global context over mere local details in image analysis.
These strategies focus on spatial relationships of the entire image to improve
segmentation efficacy. Emblematics of this approach are transformer-based [12,
2] or hybrid transformer models [6, 7, 15], which apply global attention to
image regions. Despite their objective to synthesize distant spatial
information, these modules risk integrating noise and face quadratic
computation costs tied to input size. While containing non-local interactions
offers computational relief, it paradoxically trims crucial global insights.
Efforts to balance computational efficiency and global context awareness in
image segmentation have led to innovations like the Swin-Unet [1, 9] and Non-
local Attention variants [10, 17], which partition images for blockwise
attention calculation before global synthesis. Although this reduces
complexity, it also limits the capture of wider spatial information.

In this paper, we propose Perspective$+$ Unet, a pioneering framework designed
to augment the receptive field for enhanced 3D medical image segmentation. Our
model incorporates an innovative Bi-Path encoder, utilizing two pathways: one
utilizing standard convolutions to capture high-resolution local details, and
the other employing dilated convolutions to capture broader contextual
information. This configuration addresses issues commonly associated with
dilated convolutions, allowing for the synthesis of a rich set of features
with varying receptive field sizes, fostering a deeper and wider understanding
of the imagery. Then, the extracted features are fed into an Efficient Non-
Local Transformer Block (ENLTB), which builds upon the standard non-local
attention mechanisms to provide a global perspective with a fraction of the
usual computational overhead. The ENLTB effectively condenses long-range
spatial dependencies into a compact feature set, enriching subsequent feature
maps with globally attentive characteristics. In addition, to enhance the
synergy between local and global feature representations, we design the
Spatial Cross-Scale Integrator (SCSI) to encourage a coherent integration of
information across different stages, ensuring that fine-grained details are
preserved while benefiting from macroscopic contextual insights. The output of
the SCSI module is incorporated into the decoder via skip connections,
ultimately facilitating the generation of segmented images from the decoder
output. Our model has been trained and tested on the ACDC and Synapse
datasets, achieving competitive levels of performance in terms of both the
Dice Similarity Coefficient (DSC) and Hausdorff Distance (HD) metrics.

Figure 1: The pipeline of the proposed Perspective$+$ Unet. The model consists
of (i) a bi-path CNN based encoder to effectively capture local details and
broad contextual information, (ii) a bottleneck composed of Efficient Non-
Local Transformer Blocks and Spatial Cross-Scale Integrator for enhanced
global perspective, and (iii) a decoder to incorporate both global and local
information for generating segmentation results.

##  2 Methods

Our proposed Perspective+ Unet adopts an encoder-bottleneck-decoder
configuration, with the specific network workflow illustrated in Figure 1. In
this chapter, we will provide a detailed introduction to the three modules
within the network, starting with the Bi-Path Residual Block.

###  2.1 Bi-Path Residual Block (BPRB)

Increasing the size of the receptive field to improve accuracy has been a
research focus in the advancement of 3D medical image segmentation.
Traditionally, researchers sought to achieve this by stacking global modules,
which, while expanding the view, often led to the loss of local region
information: the broader receptive field to capture global information risked
overlooking crucial local details.

To address this challenge, we have innovated the BPRB, a dual-pathway design
that balances local and global information processing to enhance segmentation.
One pathway uses dilated convolution to broaden the receptive field,
understanding wider spatial information, but introducing feature discontinuity
due to its spacing method. To solve this, BPRB incorporates another pathway
with traditional convolution, focusing on capturing detailed features and
maintaining local information continuity, thus achieving an optimal balance
between global and local information processing. The proposed BPRB can
formulated as:

$\bm{x}^{loc}_{s+1}=BatchNorm(f_{s}(BatchNorm(f_{s}(\bm{x}_{s}))))$ (1)
$\bm{x}^{glob}_{s+1}=BatchNorm(f^{k}_{s}(BatchNorm(f^{k}_{s}(\bm{x}_{s})))$
(2) $\bm{x}_{s+1}=Conv(Concat[\bm{x}^{loc}_{s+1},\bm{x}^{glob}_{s+1}])$ (3)

where $\bm{x}^{loc}_{s+1}$, $\bm{x}^{glob}_{s+1}$, $\bm{x}_{s+1}$ are local,
global, and final features in stage $s+1$. $f_{s}$ and $f^{k}_{s}$ are the
convolution and dilated convolution with dilation rate $k$ in stage $s$.

###  2.2 Efficient Non-Local Transformer Block (ENLTB)

Capturing global information in input images is crucial for enhancing feature
representation, which directly contributes to the effectiveness of
segmentation. In response to this, we integrate the ENLTB as a strategic means
to reconfigure the feature maps produced by the encoder, aiming to achieve
enhanced contextual understanding and representational diversity.

The ENLTB employs the Efficient Non-Local Self-Attention (ENLSA) mechanism,
which substantially accelerates processing by substituting the conventional
exponential kernel $\exp(\bm{Q}^{\top}\bm{K})$, referenced in non-local neural
network [16], with a more computationally efficient unbiased estimate
$\sigma$. Specifically,
$\exp(\bm{Q}^{\top}\bm{K})=\sigma(\bm{Q})^{\top}\sigma(\bm{K})$, where
$\sigma(\cdot)$ can be reparameterized into a linear mapping. The detailed
proofs are given below (constants unrelated to variables are omitted for
enhanced readability):

$\displaystyle\quad\ \exp\left(\bm{Q}^{\top}\bm{K}\right)$
$\displaystyle=\exp\left(\left\|\bm{Q}+\bm{K}\right\|^{2}/2\right)\cdot\exp\left(-\left(\left\|\bm{Q}\right\|^{2}+\left\|\bm{K}\right\|^{2}\right)/2\right)$
$\displaystyle=\exp\left(-\left(\left\|\bm{Q}\right\|^{2}+\left\|\bm{K}\right\|^{2}\right)/2\right)\int\exp\left(\left\|\bm{Q}+\bm{K}\right\|^{2}/2-\left\|\bm{\phi}-\left(\bm{Q}+\bm{K}\right)\right\|^{2}/2\right)d\bm{\phi}$
$\displaystyle=\exp\left(-\left(\left\|\bm{Q}\right\|^{2}+\left\|\bm{K}\right\|^{2}\right)/2\right)\int\exp\left(-\|\bm{\phi}\|^{2}/2+\bm{\phi}^{\top}\left(\bm{Q}+\bm{K}\right)\right)d\bm{\phi}$
$\displaystyle=\mathbb{E}_{\bm{\phi}\sim\mathcal{N}\left(\mathbf{0}_{c},\bm{I}_{c}\right)}\exp\left(\bm{\phi}^{\top}\left(\bm{Q}+\bm{K}\right)-\left(\left\|\bm{Q}\right\|^{2}+\left\|\bm{K}\right\|^{2}\right)/2\right)$
$\displaystyle=\mathbb{E}_{\bm{\phi}\sim\mathcal{N}\left(\mathbf{0}_{c},\bm{I}_{c}\right)}\exp\left(-\left\|\bm{Q}-\bm{\phi}\right\|^{2}/2\right)\exp\left(-\left\|\bm{K}-\bm{\phi}\right\|^{2}/2\right)$
$\displaystyle=\sigma\left(\bm{Q}\right)^{T}\sigma\left(\bm{K}\right)$ (4)

where $\bm{Q}$ and $\bm{K}$ stand for query and key in the attention.
$\sigma(\bm{x})$ can be reparameterized as product of a multivariate normal
variable $\bm{\Phi}$ and $\bm{x}$.

Relative to the traditional transformer’s quadratic computational complexity,
the ENLSA module only has a complexity of $O(2N)$ for the matrix projection
computation of $\bm{Q}$ and $\bm{K}$, followed by $O(N)$ for the
multiplication between
$\sigma\left(\bm{Q}\right)^{T}\sigma\left(\bm{K}\right)$ and $\bm{V}$. This
design ensures that the overall computational process is linearly related to
the input size $N$, significantly reducing computational costs.

We have re-engineered the Transformer by replacing its attention mechanism
with the ENLSA to construct the ENLTB. This modification streamlines feature
representation enhancement. The first layer of ENLTB exclusively processes
features received from the encoder. Subsequent ENLTB layers, however,
aggregate both the features directly relayed from the encoder and those
transmitted from the preceding ENLTB layer through patch merging, thereby
intricately blending fine-grained details with coarse semantic information.
The process of ENLTB can be represented as:

$\bm{x}_{s}^{in}=\begin{cases}\bm{x}_{s},&\text{if }s=3\\\
concat[\bm{x}_{s},PatchMerging(\bm{x}_{s-1}^{ENLTB})],&\text{else}\end{cases}$
(5)

$\displaystyle\bm{y}=\bm{x}_{s}^{in}+ENLSA\left(LN\left(\bm{x}_{s}^{in}\right)\right),\quad\bm{x}_{s}^{ENLTB}=\bm{y}+MLP\left(LN\left(\bm{y}\right)\right)$
(6)

where the definition of $\bm{x}_{s}$ remains consistent with that presented in
Section 2.1. $\bm{x}_{s}^{in}$, $\bm{x}_{s}^{ENLTB}$ denote the input and
output of ENLTB at stage $s$. $LN$ and $MLP$ stand for the layer normalization
and Multilayer Perceptron, respectively.

###  2.3 Spatial Cross-Scale Integrator (SCSI)

Collaborative feature interplay is instrumental in the enrichment of the
network’s interpretative performance, as a result, we design the SCSI module
to ensure that detailed image complexities are segmented with both precision
and finesse.

The SCSI starts with patch flattening, where feature maps produced by every
ENLTB are gathered and merged into a unified sequence. Following this, a
transformer processes the sequence, which supports the learning of connections
between different features. The refined feature sequences are then carefully
mapped back onto their original feature maps for each scale, maintaining their
original order of connection. The process of SCSI can be formulated as:

$\bm{x}_{conpound}=concat[flatten(\bm{x}_{s}^{ENLTB}),\cdots,flatten(\bm{x}_{s+t}^{ENLTB})$
(7)
$\bm{x}_{s}^{SCSI},\cdots,\bm{x}_{s+t}^{SCSI}=unflatten(transformer(\bm{x}_{conpound}))$
(8)

where $\bm{x}_{s}^{ENLTB}$ and $\bm{x}_{s}^{SCSI}$ denote the output of ENLTB
and SCSI at stage $s$, respectively. $concat$ represents the concatenation
operation.

The SCSI module equips the Perspective$+$ Unet with the capability to
assimilate complementary information extending across scales, thereby
simplifying resolution of the ambiguities linked with complex scale
variations.

Table 1: Segmentation accuracy of different methods on the Synapse multi-organ
CT dataset. The best results are shown in bold.

Methods | Average | Aorta | Gallbladder | Kidney(L) | Kidney(R) | Liver | Pancreas | Spleen | Stomach
---|---|---|---|---|---|---|---|---|---
DSC $\uparrow$ | HD $\downarrow$
U-Net [13] | 76.85 | 39.70 | 89.07 | 69.72 | 77.77 | 68.60 | 93.43 | 53.98 | 86.67 | 75.58
R50 Att-UNet [2] | 75.57 | 36.97 | 55.92 | 63.91 | 79.20 | 72.71 | 93.56 | 49.37 | 87.19 | 74.95
Att-UNet [12] | 77.77 | 36.02 | 89.55 | 68.88 | 77.98 | 71.11 | 93.57 | 58.04 | 87.30 | 75.75
R50 ViT [2] | 71.29 | 32.87 | 73.73 | 55.13 | 75.80 | 72.20 | 91.51 | 45.99 | 81.99 | 73.95
TransUnet [2] | 77.48 | 31.69 | 87.23 | 63.13 | 81.87 | 77.02 | 94.08 | 55.86 | 85.08 | 75.62
SwinUNet [1] | 79.12 | 21.55 | 85.47 | 66.53 | 83.28 | 79.61 | 94.29 | 56.58 | 90.66 | 76.60
AFTer-UNet [21] | 81.02 | - | 90.91 | 64.81 | 87.90 | 85.30 | 92.20 | 63.54 | 90.99 | 72.48
ScaleFormer [6] | 82.86 | 16.81 | 88.73 | 74.97 | 86.36 | 83.31 | 95.12 | 64.85 | 89.40 | 80.14
MISSFormer [7] | 81.96 | 18.20 | 86.99 | 68.65 | 85.21 | 82.00 | 94.41 | 65.67 | 91.92 | 80.81
FCT [14] | 83.53 | - | 89.85 | 72.73 | 88.45 | 86.60 | 95.62 | 66.25 | 89.77 | 79.42
MSAANet [22] | 82.85 | 18.54 | 89.40 | 73.20 | 84.31 | 78.53 | 95.10 | 68.85 | 91.60 | 81.78
Perspective+ | 84.63 | 11.74 | 89.38 | 70.80 | 87.57 | 85.78 | 95.30 | 70.71 | 94.41 | 83.06

Table 2: Segmentation accuracy of different methods on the ACDC dataset. The best results are shown in bold. Methods | DSC $\uparrow$ | RV | Myo | LV
---|---|---|---|---
R50 U-Net [2] | 87.55 | 87.10 | 80.63 | 94.92
R50 Att-UNet [2] | 86.75 | 87.58 | 79.20 | 93.47
R50 ViT [2] | 87.57 | 86.07 | 81.88 | 94.75
TransUNet [2] | 89.71 | 88.86 | 84.53 | 95.73
SwinUNet [1] | 90.00 | 88.55 | 85.62 | 95.83
ScaleFormer [6] | 90.17 | 87.33 | 88.16 | 95.04
UNETR [4] | 88.61 | 85.29 | 86.52 | 94.02
MCTE [8] | 91.31 | 89.14 | 89.51 | 95.27
MISSFormer [7] | 91.19 | 89.85 | 88.38 | 95.34
nnFormer [23] | 92.06 | 90.94 | 89.58 | 95.65
Perspective+ | 92.54 | 90.92 | 90.49 | 96.20

##  3 Experiments

###  3.1 Datasets and Evaluation

####  3.1.1 Synapse:

The Synapse dataset, from the MICCAI 2015 Multi-Atlas Abdomen Labeling
Challenge, contains 30 abdominal 3D CT scans. Eighteen cases are randomly
selected for training purposes, and the remaining 12 are allocated for
testing. Our methodology is evaluated using average Dice Similarity
Coefficient (DSC) and the average Hausdorff Distance (HD) for eight abdominal
organs.

####  3.1.2 ACDC:

The ACDC Challenge assembled MRI scan results from various patients. Each
patient’s scan is manually annotated with three labels: Left Ventricle (LV),
Right Ventricle (RV), and Myocardium (MYO). We randomly select 70 cases for
training, 10 cases for validation, and 20 cases for testing. The methodology
is evaluated using the average DSC.

###  3.2 Experiment Details

In our Perspective+ Unet, the encoder or decoder requires no pre-training and
is entirely trained from scratch. To mitigate the risk of overfitting, a
comprehensive suite of data augmentation techniques is employed, including
probabilistic image flipping, additive Gaussian noise, Gaussian blur, contrast
adjustment, and a variety of affine transformations such as scaling, rotation,
shearing, and translation. Training is conducted on the Synapse and ACDC
datasets, with a regimen of 600 and 1000 epochs, respectively, and a batch
size of 12. Images are resized to 224$\times$224 pixels. To optimize the
learning process, a learning rate of 0.05 is implemented and the weight decay
is set at 0.0001 using the SGD optimizer. All training and testing procedures
are performed on an NVIDIA RTX A5000 GPU.

Figure 2: Visualized segmentation results of different methods on the Synapse
multi-organ CT dataset. Our method (the last column) exhibits the smoothest
boundaries and the most accurate segmentation outcomes.

###  3.3 Quantitative and qualitative segmentation results

To validate the efficacy of Perspective+ Unet, we compare it against 11
advanced methods on the Synapse dataset. Highlighted in Table 1, Perspective+
Unet excelled in DSC at 84.63$\%$ and HD at 11.74$\%$, showing marked
improvements over the latest method, MSAANet, by 1.78$\%$ in DSC and a
reduction in HD by 6.8mm. This advancement is credited to the BPRB and ENLTB
modules, enhancing the model’s receptive field. Further validation on the ACDC
dataset confirmed Perspective+ Unet’s superior versatility and robustness in
capturing critical representations, as shown in Table 2. The segmentation
results of different methods on the Synapse dataset are shown in Figure 2.

In our comparative analysis, ENLSA is evaluated against another non-local
approach in terms of parameter count and number of floating point operations
(FLOPs). The results presented in Table 4 demonstrate that ENLSA significantly
outperforms NLSA in efficiency.

Figure 3: Visualization of attention heat maps from the intermediate layers of
the network. Highlighting areas are closely aligned with segmentation labels,
demonstrating our Perspective$+$ Unet’s accuracy in feature identification and
localization.

Furthermore, to further validate the effectiveness of the model, this study
employs visualization of the outputs from the intermediate layers of the
network, as well as the creation of attention heat maps. As demonstrated in
Figure 3, the highlighted areas within the heat map closely align with the
segmentation labels. This not only proves the model’s capability to
efficiently identify key features from the input images, but also showcases
its accuracy in feature localization.

Table 3: Efficiency comparison of ENLSA. -m is the number of input channel. The input resolution is set as 224$\times$224. Module | FLOPs$\downarrow$ | Params$\downarrow$
---|---|---
NLSA-64 [10] | 2.06G | 0.04M
ENLSA-64 | 0.62G | 0.01M
NLSA-256 | 32.88G | 0.66M
ENLSA-256 | 9.87G | 0.20M

Table 4: Ablation study on the impact of modules. BPRB: Bi-Path Residual Block, ENLTB: Efficient Non-Local Transformer Block, SCSI: Spatial Cross-Scale Integrator. Model | BPRB | SCSI | ENLTB | DSC$\uparrow$ | HD$\downarrow$
---|---|---|---|---|---
Setting 1 | ✘ | ✘ | ✘ | 84.04 | 16.63
Setting 2 | ✔ | ✘ | ✘ | 83.36 | 14.70
Setting 3 | ✔ | ✔ | ✘ | 83.92 | 13.94
Setting 4 | ✔ | ✔ | ✔ | 84.63 | 11.74

###  3.4 Ablation Study

In our proposed Perspective+ Unet architecture, we perform an in-depth
ablation study on the added modules: BPRB, SCSI, and ENLTB, to assess their
impact on model performance. Data from Table 4 reveal that the incorporation
of the BPRB module alone slightly reduces DSC by -0.68$\%$, but significantly
improves precision by reducing HD by 1.93mm. Further integration of the SCSI
module with BPRB enhances both DSC by 0.56$\%$ and reduces HD by 0.76mm,
evidencing the SCSI module’s role in increasing reconstruction accuracy and
precision. Employing all three modules achieves optimal outcomes, with a DSC
of 84.63$\%$ and an HD of 11.74mm, highlighting each module’s critical
contribution to enhancing model performance.

##  4 Conclusion

In conclusion, Perspective+ Unet is distinguished by its innovative approach
to enhancing spatial perception in 3D medical image segmentation. We design a
dual-channel strategy that combines traditional and dilated convolutions with
a novel transformer block and spatial cross-scale integrator. This
architecture ensures comprehensive integration of image features across
different stages and effectively handles both global structures and fine-
grained parts, significantly enhancing the receptive field. Our experimental
results demonstrate that Perspective+ Unet exhibits good segmentation accuracy
in the ACDC and Synapse datasets, highlighting its significant potential in
medical analysis.

## References

  * [1] Cao, H., Wang, Y., Chen, J., Jiang, D., Zhang, X., Tian, Q., Wang, M.: Swin-unet: Unet-like pure transformer for medical image segmentation. In: Karlinsky, L., Michaeli, T., Nishino, K. (eds.) Computer Vision – ECCV 2022 Workshops. pp. 205–218. Springer Nature Switzerland, Cham (2023)
  * [2] Chen, J., Lu, Y., Yu, Q., Luo, X., Adeli, E., Wang, Y., Lu, L., Yuille, A.L., Zhou, Y.: Transunet: Transformers make strong encoders for medical image segmentation (2021)
  * [3] Ding, X., Zhang, X., Ma, N., Han, J., Ding, G., Sun, J.: Repvgg: Making vgg-style convnets great again. In: 2021 IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR). pp. 13728–13737 (2021). https://doi.org/10.1109/CVPR46437.2021.01352
  * [4] Hatamizadeh, A., Tang, Y., Nath, V., Yang, D., Myronenko, A., Landman, B., Roth, H.R., Xu, D.: Unetr: Transformers for 3d medical image segmentation. In: 2022 IEEE/CVF Winter Conference on Applications of Computer Vision (WACV). pp. 1748–1758 (2022)
  * [5] Huang, H., Lin, L., Tong, R., Hu, H., Zhang, Q., Iwamoto, Y., Han, X., Chen, Y.W., Wu, J.: Unet 3+: A full-scale connected unet for medical image segmentation. In: ICASSP 2020 - 2020 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP). pp. 1055–1059 (2020)
  * [6] Huang, H., Xie, S., Lin, L., Iwamoto, Y., Han, X.H., Chen, Y.W., Tong, R.: Scaleformer: Revisiting the transformer-based backbones from a scale-wise perspective for medical image segmentation. In: Raedt, L.D. (ed.) Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22. pp. 964–971. International Joint Conferences on Artificial Intelligence Organization (7 2022). https://doi.org/10.24963/ijcai.2022/135, https://doi.org/10.24963/ijcai.2022/135, main Track
  * [7] Huang, X., Deng, Z., Li, D., Yuan, X., Fu, Y.: Missformer: An effective transformer for 2d medical image segmentation. IEEE Transactions on Medical Imaging 42(5), 1484–1494 (2023). https://doi.org/10.1109/TMI.2022.3230943
  * [8] Li, J.: Mcte: Marrying convolution and transformer efficiently for end-to-end medical image segmentation. In: 2023 IEEE International Conference on Image Processing (ICIP). pp. 1100–1104 (2023). https://doi.org/10.1109/ICIP49359.2023.10222041
  * [9] Liu, Z., Lin, Y., Cao, Y., Hu, H., Wei, Y., Zhang, Z., Lin, S., Guo, B.: Swin transformer: Hierarchical vision transformer using shifted windows. In: 2021 IEEE/CVF International Conference on Computer Vision (ICCV). pp. 9992–10002 (2021). https://doi.org/10.1109/ICCV48922.2021.00986
  * [10] Mei, Y., Fan, Y., Zhou, Y.: Image super-resolution with non-local sparse attention. In: 2021 IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR). pp. 3516–3525 (2021). https://doi.org/10.1109/CVPR46437.2021.00352
  * [11] Milletari, F., Navab, N., Ahmadi, S.A.: V-net: Fully convolutional neural networks for volumetric medical image segmentation. In: 2016 Fourth International Conference on 3D Vision (3DV). pp. 565–571 (2016). https://doi.org/10.1109/3DV.2016.79
  * [12] Oktay, O., Schlemper, J., Folgoc, L., Lee, M., Heinrich, M., Misawa, K., Mori, K., McDonagh, S., Hammerla, N., Kainz, B., Glocker, B., Rueckert, D.: Attention u-net: Learning where to look for the pancreas (04 2018)
  * [13] Ronneberger, O., Fischer, P., Brox, T.: U-net: Convolutional networks for biomedical image segmentation. In: Navab, N., Hornegger, J., Wells, W.M., Frangi, A.F. (eds.) Medical Image Computing and Computer-Assisted Intervention – MICCAI 2015. pp. 234–241. Springer International Publishing, Cham (2015)
  * [14] Tragakis, A., Kaul, C., Murray-Smith, R., Husmeier, D.: The fully convolutional transformer for medical image segmentation. In: 2023 IEEE/CVF Winter Conference on Applications of Computer Vision (WACV). pp. 3649–3658 (2023). https://doi.org/10.1109/WACV56688.2023.00365
  * [15] Wang, C., Zhang, D., Ge, R.: Eye-guided dual-path network for multi-organ segmentation of abdomen. In: Greenspan, H., Madabhushi, A., Mousavi, P., Salcudean, S., Duncan, J., Syeda-Mahmood, T., Taylor, R. (eds.) Medical Image Computing and Computer Assisted Intervention – MICCAI 2023. pp. 23–32. Springer Nature Switzerland, Cham (2023)
  * [16] Wang, X., Girshick, R., Gupta, A., He, K.: Non-local neural networks. In: 2018 IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR). pp. 7794–7803. IEEE Computer Society, Los Alamitos, CA, USA (jun 2018). https://doi.org/10.1109/CVPR.2018.00813, https://doi.ieeecomputersociety.org/10.1109/CVPR.2018.00813
  * [17] Xia, B., Hang, Y., Tian, Y., Wenming, Y., Liao, Q., Zhou, J.: Efficient non-local contrastive attention for image super-resolution. Proceedings of the AAAI Conference on Artificial Intelligence 36, 2759–2767 (06 2022). https://doi.org/10.1609/aaai.v36i3.20179
  * [18] Xia, B., Tian, Y., Zhang, Y., Hang, Y., Yang, W., Liao, Q.: Meta-learning-based degradation representation for blind super-resolution. IEEE Transactions on Image Processing 32, 3383–3396 (2023). https://doi.org/10.1109/TIP.2023.3283922
  * [19] Xia, B., Zhang, Y., Wang, Y., Tian, Y., Yang, W., Timofte, R., Gool, L.V.: Basic binary convolution unit for binarized image restoration network. In: The Eleventh International Conference on Learning Representations (2023), https://openreview.net/forum?id=h8T5dZWTZ-Z
  * [20] Xiao, X., Lian, S., Luo, Z., Li, S.: Weighted res-unet for high-quality retina vessel segmentation. In: 2018 9th International Conference on Information Technology in Medicine and Education (ITME). pp. 327–331 (2018)
  * [21] Yan, X., Tang, H., Sun, S., Ma, H., Kong, D., Xie, X.: After-unet: Axial fusion transformer unet for medical image segmentation. In: 2022 IEEE/CVF Winter Conference on Applications of Computer Vision (WACV). pp. 3270–3280. IEEE Computer Society, Los Alamitos, CA, USA (jan 2022). https://doi.org/10.1109/WACV51458.2022.00333, https://doi.ieeecomputersociety.org/10.1109/WACV51458.2022.00333
  * [22] Zeng, H., Shan, X., Feng, Y., Wen, Y.: Msaanet: Multi-scale axial attention network for medical image segmentation. In: 2023 IEEE International Conference on Multimedia and Expo (ICME). pp. 2291–2296 (2023). https://doi.org/10.1109/ICME55011.2023.00391
  * [23] Zhou, H.Y., Guo, J., Zhang, Y., Han, X., Yu, L., Wang, L., Yu, Y.: nnformer: Volumetric medical image segmentation via a 3d transformer. IEEE Transactions on Image Processing 32, 4036–4045 (2023). https://doi.org/10.1109/TIP.2023.3293771
  * [24] Zhou, Z., Siddiquee, M.M.R., Tajbakhsh, N., Liang, J.: Unet++: Redesigning skip connections to exploit multiscale features in image segmentation. IEEE Transactions on Medical Imaging 39(6), 1856–1867 (2020)

##  Appendix 0.A Supplementary Material

Table 5: Detailed information of the two datasets we used.  Datasets | Modality | Num. of Class | Train\Valid\Test
---|---|---|---
Synapse dataset | CT | 9 | 18\0\12
ACDC dataset | MRI | 4 | 70\10\20
Table 6: Efficiency comparison of ENLSA. -m is the number of input channel. Module | Input size | FLOPs$\downarrow$ | Params$\downarrow$
---|---|---|---
NLSA-64 | [1, 64, 224, 224] | 2.06G | 0.04M
ENLSA-64 | [1, 64, 224, 224] | 0.62G | 0.01M
NLSA-128 | [1, 128, 112, 112] | 2.06G | 0.16M
ENLSA-128 | [1, 128, 112, 112] | 0.62G | 0.05M
NLSA-256 | [1, 256, 56, 56] | 2.06G | 0.66M
ENLSA-256 | [1, 256, 56, 56] | 0.62G | 0.20M
NLSA-512 | [1, 512, 28, 28] | 2.06G | 2.62M
ENLSA-512 | [1, 512, 28, 28] | 0.62G | 0.79M
NLSA-1024 | [1, 1024, 14, 14] | 2.06G | 10.49M
ENLSA-1024 | [1, 1024, 14, 14] | 0.62G | 3.15M
Table 7: Inputs and outputs size for each stage of the BPRB and ENLTB modules. Stage | BPRB | ENLTB
---|---|---
Input size | Output size | Input size | Output size
1 | [1, 3, 224, 224] | [1, 64, 224, 224] | - | -
2 | [1, 64, 224, 224] | [1, 128, 112, 112] | - | -
3 | [1, 128, 112, 112] | [1, 256, 56, 56] | [1, 256, 56, 56] | [1, 256, 56, 56]
4 | [1, 256, 56, 56] | [1, 512, 28, 28] | [1, 512, 28, 28] | [1, 512, 28, 28]
5 | [1, 512, 28, 28] | [1, 1024, 14, 14] | [1, 1024, 14, 14] | [1, 1024, 14, 14]
Figure 4: Visualized segmentation results of different methods on the Synapse
multi-organ CT dataset. Our method (the last column) exhibits the smoothest
boundaries and the most accurate segmentation outcomes. Figure 5:
Visualization of attention heat maps from the intermediate layers of the
network. Highlighting areas are closely aligned with segmentation labels,
demonstrating our Perspective$+$ Unet’s accuracy in feature identification and
localization.


# The global $\Sigma^{1}_{n+1}$-Uniformization Property and $\mathsf{BPFA}$

Stefan Hoffelner111Supported by the Deutsche Forschungsgemeinschaft (DFG
German Research Foundation) under Germanys Excellence Strategy EXC 2044
390685587, Mathematics Münster: Dynamics-Geometry-Structure.

###### Abstract

We show that given a reflecting cardinal, one can produce a model of
$\mathsf{BPFA}$ where the $\Sigma^{1}_{n}$-uniformization property holds
simultaneously for all $n\geq 2$.

##  1 Introduction

Given $A\subset\omega^{\omega}\times\omega^{\omega}$, we say that $f$ is a
uniformization (or a uniformizing function) of $A$ if there is a function $f$
such that

$dom(f)=pr_{1}(A)=\\{x\in 2^{\omega}\,:\,\exists y((x,y)\in A\\}$

and the graph of $f$ is a subset of $A$.

######  Definition 1.1 (Uniformization Property).

We say that the projective pointclass $\Gamma\in\\{\Sigma^{1}_{n}\mid
n\in\omega\\}\cup\\{\Pi^{1}_{n}\mid n\in\omega\\}$ has the uniformization
property iff every $\Gamma$-set in the plane admits a uniformization whose
graph is in $\Gamma$, i.e. the relation $(x,y)\in f$ is in $\Gamma$.

It is a classical result due to M. Kondo that lightface $\Pi^{1}_{1}$-sets do
have the uniformization property, this also yields the uniformization property
for $\Sigma^{1}_{2}$-sets. This is all $\mathsf{ZFC}$ can prove about the
uniformization property of projective sets. In the constructible universe $L$,
for every $n\geq 3$, $\Sigma^{1}_{n}$ does have the uniformization property
which follows from the existence of a good wellorder by an old result of
Addison (see [1]). Recall that a $\Delta^{1}_{n}$-definable wellorder $<$ of
the reals is a _good_ $\Delta^{1}_{n}$-wellorder if $<$ is of ordertype
$\omega_{1}$ and the relation $<_{I}\subset(\omega^{\omega})^{2}$ defined via

$x<_{I}y\Leftrightarrow\\{(x)_{n}\,:\,n\in\omega\\}=\\{z\,:\,z<y\\}$

where $(x)_{n}$ is some fixed recursive partition of $x$ into $\omega$-many
reals, is a $\Delta^{1}_{n}$-definable. It is easy to check that the canonical
wellorder of the reals in $L$ is a good $\Delta^{1}_{2}$-wellorder so the
$\Sigma^{1}_{n}$-uniformization property follows for $n\geq 2$. The very same
argument also shows that inner models of the form $L[U]$ for $U$ a normal,
$\kappa$-complete ultrafilter on $\kappa$ share the same $L$-like pattern for
uniformization.

On the other hand, large cardinal assumptions draw a very different picture.
Due to the celebrated result of Moschovakis (see [14] 39.9), $\mathsf{PD}$
implies that $\Pi^{1}_{2n+1}$ and $\Sigma^{1}_{2n+2}$-sets have the
uniformization property for $n>1$. By the famous Martin-Steel result (see
[15], Theorem 13.6.), the assumption of infinitely many Woodin cardinals
outright implies $\mathsf{PD}$, and hence large cardinals fully settle the
behaviour of the uniformization property within the projective hierarchy.

The connection of $\mathsf{PD}$ with forcing axioms is established via core
model induction. Under the assumption of the proper forcing axiom,
Schimmerling, Steelt and Woodin showed that $\mathsf{PD}$ is true (in fact
much more is true, see [17]), thus also under $\mathsf{PFA}$ the
$\Pi^{1}_{2n+1}$-uniformization holds for $n>1$. As the uniformization
property for one pointclass rules out the uniformization property of the dual
pointclass, the behaviour of sets of reals in $L$ and under $\mathsf{PFA}$
contradict each other.

It is natural to investigate uniformization in the presence of weaker forcing
axioms, the bounded proper forcing axiom $\mathsf{BPFA}$ (introduced by
Goldstern-Shelah, see [6]) being the paradigmatic example together with
Martin’s Axiom. A first step was taken in [10], where it is shown that
$\mathsf{BPFA}$ and “$\omega_{1}$ is not inaccessible to reals$"$ outright
imply that the boldface $\bf{\Sigma}^{1}_{3}$-uniformization property holds.
However Addisons result from 1959 has been the only tool to obtain the
$L$-like global uniformization pattern. As a consequence the known universes
which satisfy the $\Sigma^{1}_{n}$ uniformization property for all $n>1$ are
quite special, in particular they must satisfy $\mathsf{CH}$, hence
$\mathsf{BPFA}$ fails in such universes.

The main goal of this paper is to produce a new method which will force the
$L$-like uniformization pattern. We will introduce a family of
$\Sigma^{1}_{n}$-predicates whose truth value can be switched from false to
true using carefully designed forcings which are $\omega_{1}$-preserving but
not proper. These predicates in turn will be used to define an iterated
forcing construction yielding a universe in which the
$\Sigma^{1}_{n}$-uniformization property holds for each $n\geq 2$
simultaneously. The definitions of the uniformizing functions are robust under
additional usage of proper forcings, which opens the possibility of forcing
$\mathsf{BPFA}$ simultaneously.

######  Theorem 1.2.

Working in $L$, assuming the existence of a reflecting cardinal, there is a
generic extension of $L$ in which $\mathsf{BPFA}$ and the
$\Sigma^{1}_{n}$-uniformization property for every $n\geq 2$ are true.

The forcing method which yields the $\Sigma^{1}_{n}$-uniformization property
seems to be quite flexible and we expect several further applications.

We end the introduction with a short description of how the article is
organized. Section 1 introduces the forcings we will use. This builds on a
technique first introduced in [12] which in turn relies on the notion of
mutual stationarity by Foreman-Magidor and Todorcevic’s argument that
$\mathsf{PFA}$ implies the failure of square. Section 1.3 sets up a coding
machinery which can be combined with the arguments for obtaining
$\mathsf{BPFA}$ without dangerous interferences. Section 2 introduces a family
of $\Sigma^{1}_{n}$-formulas which we will use for the uniformization
property. Section 3 explains the coding method which produces universes with
the $L$-like uniformization property, and section 4 combines this method with
the argument to obtain $\mathsf{BPFA}$ to finally prove the main theorem of
this work.

It belongs to a series of articles which devote themselves to the study of the
separation, the reduction and the uniformization property (see [8],[9], [10]
and [11]). We emphasize however that our arguments in this work (which deal
with the $\Sigma$-side of uniformization) must differ substantially from the
arguments which deal with the $\Pi$-side, (as [8],[9] and [11]) as the two
pictures necessarily can not be combined within $\mathsf{ZFC}$.

###  1.1 Mutually stationary sets

An algebra $\mathcal{A}$ on a cardinal $\lambda$ is a structure of the form
$(\lambda,f_{i})_{i\in\omega}$, where for each $i\in\omega$,
$f_{i}:[\lambda]^{<\omega}\rightarrow\lambda$. Typically, the $f_{i}$’s will
be definable Skolem functions over structures of the form $(H(\theta),\in,<)$
where $<$ is a well-order of $H(\theta)$ and $\theta$ is some regular
cardinal. The following notion was introduced by M. Foreman and M. Magidor in
their seminal [5].

######  Definition 1.3.

Let $K$ be a collection of regular cardinals whose supremum is strictly below
$\kappa$, and suppose that $S_{\eta}\subseteq\eta$ for each $\eta\in K$. Then
the collection of sets $\\{S_{\eta}\mid\eta\in K\\}$ is _mutually stationary_
if and only if for all algebras $\mathcal{A}$ on $\kappa$, there is an
$N\prec\mathcal{A}$ such that

$\text{for all }\eta\in K\cap N,\ \sup(N\cap\eta)\in S_{\eta}.$

Foreman-Magidor ([5]) show that every sequence $\vec{S}=(S_{\eta}\mid\eta\in
K)$ of stationary sets which concentrate on ordinals of countable cofinality
is mutually stationary. For a fixed sequence $\vec{S}$ of stationary sets, let
$\mathcal{T}_{\vec{S}}$ be the collection of all countable $N$ such that for
all $\eta_{i}\in N$, $\sup(N\cap\eta_{i})\in S_{i}.$

######  Theorem 1.4 (Foreman-Magidor).

Let $(\eta_{i}\mid i<j)$ be an increasing sequence of regular cardinals. Let
$\vec{S}=(S_{i}\mid i<j)$ be a sequence of stationary sets such that
$S_{i}\subseteq\eta_{i}\cap\textrm{Cof}(\omega)$. If $\theta$ is a regular
cardinal greater than all $\eta_{i}$ and $\mathcal{A}$ is an algebra on
$\theta$, then there is an $N\prec\mathcal{A}$ which belongs to the class
$\mathcal{T}_{\vec{S}}$. Hence $\vec{S}$ is mutually stationary.

From now on, we assume all stationary subsets of ordinals discussed in this
section are concentrated on countable cofinality. The corresponding notion for
being club in this context is that of an unbounded set which is closed under
$\omega$-sequences.

######  Definition 1.5.

Suppose $\vec{S}=\\{S_{\eta}\mid\eta\in K\\}$ is mutually stationary and that
for every $\eta\in K$, $S_{\eta}$ is stationary, co-stationary in $\eta$
$\cap$ Cof $({\omega})$. We say a forcing poset $\mathbb{P}$ is
$\vec{S}$-preserving if the following holds: Suppose
$\theta>2^{|\mathbb{P}^{+}|}$ is regular. Suppose $M$ is a countable
elementary submodel of $H(\theta)$ with $\\{\mathbb{P},\vec{S}\\}\subset M$
and $M\in\mathcal{T}_{\vec{S}}$. Suppose $p\in\mathbb{P}\cap M$. Then there
exists a $(M,\mathbb{P})$-generic condition $q$ extending $p$.

We add some remarks concerning the notions:

  1. 1.

Any proper forcing is $\vec{S}$-preserving.

  2. 2.

When $K=\\{\omega_{1}\\}$ and $\vec{S}=S\subset\omega_{1}$, the definition of
$\vec{S}$-preserving is identical to the usual definition of $S$-proper
forcing.

  3. 3.

Let $\vec{S}$ be such that each $S_{\eta}\in\vec{S}$ is stationary, co-
stationary in $\eta\cap Cof(\omega)$. Then an example of a non-proper,
$\vec{S}$ preserving forcing is the forcing poset $Club(S_{\eta})$ for a fixed
$\eta$, i.e, the forcing which adds an unbounded subset to $S_{\eta}$ which is
closed under $\omega$-sequences, via countable approximations.

The preservation theorems for countable support iterations of proper forcings
can be generalized to $\vec{S}$-preserving forcings.

######  Lemma 1.6.

If $\langle P_{i},\dot{Q}_{i}\mid i<\alpha\rangle$ is a countable support
iteration of forcing notions and for each $i<\alpha$,
$\Vdash_{P_{i}}$“$\dot{Q}_{i}$ is $\vec{S}$-preserving” then $P_{\alpha}$ is
$\vec{S}$-preserving.

###### Proof.

(Sketch, following the proof of [13], Theorem 31.15, in particular Lemma
31.17) We will only need to show by induction on $j\leq\alpha$ that for any
$N\in\mathcal{T}_{\vec{S}}$, if $j,\langle P_{i},\dot{Q}_{i}\mid
i<\alpha\rangle\in N$, then:

  * $(\ast)_{N}$

For every $q_{0}\in N\cap P_{j}$ that is $(N,P_{j})$-generic and every
$\dot{p}\in V^{P_{j}}$ such that

$q_{0}\Vdash_{j}\dot{p}\in(P_{\alpha}\cap N)\land\dot{p}\upharpoonright
j\in\dot{G}_{j}$

there is an $(N,P_{\alpha})$ generic condition $q\in P_{\alpha}$ extending
$q_{0}$, that is $q\upharpoonright j=q_{0}$ and
$q\Vdash_{\alpha}\dot{p}\in\dot{G}_{\alpha}$.

The statement $(\ast)_{N}$ is identical to Lemma 31.17 in [13]. It can be
checked that the original proof also works here, which gives the iteration
theorem exactly as in the proof of Theorem 31.15. ∎

We will use club shooting forcings relative to definable sequences $\vec{S}$
of mutually stationary sets to code information. These codings do not
interfere with the proper forcings we will use to work towards
$\mathsf{BPFA}$.

######  Definition 1.7.

Let $\kappa$ be an inaccessible cardinal. Let $\vec{S}=(S_{i}\mid i<\kappa)$
be mutually stationary. We say a forcing poset $\mathbb{P}$ is an
$\vec{S}$-coding if $\delta\leq\kappa$ and
$\mathbb{P}=\langle\mathbb{P}_{\alpha},\dot{\mathbb{Q}}_{\alpha}\mid\alpha<\delta\rangle$
satisfies the following:

  * •

$\mathbb{P}$ is a countable support iteration.

  * •

For any $\alpha<\delta$, one of the followings holds:

    1. 1.

Assume that $\alpha$ is inaccessible and $\mathbb{P}_{\alpha}$ is forcing
equivalent to a forcing of size less than or equal to $\alpha$.222We say two
forcing $P$ and $Q$ are equivalent if their Boolean completions $B(P)$ and
$B(Q)$ are isomorphic. Assume that in $V^{\mathbb{P}_{\alpha}}$,
$(B_{\beta}\subset\alpha\mid\beta<2^{\alpha})$ is an enumeration of an
arbitrary set $X\subset P({\alpha})$. Then $\dot{\mathbb{Q}}_{\alpha}$ is
allowed to be the countably supported product
$\prod_{\beta<2^{\alpha}}\dot{\mathbb{R}}_{\beta}$, where each
$\dot{\mathbb{R}}_{\beta}$ is itself defined to be

$\prod_{j\in B_{\beta}}Club(S_{\alpha\cdot(\beta+1)+2j})\times\prod_{j\notin
B_{\beta}}Club(S_{\alpha\cdot(\beta+1)+2j+1})$

using countable support.

    2. 2.

In all other cases, we have that
$\Vdash_{\mathbb{P}_{\alpha}}\dot{\mathbb{Q}}_{\alpha}$ is proper.

Let $\eta$ be an regular cardinal, we say $\mathbb{P}$ is an $\eta$-$\vec{S}$
coding if (1) is replaced by

  * (1’)

$\alpha\geq\eta$ is inaccessible and $\mathbb{P}_{\alpha}$ is forcing
equivalent to a forcing of size less than or equal to $\alpha$. In
$V^{\mathbb{P}_{\alpha}}$, $\langle B_{\beta}\mid\beta<2^{\alpha}\rangle$ is
an enumeration of $P(\alpha)$. Then $\dot{\mathbb{Q}}_{\alpha}$ is allowed to
be the countably supported product
$\prod_{\beta<2^{\alpha}}\dot{\mathbb{R}}_{\beta}$ where each
$\dot{\mathbb{R}}_{\beta}$ is itself

$\prod_{j\in B_{\beta}}Club(S_{\alpha\cdot(\beta+1)+2j})\times\prod_{j\notin
B_{\beta}}Club(S_{\alpha\cdot(\beta+1)+2j+1}).$

By Lemma 1.6, once we can show that every factor of an $\vec{S}$-coding is
$\vec{S}$-preserving, we can deduce that if $\mathbb{P}$ is a $\vec{S}$-coding
forcing, then $\mathbb{P}$ is $\vec{S}$-preserving. This assertion follows
from the proof of the next lemma which says that we will not accidentally code
unwanted information whenever we use a $\vec{S}$-coding forcing.

######  Lemma 1.8.

Suppose that $\vec{S}$ is stationary, co-stationary. Suppose $\mathbb{P}$ is
an $\vec{S}$-coding forcing. Then for any $i\in\kappa$, the followings are
equivalent:

  * (a)

$\Vdash_{\mathbb{P}}S_{i}$ contains an $\omega$-club.

  * (b)

there are $\beta,\alpha,j$ and sets $B_{\beta}\in X\subset V_{\alpha}$ such
that $j\in B_{\beta}$ if $\beta\cdot(\alpha+1)+2j=i$ and $i$ is even and
$j\notin B_{\beta}$ if $\beta\cdot(\alpha+1)+2j+1=i$ and $i$ is odd.

###### Proof.

((b) $\rightarrow$ (a)) Follow from the definition of the forcing.

((a) $\rightarrow$ (b)) Fix an $i$ and assume without loss of generality that
$i$ is even. Write $i=\beta\cdot({\alpha+1})+2j$ and suppose for a
contradiction that $j$ is not an element of $B_{\beta}$. By the definition of
$\vec{S}$ coding forcing, we must have added a club through
$S_{\beta(\alpha+1)+2j+1}$ instead. Let $\vec{T}$ be the sequence $\langle
T_{k}\mid k<\kappa\rangle$, where $T_{k}=S_{k}$ if $k\neq i$ and
$T_{i}=\eta_{i}\setminus S_{i}$. It follows from Theorem 1.4 again that
$\vec{T}$ is mutually stationary. We will prove that $\mathbb{P}$ is
$\vec{T}$-preserving to derive a contradiction. Indeed, we shall see that
$\vec{T}$-preservation implies that $\eta_{i}\setminus S_{i}$ must remain
stationary after forcing with $\mathbb{P}$, yet $\mathbb{P}\Vdash``S_{i}$
contains an $\omega$-club$"$ which is impossible.

To see that $\vec{T}$ preserving forcings preserve the stationarity of every
$S_{\eta_{i}}\in\vec{T}$, we only need to note that for any name $\dot{C}$ of
a subset of $\eta_{i}$ which is unbounded and $\omega$-closed, and any
countable elementary substructure $N$ which contains $\dot{C}$ and for which
$\sup(N\cap\eta_{i})\in S_{\eta_{i}}$, any $(N,\mathbb{P})$-generic condition
$q$ forces $\dot{C}\cap(S_{\eta_{i}})\neq\emptyset$.

Next we show by induction that each $\dot{Q}_{\beta}$ is forced to be
$\vec{T}$-preserving. Work in $V[G_{\beta}]$. If $\dot{Q}_{\beta}/G_{\beta}$
is proper, then it is also $\vec{T}$-preserving. Otherwise, (1) holds. Now
$\dot{Q}_{\beta}/G_{\beta}$ is a countable support product of club adding
forcings. Fix any $N\in\mathcal{T}_{\vec{T}}$ which is a countable
substructure of $H(\theta)^{V[G_{\beta}]}$. For any $p\in
N\cap\dot{Q}_{\beta}$, we can construct a countable decreasing sequence of
conditions $\langle p_{n}\mid n<\omega\rangle$ meeting all dense set in $N$.
Define $q$ coordinatewise by setting $q(j)$ to be the closure of
$\bigcup_{n<\omega}p_{n}(j)$ if $i\in N$ and trivial otherwise. Note that any
non-trivial $q(j)$ is equal to
$\bigcup_{n<\omega}p_{n}(j)\cup\\{\sup(N\cap\eta_{j})\\}$, where
$\eta_{j}=\sup(S_{j})$ is a regular cardinal. As $N\in\mathcal{T}_{\vec{T}}$
we have $\sup(N\cap\eta_{j})\in S_{j}$, whenever $q(j)$ is non-trivial. Hence
$q<p$ is a condition witnessing that each factor of the iteration is
$\vec{T}$-preserving, so the iteration $\mathbb{P}$ is $\vec{T}$-preserving as
well. But now $S_{i}$ must remain stationary after we forced with
$\mathbb{P}$, which is a contradiction to $(a)$. ∎

The proof also shows that $\vec{S}$-coding preserves stationary subset of
$\omega_{1}$ if $\sup(S_{0})>\omega_{1}$. As a Corollary of Lemma 1.8 and the
definition of $\vec{S}$-coding, in any generic extension by $\vec{S}$-coding
and any even $i$, at most one of $S_{i}$ and $S_{i+1}$ contains a club.

The next lemma follows immediately from the definitions so we skip its proof.

######  Lemma 1.9.

Suppose $\mathbb{P}=\langle
P_{\alpha},\dot{Q}_{\alpha}\mid\alpha<\delta\rangle$ is a countable support
iteration. Suppose for any $\alpha>0$, $\dot{Q}_{\alpha}$ is forced to be
$\eta_{\alpha}$-$\vec{S}$ coding of length $l(\alpha)$, where
$\eta_{\alpha}=\max\\{|\mathbb{P}_{\alpha}|^{+},\Sigma_{\beta<\alpha}l(\beta)\\}$.
Also let $\eta_{0}$ be regular. Then $\mathbb{P}$ is forcing equivalent to an
$\eta_{0}$-$\vec{S}$ coding.

###  1.2 Specializing threads through $\square$-sequences

We will briefly present a celebrated theorem, due to S. Todorcevic, which we
use to find $\Sigma_{1}$-definitions of regular $L$\- cardinals. The argument
is again entirely due to Todorcevic (see [19]).

######  Theorem 1.10 (Todorcevic, see [18]).

Let $\kappa>\omega_{1}$ be a regular cardinal and let $\Gamma\subset\kappa$ be
a set of limit ordinals such that
$\\{\delta<\kappa\mid\text{cf}\,(\delta)=\omega_{1}\\}\subset\Gamma.$ Let
$(C_{\alpha}\mid\alpha\in\Gamma\\}$ be a sequence of subsets of $\kappa$ such
that

  1. 1.

$\forall\alpha\in\Gamma$ $C_{\alpha}\subset\alpha$ and $C_{\alpha}$ is a club,

  2. 2.

if $\beta$ is a limit point of $C_{\alpha}$, then $\beta\in\Gamma$ and
$C_{\beta}=C_{\alpha}\cap\beta$.

  3. 3.

There is no club $C\subset\kappa$ such that if $\alpha$ is a limit point of of
$C$, then $\alpha\in\Gamma$ and $C_{\alpha}=C\cap\alpha$.

Then there is a proper forcing $\mathbb{T}^{\kappa}$ such that
$\mathbb{T}^{\kappa}$ forces that in the generic extension, there is a closed
subset $D$ of $\kappa$ of ordertype $\omega_{1}$ and a function
$f:D\rightarrow\omega$ such that for all $\alpha,\beta$, if $\alpha,\beta\in
D$ and $\alpha\in\operatorname{lim}C_{\beta}$, then $f(\alpha)\neq f(\beta)$.

###### sketch of a proof.

For $\alpha,\beta\in\Gamma$ we let $\beta<_{T}\alpha$ if and only if $\beta$
is a limit point of $C_{\alpha}$. This induces a tree ordering on $\Gamma$.

Next we turn to some very useful definitions. For a regular, sufficiently
large cardinal $\lambda$, an elementary chain $(M_{\alpha}\prec
H(\lambda)\mid\alpha<\omega_{1})$ is a sequence of elementary submodels of
$H(\lambda)$ which additionally satisfies that $M_{\alpha}\subset M_{\beta}$
and $M_{\alpha}\in M_{\beta}$ whenever $\alpha<\beta$; and
$M_{\alpha}=\bigcup_{\beta<\alpha}M_{\beta}$ if $\alpha$ is a limit ordinal.

We now define the desired forcing $\mathbb{T}^{\kappa}$, which is a prototype
for the extremely useful class of forcing with side conditions, as follows: A
condition $p\in\mathbb{T}^{\kappa}$ is a pair $((N_{\alpha}\mid\alpha\in
E),f)$ where

  1. 1.

$E$ is a finite subset of $\omega_{1}$ and there is an elementary chain
$(M_{\alpha}\mid\alpha<\omega_{1})$ of countable, elementary substructures of
$H(\kappa^{+})$ such that $N_{\alpha}=M_{\alpha}$ for each $\alpha\in E$.

  2. 2.

$f$ is a specializing function, i.e. if
$\delta_{N_{\alpha}}:=\operatorname{sup}(N_{\alpha}\cap\kappa$ then $f$ is a
function from $\\{\delta_{N_{\alpha}}\mid\alpha\in E\\}$ into $\omega$ such
that $f(\gamma)\neq f(\delta)$ whenever $\gamma<_{T}\delta$.

The key assertion is now that $\mathbb{T}^{\kappa}$ is proper provided we
assume that there is no $\kappa$-chain in the tree $T$ on $\Gamma$.

Assuming that $\mathbb{T}^{\kappa}$ is proper, it is standard argument to
verify that $\mathbb{P}$ indeed adds an $\omega_{1}$-closed set $D$ and a
specializing $f:D\rightarrow\omega$. ∎

From now on we assume that $0^{\\#}$ does not exist. Let
$(C_{\alpha}\mid\alpha\in\text{Sing}\\}$ be Jensen’s global $\square$-sequence
in $L$; here Sing denotes the set of limit ordinals $\alpha$ for which
$cf(\alpha)^{L}<\alpha$. Recall that

  1. 1.

$\forall\alpha\in\text{Sing}(C_{\alpha}\subset\alpha)$ and $C_{\alpha}$ is
club.

  2. 2.

$\forall\alpha\in\text{Sing}(\text{o.t.}(C_{\alpha})<\alpha)$.

  3. 3.

$\forall\beta\in\text{Lim}(C_{\alpha})(\beta\in\text{Sing}\land
C_{\beta}=C_{\alpha}\cap\beta)$.

We define a tree $T$ on Sing via setting $\alpha<_{T}\beta$ iff $\alpha$ is a
limit point of $C_{\beta}$. Note that for a cardinal $\lambda$, the tree for
the corresponding $\square_{\lambda}$-sequence does not have a
$\lambda^{+}$-branch, thus $\square_{\lambda}$ satisfies the three properties
from Todorcevic’s theorem. As a consequence, the proper poset
$\mathbb{T}^{\lambda^{+}}$ adds a closed set $D$ in $(\lambda^{+})^{L}$ of
ordertype $\omega_{1}$ and simultaneously specializes the tree $T$ restricted
on ordinals in $D$, i.e. the forcing adds a function $f:D\rightarrow\omega$
such that for $\alpha,\beta\in D$, if $\alpha<_{T}\beta$ then $f(\alpha)\neq
f(\beta)$.

Consider now the $\Sigma_{1}$-formula $\psi(x,y)$ which says that $x$ is a set
of ordinals which are all singular in $L$, $x$ is closed and of ordertype
$\omega_{1}$; $y$ is a function from $x$ into $\omega$ such that
$y(\alpha)\neq y(\beta)$ whenever $\alpha,\beta\in x$ and
$\alpha\in\text{lim}\,C_{\beta}$.

We claim that if $\theta=sup(D)$ and $D\subset\theta^{\prime}<\omega_{2}$, and
if $f:D\rightarrow$ is such that for $\alpha,\beta\in D$, if
$\alpha<_{T}\beta$ then $f(\alpha)\neq f(\beta)$, then $\theta^{\prime}$ is a
regular cardinal in $L$.

Indeed assume $\theta^{\prime}$ were singular in $L$, then
$C_{\theta^{\prime}}$ would have been defined, so
$D\cap\text{lim}\,C_{\theta^{\prime}}$ is uncountable. In particular, there is
$\alpha<\beta\in D$ such that $f(\alpha)=f(\beta)$, yet $\alpha<_{T}\beta$,
which is a contradiction. To summarize:

######  Theorem 1.11.

For every $L$-regular cardinal $\kappa$, there is a proper forcing denoted by
$\mathbb{T}^{\lambda}$ and a $\Sigma_{1}$-formula $\phi$ such that in the
generic extension $V[\mathbb{T}^{\kappa}]$,

$V[\mathbb{T}^{\kappa}]\models\phi(\kappa)\Leftrightarrow\kappa\text{ is a
regular cardinal in $L$ }$

###  1.3 Coding machinery

When applied over $L$, the $\vec{S}$-coding forcings can be used to surgically
alter the truth-value of certain projective formulas. These formulas and the
$\vec{S}$-coding forcings will be used to form projective predicates
$\Phi_{n,m}$, for $n,m\in\omega$, where each $\Phi_{n,m}$ is a
$\Sigma^{1}_{n}$-formula which will eventually serve as our graph of our
uniformizing functions for $A_{n,m}$, where $A_{n,m}$ is the $m$-th
$\Sigma^{1}_{n}$-set in the plane.

We first describe how to use the $\vec{S}$-coding forcings to obtain suitable
$\Sigma^{1}_{n}$-predicates, whose truth-value can be manipulated using the
right forcings.

We work over $L$ as our ground model. Let $r\in L$ be a real. Note that over
$L$ there is a sequence

$\vec{S}=(S_{\alpha}\mid\alpha\in\mathop{\textrm{Lim}})$

uniformly definable satisfying

  * •

$S_{\alpha}\subset\alpha$

  * •

If $\alpha$ is a regular cardinal, then $S_{\alpha}$ is stationary co-
stationary in $\alpha\cap\textrm{Cof}(\omega)$.

The existence of such a sequence
$(S_{\alpha}\mid\alpha\in\mathop{\textrm{Lim}}(\delta))$ follows from the fact
that $\diamondsuit_{\lambda}$ holds in $L$ for any $L$-cardinal $\lambda$ and
is a routine construction.

We aim to find first a $\Sigma^{1}_{3}$-formula $\Phi$ such that
$L\models\lnot\exists x\Phi(x)$, yet for $\eta\in$ Ord there is a coding
forcing Code$(r,\eta)\in L$ such that after forcing with Code$(r,\eta)$, in
the resulting universe $L[\text{Code}(r,\eta)]\models\Phi(r)$ and $\forall
s(s\neq r\rightarrow\lnot\Phi(s))$ does hold.

The desired forcing Code($r,\eta$) will be itself a three step iteration
denoted by
$\mathbb{Q}^{0}(r,\eta)\ast\dot{\mathbb{Q}}^{1}(r,\eta)\ast\dot{\mathbb{Q}}^{2}(r,\eta)$,
where the first and second factor are iterations themselves, and we will
describe it now. Given our real $r$ and $\eta\in L$ such that $\eta$ is a
limit cardinal in $L$, we first look at the $\omega$-block of $L$-cardinals
which follow $\eta$, that is we form the interval
$[\eta,(\eta^{+\omega})^{L})$.

The first factor of the iteration, denoted by $\mathbb{Q}^{0}(r,\eta)$, will
use a fully supported $\omega$-length iteration, with $\mathbb{T}^{\eta^{+i}}$
for $i\in\omega$ as factors. Consequentially, after forcing with this partial
order, each $L$-cardinal in the interval $[\eta,\eta^{+\omega})$ is
$\Sigma_{1}$-definable using $\omega_{1}$ as the only parameter in its
definition.

For the second factor of our coding forcing we first identify the real $r$
with the according subset of $\omega$ and form the second factor of
$\text{Code}(r,\eta)$ as follows:

$\mathbb{Q}^{1}(r,\eta):=\prod_{j\in r}Club(S_{\eta+2j})\times\prod_{j\notin
r}Club(S_{\eta+2j+1})$

using countable support.

After the two forcings are done we define (in the resulting generic extension)
$X\subset\omega_{1}$ to be the $<$-least set (in some previously fixed well-
order of some sufficiently large $H(\theta)$) which codes the following
objects:

  * •

The $<$-least set of closed sets of $\eta^{+i}$ of ordertype $\omega_{1}$ and
the according specializing functions, both added with the factors of the
forcing of the form $\mathbb{T}^{\eta^{+i}}$. These sets together ensure the
$\Sigma_{1}$-definability of the $L$-cardinals in the interval
$[\eta,\eta^{+\omega})$.

  * •

And $\omega$-many $\omega$-closed, unbounded subsets through some of the
canonically definable stationary sets
$S_{\eta^{+i}}\subset\eta^{+i}\cap\operatorname{cof}(\omega)$. These
$\omega$-closed sets are so chosen that the characteristic function of $r$ can
be read off. That is we collect $\\{c_{\eta^{+i}}\subset
S_{\eta^{+i}}\,:\,i=2n\land n\notin r\\}$ and $\\{c_{\eta^{+i}}\subset
S_{\eta^{+i}}\,:\,i=2n+1\land n\in r\\}$.

As mentioned already, when working in $L[X]$ then we can read off $r$ via
looking at the $\omega$-block of $L$-cardinals starting at $\eta$ and
determine which canonical $L$-stationary set $S_{\eta^{+i}}$ contains an
$\omega$-closed, unbounded set in $L[X]$:

  * $(\ast)$

$n\in r$ if and only if $S_{\eta^{+(2n+1)}}$ contains an $\omega$-closed
unbounded set, and $n\notin r$ if and only if $S_{\eta^{+(2n)}}$ contains an
$\omega$-closed unbounded set.

Indeed this follows readily from Lemma 1.8.

We note that we can apply an argument resembling David’s trick in this
situation. We rewrite the information of $X\subset\omega_{1}$ as a subset
$Y\subset\omega_{1}$ using the following line of reasoning. It is clear that
any transitive, $\aleph_{1}$-sized model $M$ of $\mathsf{ZF}^{-}$ which
contains $X$ will be able to correctly decode out of $X$ all the information.
Consequentially, if we code the model $(M,\in)$ which contains $X$ as a set
$X_{M}\subset\omega_{1}$, then for any uncountable $\beta$ such that
$L_{\beta}[X_{M}]\models\mathsf{ZF}^{-}$ and $X_{M}\in L_{\beta}[X_{M}]$:

$L_{\beta}[X_{M}]\models``\text{The model decoded out of }X_{M}\text{
satisfies $(\ast)"$.}$

In particular there will be an $\aleph_{1}$-sized ordinal $\beta$ as above and
we can fix a club $C\subset\omega_{1}$ and a sequence
$(M_{\alpha}\,:\,\alpha\in C)$ of countable elementary submodels of
$L_{\beta}[X_{M}]$ such that

$\forall\alpha\in C(M_{\alpha}\prec L_{\beta}[X_{M}]\land
M_{\alpha}\cap\omega_{1}=\alpha)$

Now let the set $Y\subset\omega_{1}$ code the pair $(C,X_{M})$ such that the
odd entries of $Y$ should code $X_{M}$ and if $Y_{0}:=E(Y)$ where the latter
is the set of even entries of $Y$ and $\\{c_{\alpha}\,:\,\alpha<\omega_{1}\\}$
is the enumeration of $C$ then

  1. 1.

$E(Y)\cap\omega$ codes a well-ordering of type $c_{0}$.

  2. 2.

$E(Y)\cap[\omega,c_{0})=\emptyset$.

  3. 3.

For all $\beta$, $E(Y)\cap[c_{\beta},c_{\beta}+\omega)$ codes a well-ordering
of type $c_{\beta+1}$.

  4. 4.

For all $\beta$, $E(Y)\cap[c_{\beta}+\omega,c_{\beta+1})=\emptyset$.

We obtain

  * $({\ast}{\ast})$

For any countable transitive model $M$ of $\mathsf{ZF}^{-}$ such that
$\omega_{1}^{M}=(\omega_{1}^{L})^{M}$ and $Y\cap\omega_{1}^{M}\in M$, $M$ can
construct its version of the universe $L[Y\cap\omega_{1}^{N}]$, and the latter
will see that there is an $\aleph_{1}^{M}$-sized transitive model $N\in
L[Y\cap\omega_{1}^{N}]$ which models $(\ast)$ for $r$ and $\eta$.

Thus we have a local version of the property $(\ast)$.

We know define the third, and last factor of $\operatorname{Code}(r,\eta)$,
working in $L[\mathbb{Q}^{0}(r,\eta)][\dot{\mathbb{Q}}^{1}(r,\eta)]$ we shall
define $\mathbb{Q}^{2}(r,\eta)$ as follows. We use almost disjoint forcing
$\mathbb{A}_{D}(Y)$ relative to our previously defined, almost disjoint family
of reals $D\in L$ (see the paragraph after Definition 2.5) to code the set
$Y\subset\omega_{1}$ into one real $r$. This forcing only depends on the
subset of $\omega_{1}$ we code, thus $\mathbb{A}_{D}(Y)$ will be independent
of the surrounding universe in which we define it, as long as it has the right
$\omega_{1}$ and contains the set $Y$.

We finally obtained a real $R$ such that

  * $({\ast}{\ast}{\ast})$

For any countable, transitive model $M$ of $\mathsf{ZF}^{-}$ such that
$\omega_{1}^{M}=(\omega_{1}^{L})^{M}$ and $R\in M$, $M$ can construct its
version of $L[R]$ which in turn thinks that there is a transitive
$\mathsf{ZF}^{-}$-model $N$ of size $\aleph_{1}^{M}$ such that $N$ believes
$(\ast)$ for $r$ and $\eta$.

Note that $({\ast}{\ast}{\ast})$ is a $\Pi^{1}_{2}$-formula in the parameters
$R$ and $r$. We will often suppress the sets$r,\eta$ when referring to
$({\ast}{\ast}{\ast})$ as they will be clear from the context. We say in the
above situation that the real $r$ _is written into $\vec{S}$_, or that $r$ _is
coded into_ $\vec{S}$ (at $\eta$) and $R$ witnesses that $r$ is coded (at
$\eta$).

The projective and local statement $({\ast}{\ast}{\ast})$, if true, will
determine how certain inner models of the surrounding universe will look like
with respect to branches through $\vec{S}$. That is to say, if we assume that
$({\ast}{\ast}{\ast})$ holds for a real $r$ and is the truth of it is
witnessed by a real $R$. Then $R$ also witnesses the truth of
$({\ast}{\ast}{\ast})$ for any transitive $\mathsf{ZF}^{-}$-model $M$ which
contains $R$ (i.e. we can drop the assumption on the countability of $M$).
Indeed if we assume that there would be an uncountable, transitive $M$, $R\in
M$, which witnesses that $({\ast}{\ast}{\ast})$ is false. Then by Löwenheim-
Skolem, there would be a countable $N\prec M$, $R\in N$ which we can
transitively collapse to obtain the transitive $\bar{N}$. But $\bar{N}$ would
witness that $({\ast}{\ast}{\ast})$ is not true for every countable,
transitive model, which is a contradiction.

Consequentially, the real $R$ carries enough information that the universe
$L[R]$ will see that certain $L$-stationary sets from $\vec{S}$ have clubs in
that

$\displaystyle n\in r\Rightarrow L[R]\models``S_{\eta^{+(2n+1)}}\text{
contains an $\omega$-closed unbounded set}".$

and

$\displaystyle n\notin r\Rightarrow L[R]\models``S_{\eta^{+(2n)}}\text{
contains an $\omega$-closed unbounded set}".$

Indeed, the universe $L[R]$ will see that there is a transitive
$\mathsf{ZF}^{-}$-model $N$ which believes $(\ast)$. The latter being coded
into $R$. But by upwards $\Sigma_{1}$-absoluteness, and the fact that $N$ can
compute $\vec{S}$ correctly, if $N$ thinks that some $L$-stationary set in
$\vec{S}$ contains an $\omega$-closed, unbounded set, then $L[R]$ must think
so as well.

##  2 Suitable $\Sigma^{1}_{n}$-predicates

We shall use the $\Sigma^{1}_{3}$-predicate “being coded into $\vec{S}"$ (we
will often write just “being coded$"$ for the latter) to form suitable
$\Sigma^{1}_{n}$-predicates $\Phi^{n}$ for every $n\in\omega$. These
predicates share the following properties:

  1. 1.

$L\models\forall x\lnot(\Phi^{n}(x))$

  2. 2.

For every real $x\in L$, there is a coding forcing
$\operatorname{Code}^{n}(x)\in L$ such that after forcing with it,
$L[\operatorname{Code}^{n}(x)]\models\Phi^{n}(x)$, and for every real $y\neq
x$, $L[\operatorname{Code}^{n}(x)]\models\lnot\Phi^{n}(y)$.

Most importantly, these properties remain true even when iterating the coding
forcings $\operatorname{Code}^{n}(x_{i})$ for a sequence of (names of) reals.

The predicates $\Phi^{n}(x)$ will be defined now.

  * •

$\Phi^{3}(x,y,m)\equiv\exists a_{0}((x,y,m,a_{0})$ is coded into $\vec{S})$.

  * •

$\Phi^{4}(x,y,m)\equiv\exists a_{0}\forall a_{1}((x,y,m,a_{0},a_{1})$ is not
coded into $\vec{S})$.

  * •

$\Phi^{5}(x,y,m)\equiv\exists a_{0}\forall a_{1}\exists
a_{2}((x,y,m,a_{0},a_{1},a_{2})$ is coded into $\vec{S})$.

  * •

$\Phi^{6}(x,y,m)\equiv\exists a_{0}\forall a_{1}\exists
a_{2}a_{3}((x,y,m,a_{0},a_{1},a_{2},a_{3})$ is not coded into $\vec{S})$.

  * •

…

  * •

…

  * •

$\Phi^{2n}(x,y,m)\equiv\exists a_{0}\forall a_{1}...\forall
a_{2n}((x,y,m,a_{0},...,a_{2n})$ is not coded into $\vec{S})$.

  * •

$\Phi^{2n+1}(x,y,m)\equiv\exists a_{0}\forall a_{1}...\exists
a_{2n+1}((x,y,m,a_{0},...,a_{2n+1})$ is coded into $\vec{S})$.

  * •

…

  * •

…

Each predicate $\Phi^{n}$ is exactly $\Sigma^{1}_{n}$. In the choice of our
$\Sigma^{1}_{n}$-formulas $\Phi^{n}(x)$, we encounter again a periodicity
phenomenon, that is two different cases depending on $n\in\omega$ being even
or odd, a theme which is pervasive in this area. It is clear that for each
predicate $\Phi^{n}$ and each given real $x$ there is a way to create a
universe in which $\Phi^{n}(x)$ becomes true using our coding forcings. We
just need to iterate the relevant coding forcings using countable support.

######  Lemma 2.1.

Let $n\in\omega$ and let $x$ be a real in our ground model $L$. Then there is
a forcing $\operatorname{Code}^{n}(x)$ such that if
$G\subset\operatorname{Code}^{n}(x)$ is generic, the generic extension $L[G]$
will satisfy $\Phi^{n}(x)$ and for every $y\neq x$,
$L[G]\models\lnot\Phi^{n}(y)$. This property can be iterated, that is it
remains true if we replace $L$ with $L[G]$ in the above.

##  3 Based forcing

This section introduces a suitable collection of forcings, dubbed based
forcings, which we use for the proof. As we proceed in our iteration, we
simultaneously refine based forcings, via adding more and more constraints,
yielding a decreasing hierarchy of $\alpha$-based forcings.

As a first step, we shall consider the problem of forcing the
$\Sigma^{1}_{3}$-uniformization property over universes which satisfy the
anti-large cardinal hypothesis that $\omega_{1}=\omega_{1}^{L}$ (or more
generally satisfy that $\omega_{1}$ is not inaccessible to reals). Recall our
$\Sigma^{1}_{3}$-predicate $\Phi^{3}(x)$ defined in the last two sections, and
the attached coding forcing $\operatorname{Code}(x)$. There is a very easy
strategy to force the $\Sigma^{1}_{3}$-uniformization property for universes
$V$ which satisfy $\omega_{1}=\omega_{1}^{L}$ provided $V$ thinks that
$\Phi^{3}(x)$ does not hold for every real $x\in V$: we pick some bookkeeping
function $F\in V$ which should list all the (names of) reals in our iteration
and at each stage $\beta$, under the assumption that we created already
$V[G_{\beta}]$, if $F(\beta)$ lists a real $x\in V[G_{\beta}]$ and a natural
number $k$, we ask whether there is a real $y$ such that

$V[G_{\beta}]\models\varphi_{k}(x,y)$

holds, where $\varphi_{k}$ is the $k$-th $\Sigma^{1}_{3}$-formula. If so, we
pick the least such $y$ (in some fixed well-order), and let the value of the
desired $\Sigma^{1}_{3}$-uniformizing $f_{k}(x)$ to be $y$. Additionally we
force with $\operatorname{Code}(x,y,k)$ over $V[G_{\beta}]$ and obtain
$V[G_{\beta+1}]$. The resulting universe $V[G_{\beta+1}]$ will satisfy that
$\Phi^{3}(x,y,k)$ is true, whereas $\Phi^{3}(x,y^{\prime},k)$ is not true for
each $y^{\prime}\neq y$. Moreover, because of upwards absoluteness of
$\Sigma^{1}_{3}$-formulas, this property will remain true in all further
generic extensions we create.

If we iterate long enough in order to catch our tail, the final model $V[G]$
will satisfy the $\Sigma^{1}_{3}$-uniformization property via

$f_{k}(x)=y\Leftrightarrow\Phi^{3}(x,y,k).$

To summarize, the easy strategy to force $\Sigma^{1}_{3}$-uniformization is to
consider at each step some $x$-section of some $\Sigma^{1}_{3}$-set
$A_{k}\subset\omega^{\omega}\times\omega^{\omega}$, and if non-empty, pick the
least $y$ for which $A_{k}(x,y)$ is true. Then force to make $\Phi^{3}(x,y,k)$
true and repeat.

Based forcings use this strategy for $\Sigma^{1}_{3}$-sets, while putting no
constraints on $\Sigma^{1}_{n}$-sets for $n>3$. Anticipating that we aim for a
universe of $\mathsf{BPFA}$, we let $\kappa$ be the least reflecting cardinal
in $L$.

######  Definition 3.1.

Let $\lambda<\kappa$ and let $F:\lambda\rightarrow H(\kappa)$ be a bookkeeping
function. We say that an iteration
$(\mathbb{P}_{\beta},\dot{\mathbb{Q}}_{\beta}\mid\beta<\lambda)$ is (0-)based
with respect to $F$ if the iteration is defined inductively via the following
rules: Assume that $F(\beta)=(\dot{x},3,\dot{k})$ where $\dot{x}$ is a
$\mathbb{P}_{\beta}$-name of a real and $\dot{k}$ a $\mathbb{P}_{\beta}$-name
of a natural number. Also assume that $V[G_{\beta}]\models\exists
y(\varphi_{3,k}(x,y))$ and let $\dot{y}$ be the $<$-least name of such a real
in some fixed well-order of $H(\kappa)$. Then let
$\dot{\mathbb{Q}}_{\kappa}^{G_{\beta}}$ be $\operatorname{Code}(x,y,3,k)$. If
$V[G_{\beta}]\models\exists y(\phi_{3,k}(x,y))$ is not true use the trivial
forcing.

Otherwise, we let the bookkeeping decide whether it provides us with a some
reals $y,a_{0},a_{1},...,a_{n}$ and whether a tuple of the form
$(x,y,a_{0},...,a_{n},m,k)$ is coded or not.

###  3.1 Strategy to obtain global $\Sigma$-uniformization

We shall describe the underlying idea to force the global
$\Sigma$-uniformization. The definition of the factors of the iteration will
depend on whether the formula $\varphi_{m}$ we consider at our current stage
is in $\Sigma^{1}_{2n}$ or in $\Sigma^{1}_{2n+1}$ where $n\geq 2$. We start
with the case where $\varphi_{m}$ appears first on an odd level of the
projective hierarchy. Assume that $\varphi_{m}\equiv\exists a_{0}\forall
a_{1}\exists a_{2}...\exists a_{2n-2}\psi(x,y,a_{0},a_{1},...a_{2n})$ is a
$\Sigma^{1}_{2n+1}$-formula (where $\psi(x,y,a_{0},...a_{2n})$ is a
$\Pi^{1}_{2}$-formula quantifying over the two remaining variables $a_{2n-1}$
and $a_{2n}$) and $x$ is a real. We want to find a value for the
uniformization function for $\varphi_{m}$ at the $x$-section.

To start, we list all triples of reals
$((x,y^{0},a_{0}^{0}),(x,y^{1},a_{0}^{1}),(x,y^{2},a_{0}^{2}),...)$ according
to some fixed well-order $<$. There will be a $<$-least triple
$(x,y^{\alpha},a_{0}^{\alpha})$ for which $\forall a_{1}\exists
a_{2}...\exists a_{2n-2}\psi(x,y^{\alpha},a^{\alpha}_{0},a_{1},a_{2}...)$ is
true, otherwise the $x$-section would be empty and there is nothing to
uniformize.

The goal will be to set up the iteration in such a way that all triples
$(x,y^{\beta},a_{0}^{\beta})$, $\beta>\alpha$ will satisfy the following
formula, which is $\Pi^{1}_{2n+1}$ in the parameters
$(x,y^{\beta},a^{\beta}_{0},m)$ as is readily checked:

$\displaystyle\forall a_{1}\exists a_{2}\forall a_{3}...\exists
a_{2n-2}((x,y^{\beta},m,a_{0}^{\beta},a_{1},a_{2}...,a_{2n-2})\text{ is not
coded into $\vec{S})$.}$

At the same time the definition of the iteration will ensure that
$(x,y^{\alpha},a^{\alpha}_{0})$ will satisfy

$\displaystyle\exists a_{1}\forall a_{2}\exists a_{3}...\forall
a_{2n-2}((x,y^{\alpha},m,a_{0}^{\alpha},a_{1},a_{2}...,a_{2n-2})\text{ is
coded into $\vec{S})$.}$

Provided we succeed, the pair $(x,y^{\alpha})$ will then be the unique
solution to the following formula, which is $\Sigma^{1}_{2n+1}$, and which
shall be the defining formula for our uniformizing function:

$\displaystyle\sigma_{\text{odd}}(x,y,m)\equiv\exists a_{0}(\forall
a_{1}\exists a_{2}...\psi(x,y,a_{0},a_{1},...)\land$
$\displaystyle\lnot(\forall a_{1}\exists
a_{2}...((x,y,m,a_{0},a_{1},a_{2}...)\text{ is not coded into $\vec{S}$}))$

Indeed, for all $\beta>\alpha$, $(x,y^{\beta},a^{\beta}_{0})$ can not satisfy
the second subformula of $\Psi$ whereas for all $\beta<\alpha$,
$(x,y^{\beta},a_{0}^{\beta}$ can not satisfy the first subformula, as
$(x,y^{\alpha},a_{0}^{\alpha})$ is the least such triple.

If we assume that $\varphi_{m}$ is on an even level of the projective
hierarchy we will define things in a dual way to the odd case. Assume that
$\varphi_{m}\equiv\exists a_{0}\forall a_{1}\exists a_{2}...\forall
a_{2n-3}\psi(x,y,a_{0},a_{1},...a_{2n-1})$ is a $\Sigma^{1}_{2n}$-formula and
$x$ is a real. We want to find a value for the uniformization function for
$\varphi_{m}$ at the $x$-section.

Again, we list all triples of reals
$((x,y^{0},a_{0}^{0}),(x,y^{1},a_{0}^{1}),(x,y^{2},a_{0}^{2}),...)$ according
to some fixed well-order $<$. There will be a $<$-least triple
$(x,y^{\alpha},a_{0}^{\alpha})$ for which $\forall a_{1}\exists
a_{2}...\forall a_{2n-3}\psi(x,y^{\alpha},a^{\alpha}_{0},a_{1},a_{2}...)$ is
true, otherwise the $x$-section would be empty and there is nothing to
uniformize.

The goal will be to set up the iteration in such a way that all triples
$(x,y^{\beta},a_{0}^{\beta})$, $\beta>\alpha$ will satisfy the following
formula, which is $\Pi^{1}_{2n}$ in the parameters
$(x,y^{\beta},a^{\beta}_{0},m)$ as is readily checked:

$\displaystyle\forall a_{1}\exists a_{2}\forall a_{3}...\exists
a_{2n-3}((x,y^{\beta},m,a_{0}^{\beta},a_{1},a_{2}...,a_{2n-3})\text{ is coded
into $\vec{S})$.}$

At the same time the definition of the iteration will ensure that
$(x,y^{\alpha},a^{\alpha}_{0})$ will satisfy

$\displaystyle\exists a_{1}\forall a_{2}\exists a_{3}...\exists
a_{2n-3}((x,y^{\alpha},m,a_{0}^{\alpha},a_{1},a_{2}...,a_{2n-3})\text{ is not
coded into $\vec{S})$.}$

Provided we succeed, the pair $(x,y^{\alpha})$ will then be the unique
solution to the following formula, which is $\Sigma^{1}_{2n}$, and which shall
be the defining formula for our uniformizing function:

$\displaystyle\sigma_{\text{even}}(x,y,m)\equiv\exists a_{0}(\forall
a_{1}\exists a_{2}...\psi(x,y,a_{0},a_{1},...)\land$
$\displaystyle\lnot(\forall a_{1}\exists
a_{2}...((x,y,m,a_{0},a_{1},a_{2}...)\text{ is coded into $\vec{S}$}))$

###  3.2 Definition of the iteration according to the strategy.

We shall elaborate on the ideas presented in the last section. Our goal is to
define an iteration such that our formulas $\sigma_{\text{even}}$ and
$\sigma_{\text{odd}}$ work as defining formulas for the uniformization
functions. Later we will combine these ideas with the standard iteration to
obtain $\mathsf{BPFA}$ from a reflecting cardinal to finally finish the proof
of the main theorem.

We will need the following predicates. For an arbitrary real $x$, list the
triples $(x,y^{0},a_{0}^{0}),(x,y^{1},a_{0}^{1}),(x,y^{2},a_{0}^{2}),...)$
according to our fixed well-order $<$. For each ordinal
$\alpha<2^{\aleph_{0}}$ we fix bijections
$\pi_{\alpha}:(2^{\aleph_{0}})^{\alpha}\rightarrow 2^{\aleph_{0}}$ (we assume
w.l.o.g that such a bijection exist as we always force its existence with a
proper forcing).

We say

$\Psi(\\#\psi,x,y^{\alpha},a_{0}^{\alpha},b_{1},...,b_{n})\text{ is true }$

if for every $\beta<\alpha$, if we let
$\pi_{\alpha}^{-1}(b^{k})=(c^{k}_{\beta})_{\beta<\alpha}$ then
$\psi(x,y^{\beta},a_{0}^{\beta},c^{1}_{\beta},c^{2}_{\beta},...,c^{n}_{\beta})$
is true, where $\psi$ is a $\Pi^{1}_{2}$-formula. Note that strictly speaking,
$\Psi$ is not first order as it is a conjunction of $\alpha$-many formulas. We
will use coding to create a projective predicate which is true whenever $\Psi$
is true.

Let $F:\kappa\rightarrow H(\lambda)$ be some bookkeeping function in $L$ which
shall be our ground model and which guides our iteration. We assume that we
have defined already the following list of notions:

  * •

We do have the notion of $\alpha_{\beta}$-based forcings, which is a subset of
the set of based forcings. There is a set of tuples of reals which is tied to
the $\alpha_{\beta}$-based forcings and which consists of tuples of reals we
must not use in coding forcings anymore as factors of an
$\alpha_{\beta}$-based forcing.

  * •

We defined already our iteration $\mathbb{P}_{\beta}\in L$ up to stage
$\beta$.

  * •

We picked a $\mathbb{P}_{\beta}$-generic filter $G_{\beta}$ for
$\mathbb{P}_{\beta}$ and work, as usual, over $L[G_{\beta}]$.

The bookkeeping function $F$ at $\beta$ hands us an $\omega$-tuple
$(\dot{x},\dot{m},\dot{l},\dot{b}_{0},\dot{b}_{1},\dot{b}_{2},...)$ where
$\dot{x}$ and $\dot{b}_{n}$ are $\mathbb{P}_{\beta}$-names of a reals and
$\dot{m}$ and $\dot{l}$ are both $\mathbb{P}_{\beta}$-names of natural numbers
(in fact at each stage we will only need finitely many of those names of
reals, and the rest of the information will be discarded). We let
$x=\dot{x}^{G_{\beta}}$, and define $b_{n},m,l$ accordingly. Our goal is to
define the forcing $\dot{\mathbb{Q}}_{\beta}$ we want to use at stage $\beta$,
and to define the notion of $\alpha_{\beta}+1$-allowable forcing. We consider
various cases for our definition.

####  3.2.1 Case 1

In the first case, writing $\varphi_{m}=\exists a_{0}\forall a_{1}...\exists
a_{2n-2}\psi(x,y,a_{0},...,a_{2n-2})$, where $\psi$ is a $\Pi^{1}_{2}$-formula
(and $\varphi_{m}$ is a $\Sigma^{1}_{2n-1}$ formula for $n\geq 3$) we assume
that the bookkeeping $F$ at $\beta$ hands us a tuple $c_{1},...c_{2n-2}$ of
real numbers, $x$, and $\alpha<2^{\aleph_{0}}$ with the assigned reals
$a_{0}^{\alpha}$ and $y^{\alpha}$.

Recall that we have our fixed bijection
$\pi_{\alpha}:(2^{\aleph_{0}})^{\alpha}\rightarrow 2^{\aleph_{0}}$ (note that
such a bijection exists at least in a proper generic extension, so we pass to
that universe if necessary) We assume that

$\displaystyle\psi(x,y,a_{0},c_{1},...,c_{2n-2})\text{ is true}.$

We first define $\alpha_{\beta}+1$-based forcings as just
$\alpha_{\beta}$-based with the additional constraints that we must not use
any forcings of the form

$\displaystyle\operatorname{Code}(\\#\psi,x,y^{i},a^{i}_{0},e_{1},e_{2},...,e_{2n-2})$

as a factor of our iteration, where $i>\alpha$ and $e_{1},e_{2},...,e_{2n-2}$
are such that there are reals $r^{j}_{0},r^{j}_{1},...,r^{j}_{i}$ with
$r^{j}_{\alpha}=c_{j}$ and $\pi_{i}(r^{j}_{0},...,r^{j}_{i})=e_{j}$ for every
$j\in[1,2n-2].$

We use the coding forcing

$\displaystyle\operatorname{Code}(\\#\psi,x,y^{\alpha},a_{0}^{\alpha},g_{1},g_{2},...,g_{2n-2})=:\dot{\mathbb{Q}}_{\beta}$

as the $\beta$-th factor of our iteration, where $g_{1},...,g_{2n-2}$ are
reals which we are given by the bookkeeping and such that
$\Psi(\\#\psi,x,y^{\alpha},a_{0}^{\alpha},g_{1},...,g_{2n-2})$ is true.

If $\Psi(\\#\psi,x,y^{\alpha},a_{0}^{\alpha},g_{1},...,g_{2n-2})$ is not true,
then pick the $<$-least tuple $g_{1},...,$ $g_{2n-2}$ ) such that
$\Psi(\\#\psi,x,y^{\alpha},a_{0}^{\alpha},g_{1},...,g_{2n-2})$ is true. If
there is no such tuple then do nothing.

The upshot of this definition is the following. Suppose we iterate following
our rules, and in the final model $L[G_{\kappa}]$, $\exists a_{0}\forall
a_{1}...\exists a_{2n-2}\psi(x,y,a_{0},a_{1},...,a_{2n-2})$ is true and
$(x,y,a_{0})$ is the $<$-least triple witnessing this. Then also

$\exists a_{0}\forall a_{1}...\exists
a_{2n-2}((\\#\psi,x,y,a_{0},a_{1},...,a_{2n-2})\text{ is coded) }$

is true in $L[G_{\kappa}]$ by the rules of the iteration. At the same time for
every $(x,y^{\prime\prime},a^{\prime\prime}_{0})>(x,y,a_{0})$ and for every
real $c_{1}$ there will be a real $b^{\prime}_{2}$ such that for every $c_{3}$
there is a further $b^{\prime}_{4}$ and so on such that
$(x,y^{\prime\prime},a^{\prime\prime}_{0},\\#\psi,c_{1},b^{\prime}_{2},...)$
is not coded.

####  3.2.2 Case 2

We again let $\varphi_{m}=\exists a_{0}\forall a_{1}...\exists
a_{2n-2}\psi(x,y,a_{0},...,a_{2n-2})$ and we assume that the bookkeeping $F$
at $\beta$ hands us a tuple $c_{1},...c_{2n-2}$ of real numbers, $x$, and
$\alpha<2^{\aleph_{0}}$ with the assigned reals $a_{0}^{\alpha}$ and
$y^{\alpha}$.

We assume that

$\displaystyle\psi(x,y,a_{0},c_{1},...,c_{2n-2})\text{ is not true}.$

In this situation we force with the trivial forcing at the $\beta$-th stage
and do not define the notion of $\alpha_{\beta}+1$-based forcing. Instead we
continue working with $\alpha_{\beta}$-based forcings.

####  3.2.3 Case 3

This is the dual case to the first one. We assume that

$\varphi_{m}\equiv\exists a_{0}\forall a_{1},...,\forall
a_{2n}(\psi(x,y,a_{0},...,a_{2n-3}))$

that is $\varphi_{m}$ belongs to an even projective level. We assume that the
bookkeeping $F$ at $\beta$ hands us a tuple $c_{1},...c_{2n-3}$ of real
numbers, $x$, and $\alpha<2^{\aleph_{0}}$ with the assigned reals
$a_{0}^{\alpha}$ and $y^{\alpha}$.

We assume that

$\displaystyle\psi(x,y^{\alpha},a^{\alpha}_{0},c_{1},...,c_{2n-3})\text{ is
true}.$

First we define the $\beta$-the factor of our iteration. We force with

$\displaystyle\operatorname{Code}(\\#\psi,x,y^{i},a^{i}_{0},e_{1},e_{2},...,e_{2n-3})=:\dot{\mathbb{Q}}_{\beta}$

where $i>\alpha$ and $e_{1},e_{2},...,e_{2n-3}$ are reals given by the
bookkeeping which have the property that there are reals
$r^{j}_{0},r^{j}_{1},...,r^{j}_{i}$ with $r^{j}_{\alpha}=c_{j}$ and
$\pi_{i}(r^{j}_{0},...,r^{j}_{i})=e_{j}$ for every $j\in[1,2n-3].$

Next we define the notion of $\alpha_{\beta}+1$-based which should be
$\alpha_{\beta}$-based and the additional constraint that

$\displaystyle\operatorname{Code}(\\#\psi,x,y,\alpha,g_{1},g_{2},...,g_{2n-3})=:\dot{\mathbb{Q}}_{\beta}$

must not be used as a factor of any future forcing we use in our iteration.
Here $g_{1},...,g_{2n-3}$ are reals which we are given by the bookkeeping with
the property that
$\Psi(\\#\psi,x,y^{\alpha},a_{0}^{\alpha},g_{1},...,g_{2n-3})$ (see at the
beginning of section 2.2 for a definition of $\Psi$) holds true.

####  3.2.4 Case 4

This is the same as in case 2. We find ourselves in the situation where
$\psi(x,y^{\alpha},a_{0}^{\alpha},c_{1},...,c_{2n-3})$ is not true. Then we do
nothing.

This ends the definition of our iteration. We shall argue later, that the
definition works in that it will produce a universe where
$\sigma_{\text{even}}$ and $\sigma_{\text{odd}}$ serve as definitions of
uniformizing functions, when applied in the right context.

######  Definition 3.2.

Let $F:\kappa\rightarrow H(\lambda)$ be a bookkeeping function. We say that an
iteration $(\mathbb{P}_{\beta},\dot{\mathbb{Q}}_{\beta}\mid\beta<\kappa)$ is
suitable if each factor of the iteration either is proper or each factor is
obtained using $F$ and the four rules described above.

##  4 Proving the main theorem

Recall first that $\kappa$ is reflecting whenever it is regular and such that
$V_{\kappa}$ is $\Sigma_{2}$-elementary in the universe $V$. We let $\kappa$
be the least reflecting cardinal in $L$. We let $F:\kappa\rightarrow
H(\kappa)$ be such that every element of $H(\kappa)$ has an unbounded pre-
image under $F$. We assume that we arrived at stage $\beta<\kappa$ of our
iteration and will describe what to force with now.

###  4.1 Definition of the iteration. Odd stages

Assume that $F(\beta)$ hands us names such that they evaluate with the help of
our current generic $G_{\beta}$ to a tuple
$(\\#\psi,x,y^{\alpha},a_{0}^{\alpha},c_{1},...,c_{n},...,)$ where $\\#\psi$
is the the Gödelnumber of a $\Sigma^{1}_{n}$-formula and
$x,y^{\alpha},a_{0}^{\alpha},c_{1},...)$ are reals.

In this situation we just follow the one of the four cases in the definition
of suitable forcings which applies.

###  4.2 Definition of the iteration. Even stages.

We work towards $\mathsf{BPFA}$ on the even stages of the iteration. Recall
that due to J. Bagaria (see [2]) $\mathsf{BPFA}$ is equivalent to the
assertion that $H(\omega_{2})\prec_{\Sigma_{1}}V^{\mathbb{P}}$ for any proper
forcing $\mathbb{P}$. We shall work towards Bagaria’s reformulation of
$\mathsf{BPFA}$ adapting the usual way.

Assume that the bookkeeping $F$ at stage $\beta$ hands us a
$\Sigma_{1}$-formula $\sigma$ and parameters $p_{0},...,p_{l}$ of $\sigma$
which are elements of $P(\omega_{1})\cap L[G_{\beta}]$. We ask of
$\sigma(p_{0},...,p_{l})$ whether it holds in a suitable generic extension of
$L[G_{\beta}]$. If yes, then as $\kappa$ is reflecting, there is such a
forcing already in $L_{\kappa}[G_{\beta}]$. Moreover the witness to the true
$\Sigma_{1}$-formula can be assumed to have a name in $L_{\kappa}[G_{\beta}]$.
We fix a $\gamma<\kappa$ such that $L_{\gamma}$ is $\Sigma_{2}$-elementary in
$L_{\kappa}$, which implies that also $L_{\gamma}[G_{\beta}]$ is
$\Sigma_{2}$-elementary in $L_{\kappa}[G_{\beta}]$. Hence the suitable
forcing$\mathbb{Q}$ which forces $\sigma(p_{0},...,p_{l})$ to become true can
be assumed to belong to $L_{\gamma}[G_{\beta}]$ already. We force with
$\mathbb{Q}$ at stage $\beta$ then.

###  4.3 Properties of the defined universe

######  Lemma 4.1.

Let $G_{\kappa}$ denote a generic filter for the full, $\kappa$-length
iteration.

  1. 1.

Then $L[G_{\kappa}]$ satisfies that whenever $\varphi_{m}=\exists a_{0}\forall
a_{1}...\exists a_{2n-2}\psi(x,y,a_{0},...,a_{2n-2})$ and
$(x,y^{\alpha},a_{0}^{\alpha})$ is such that

$L[G_{\kappa}]\models\varphi_{m}(x,y^{\alpha},a_{0}^{\alpha})$

Then for each $\beta>\alpha$

$L[G_{\kappa}]\models\forall a_{1}\exists a_{2}...\exists
a_{2n-2}((\\#\psi,x,y^{\beta},a_{0}^{\beta},a_{1},..,a_{2n-2})\text{ is not
coded })$

  2. 2.

If $\varphi_{m}=\exists a_{0}\forall a_{1}...\exists
a_{2n-3}\psi(x,y,a_{0},...,a_{2n-3})$ and $(x,y^{\alpha},a_{0}^{\alpha})$ is
such that

$L[G_{\kappa}]\models\varphi_{m}(x,y^{\alpha},a_{0}^{\alpha})$

Then for each $\beta>\alpha$

$L[G_{\kappa}]\models\forall a_{1}\exists a_{2}...\exists
a_{2n-3}((\\#\psi,x,y^{\beta},a_{0}^{\beta},a_{1},..,a_{2n-3})\text{ is coded
})$

###### Proof.

We will only proof the first item, as the second is shown in the dual way. Let
$a_{1}$ be an arbitrary real. As
$L[G_{\kappa}]\models\varphi_{m}(x,y^{\alpha},a_{0}^{\alpha})$, we know that
there is an $a_{2}$ such that for every $a_{3}$ and so on there is an
$a_{2n-2}$ such that
$L[G_{\kappa}]\models\psi(x,y^{\alpha},a_{0}^{\alpha},a_{1},...,a_{2n-2})$. By
case 1 in the definition of the iteration, this translates to
$L[G_{\kappa}]\models``(\\#\psi,x,y^{\beta},a_{0}^{\beta},a_{1},...,a_{2n-2})$
is not coded$"$. As $a_{1}$ was arbitrary we can conclude that

$L[G_{\kappa}]\models\forall a_{1}\exists a_{2}...\exists
a_{2n-2}((\\#\psi,x,y^{\beta},a_{0}^{\beta},a_{1},..,a_{2n-2})\text{ is not
coded })$

as desired.

∎

######  Lemma 4.2.

Again $G_{\kappa}$ denotes a generic filter for the entire, $\kappa$-length
iteration.

  1. 1.

If $\alpha$ is least such that

$L[G_{\kappa}]\models\forall a_{1}...\exists
a_{2n-2}\psi(x,y^{\alpha},a^{\alpha}_{0},...,a_{2n-2}),$

then

$L[G_{\kappa}]\models\exists a_{1}\forall a_{2}...\forall
a_{2n-2}((\\#\psi,x,y^{\alpha},a_{0}^{\alpha},a_{1},a_{2},...,a_{2n-2})\text{
is coded}.)$

  2. 2.

If $\alpha$ is least such that

$L[G_{\kappa}]\models\forall a_{1}...\exists
a_{2n-3}\psi(x,y^{\alpha},a^{\alpha}_{0},...,a_{2n-3}),$

then

$L[G_{\kappa}]\models\exists a_{1}\forall a_{2}...\forall
a_{2n-3}((\\#\psi,x,y^{\alpha},a_{0}^{\alpha},a_{1},a_{2},...,a_{2n-3})\text{
is not coded}.)$

###### Proof.

As $\alpha$ is the first ordinal for which

$L[G_{\kappa}]\models\forall a_{1}...\exists
a_{2n-2}\psi(x,y^{\alpha},a^{\alpha}_{0},...,a_{2n-2}),$

we know that $\forall\beta<\alpha$, $L[G_{\kappa}]\models\exists a_{1}\forall
a_{2},...,\forall a_{2n-2}(\lnot\psi(x,y^{\beta},a_{0}^{\beta},a_{1},...))$.
In particular, for every $\beta<\alpha$ there are reals $a_{1}^{\beta}$ such
that for every $a_{2}^{\beta}$ there are reals $a_{3}^{\beta}$ and so on such
that $\lnot\psi$ holds. Using the bijection $\pi_{\alpha}$, we can find an
$a_{1}=\pi_{\alpha}((a_{1}^{\beta})_{\beta<\alpha})$ which has the property
that for any real $a_{2}$ there will be a real
$a_{3}=\pi_{\alpha}(a_{3}^{\beta})_{\beta<\alpha})$ such that for any real
$a_{4}$ and so on $\lnot\psi$ is true.

But this translates via the case 1 rule of our iteration to the assertion that

$L[G_{\kappa}]\models\exists a_{1}\forall a_{2}...\forall
a_{2n-2}((\\#\psi,x,y^{\alpha},a_{0}^{\alpha},a_{1},a_{2},...,a_{2n-2})\text{
is coded}.)$

∎

######  Lemma 4.3.

In $L[G_{\kappa}]$ the $\Sigma^{1}_{n+1}$-uniformization property holds true
for every $n\geq 1$.

###### Proof.

Let $\varphi\equiv\exists a_{0}\forall
a_{1}...(\psi(x,y,a_{0},a_{1},...,a_{2n-2}))$ be an arbitrary
$\Sigma^{1}_{2n+1}$-formula in two free variables where $\psi$ is
$\Pi^{1}_{2}$. Let $x$ be a real such that there is a real $y$ with
$L[G_{\kappa}]\models\varphi(x,y)$. We list all the triples
$(x,y^{\alpha},a_{0}^{\alpha})$ according to our well-order $<$. Let $\alpha$
be least such that

$L[G_{\kappa}]\models\forall
a_{1}...(\psi(x,y^{\alpha},a_{0}^{\alpha},a_{1},...)).$

Then by the last Lemma

$L[G_{\kappa}]\models\exists a_{1}\forall a_{2}...\forall
a_{2n-2}((\\#\psi,x,y^{\alpha},a^{\alpha}_{0},...)\text{ is coded})$

holds true. Note that this formula is $\Sigma^{1}_{2n+1}$. By the penultimate
Lemma, for each $\beta>\alpha$

$L[G_{\kappa}]\models\forall a_{1}\exists a_{2}...\exists
a_{2n-2}((\\#\psi,x,y^{\beta},a^{\beta}_{0},a_{1},..)\text{ is not coded}),$

which is $\Pi^{1}_{2n+1}$

So $(x,y^{\alpha})$ is the unique pair satisfying the
$\Sigma^{1}_{2n+1}$-formula

$\displaystyle\exists a_{0}((\forall a_{1}\exists a_{2}...\exists
a_{2n-2}(\psi(x,y,a_{0},...)\land$ $\displaystyle\lnot(\forall a_{1}\exists
a_{2}...\exists a_{2n-2}((\\#\psi,x,y,a_{0},a_{1},...a_{2n-2}\text{ is not
coded}))$

Indeed

∎

######  Lemma 4.4.

$L[G_{\kappa}]\models\mathsf{BPFA}$.

###### Proof.

This is standard. We show that $H(\omega_{2})^{L[G_{\kappa}]}$ is
$\Sigma_{1}$-elementary in any $L[G_{\kappa}]^{\mathbb{P}}$, where
$\mathbb{P}$ is proper. We assume that the $\Sigma_{1}$-formula
$\tau(x,p_{0},...,p_{n})$ can be forced to become true with a proper
$\mathbb{P}\in L[G_{\kappa}]$. The choice of $F$ ensures that $\tau$ and its
parameters are considered at an even stage $\beta<\kappa$ of our iteration.
But $\mathbb{P}_{\kappa}\ast\mathbb{P}$ is suitable and witnesses that $\tau$
can be forced to become true. Hence we forced so that $\tau$ becomes true
already at stage $\beta<\kappa$ and by upwards absoluteness of
$\Sigma_{1}$-statements the proof is done. ∎

## References

  * [1] J. W. Addison Some Consequences of the Axiom of Constructibilty. Fundamenta Mathematicae 46, pp. 337-357, 1959.
  * [2] J. Bagaria, Bounded forcing axioms as principles of generic absoluteness, Archive for Mathematical Logic, vol. 39 (2000), no. 6, pp. 393– 401.
  * [3] A. Caicedo and S.D. Friedman $\mathsf{BPFA}$ and Projective Wellorderings of the Reals. Journal of Symbolic Logic 76, pp. 1126-1136, (4) 2011.
  * [4] A. Caicedo and B. Velickovic The bounded proper forcing axiom and wellorderings of the reals. Mathematical Research Letters, 13 (2-3) (2006). pp. 393-408
  * [5] M. Foreman and M. Magidor  Mutually stationary sequences of sets and the non-saturation of the non-stationary ideal on $P_{\kappa}(\lambda)$. Acta Math. 186 (2001), no. 2, 271–300.
  * [6] M. Goldstern and S. Shelah  The bounded proper forcing axiom. The Journal of Symbolic Logic, Volume 60, Number 1. March 1995. pp.58–73.
  * [7] L. Harrington Long projective wellorderings. Ann. Math. Logic, 12(1):1–24, 1977.
  * [8] S. Hoffelner Forcing the $\Pi^{1}_{3}$-Reduction Property and a Failure of $\Pi^{1}_{3}$-Uniformization, Annals of Pure and Applied Logic 174 (8), 2023.
  * [9] S. Hoffelner Forcing the $\Pi^{1}_{n}$-Uniformization Property, submitted.
  * [10] S. Hoffelner Forcing Axioms and the Uniformization Property, submitted.
  * [11] S. Hoffelner Forcing the $\Sigma^{1}_{3}$-Separation Property. Journal of Mathematical Logic, 2022.
  * [12] S. Hoffelner, P. B. Larson, R. D. Schindler and L. Wu Forcing Axioms and the Definability of the Nonstationary Ideal on the first Uncountable. Journal of Symbolic Logic. Published online 2023:1-18. doi:10.1017/jsl.2023.40
  * [13] T. Jech Set Theory. Third Millenium Edition. Springer 2003.
  * [14] A. Kechris Classical Descriptive Set Theory. Springer 1995.
  * [15] R. D. Schindler Set Theory. Exploring Independence and Truth Springer 2014.
  * [16] S. Shelah  Proper and improper forcing. Second edition. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1998. xlviii+1020 pp
  * [17] J. Steel $\mathsf{PFA}$ implies $\mathsf{AD}^{L(\mathbb{R})}$.  Journal of Symbolic Logic Vol. 70, No. 4, pp. 1255-1296, 2005.
  * [18] S. Todorcevic A Note on the Proper Forcing Axiom, Contemporary Mathematics vol. 31, 1984.
  * [19] S.Todorcevic Localized reflection and fragments of PFA, Set theory (Piscataway, NJ, 1999), volume 58 of DIMACS series in discrete mathematics and theoretical computer science, pp. 135–148. American Mathematics Society, Providence, RI (2002)