Rachid Riad

Julien Karadayi

Anne-Catherine Bachoud-Lévi

Emmanuel Dupoux

Learning spectro-temporal representations of complex sounds with parameterized neural networks

Deep Learning models have become potential candidates for auditory neuroscience research, thanks to their recent successes on a variety of auditory tasks. Yet, these models often lack interpretability to fully understand the exact computations that have been performed. Here, we proposed a parametrized neural network layer, that computes specific spectro-temporal modulations based on Gabor kernels (Learnable STRFs) and that is fully interpretable. We evaluated predictive capabilities of this layer on Speech Activity Detection, Speaker Verification, Urban Sound Classification and Zebra Finch Call Type Classification. We found out that models based on Learnable STRFs are on par for all tasks with different toplines, and obtain the best performance for Speech Activity Detection. As this layer is fully interpretable, we used quantitative measures to describe the distribution of the learned spectrotemporal modulations. The filters adapted to each task and focused mostly on low temporal and spectral modulations. The analyses show that the filters learned on human speech have similar spectro-temporal parameters as the ones measured directly in the human auditory cortex. Finally, we observed that the tasks organized in a meaningful way: the human vocalizations tasks closer to each other and bird vocalizations far away from human vocalizations and urban sounds tasks. INTRODUCTION The main objective of auditory neuroscience is to build models that can both predict the brain neural responses to relevant sounds and the behaviours associated with these responses [START_REF] Kell | Deep neural network models of sensory systems: windows onto the role of task constraints[END_REF][START_REF] Pillow | Editorial overview: Machine learning, big data, and neuroscience[END_REF]. While most of the auditory neuroscience research has focused on the neural side, there is growing recognition for the importance to also match the performance of living organisms on a variety of behavioral tasks [START_REF] Yarkoni | Choosing prediction over explanation in psychology: Lessons from machine learning[END_REF]. In recent years, major progress has been achieved with Deep Neural Networks (DNNs) which, after training with supervised classification objectives on large datasets, proved able to perform near human performance on a variety of audio tasks such as automatic speech recognition [START_REF] Amodei | Deep speech 2: End-to-end speech recognition in english and mandarin[END_REF], speaker verification [START_REF] Snyder | X-vectors: Robust dnn embeddings for speaker recognition[END_REF] or audio scene classification [START_REF] Salamon | Deep convolutional neural networks and data augmentation for environmental sound classification[END_REF]. These trained systems therefore become potential candidate models for auditory neuroscience [START_REF] Koumura | Cascaded tuning to amplitude modulation for natural sound recognition[END_REF], and have already started to be used to account for perceptual results [START_REF] Saddler | Deep neural network models reveal interplay of peripheral coding and stimulus statistics in pitch perception[END_REF] and brain data [START_REF] Kell | A task-optimized neural network replicates human auditory behavior, predicts brain responses, and reveals a cortical processing hierarchy[END_REF] in humans.

DNNs models typically take as input a spectral representation (although some new trends consist in side-stepping this representation and work directly from the raw waveform). Working from a spectral representation has biological plausibility, since it matches approximately what we know about the first stage of auditory processing [START_REF] Stevens | A scale for the measurement of the psychological magnitude pitch[END_REF]. However, DNNs models are less biologically motivated regarding the next steps. Most of them use rather generic connectivity patterns (fully connected, convolutional or recurrent networks), which while being very powerful in learning task-specific representations from an engineering point of view, lack both interpretability and support in the auditory neuroscience. To push the understanding of both the artificial and real neural networks, there have been some attempts to decode the representation extracted from biological measurements or computed by deep learning models [START_REF] Ondel | Deriving spectro-temporal properties of hearing from speech data[END_REF][START_REF] Thoret | Probing machine-learning classifiers using noise, bubbles, and reverse correlation[END_REF]. Even though these methods allow to uncover the important aspects of the stimuli, they rely on simplifying hypotheses (linearity of the responses, independence across neurons [START_REF] Meyer | Models of neuronal stimulus-response functions: elaboration, estimation, and evaluation[END_REF][START_REF] Shamma | Auditory cortical representation of complex acoustic spectra as inferred from the ripple analysis method[END_REF]) and they do not provide in depth explanation on how the DNNs made their decisions.

Fortunately, the stages beyond the extraction of the acoustic spectrum have been studied over the past few years with novel understanding of the representations and processing involved [START_REF] Mcdermott | Audition[END_REF]. Slow spectral and temporal modulation built on top of the spectrum have been shown in psychophysical tests to be useful for several audio tasks solved by mammals: they contribute to speech intelligibility [START_REF] Edraki | Improvement and assessment of spectro-temporal modulation analysis for speech intelligibility estimation[END_REF][START_REF] Elhilali | A spectro-temporal modulation index (stmi) for assessment of speech intelligibility[END_REF][START_REF] Elliott | The modulation transfer function for speech intelligibility[END_REF], they help to boost performance for speech processing in noisy environments [START_REF] Chang | Robust cnn-based speech recognition with gabor filter kernels[END_REF][START_REF] Mesgarani | Discrimination of speech from nonspeech based on multiscale spectro-temporal modulations[END_REF][START_REF] Vuong | Learnable Spectro-Temporal Receptive Fields for Robust Voice Type Discrimination[END_REF].

In addition, the responses to such spectral and temporal modulations of natural sounds can be decoded from human fMRI [START_REF] Santoro | Reconstructing the spectrotemporal modulations of real-life sounds from fmri response patterns[END_REF] and have been measured directly with invasive techniques in ferrets [START_REF] Depireux | Spectro-temporal response field characterization with dynamic ripples in ferret primary auditory cortex[END_REF], in birds [START_REF] Woolley | Tuning for spectrotemporal modulations as a mechanism for auditory discrimination of natural sounds[END_REF], and also in the human brain [START_REF] Hullett | Human superior temporal gyrus organization of spectrotemporal modulation tuning derived from speech stimuli[END_REF]. Analytic models of these modulations have been proposed [START_REF] Chang | Robust cnn-based speech recognition with gabor filter kernels[END_REF]; [START_REF] Chi | Multiresolution spectrotemporal analysis of complex sounds[END_REF]; [START_REF] Ezzat | Spectro-temporal analysis of speech using 2d gabor filters[END_REF]; [START_REF] Schädler | Spectro-temporal modulation subspace-spanning filter bank features for robust automatic speech recognition[END_REF], on the basis of wavelet analysis.

The idea is that on top of the spectrum, spectro-temporal wavelets or gabor patches can be defined which drive both behavioral responses and brain signals. The problem of such analytic models is that they only propose a potentially very large representation space, but provide no method to select which gabor patch is relevant for which task. But analyses of brain signals show that the responses from the auditory cortex are not fixed, but vary depending on the task at hand [START_REF] Francis | Laminar profile of task-related plasticity in ferret primary auditory cortex[END_REF][START_REF] Fritz | Rapid task-related plasticity of spectrotemporal receptive fields in primary auditory cortex[END_REF][START_REF] Jääskeläinen | Shortterm plasticity in auditory cognition[END_REF]. Therefore, what is needed, is a model that can learn the characteristics of the spectrotemporal representations that are relevant to the task. This is the goal of this work. We introduce a parametrized neural network which explicitly represent spectro-temporal filters, but which parameters are differentiable and can therefore be tuned to each particular task. There are two advantages of this approach as illustrated in Figure 1. First, as Analytic Models, and contrary to standard DNN models, this model is fully interpretable. The parameters of each filter can be directly read off the model and compared to physiological or neural data. Second, as DNNs, but contrary to Analytic Models, this model can be tuned to different tasks, accounting both for behavioral results and for the task-specificity of the brain representations. As a side issue, since the model is constrained and has few parameters, it has the potential to explain perceptual learning aspect of plasticity with a lot less training data than is typically used in generic DNNs. Therefore, the model makes direct and testable predictions about the auditory representation as a function of the task.

The paper is organized as follows: Section II presents the Methods with our parametrized neural network model, and the different ways to analyze the distribution of the learned spectro-temporal modulations; in Section III we described the experimental setup with the different computational tasks, data, toplines, and evaluations; Section IV presents the per-formance results, the analysis of the learned distribution of spectro-temporal modulation for each setup and the discussions. Section V presents our conclusions and the potential future work. [START_REF] Bellur | Detection of speech tokens in noise using adaptive spectrotemporal receptive fields[END_REF][START_REF] Chang | Robust cnn-based speech recognition with gabor filter kernels[END_REF][START_REF] Elie | The vocal repertoire of the domesticated zebra finch: a data-driven approach to decipher the information-bearing acoustic features of communication signals[END_REF][START_REF] Mesgarani | Discrimination of speech from nonspeech based on multiscale spectro-temporal modulations[END_REF][START_REF] Schädler | Spectro-temporal modulation subspace-spanning filter bank features for robust automatic speech recognition[END_REF]. The upper index n i and lower index k th represent the n i -step during learning for the k th filter.

φ n1 i φ n2 i φ n3 i g n 1 i g n 2 i g n 3 i ψ 1 ψ 2 ψ 3 L e a
Temporal modulation (Hz)

First stage of processing

The first audio processing step is the transformation of the audio signal from the time domain into the frequency domain Y(t, f ). Each excerpt of sound given to the network is normalized per instance with a 1 dimensional Instance Normalization layer [START_REF] Ulyanov | Instance normalization: The missing ingredient for fast stylization[END_REF]. Then the sound is decomposed into a Filter banks spaced based on the Mel scale after a log compression (Mel-filterbanks) similarly as the resolution of the human cochlea.

There are 64 filters with center frequencies in the range [0.0, 8000.0Hz]. The computations for the Mel-filterbanks of the audio can be performed on-the-fly directly on GPU thanks to [START_REF] Cheuk | nnaudio: An on-thefly gpu audio to spectrogram conversion toolbox using 1d convolutional neural networks[END_REF].

Definition of the Learnable spectro-temporal filters

The second step of front-end processing is a set of convolution between the time-frequency representation of the audio and a set of Gabor Filters [START_REF] Gabor | Theory of communication. part 1: The analysis of information[END_REF].

The 2-D Gabor filter kernel g k is a sine-wave w k modulated by a 2-D Gaussian envelope s k . Each Gabor filter g k is expressed based on the set of parameters (σ t , σ f , γ k , F k ) in polar coordinates. We used the following formulation in this work:

g k (t, f ) = s k (t, f ) • w k (t, f ) (1a) s k (t, f ) = 1 2πσ t k σ f k e -1 2 t 2 σ 2 t k + f 2 σ 2 f k (1b) w k (t, f ) = e j(2π(F k Rγ k )) (1c) R γ k = t cos(γ k ) + f sin(γ k ) (1d)
We obtain a bank of N filters {g k (t, f )} k=0..N -1 . These bank of filters is convoluted with the time-frequency representation Y to obtain the 3D representation Z.

Z(t, f, k) = u,v Y (u, v) g k (t -u, f -v) ∈ C (2)
These filters and their parameters can be used in 2D Convolution neural Networks (Alekseev and Bobe, 2019) in different ways: (1) as an Initialisation (Free 2D conv. Gabor

Init.) of a 2D convolution neural network and the 2D grid is tuned completely by backpropagation (as in [START_REF] Chang | Robust cnn-based speech recognition with gabor filter kernels[END_REF][START_REF] Ezzat | Spectro-temporal analysis of speech using 2d gabor filters[END_REF][START_REF] Schädler | Spectro-temporal modulation subspace-spanning filter bank features for robust automatic speech recognition[END_REF]),

(2) or finally as Learnable spectro-temporal Filters (Learnable STRFs), so the gradient descent is only performed on the set of parameters (σ t k , σ f k , F k , γ k ). Indeed, all the operators to derive the Gabor Filter based on (σ t k , σ f k , F k , γ k ) are differentiable almost everywhere:

x → e x , x → cos(x), x → sin(x), x → x 2 , x → 1 x , x → constant • x.
The 2D grid instantiated by the Gabor Filter used the parameters (σ t k , σ f k , F k , γ k ) in each cell, therefore, the gradients are summed over the 2D grid for each parameter. Each Learnable STRF filters were given 9 Mel-frequency spectral filters and 1.1s of context, thus yielding a size of 9x111 for each filter.

Finally, the output representation Z is in the complex domain C. To be used by classic neural network architectures, we concatenated [ (Z), (Z)] to obtain the representation to be fed to the rest of each network. We denoted by Learnable STRFs this specific front-end in all result tables, and by Learned STRFs once we examined these representations.

Descriptive quantifiers of the distribution

We used quantitative measures to describe the structure of the distribution of the learned spectro-temporal Convolutions. This is in the same spirit as [START_REF] Singh | Modulation spectra of natural sounds and ethological theories of auditory processing[END_REF] for the 2-D Modulation Power Spectrum of sound ensembles, and Modulation Power Spectrum of the spectral-temporal receptive field of auditory neurons in ferrets [START_REF] Depireux | Spectro-temporal response field characterization with dynamic ripples in ferret primary auditory cortex[END_REF].

We converted the learned parameters in Cartesian coordinates [START_REF] Schädler | Spectro-temporal modulation subspace-spanning filter bank features for robust automatic speech recognition[END_REF] with the Temporal Modulation ω k and Spectral Modulation Ω k :

(σ t , σ f , ω k , Ω k ), where ω k = F k cos(γ k ) and Ω k = F k sin(γ k ).
We took the same convention as [START_REF] Chi | Multiresolution spectrotemporal analysis of complex sounds[END_REF][START_REF] Singh | Modulation spectra of natural sounds and ethological theories of auditory processing[END_REF] for the up-sweep and down-sweep modulations, and represented only half the plan due to the symmetry.

We adapted the measures of Separability, Asymmetry, Low-pass coefficient and Starriness coefficients with the interpretable parameters obtained for each Supervised Learning tasks.

As the Learned spectro-temporal receptive fields (Learned STRFs) self-organized to solve each task, we examined each of this parameter for each task. Each α is estimated with the bootstrap re-sampling method [START_REF] Efron | An introduction to the bootstrap[END_REF] on the Learned STRFs (100 bootstraps).

a. Asymmetry. The distribution of the learned STRFs can show asymmetry preferences. The distribution is considered asymmetric if there are preferences for either downsweeps or up-sweeps Learned STRFs.

α asymmetry = |{g k s.t. ω k > 0}| |{g k }| = |{g k s.t. ω k > 0}| N (3) If α asymmetry ≈ 0, the distribution of STRFs filters {g k (t, f )} k=0..N -1 is considered sym- metric.
If α asymmetry > 0, there are more up-sweeps than down-sweeps.

b. Low Pass Coefficient and Starriness. It has been observed in [START_REF] Singh | Modulation spectra of natural sounds and ethological theories of auditory processing[END_REF], that most energy in Modulation Power Spectrum was concentrated in low spectral and temporal modulations for natural sounds. In addition, the higher spectral and temporal modulations were not distributed uniformly but were mostly along the axes. We derived two coefficients to quantify these phenomena with the Learned STRFs:

α low = |{g k s.t. |ω k | < ∆ t , Ω k < ∆ f }| N = N low N (4)
For the temporal modulation low limit we opt as [START_REF] Singh | Modulation spectra of natural sounds and ethological theories of auditory processing[END_REF] for ∆ t = 16Hz. The spectral modulation low limit is set to ∆ f = 0.08 Cycle/Octave. These parameters were chosen deliberately low as most learned modulations were mostly concentrated in low temporal and spectral modulations. The parameter α star to measure "stariness" of the distribution is the relative measure of distribution excluding regions with high joint temporal and spectral modulations and the regions with low joint temporal and spectral modulations.

α star = N ∆t + N ∆ f -2 × N low N -N low (5)
The quantities c. Separability. To obtain a separability measure from the learned STRFs, we approximated the 2D-distribution P(ω, Ω) of the filters with Kernel Density Estimation with Gaussian Filters. Then we evaluate if the normalized 2D-distribution P can be factorized into a product of two independent functions P(ω, Ω) = G(ω) • F (Ω). To quantify the separability, we calculated as [START_REF] Singh | Modulation spectra of natural sounds and ethological theories of auditory processing[END_REF] the singular value decomposition of the P(ω, Ω) obtained from each task:

N ∆t = |{g k s.t. |ω k | < ∆ t }| and N ∆ f = |{g k s.t. Ω k < ∆ f }|
P (ω, Ω) = n i=1 λ i g i (ω) • h i (Ω) , λ 1 > λ 2 > • • • > λ n (6)
Then, we computed the ratio of first singular value relative to the sum of all singular values.

α sep = λ 1 n i=1 λ i (7)
If α sep ≈ 1, the distribution of the learned STRFs can be considered separable.

Measuring distance between tasks based on the learned STRF filters and optimal transport

The α measures provide some descriptors allowing some comparison between the learned distributions. However, they only look at one view and aspect of the learned distributions at a time. There is no clear way to measure the distances between each task based on the α. Besides, these α measures do not take into account the learned Gaussian envelope parameters (σ t k , σ f k ). Here, the goal is to obtain a quantitative metric able to compare the distributions obtained from each task. Usually, researchers fall back to the Mahalanobis distance or an approximation of the KL-divergence to compare observations of two sets of points. Yet, these metrics either make modelling assumptions about the data (approximation of the underlying density functions that generated the data), or it is impossible to compare set of points with different cardinals.

The non-parametric, natural and most powerful way to compare distributions is to use optimal transport distances [START_REF] Peyré | Computational optimal transport: With applications to data science[END_REF]. We compared the different tasks by comparing the learned STRFs using the regularized version Sinkhorn distance [START_REF] Cuturi | Sinkhorn distances: Lightspeed computation of optimal transport[END_REF][START_REF] Flamary | Pot python optimal transport library[END_REF]. Especially, this regularized version of the optimal transport distance allow fast computation of distances and multiple assignments between points.

We made the choice to compare two individual learned STRFs with the Euclidean distance ||.|| We normalized along each axis/parameter to not privilege for a specific parameter variability. Based on each task we tackled in this work, we obtained a distribution of normalized learned parameters {σ t k , σ f k , ω k , Ω k } task with the size n task being the total number of filters used for this task. Therefore, equipped with the Euclidean distance to compare the individual filters, we can obtain the cost matrix between two tasks M (taska,task b ) ∈ R n taska ×n task b . We did not privilege any learned STRFs to build the distribution, therefore we attributed equal weight to each individual filter w task = (1/n task )1 n task . This allows to compare the different task if we have several models due to cross validation (Urban and Bird ) or less filters for a specific task (Bird ). If we denote, by < ., . > F the norm of Froebenius between matrices, the regularized distance d λ between two tasks is defined as:

d λ = min P < P, M > F -λ • h(P ) s.t. P 1 n taska = w taska P T 1 n task b = w task b P ∈ R n taska ×n task b + h(P ) = - i,j P i,j log(P i,j ) λ = 10 -3 (8)
and task b to each other based on the Sinkhorn-distance

d λ ({σ t k , σ f k , ω k , Ω k } taska , {σ t k , σ f k , ω k , Ω k } task b ).
Based on the distances between all tasks, we built a hierarchical cluster tree and represent these distances with a dendogram (See Figure 5).

III. EXPERIMENTAL SETUP

We compared the Learnable STRFs layer with strong toplines that have been lately

introduced to solve each task as well more classic baselines for each task. We tried to keep the systems with Learnable STRFs as close as possible from topline systems.

A. Speech Activity Detection

The goal of Speech Activity Detection is to segment a given stream audio into portions of Speech or Non-Speech. We choose this task, as it allows us to examine what are the exact spectro-temporal modulations that makes standout speech in a audio stream with silences and background noises [START_REF] Mesgarani | Discrimination of speech from nonspeech based on multiscale spectro-temporal modulations[END_REF].

We conduct experiments with 2 challenging datasets with different characteristics:

The We also reported the Missed detection Rate(%) and False Alarm Rate (%). We used the implementation of the metrics from pyannote.metrics [START_REF] Bredin | pyannote.metrics: a toolkit for reproducible evaluation, diagnostic, and error analysis of speaker diarization systems[END_REF] and all experiments were run with pyannote.audio [START_REF] Bredin | Pyannote. audio: neural building blocks for speaker diarization[END_REF].

We ran an additional analysis for the Speech Activity Detection Task to compare the use of (Z), (Z), |Z| and [ (Z), (Z)] (See Table V in Appendix A).

B. Speaker Verification

The goal of the Speaker Verification task in speech processing is to accept or reject the hypothesis that a given speaker pronounced a given sentence. To do so, we learned an embedding function of any speech sequence of variable length. We examined this task, as it is believed that spectro-temporal modulations encode specifically the speaker information [START_REF] Elliott | The modulation transfer function for speech intelligibility[END_REF][START_REF] Lei | Spectro-temporal gabor features for speaker recognition[END_REF].

We followed the same procedure as Coria et al. Error Rate (EER). We also measured the performance of each approach when using the the S-normalization. We also reported the baseline performance of the I-vector system trained on VoxCeleb1 combined with Probabilistic Linear Discriminant Analysis (PLDA) [START_REF] Dehak | Front-end factor analysis for speaker verification[END_REF]. We denoted by Speaker the experiments and the distribution of learned STRFs on this dataset and this task.

C. Urban Sound Classification

The problem of Urban Sound Classification is to classify short excerpt of audio sounds into broad categories (Ex: Car horns, Air Conditioner, Drilling). We investigated the use of the Learnable STRFs for Urban sound classification, especially to test the use of spectrotemporal modulations for other type of sounds than animal (human or bird) vocalizations [START_REF] Mcdermott | Learning midlevel auditory codes from natural sound statistics[END_REF].

We followed the same evaluation procedure as [START_REF] Salamon | Deep convolutional neural networks and data augmentation for environmental sound classification[END_REF] to evaluate the experiments with the UrbanSound8K database [START_REF] Salamon | A dataset and taxonomy for urban sound research[END_REF]. The dataset is composed of 8732 excerpts of urban sounds from 10 categories (air conditioner, car horn, children playing, dog bark, drilling, engine idling, gun shot, jackhammer, siren, street music), and split in 10 separate folds. To compare with previous approaches, each model is evaluated by cross-validation on the 10 folds. We reported the Mean, Min and Max of the Accuracy across the 10 folds. We used the code-base from [START_REF] Arnault | Urban sound classification: striving towards a fair comparison[END_REF] for the training and evaluations of the 2 approaches. The topline approach is the use of a Mel-filterbanks with the CNN10 architecture from [START_REF] Kong | Panns: Large-scale pretrained audio neural networks for audio pattern recognition[END_REF]. For the Learnable STRFs approach, the first convolution layer of the CNN10 architecture (Free 2D convolution with size 3x3 with 64 filters) is replaced by the Learnable STRFs layer (64 filters) on top of the Mel-filterbanks described in section II. The models are trained with the RAdam optimizer [START_REF] Liu | On the variance of the adaptive learning rate and beyond[END_REF] with LookAhead [START_REF] Zhang | Lookahead optimizer: k steps forward, 1 step back[END_REF]. We also reported the results from [START_REF] Salamon | Deep convolutional neural networks and data augmentation for environmental sound classification[END_REF] as baseline. We denoted by Urban the experiments and the distribution of learned STRFs on this dataset and this task.

D. Zebra Finch Call Type classification

Finally, we examined the Zebra Finch Call Type classification task [START_REF] Elie | The vocal repertoire of the domesticated zebra finch: a data-driven approach to decipher the information-bearing acoustic features of communication signals[END_REF]. The goal of this task is to classify short-excerpt of sounds into Call Type categories for the Zebra Finch bird. Indeed, it has been found by [START_REF] Elie | The vocal repertoire of the domesticated zebra finch: a data-driven approach to decipher the information-bearing acoustic features of communication signals[END_REF] that several properties the acoustic space allow to separate to some extent the Call Types in the repertoire of Zebra Finches. We tried to stay as close as possible from the experimental protocol of [START_REF] Elie | The vocal repertoire of the domesticated zebra finch: a data-driven approach to decipher the information-bearing acoustic features of communication signals[END_REF]. The dataset is composed of 3433 excerpts of Zebra Theunissen (2016).

Finally, we evaluated the potential of the Learnable STRFs (24 filters) for this task. We combined the Learnable STRFs with a simple linear layer to output directly the decision layer. The models were trained with the Adam optimizer [START_REF] Kingma | Adam: A method for stochastic optimization[END_REF]. We denote by Bird the experiments and the distribution of learned STRFs on this dataset and this task.

IV. RESULTS AND DISCUSSIONS

First, we analyzed the quantitative performances to perform the tasks for the Learnable STRFs for the different audio benchmarks. Then, we examined and compared, qualitatively and quantitatively, the statistics of the Learned STRFs representations.

Overall, the performances of the Learnable STRFs is on par for all tasks with the different baselines. There is no skip connection between the Mel-filterbanks and the rest of each neural network that has been considered. This means that these Learned STRFs are in someway useful to perform each task, as this layer act as a filter. A degradation of performance means that it might be not fully sufficient to use spectro-temporal modulations to perform this specific task.

The objective results for the Speech Activity Detection task are shown for all models in Table I. Overall, learnable front-end approaches with injected prior improved over the classic signal processing baselines, Mel-filterbanks and MFCCs. Yet, the approaches with Free 2D conv. were not capable to improve over the classic signal processing baselines and had the worst performance, even for the convolution initialized with Gabor filters. The best-performing models for this task, were the ones trained with the Learnable STRFs, and outperformed all the baselines. It is improving over the State-of-the-Art model with SincNet on the AMI dataset, and matched the performance on the CHIME5 dataset. Therefore, adding prior for spectro-temporal modulations was beneficial for Speech Activity Detection.

The closest work to our knowledge around speech activity detection is [START_REF] Vuong | Learnable Spectro-Temporal Receptive Fields for Robust Voice Type Discrimination[END_REF],

where they derived a layer that learn the spectro temporal modulation especially for Voice Type Discrimination in an industrial environment. The main difference with our work, is that they relied on the expression of the discrete implementation of the Hilbert transform.

They also reported that parametrized Neural Network were better than free convolutions.

They also used a long receptive field along the time axis, and a small receptive field along the frequency axis. SincNet [START_REF] Coria | A Comparison of Metric Learning Loss Functions for End-To-End Speaker Verification[END_REF] 3.9 3.5

Learnable STRFs + CL 6.4 6.1

a This result is directly extracted from their paper and was not replicated for this study.

The results for the Speaker Verification task are reported in Table II. We found out that the SincNet that was designed initially for Speaker Recognition [START_REF] Ravanelli | Speaker recognition from raw waveform with sincnet[END_REF] is getting better results than the Learnable STRFs + CL. The S-normalization improved both systems. This result differ with previous results reported by [START_REF] Lei | Spectro-temporal gabor features for speaker recognition[END_REF] that the spectro-temporal modulations were useful for speaker recognition. One difference, that could explain this discrepancy, is the use of Bayesian models after the different features est progresses of Deep Learning research to tackle the Speaker recognition task and were validated initially on spectral representations of the audio. Our results suggest that spectrotemporal modulations are not fully sufficient to distinguish speakers. Harmonic structure was found useful for the Speaker Verification and Recognition task [START_REF] Imperl | A study of harmonic features for the speaker recognition[END_REF]. One of the hypothesis is that the learning of the harmonic structure is more difficult with the outputs Learnable STRFs layer than directly with the Mel-filterbanks. a This result is directly extracted from their paper and was not replicated for this study.

The performances for the Urban Sound Classification task are reported in Table III. The accuracy of the Learnable STRFs is above the baseline approach from [START_REF] Salamon | Deep convolutional neural networks and data augmentation for environmental sound classification[END_REF] and is on par (slightly below) with the CNN10 architecture using Mel-filterbanks sizes of the Spectral representation was increasing the performance of deep learning models for acoustic Event Detection. This suggests that the varying sizes of the focus on the Melfilterbanks representations boost the performances, both in time and frequency. In our case, the model learned to focus through the fitting of the (σ f , σ t ) parameters. Finally, the results for the Zebra Finch Call Type classification are in Table IV. On one hand, the PAF features depended slightly on the model used after for classification (LDA 57% to RF 58%) while the MPS had the worst performance overall with linear model such as LDA while the MPS had the best performance overall when combined with the RF (going from 41 % to 69%). The Learnable STRFs models was decoded with a simple linear layer, so the closest baseline is the combination of the MPS with the LDA. The Learnable STRFs perform below the PAF features and the MPS with RF. The performance with combination of features in the MPS with RF suggest that the model with Learnable STRFs could benefit greatly from Adaptive Neural Trees [START_REF] Tanno | Adaptive neural trees[END_REF] to perform the task. In addition, this encourages the use co-occurrences or anti-occurrences of the spectro-temporal patterns in models as in M lynarski and [START_REF] Mcdermott | Audition[END_REF]McDermott ( , 2019)), since the routing in RF imply to measure joint patterns in the feature space of the MPS.

B. Description of the learned filters

First, we observed that the Learned STRFs organized differently for each task, both the modulations (ω, Ω) (See Figure 3) and the size of the Gaussian envelopes through (σ t , σ f ) (See Figure 6 in Appendix). Within the space allowed by the Nyquist theorem and the size of the convolutions, all the learned STRFs still concentrated in low spectral and temporal modulations (See Figure 3). We also observed as [START_REF] Singh | Modulation spectra of natural sounds and ethological theories of auditory processing[END_REF] that higher spectral modulations were found at low temporal modulations (and vice-versa). We found Call Type Classification (Bird). We displayed only a subset of the Learned STFRs of the Bird and Urban tasks for clarity. We also plotted the bi-variate distributions using kernel density estimation for each task.

similar than the Bird and Urban ones. We quantified these observations with the description of the parameters described in Sub-section II A 3 and the measure of distance between tasks with optimal transport in Sub-section II A 4.

First, the separability index α separability showed that most Learned STRFs are quite separable, and that the task related to human vocalizations (Speech and Speaker ) were less separable than the other ones. We also found that all modulations have quite high α starriness indexes. Similar results were found in [START_REF] Singh | Modulation spectra of natural sounds and ethological theories of auditory processing[END_REF] for the separability and the starriness for the ensembles of sounds of Speech corpora, Zebra Finches vocalizations, and environmental sounds. [START_REF] Schädler | Spectro-temporal modulation subspace-spanning filter bank features for robust automatic speech recognition[END_REF] evaluated the use of high joint spectral and temporal modulation, and also found that they were degrading the performances for Speech Recognition tasks.

Besides, the Learned STRFs for the Speech did not show preferences for up or down sweeps modulations (α asymmetry ≈ 0.0), while the Speaker and Bird tasks exhibit slight preferences for down-sweeps and the Urban for up-sweeps. The result for the Bird task differed from [START_REF] Singh | Modulation spectra of natural sounds and ethological theories of auditory processing[END_REF]. This could be explained by the fact that [START_REF] Singh | Modulation spectra of natural sounds and ethological theories of auditory processing[END_REF] used a quantification of these parameters with an ensemble of sounds.

The information about the specific characteristic of an individual Zebra Finch is mixed with the information of the Call Type. This suggests that a fully interpretable supervised approach might allow to decipher the different factors and contributions that influenced the acoustic properties of vocalizations. Finally, the Bird task focused more on the low frequency Speaker Verification on VoxCeleb (Speaker) Zebra Finch Call Type Classification (Bird). The distance between tasks is computed between the learned STRF filters of each task with the Sinkhorn distance (we used the euclidean distance between each filter and the regularization parameter of the Sinkhorn distance is λ = 10 -3 ).

modulations (α lowf req ≈ 0.70) than the other tasks (α lowf req ≤ 0.35). We also observed that the Learned STRFs of the Speaker task moved away from the low spectral modulations and yielded the lowest low-pass coefficient (α lowf req ≈ 0.19). Especially, [START_REF] Elliott | The modulation transfer function for speech intelligibility[END_REF] also found out that the removing of spectral modulations between 3 and 7 cycles/kHz significantly increases the gender mis-identifications of female speakers. In addition, the results for the Speech on the AMI and CHIME5 datasets and the Speaker are very similar to the ones found directly in the auditory cortex neurons in awake monkeys [START_REF] Massoudi | Spectrotemporal response properties of core auditory cortex neurons in awake monkey[END_REF] and in awake humans [START_REF] Hullett | Human superior temporal gyrus organization of spectrotemporal modulation tuning derived from speech stimuli[END_REF].

V. CONCLUSION AND FUTURE WORK

In summary, we examined the use of a parametrized neural network front-end to learn spectro-temporal modulations optimal for different behavioral tasks. This front-end, the Learnable STRFs, yielded performances close to published state-of-the-art using engineeringoriented neural network for Speaker Verification, Urban Sound Classification, Zebra Finch Call Type Classification, and obtained the best results on two datasets for Speech Activity Detection. As our front-end is fully interpretable, we found markedly different spectrotemporal modulations as a function of the task, showing that each task relies on a specific set of modulations. These task-specific modulations were globally congruent with previous work based on three approaches: spectro-temporal analysis of different audio signals [START_REF] Elliott | The modulation transfer function for speech intelligibility[END_REF], analysis of trained neural networks [START_REF] Schädler | Spectro-temporal modulation subspace-spanning filter bank features for robust automatic speech recognition[END_REF], and analysis of the auditory cortex [START_REF] Hullett | Human superior temporal gyrus organization of spectrotemporal modulation tuning derived from speech stimuli[END_REF][START_REF] Santoro | Reconstructing the spectrotemporal modulations of real-life sounds from fmri response patterns[END_REF]. In particular, for the Speech Activity Detection task, we observed the same modulation distributions as the ones found directly the human auditory cortex listening while listening to naturalistic speech [START_REF] Hullett | Human superior temporal gyrus organization of spectrotemporal modulation tuning derived from speech stimuli[END_REF]. The modulations also displayed generic characteristics across tasks, namely, a predominance of low frequency spectral and temporal modulations and a high degree of 'stariness' and 'separability', corresponding to the fact that filters tend to remain close to either the temporal or spectral axis, with low occupation of joint spectro and temporal responses. This is consistent with [START_REF] Singh | Modulation spectra of natural sounds and ethological theories of auditory processing[END_REF]. In order to encourage reproducible research, the developed Learnable STRFs layer, the learned STRFs [START_REF] Bellur | Detection of speech tokens in noise using adaptive spectrotemporal receptive fields[END_REF] have investigated the adaptation of modulations in analytical models and witnessed several improvements in terms of engineering performances suggesting that this is also an interesting avenue in terms of behavioral modeling. Second, the analyses from [START_REF] Hullett | Human superior temporal gyrus organization of spectrotemporal modulation tuning derived from speech stimuli[END_REF] showed that not only neurons have spectro-temporal selectivity but are also topographically distributed along the posterior-toanterior axis in the superior temporal gyrus. In future work, it would be interesting to reproduce such topography by using an auxiliary self-organizing maps objective in addition to the task-specific loss function for the STRFs. Finally, despite their wide use in auditory neuroscience, the spectro-temporal modulations do not provide a complete picture of computations in the auditory cortex [START_REF] Williamson | Input-specific gain modulation by local sensory context shapes cortical and thalamic responses to complex sounds[END_REF]. A potential extension of our work would be to add an extra layer able to express co-occurrences and anti-occurrences of pairs of spectro-temporal receptive fields as in M lynarski and [START_REF] Mcdermott | Audition[END_REF]McDermott ( , 2019)). Such an extra layer would provide a learnable and interpretable extension to spectro-temporal representations.

To conclude, we emphasize that neuroscience-inspired parametrized neural networks can provide models that are both efficient in terms of behavioral tasks and interpretable in terms of auditory signal processing. Classification (Bird). We displayed only a subset of the Learned STFRs of the Bird and Urban tasks for clarity. We also plotted the bi-variate distributions using kernel density estimation for each task.

We performed an additional analysis of Speech Activity Detection of the choice of representations Z from the Learnable STRFs used in the subsequent neural network. The performance of the real part, the imaginary part and absolute values of the filter output are compared. The results are presented in Table V. In comparison with the concatenation of the real and imaginary parts, the performance obtained for each part were in the same

  FIG.1. Schematic illustration of the space of functions and different approaches to obtain spectro-

  FIG. 2. Temporal and Spectral Modulations populations learned to tackle Speech Activity Detec-

  are the regions near the axes.

  AMI database (McCowan et al., 2005) a meeting dataset in English recorded with multiple microphones in 3 different rooms. There are 180 different speakers in the datasets.Here, we focus on the AMI.SpeakerDiarization.MixHeadset protocol as we are working only single channel feature analysis. We denoted by Speech AMI the experiments and the distribution of learned STRFs on this dataset and this task. The CHiME5 database[START_REF] Barker | The fifth 'chime' speech separation and recognition challenge: Dataset, task and baselines[END_REF] is a dataset recorded at home during parties. Here, we focus also on single channel feature analysis with the CHiME5.SpeakerDiarization.U01 protocol. We denoted by Speech CHIME5 the experiments and the distribution of learned STRFs on this dataset and this task.We compared different input front-end to tackle this task. We evaluated the Learnable STRFs (64 filters) with a contraction layer (CL) as well the Free 2D convolution with a contraction layer (CL). The contraction layer is a convolution layer taking the outputs at each time step of the Learnable STRFs to reduce the number of dimensions of Z. We compared these techniques with classic signal processing baselines used in speech processing: Melfilterbanks (64 filters) and MFCC (19 coefficients, with their deltas and their delta-deltas).We also compared with the more recent parametrized neural network SincNet. SincNet is composed of parametrized sinc functions, which implement 80 band-pass filters (to replace directly more classic input spectral representations), and 3 temporal convolution/pooling layers. All the input front-end are then fed to a stack of two layers of BiLSTM layers of dimension 128 and two forward layers of dimension 32 before a final decision layer. The learning rate is controlled by a cyclical scheduler, each cycle lasting for 21 epochs. Data augmentation is performed directly on the waveform using additive noise based on the MUSAN database[START_REF] Snyder | Musan: A music, speech, and noise corpus[END_REF] with a random target signal-to-noise ratio ranging from 5 to 20 dB. To evaluate Speech Activity detection, we used the Detection Error Rate (DetER): Detection Error Rate = T false alarm + T missed detection T total speech

  (2020) to conduct experiments with the two version of the VoxCeleb databases: VoxCeleb2[START_REF] Chung | Voxceleb2: Deep speaker recognition[END_REF] is used for training, and VoxCeleb1[START_REF] Nagrani | Voxceleb: a large-scale speaker identification dataset[END_REF] is split into two parts for a development and test sets.We compared two different input front-end for the speaker verification task. We compared the Learnable STRFs (64 filters) with a contraction layer (CL) and the SincNet front-end, as described in the Speech Activity Detection setup. Each model is trained with the Additive Angular Margin Loss (α = 10, m = 0.05) with stochastic gradient descent with a learning rate of 0.01. We compared the different Speaker Verification approaches with the Equal

Finches' calls from

  11 categories ('Wsst or aggressive call','Begging calls', 'Distance call', 'Distress call','Long Tonal call', 'Nest call', 'Song','Tet call', 'Thuk call','Tuck call', 'Whine call') produced by Adults and Chicks. The calls were segmented to keep only the 3 first seconds of each excerpt and if the file is too short, the sound was zero-padded. Each set of features and model was evaluated with a random cross-validation procedure, that took into account the nested format the database. 80% of the birds were kept for training and 20% for testing. 50 different permutations of excluded birds were obtained to generate 50 training and validation data sets. To compare the approaches, we computed the Mean, Min, Max of the Accuracy over the permutations. We ran 4 different baselines for this task based on 2 different input features and 2 types of classifiers. We extracted the features introduced by Elie and Theunissen (2016): Predefined Acoustical Features (PAF) and the Modulation Power Spectrum (MPS). The PAF features are composed of 23 parameters extracted from Spectral envelope, Temporal Envelope and the Fundamental Frequency. (Mean, Min, Max, Std of the F0; Mean of F1; Mean of F2; Mean of F3; Saliency; RMS energy; Max of the Amplitude; Mean, Std, Skewness, Kurtosis, Entropy, first, second and third quartiles of the frequency power spectrum; Mean, Std, Skewness, Kurtosis, Entropy of the temporal envelope) The MPS representation is the amplitude spectrum of the 2D Fourier Transform applied on the spectrum representation of the sound waveform. The MPS extracts the spectro-temporal modulations in a fine-grained fashion and sum the contribution along the frequency axis. We tested both these input features with Linear Discriminant Analysis (LDA) and Random Forest (RF) classifiers as in Elie and

  FIG. 3. Temporal and Spectral Modulation of the Learned STRFs to tackle Speech Activity

  [START_REF] Hullett | Human superior temporal gyrus organization of spectrotemporal modulation tuning derived from speech stimuli[END_REF];[START_REF] Massoudi | Spectrotemporal response properties of core auditory cortex neurons in awake monkey[END_REF] measured responses of natural sounds directly in the superior temporal gyrus and found specific spectral modulation selectivity for 0.4 ± 0.55 Cycle/Octave and specific temporal modulation 16 ± 11Hz; and most of the modulations were concentrated along the axes with high separability.Finally, we examined the structure obtained from the hierarchical clustering based on the distances between tasks, see Sub-section II A 4 for the full description. We obtained the clustering tree in Figure5. We observed that the learned STRFs of the different tasks organized in a meaningful disposition. The Learned STRFs for Speech on the CHIME5 and AMI are the closest to each other. Then, we found out that other Human vocalization task, Speaker, is closer to the Speech ones. On the other hand, the Bird task organized far away from both the Urban and the Human vocalizations tasks (Speech and Speaker ). In future work, this method could be used to discover automatically phylogeny trees based only on acoustic properties of spectro-temporal modulations and test these predictions against a molecular-based phylogeny[START_REF] Mccracken | Avian vocalizations and phylogenetic signal[END_REF].

  modulations, and the recipes to replicate results are available in a open-source package 1 . Several avenues of extensions are possible for this work, based on what is known in auditory neuroscience. First, this work only modelled the final outcome of plasticity after each task has been fully learned, starting from a random initialization. Yet, the same model could be used to address a range of issues relevant to changes occurring during task learning (top-down plasticity) or due to modification of the distribution of audio input (bottom-up plasticity). Recent work

  FIG.6. Gaussian envelopes (σ t , σ f ) of the Learned STRFs to tackle Speech Activity Detection

TABLE I .

 I Speech Activity Detection results for the different approaches described. Init. stands for Initialisation. CL stands for contraction layer, it is a convolution (conv.) layer reducing the size of the tensor dimension after the convolution (Free 2D conv. or Learnable STRFs) on the Mel-filterbanks. The Free 2D conv. had the same grid size as the Learnable STRFs (9x111). Each input front-end is then fed to a 2-layer BiLSTM and 2 feed-forward layers. The best scores for each metric overall are in bold. MD stands for Missed detection rate. FA stands for False Alarm rate. DetER stands for Detection Error Rate. For all metrics, lower is better.

	Database	AMI	CHIME5
	Metric	DetER MD FA DetER MD FA
	Input front-end
	Mel-filterbanks	7.7 2.6 5.1	24.1 2.8 21.3
	MFCC	6.3 2.7 3.5	19.6 1.6 18.0
	SincNet (Ravanelli and Bengio, 2018) 6.0 2.4 3.6	19.2 1.7 17.6
	Free 2D conv. Random Init. + CL	8.0 3.0 5.0	26.5 0.6 25.9
	Free 2D conv. Gabor Init. + CL	7.9 2.5 5.3	26.4 0.2 26.1
	Learnable STRFs + CL	5.8 2.4 3.4	19.2 3.1 16.1

TABLE II .

 II Speaker Verification results for the different approaches described. CL stands for contraction layer, it is a convolution layer reducing the size of the tensor dimension after the convolution (Learnable STRFs). The X-vector[START_REF] Snyder | X-vectors: Robust dnn embeddings for speaker recognition[END_REF] is used after each input frontend. We evaluated the performance of the Speaker Verification with and without S-normalization[START_REF] Coria | A Comparison of Metric Learning Loss Functions for End-To-End Speaker Verification[END_REF]. We also reported the baseline performance of the I-vector combined with Probabilistic Linear Discriminant Analysis (PLDA)[START_REF] Dehak | Front-end factor analysis for speaker verification[END_REF]. The best scores for each metric overall are in bold. For the EER, lower is better.

	Metric	EER EER w/ S-norm
	Baseline
	I-vectors+PLDA (Dehak et al., 2010) a 8.8	-
	Input front-end

TABLE III .

 III Urban Sound Classification results for the different approaches described. The best score for the mean Accuracy over the 10 folds overall is in bold. the CNN10 architecture from[START_REF] Kong | Panns: Large-scale pretrained audio neural networks for audio pattern recognition[END_REF] is used after each input front-end. Higher is better.

	Accuracy	Mean [Min -Max]
	Baseline
	SB-CNN (Salamon and Bello, 2017) a 79 % [71%-85%]
	Input front-end
	Free 2D conv. 3by3 (Kong et al., 2020) 84% [76%-93%]
	Learnable STRFs	82% [74%-90%]

TABLE IV .

 IV Zebra Finch Call Type classification results for the different approaches. The best scores for each metric overall are in bold. PAF stands for Predefined Acoustical Features and MPS for the Modulation Power Spectrum. LDA stands for Linear Discriminant Analysis. RF stands for Random Forest. The Learnable STRFs input front-end is combined with a simple linear model to output directly the decisions. Higher is better.

	Accuracy	Mean [Min -Max]
	Chance level	17% [6%-23%]
	Features + Model
	PAF Elie and Theunissen (2016) + LDA 57% [43%-71%]
	PAF Elie and Theunissen (2016) + RF	59% [47%-68%]
	MPS Elie and Theunissen (2016) + LDA 41% [23%-53%]
	MPS Elie and Theunissen (2016) + RF 69% [49%-84%]
	Input front-end
	Learnable STRFs	43% [23 %-73%]

  We displayed the median value for each α and task above each box-plot.

	separability		asymmetry	lowfreq	starriness
	Speech AMI
	Speech CHIME5
	Speaker
	Urban
	Bird
	0.6	0.7	0.8	0.9	0.4 0.2 0.0 0.2 0.4	0.2 0.4 0.6 0.8	0.6 0.7 0.8 0.9 1.0
	FIG. 4. Separability, asymmetry, low-pass, starriness coefficients. Four quantifiers that measured
	different aspects learned distribution for the different tasks under study: Speech Activity Detection
	on the CHIME5 dataset (Speech CHIME5) and on the AMI (Speech AMI), Urban Sound Classi-
	fication on Urban8k (Urban), Speaker Verification on VoxCeleb (Speaker) Zebra Finch Call Type
	Classification (Bird).

https://github.com/bootphon/learnable-strf

ACKNOWLEDGMENTS This work is funded in part from the Agence Nationale pour la Recherche (ANR-17-EURE-0017 Frontcog, ANR-10-IDEX-0001-02 PSL*, ANR-19-P3IA-0001 PRAIRIE 3IA Institute). ACBL was funded through Neuratris, and ED in his EHESS role by Facebook AI Research (Research Gift) and CIFAR (Learning in Minds and Brains). The university (EHESS, CNRS, INRIA, ENS Paris-Sciences Lettres) obtained the datasets reported in this paper, and the experiment were run on it's computer resources.


Itaï Ben Yaacov

José Iovino
email: iovino@math.utsa.edu

MODEL THEORETIC FORCING IN ANALYSIS ITA Ï BEN YAACOV AND JOS É IOVINO

Model theoretic forcing in analysis

Introduction

In this paper we introduce a framework of model theoretic forcing for metric structures, i.e., structures based on metric spaces. We use the language of infinitary continuous logic, which we define below. This is a variant of finitary continuous logic which is exposed in [BU] or [START_REF] Ben Yaacov | Model theory for metric structures, Model theory with Applications to Algebra and Analysis[END_REF].

The model theoretic forcing framework introduced here is analogous to that developed by Keisler [Kei73] for structures of the form considered in first-order model theory.

The paper concludes with an application to separable quotients of Banach spaces. The long standing Separable Quotient Problem is whether for every nonseparable Banach space X there exists a operator T : X → Y such that T (X) is a separable, infinite dimensional Banach space. We prove the following result (Theorem 5.4): If X is an infinite dimensional Banach space and T : X → Y is a surjective operator with infinite dimensional kernel, then there exist Banach spaces X, Ŷ and a surjective operator T : X → Ŷ such that (i) X has density character ω 1 , (ii) The range of T is separable, (iii) (X, Y, T ) and ( X, Ŷ , T ) are elementarily equivalent as metric structures.

The paper is organized as follows. In Section 1 we introduce the syntax that will be used in the paper. In Section 2, we introduce model theoretic forcing for metric structures. Section 3 we focus our attention on two particular forcing properties. These properties are used in Section 4 to prove the general Omitting Types Theorem. The last section, Section 5, is devoted to the aforementioned application to separable quotients.

For the exposition of the material we focus on one-sorted languages. However, as the reader will notice, the results presented here hold true, mutatis mutandi, for multi-sorted contexts. In fact, the structures used in the last section are multi-sorted.

The authors are grateful to Yi Zhang for his encouragement and patience.

Preliminaries

Recall that if f : (X, d) → (X ′ , d ′ ) is a mapping between two metric spaces, then f is uniformly continuous if and only if there exists a mapping δ : (0, ∞) → (0, ∞] such that for all x, y ∈ X and ǫ > 0, d(x, y) < δ(ǫ) =⇒ d ′ (f (x), f (y)) ≤ ǫ.

(1)

If (1) holds, we say that δ is a uniform continuity modulus and that f respects δ. The choice of strict and weak inequalities here is so that the property of respecting δ be preserved under certain important constructions (e.g., completions and ultraproducts).

Let δ ′ : (0, ∞) → (0, ∞] be any mapping, and define:

δ(ǫ) = sup{δ ′ (ǫ ′ ) | 0 < ǫ ′ < ǫ}. (2)
Then δ and δ ′ are equivalent as uniform continuity moduli, in the sense that a function f respects δ if and only if it respects δ ′ . In addition we have

δ(ǫ) = sup{δ(ǫ ′ ) | 0 < ǫ ′ < ǫ}, (3)
i.e., δ is increasing and continuous on the left. As a consequence, (1) is equivalent to the apparently stronger version:

d(x, y) < δ(ǫ) =⇒ d ′ (f (x), f (y)) < ǫ. (4)
From this point on, when referring to a uniform continuity modulus δ, we mean one that satisfies (3).

In this section we introduce infinitary continuous formulas. For a general text regarding continuous structures and finitary continuous first order formulas we refer the reader to Sections 2 and 3 of [BU] or Sections 2-6 of [START_REF] Ben Yaacov | Model theory for metric structures, Model theory with Applications to Algebra and Analysis[END_REF].

Recall that a continuous signature L consists of the following data:

• For each n, a set of n-ary function and predicate symbols.

• A distinguished binary predicate symbol d.

• For each n-ary symbol s and i < n, a uniform continuity modulus for the ith argument denoted δ s,i . A continuous L-structure is a set M equipped with interpretations of the symbols of the language:

• Each n-ary function symbol is interpreted by an n-ary function:

f M : M n → M.
• Each n-ary predicate symbol is interpreted by a continuous n-ary predicate:

P M : M n → [0, 1].
• The interpretation d M of the distinguished symbol d is a complete metric.

• For each n-ary symbol s and i < n, the interpretation s M , viewed as a function of its ith argument, respects the uniform continuity modulus δ s,i .

It is proved in [BU] that the following system of connectives is full :

x → ¬x, x → x 2 , (x, y) → x -. y := max(x -y, 0)
This means that for every n ≥ 1, the family of functions from [0, 1] n → [0, 1] which can be written using these three operations is dense in the class of all continuous functions [0, 1] n → [0, 1]. For the purposes of this paper (namely, to simplify the treatment of forcing, in Section 2), it is convenient to use the connective ∔ instead of -. . Note that this causes no loss in expressive power, since x -. y = ¬(¬x ∔ y).

In this paper we extend the class of first-order continuous formulas by considering formulas that may contain the infinitary connectives and , where for a set of formulas Φ, ϕ∈Φ ϕ and ϕ∈Φ ϕ stand for sup{ϕ | ϕ ∈ Φ}ϕ and inf{ϕ | ϕ ∈ Φ}, respectively. Because of the infinitary nature of this language, in order to form formulas with these connectives, one needs to be particularly careful about the uniform continuity moduli of the terms and formulas with respect to each variable, denoted δ τ,x and δ ϕ,x , respectively; thus, we have the following definition.

Definition 1.1. Let L be a continuous signature. We define the formulas of L ω 1 ,ω . Simultaneously, for each variable x, each term τ and each formula ϕ of L ω 1 ,ω we define uniform continuity moduli δ τ,x and δ ϕ,x . Both definitions are inductive.

• A variable is a term, with δ x,x = id and δ x,y = ∞ for y = x.

• If f is an n-ary function symbol and τ 0 , . . . , τ n-1 are terms, then f τ 0 . . . τ n-1 is a term. If τ is a term of this form,

δ τ,x (ǫ) = sup ǫ 0 +...+ǫ n-1 <ǫ min{δ τ i ,x • δ f,i (ǫ i ) | i < n}.
Here we follow the convention that δ(∞) = ∞. • If P is an n-ary predicate symbol and τ 0 , . . . τ n-1 are terms, then P τ 0 . . . τ n-1 is a formula (called an atomic formula). The definition of δ P τ 0 ...τ n-1 ,x is formally identical that of δ f τ 0 ...τ n-1 ,x . • If ϕ and ψ are formulas then so are ¬ϕ, 1 2 ϕ and ϕ ∔ ψ. We have:

δ ¬ϕ,x (ǫ) = δ ϕ,x (ǫ) δ1 2 ϕ,x (ǫ) = δ ϕ,x (2ǫ) δ ϕ∔ψ,x (ǫ) = sup ǫ 0 +ǫ 1 <ǫ min{δ ϕ,x (ǫ 0 ), δ ψ,x (ǫ 1 )}.
• Let Φ be a countable set of formulas in a finite tuple of free variables x. For each variable

x, let δ ′ Φ,x = inf ϕ∈Φ δ ϕ,x : (0, ∞) → [0, ∞]. If δ ′ Φ,x (
ǫ) > 0 for all ǫ > 0 and x ∈ x, then Φ is a formula, also denoted ϕ∈Φ ϕ. Its uniform continuity moduli are given by δ Φ,x (ǫ) = sup{δ ′ Φ,x (ǫ ′ ) : 0 < ǫ ′ < ǫ}, so that (3) is satisfied.

• If ϕ is a formula and x a variable, then inf x ϕ is a formula. For y = x we have δ infx ϕ,y = δ ϕ,y , while δ infx ϕ,x = ∞.

Notation 1.2. Rather than putting and sup in our language we define them as abbreviations:

Φ := ¬ ϕ∈Φ ¬ϕ sup x ϕ := ¬ inf x ¬ϕ.
If M is an L-structure and ϕ(x 0 , . . . , x n-1 ) ∈ L ω 1 ,ω , one constructs the interpretation ϕ M : M n → [0, 1] in the obvious manner. By induction on the structure of ϕ one also shows that for each variable x, ϕ M is uniformly continuous in x respecting δ ϕ,x .

Finitary continuous first order formulas, as defined in [BU] and [START_REF] Ben Yaacov | Model theory for metric structures, Model theory with Applications to Algebra and Analysis[END_REF], are constructed in the same manner, with the exclusion of the infinitary connectives and (i.e., only using the connectives ¬, 1 2 , ∔, or equivalently ¬, 1 2 , -. ). We observe that ϕ ∧ ψ is equivalent to ϕ -. (ϕ -. ψ), so finitary instances of and are allowed there as well. The set of all such formulas is denoted L ω,ω .

Definition 1.3. Let L be a continuous signature and let ϕ be an L ω 1 ,ω -formula. The set of subformulas of ϕ denoted sub(ϕ), is defined inductively as follows.

• If P is a predicate symbol and τ 0 , . . . τ n-1 are terms, then sub(P τ 0 . . . τ n-1 ) = {P τ 0 . . . τ n-1 }. • sub(¬ϕ) = {¬ϕ} ∪ sub(ϕ) and sub(

1 2 ϕ) = { 1 2 ϕ} ∪ sub(ϕ). • sub(ϕ ∔ ψ) = { ϕ ∔ ψ } ∪ sub(ϕ) ∪ sub(ψ). • sub( ϕ∈Φ ϕ) = { ϕ∈Φ ϕ } ∪ ϕ∈Φ sub(ϕ). • sub(inf x ϕ) = { inf x ϕ } ∪ sub(ϕ). L ω 1 ,ω need not be countable if L is countable. Nevertheless, it is often sufficient to work with countable fragments of L ω 1 ,ω : Definition 1.4. A fragment of L ω 1 ,ω is subset of L ω 1 ,ω
which contains all atomic formulas and is closed under subformulas and substitution of terms for free variables.

Remark 1.5. Every countable subset of L ω 1 ,ω is contained in a countable fragment of L ω 1 ,ω .
For the next three sections (that is, the rest of the paper minus the last section), L will denote a fixed countable continuous signature, and L A will denote a fixed countable fragment of L ω 1 ,ω . We will let C = {c i | i < ω} be a set of new constant symbols, and

L(C) = L ∪ C. An L(C)-structure M will be called canonical if the set {c M i | i < ω} is dense in M.
By L A (C) we will denote the smallest countable fragment of L ω 1 ,ω (C) that contains L A ; notice that L A (C) is obtained allowing closing L A under substitution of constant symbols from C for free variables.

We will also use the following notation:

• The set of all sentences in L A (C) will be denoted L s A (C). • The set of all atomic sentences in L A (C) will be denoted L as A (C). • The set of variable-free terms in L(C) will be denoted T(C).

Forcing

Definition 2.1. A forcing property for L A is a triplet (P, ≤, f ) where (P, ≤) is a partially ordered set. The elements of P are called conditions. For each condition p, f assigns a mapping f p : L as A (C) → [0, 1] satisfying the following conditions. (i) p ≤ q implies f p ≤ f q i.e., f p (ϕ) ≤ f q (ϕ) for all ϕ ∈ L as A (C). (ii) Given p ∈ P, ǫ > 0, τ, σ ∈ T(C), and an atomic L(C)-formula ϕ(x) there are q ≤ p and c ∈ C such that:

f q (d(τ, c)) < ǫ, f q (d(τ, σ)) < f p (d(σ, τ )) + ǫ,
and if f p (d(τ, σ)) < δ ϕ,x (ǫ), f q (ϕ(σ)) < f p (ϕ(τ )) + ǫ.
For the rest of this section, (P, ≤, f ) will denote a fixed forcing property.

Definition 2.2. Let p ∈ P be a condition and ϕ ∈ L s A (C) a sentence. We define F p (ϕ) ∈ [0, 1] by induction on ϕ. For ϕ atomic,

F p (ϕ) = f p (ϕ). Otherwise, F p (¬ϕ) = ¬ inf q≤p F q (ϕ) F p ( 1 2 ϕ) = 1 2 F p (ϕ) F p (ϕ ∔ ψ) = F p (ϕ) ∔ F p (ψ) F p ( Φ) = inf ϕ∈Φ F p (ϕ) F p (inf x ϕ(x)) = inf c∈C F p (ϕ(c)).
If r ∈ R and F p (ϕ) < r we say that p forces that ϕ < r, in symbols p ϕ < r.

Remark 2.3. Let p ∈ P be a condition, ϕ ∈ L s A (C) a sentence, and r ∈ R. Then,

p ϕ < r ⇐⇒ f p (ϕ) < r, if ϕ is atomic p 1 2 ϕ < r ⇐⇒ p ϕ < 2r p ¬ϕ < r ⇐⇒ (∃s > 1 -r)(∀q ≤ p)(q ϕ < s) p (ϕ ∔ ψ) < r ⇐⇒ (∃s)(p ϕ < s and p ψ < r -s) p Φ < r ⇐⇒ (∃ϕ ∈ Φ)(p ϕ < r) p inf x ϕ(x) < r ⇐⇒ (∃c ∈ C)(p ϕ(c) < r).
Remark 2.4. The forcing relation can be defined inductively, without reference to the function F p (ϕ), by the list of equivalences in the preceding remark. One can then define

F p (ϕ) as inf{ r ∈ R | p ϕ < r }.
The following basic properties will be used many times.

Lemma 2.5. For all p, ϕ,

(i) F p (ϕ) ∈ [0, 1]. (ii) q ≤ p =⇒ F q (ϕ) ≤ F p (ϕ). (iii) F p (ϕ) + F p (¬ϕ) ≥ 1.
Proof. The first two items are by induction on the structure of ϕ. The last one follows directly from the definition.

2.5

Definition 2.6. We also define F w p by:

F w p (ϕ) = sup q≤p inf q ′ ≤q F q ′ (ϕ).
If r ∈ R and F w p (ϕ) < r we say that p weakly forces that ϕ < r, in symbols p w ϕ < r. By Lemma 2.5, F w p (ϕ) ≤ F p (ϕ). Remark 2.7. The weak forcing relation w can be defined without reference to the function F w p as follows: p w ϕ < r if and only if (∃s < r)(∀q ≤ p)(∃q ′ ≤ q)(q ′ ϕ < s). We can then define F w p (ϕ) as inf{ r | p w ϕ < r }.

Lemma 2.8.

Let p ∈ P, ϕ ∈ L s A (C) and r ∈ R. Then F w p (ϕ) = sup q≤p F w q (ϕ) = sup q≤p inf q ′ ≤q F w q ′ (ϕ).
Proof. That F w p (ϕ) = sup q≤p F w q (ϕ) follows easily from the definitions, and

sup q≤p F w q (ϕ) ≥ sup q≤p inf q ′ ≤q F w q ′ (ϕ) is immediate. Finally: sup q≤p inf q ′ ≤q F w q ′ (ϕ) = sup q≤p inf q ′ ≤q sup q ′′ ≤q ′ inf q ′′′ ≤q ′′ F q ′′′ (ϕ) ≥ sup q≤p inf q ′ ≤q inf q ′′′ ≤q ′ F q ′′′ (ϕ) = sup q≤p inf q ′ ≤q F q ′ (ϕ) = F w p (ϕ).

2.8

Proposition 2.9. The weak forcing function F w obeys the following inductive rules:

F w p (¬ϕ) = ¬ inf q≤p F w q (ϕ) F w p ( 1 2 ϕ) = 1 2 F w p (ϕ) F w p (ϕ ∔ ψ) = sup q≤p inf q ′ ≤q F w q ′ (ϕ) ∔ F w q ′ (ψ) F w p ( Φ) = sup q≤p inf q ′ ≤q inf ϕ∈Φ F w q ′ (ϕ) F w p (inf x ϕ(x)) = sup q≤p inf q ′ ≤q inf c∈C F w q ′ (ϕ(c)).
Proof. For ¬ϕ and 1 2 ϕ this follows from a straightforward calculation. For example:

F w p (¬ϕ) = sup q≤p inf q ′ ≤q F q ′ (¬ϕ) = sup q≤p inf q ′ ≤q ¬ inf q ′′ ≤q ′ F q ′ (ϕ) = ¬ inf q≤p sup q ′ ≤q inf q ′′ ≤q ′ F q ′ (ϕ) = ¬ inf q≤p F w q (ϕ),
For the other three, the inequality ≥ is obtained substituting the definition of F w p on the left hand side and using the fact that F p ≥ F w p . For ≤, we first use Lemma 2.8 to replace each occurrence of F w p on the left hand side with sup q<p inf q ′ ≤q F w q ′ . Thus, it will suffice to show that:

F w p (ϕ ∔ ψ) ≤ F w p (ϕ) ∔ F w p (ψ) F w p ( Φ) ≤ inf ϕ∈Φ F w p (ϕ) F w p (inf x ϕ(x)) ≤ inf c∈C F w p (ϕ(c)). For ∔ assume F w p (ϕ) = r and F w p (ψ) = s.
Then for all ǫ > 0 and for all q ≤ p there is q ′ 0 ≤ q such that F q ′ 0 (ϕ) < r + ǫ, and as q ′ 0 ≤ p there is q ′ ≤ q ′ 0 such that F q ′ (ψ) < s + ǫ. Then F q ′ (ϕ ∔ ψ) < r + s + 2ǫ, yielding F w q ′ (ϕ ∔ ψ) ≤ r + s. For Φ and inf x ϕ(x) it's a straightforward quantifier exchange argument, e.g.:

F w p ( Φ) = sup q≤p inf q ′ ≤q inf ϕ∈Φ F p (ϕ) ≤ inf ϕ∈Φ sup q≤p inf q ′ ≤q F p (ϕ) = inf ϕ∈Φ F w (ϕ).
2.9

Lemma 2.10. For all p ∈ P and τ : F w p (inf x d(τ, x)) = 0. Proof. If not then F w p (inf x d(τ, x)) = sup q≤p inf q ′ ≤q inf c∈C f p (d(τ, x)) > 0. But this contradicts the definition of forcing property.

2.10

Definition 2.11. A nonempty G ⊆ P is generic if:

(i) It is directed downwards, i.e., for all p, q ∈ G there is p ′ ∈ G such that p ′ ≤ p, q.

(ii) It is closed upwards, i.e., if p ∈ G and q ≥ p then q ∈ G.

(iii) For every ϕ ∈ L s A (C) and r > 1 there is p ∈ G such that

F p (ϕ) + F p (¬ϕ) < r. If G is a generic set and ϕ ∈ L s A (C) we define ϕ G = inf p∈G F p (ϕ).
Proposition 2.12. Every condition belongs to a generic set.

Proof. Fix p ∈ P. Let ( (r n , ϕ n ) : n < ω ) enumerate all pairs (r, ϕ), where r ∈ Q, r > 1, and ϕ ∈ L s A (C). Construct a sequence p 0 ≥ p 1 ≥ . . . ≥ p n ≥ . . . in P as follows. We start with p 0 = p. Assume p n has already been chosen. By definition

F pn (¬ϕ n ) + inf q≤pn F q (ϕ n ) = 1 < r n , so we can choose p n+1 ≤ p n such that F pn (¬ϕ n )+F p n+1 (ϕ n ) < r n , whereby F p n+1 (¬ϕ n ) + F p n+1 (ϕ n ) < r n . Define G = { q ∈ P | q ≥ p n for some n }.
Then G is generic, and p ∈ G.

2.12

Lemma 2.13. Let G be generic and ϕ ∈ L s A (C). Then ϕ G = inf p∈G F w p (ϕ).

Proof. The inequality ≥ is immediate since F w p (ϕ) ≤ F p (ϕ). For the other, assume ϕ G > inf p∈G F w p (ϕ), so there are ǫ > 0 and p ∈ G such that ϕ G -ǫ > F w p (ϕ). As G is generic there is q ∈ G such that F q (ϕ) + F q (¬ϕ) < 1 + ǫ, and as p ∈ G we may assume q ≤ p. We obtain

F w p (ϕ) ≥ inf q ′ ≤q F q ′ (ϕ) = 1 -F q (¬ϕ) > F q (ϕ) -ǫ ≥ ϕ G -ǫ > F w p (ϕ),
a contradiction.

2.13

Lemma 2.14.

If G is generic and ϕ ∈ L s A (C), then (¬ϕ) G = 1 -ϕ G . Proof. From Lemma 2.5 we have ϕ G + (¬ϕ) G ≥ 1, while ϕ G + (¬ϕ) G ≤ 1 follows from Definition 2.11.

2.14

Lemma 2.15. Let G be a generic set and τ, σ ∈ T(C). Then:

(i) For every ǫ > 0 there is c τ,ǫ,G ∈ C such that d(τ, c τ,ǫ,G ) G < ǫ. (ii) d(τ, σ) G = d(σ, τ ) G . (iii) For every atomic L(C)-formula ϕ(x), if d(τ, σ) G < δ ϕ,x (ǫ) then |ϕ(τ ) G -ϕ(σ) G | < ǫ.
Proof. For (i), observe that (inf x d(τ, x)) G = 0 by Lemma 2.10 and Lemma 2.13, so there is p ∈ G such that F p (inf x d(τ, x)) < ǫ, and thus there exists c ∈ C such that d(τ, c) G ≤ F p (d(τ, c)) < ǫ. The other two statements follow directly from Lemma 2.13 and the definition of forcing property.

2.15

Lemma 2.16. Let M G 0 be the term algebra T(C) equipped with the natural interpretation of the function symbols, and interpreting the predicate symbols by: P M G 0 (τ ) = P (τ ) G . Then M G 0 is a pre-L(C)-structure, and its completion M G is a canonical structure. Proof. First we use Lemma 2.15 to show that d M G 0 is a pseudometric. Symmetry is Lemma 2.15(ii). The triangle inequality follows from Lemma 2.15(iii), keeping in mind that δ d(x,σ),x = id. That d M G 0 (τ, τ ) = 0 follows from the triangle inequality and Lemma 2.15(i). Finally, by Lemma 2.15(iii), every symbol respects its uniform continuity modulus. Thus M G 0 is a pre-structure, and we can define M G to be its completion. That C M G is dense in M G now follows from Lemma 2.15(i).

2.16

Theorem 2.17. For all ϕ ∈ L s A (C) we have ϕ M G = ϕ G . Proof. By induction on ϕ:

(i) For ϕ atomic, this is immediate from the construction of M G . (ii) For 1 2 ϕ, ϕ ∔ ψ and Φ, this is immediate from the definition of forcing and the induction hypothesis. (iii) For ¬ϕ, this is immediate from Lemma 2.14 and the induction hypothesis. (iv) For inf x ϕ(x), it follows from the definition of forcing and the induction hypothesis that (inf

x ϕ) G = inf{ϕ(c) M G | c ∈ C}. Since C M G is dense in M G and ϕ(x) M G is uniformly continuous in x, the latter is equal to (inf x ϕ) M G .
2.17

The forcing Properties P(M) and P(M, Σ)

If M is class of L-structures, we denote by M(C) the class of all structures of the form (M, a c ) c∈C 0 , where M is in M and C 0 is a finite subset of C; such a structure is regarded naturally as an L(C 0 )-structure by letting a c be the interpretation of c in M, for each c ∈ C 0 .

Let Σ be a class of formulas of L A that contains all the atomic formulas and is closed under subformulas, and let Σ(C) denote the subset of L(C) obtained from formulas ϕ in Σ by replacing finitely many free variables of ϕ with constant symbols from C.

The forcing property P(M, Σ) is defined as follows. The conditions of P(M, Σ) are the finite sets of the form { ϕ 1 < r 1 , . . . , ϕ n < r n }, where ϕ 1 , . . . , ϕ n ∈ Σ(C) and there exist M ∈ M(C) such that ϕ M i < r i , for i = 1, . . . , n. The partial order ≤ on conditions is reverse inclusion, i.e., if p, q are conditions of P(M, Σ), then p ≤ q if and only p ⊇ q. If p is a condition of P(M ∆ , Σ) and ϕ is an atomic sentence of L(C), we define

f p (ϕ) = min{r ≤ 1 | ϕ < r ∈ p}, if {r ≤ 1 | ϕ < r ∈ p} = ∅, 1, otherwise.
When Σ is the set of all atomic L-formulas, the forcing property P(M, Σ) is denoted simply P(M).

The main result of this section is Proposition 3.4, below, which characterizes weak forcing for the forcing property P(M, Σ); for the proof, we need two lemmas. Definition 3.1. We extend the definition of f p above to all sentences of Σ(C):

H p (ϕ) = min{r ≤ 1 | ϕ < r ∈ p}, if {r ≤ 1 | ϕ < r ∈ p} = ∅, 1, otherwise.
We define H w p accordingly: H w p (ϕ) = sup q≤p inf p≤q H p (ϕ). Clearly if q ≤ p then H q (ϕ) ≤ H p (ϕ) and H w q (ϕ) ≤ H w p (ϕ), whereby for all p: H w p (ϕ) ≤ H p (ϕ). Lemma 3.2. For all p ∈ P(M, Σ) and ϕ ∈ Σ(C):

H w p (ϕ) = inf{r ∈ [0, 1] | (∀q ≤ p)(q ∪ {ϕ < r} ∈ P(M, Σ))} = sup{r ∈ [0, 1] | p ∪ {¬ϕ < 1 -r} ∈ P(M, Σ)} (Here inf ∅ = 1, sup ∅ = 0.)
Proof. The first equality is a mere rephrasing: H w p (ϕ) ≤ r if and only if inf q ′ ≤q H p (ϕ) ≤ r for all q ≤ p, i.e., if and only if q ∪ {ϕ < r} ∈ P(M, Σ) for all q ≤ p.

For the second equality: Assume first that q = p ∪ {¬ϕ < 1 -r} ∈ P(M, Σ). Then q ≤ p but q∪{ϕ < r} / ∈ P(M, Σ). This gives ≥. Now assume p∪{¬ϕ < 1-r} / ∈ P(M, Σ).

Then p ∪ {¬ϕ < 1 -r} cannot be realized in the given class. Thus, for every q ≤ p, as q can be realized, it is realized in a model where ϕ ≤ r. Thus q ∪ {ϕ < s} ∈ P(M, Σ) for all q ≤ p and s > r. This gives ≤.

3.2

Proposition 3.3. The functions H w p satisfy the properties stated for F w p in Lemma 2.8 and Proposition 2.9, i.e.:

H w p (ϕ) = sup q≤p H w q (ϕ) = sup q≤p inf q ′ ≤q H w q ′ (ϕ) H w p (¬ϕ) = ¬ inf q≤p H w q (ϕ) H w p ( 1 2 ϕ) = 1 2 H w p (ϕ) H w p (ϕ ∔ ψ) = sup q≤p inf q ′ ≤q H w q ′ (ϕ) ∔ H w q ′ (ψ) H w p ( Φ) = sup q≤p inf q ′ ≤q inf ϕ∈Φ H w q ′ (ϕ) H w p (inf x ϕ(x)) = sup q≤p inf q ′ ≤q inf c∈C H w q ′ (ϕ(c)). Proof.
The first property is proved precisely as in Lemma 2.8.

For ¬: it follows from Lemma 3.2 that H w p (¬ϕ) = ¬ inf q≤p H q (ϕ), and we conclude as in the proof of Proposition 2.9.

For 1 2 : observe that q ∪ {ϕ < r} ∈ P(M, Σ) if and only if q ∪ { 1 2 ϕ < 1 2 r} ∈ P(M, Σ) and apply Lemma 3.2.

For the last three we reduce as in the proof of Proposition 2.9 to showing that:

H w p (ϕ ∔ ψ) ≤ H w p (ϕ) ∔ H w p (ψ) H w p ( Φ) ≤ inf ϕ∈Φ H w p (ϕ) H w p (inf x ϕ(x)) ≤ inf c∈C H w p (ϕ(c)
). For ∔ this follows from Lemma 3.2. For and inf the quantifier exchange argument from proof of the corresponding items in Proposition 2.9 works here too.

3.3

Proposition 3.4. Suppose that p is a condition in the forcing property P(M, Σ) and σ is a sentence of Σ(C). Then F w p (σ) = H w p (σ). Proof. For atomic σ the equality is immediate. We then proceed by induction on σ, noting that Proposition 2.9 on the one hand and Proposition 3.3 on the other tell us that F w p and H w p obey the same inductive definitions.

3.4

Generic Models and sup inf-Formulas

Recall from Section 1 that the expressions Φ and sup x ϕ are regarded abbreviations of ¬ ϕ∈Φ ¬ϕ and ¬ inf x ¬ϕ respectively. Proposition 4.1. Let (P, ≤, f ) be a forcing property for L A (C) and let p ∈ P. Then

(i) F p ( Φ) = sup ϕ∈Φ F w p (ϕ). (ii) F p (sup x ϕ(x)) = sup c∈C F w p (ϕ(c)).
Proof. The proofs are straightforward applications of the definitions: for (i),

F p ( Φ) = F p (¬ ϕ∈Φ ¬ϕ) = ¬ inf q≤p F q ( ϕ∈Φ ¬ϕ) = ¬ inf q≤p inf ϕ∈Φ F q (¬ϕ) = ¬ inf q≤p inf ϕ∈Φ ¬ inf q ′ ≤q F q ′ (ϕ) = sup q≤p sup ϕ∈Φ inf q ′ ≤q F q ′ (ϕ) = sup ϕ∈Φ sup q≤p inf q ′ ≤q F q ′ (ϕ) = sup ϕ∈Φ F w p (ϕ),
and for (ii),

F p (sup x ϕ(x)) = F p (¬ inf x ¬ϕ(x)) = ¬ inf q≤p F q (inf x ¬ϕ(x)) = ¬ inf q≤p inf c∈C F q (¬ϕ(c)) = ¬ inf q≤p inf c∈C ¬ inf q ′ ≤q F q ′ (ϕ(c)) = sup q≤p sup c∈C inf q ′ ≤q F q ′ (ϕ(c)) = sup c∈C sup q≤p inf q ′ ≤q F q ′ (ϕ(c)) = sup c∈C F w q ′ (ϕ(c)).

4.1

Notation 4.2. If Φ is a finite set of formulas, say Φ = {ϕ 1 , . . . , ϕ n }, we write

ϕ 1 ∧ • • • ∧ ϕ n and ϕ 1 ∨ • • • ∨ ϕ n
as abbreviations of Φ and Φ, respectively.

Proposition 4.3. If (P, ≤, f ) is a forcing property for L A (C) and p ∈ P, then

F p (ϕ 1 ∨ • • • ∨ ϕ n ) = max i F w p (ϕ i ).
Proof. By Proposition 4.1.

4.3

Definition 4.4. Let Σ be a class of formulas of L A which contains all atomic formulas and is closed under subformulas. A sup inf-formula over Σ is an L A -formula of the form sup

x 1 . . . sup xm n<ω inf y 1 . . . inf y i(n) (σ n,1 (x, ȳn ) ∨ • • • ∨ σ n,j(n) (x, ȳn )),
where σ n,ν belongs to Σ for n < ω and ν = 1, . . . , j(n), x = x 1 , . . . , x m , and ȳn = y 1 , . . . , y i(n) .

Proposition 4.5. Let Σ be a class of formulas of L A which contains all atomic formulas and is closed under subformulas. Suppose that ϕ is a sup inf-formula over Σ, of the form

sup x 1 . . . sup xm n<ω inf y 1 . . . inf y i(n) (σ n,1 (x, ȳn ) ∨ • • • ∨ σ n,j(n) (x, ȳn )),
where σ n,ν belongs to Σ for n < ω and ν = 1, . . . , j(n), x = x 1 , . . . , x m , and ȳn = y 1 , . . . , y i(n) . Then, if (P, ≤, f ) is a forcing property for L A (C) and p ∈ P,

F p (ϕ) = sup c∈C m q≤p inf q ′ ≤q d∈C i(n) n<ω max 1≤ν≤j(n) F w q ′ ( σ n,ν (c, d) ).
Proof. We use Propositions 4.1 and 4.3 to compute F p (ϕ):

F p ( sup x 1 . . . sup xm n<ω inf y 1 . . . inf y i(n) (σ n,1 (x, ȳn ) ∨ • • • ∨ σ n,j(n) (x, ȳn ) )) = sup c∈C m F w p ( n<ω inf y 1 . . . inf y i(n) (σ n,1 (c, ȳn ) ∨ • • • ∨ σ n,j(n) (c, ȳn )) ) (by 4.1) = sup c∈C m sup q≤p inf q ′ ≤q F q ′ ( n<ω inf y 1 . . . inf y i(n) (σ n,1 (c, ȳn ) ∨ • • • ∨ σ n,j(n) (c, ȳn )) ) = sup c∈C m sup q≤p inf q ′ ≤q inf n<ω inf d∈C i(n) F q ′ ( σ n,1 (c, d) ∨ • • • ∨ σ n,j(n) (c, d) ) = sup c∈C m sup q≤p inf q ′ ≤q inf n<ω inf d∈C i(n) max 1≤ν≤j(n)
F w q ′ ( σ n,ν (c, d) ) (by 4.3).

4.5

Remark 4.6. If p is a condition in the forcing property P(M, Σ), then F w p (ϕ) = H w p (ϕ), by Proposition 3.4. Hence, if ϕ is as in Proposition 4.5,

F p (ϕ) = sup c∈C m q≤p inf q ′ ≤q d∈C i(n) n<ω max 1≤ν≤j(n) H w q ′ ( σ n,ν (c, d) ).
Recall (Section 1) that C denotes countable set of constants not in L and that L(C) = L∪C. As in Section 3, if M is a class of L-structures, M(C) denotes the class of structures of the form (M, a c ) c∈C 0 , where M is in M and C 0 is a finite subset of C. If Γ is a set of inequalities of the form ϕ < r, where ϕ is an L A (C)-formula and r is a real number, we will say that Γ is satisfiable in M if there exists a structure M in M(C) such that ϕ M < r for every inequality ϕ < r in Γ.

Let Σ be class of formulas of L A that contains all the atomic formulas and is closed under subformulas. A finite Σ-piece of M is a finite set p of inequalities of the form ϕ < r, where ϕ ∈ Σ, such that p that is satisfiable in M.

Corollary 4.7 (Omitting Types Theorem). Let ( ϕ n | n < ω ) be a sequence of Lformulas such that for each n < ω ϕ n is a sup inf-formula over Σ, of the form

sup x 1 . . . sup x m(n) ψ n (x 1 , . . . , x m(n) ),
where for each n < ω ψ n is of the form

k<ω inf y 1 . . . inf y i(n,k) (σ n,k,1 (x n , ȳn,k ) ∨ • • • ∨ σ n,k,j(n,k) (x n , ȳn,k )),
with xn = x 1 , . . . , x m(n) , and ȳn,k = y 1 , . . . , y i(n,k) , and let ( r n | n < ω ) be a sequence of real numbers such that for every finite Σ-piece p of M and every cn ∈ C m(n) , the set p ∪ {ψ n (c n ) < r n } is satisfiable in M. Then there exists a canonical L(C)-structure M such that ϕ M n ≤ r n for every n < ω. Proof. Let p be a condition in the forcing property P(M, Σ). Fix a condition q ≤ p, n < ω and cn

∈ C m(n) . Since q ∪ {ψ n (c n ) < r n } is satisfiable in M, there exist k < ω and dn,k ∈ C i(n,k) such that q ∪ { σ n,k,1 (c n , dn,k ) ∨ • • • ∨ σ n,k,j(n,k) (c n , dn,k ) < r n } is satisfiable in M. Let q ′ = q ∪ { σ n,k,1 (c n , dn,k ) < r n , . . . , σ n,k,j(n,k) (c n , dn,k ) < r n }.
Then, q is a condition in P(M, Σ), and by Lemma 3.2, max 1≤ν≤j(n,k)

H w q ′ ( σ n,k,ν (c n , dn,k ) ) < r n , so inf q ′ ≤q d∈C i(n,k) k<ω max 1≤ν≤j(n,k) H w q ′ ( σ n,k,ν (c n , dn,k ) ) < r n .
Thus, by Remark 4.6, F p (ϕ n ) ≤ r n . Let G be a generic set for P(M, Σ) (the existence of G is guaranteed by Proposition 2.12). For every n < ω, ϕ G n = inf p∈G F p (ϕ n ) ≤ r n (see Definition 2.11). Let now M G be as in Lemma 2.16. Then, by Theorem 2.17,

ϕ M G n = ϕ G n ≤ r n .

4.7

Remark 4.8. The reader may worry about the fact that the assumptions of Corollary 4.7 involve strict inequalities while the conclusion only yields a weak inequality. In fact it would be enough to assume a weak inequality, i.e., that p ∪ {ψ n (c n ) ≤ r n } is satisfiable in M for every p and ψ n as in the statement of Corollary 4.7, or more precisely, that p ∪ {ψ n (c n ) < r n + ǫ} is satisfiable for every ǫ > 0. Indeed, in this case we would be able to find M in which ϕ M n ≤ r n + 2 -m for all n, m, i.e., such that ϕ M n ≤ r n for all n.

Application: Separable Quotients

If ϕ is a formula of L ω 1 ,ω , we will say that ϕ is finitary if all the occurrences of in ϕ are finitary, i.e., if whenever ψ∈Φ ψ is a subformula of ϕ, the set Φ is finite. We recall from Section 1 that the set of all finitary formulas is denoted L ω,ω .

If M and N are L-structures, M and N are said to be elementary equivalent, written M ≡ N, if ϕ M = ϕ N for every finitary L-sentence ϕ. Thus M ≡ N if and only if ϕ M < r implies ϕ N < r for every finitary L-sentence ϕ and every rational number r. If M is a substructure of N, M is said to be an elementary substructure

of N if (M, a | a ∈ M) ≡ (N, a | a ∈ M).
A Banach space (X, • ) can be regarded as a metric structure in a number of ways. A natural approach is to introduce for each nonnegative rational r a distinct sort for the closed ball B X (r) of radius r around 0; the metric on B X (r) is given by the norm • ; in the structure we also include:

• the inclusion maps I r,s : B X (r) → B X (s) for r < s,

• the vector addition, which maps B X (r) × B X (s) onto B X (r + s),

• for each λ ∈ Q, the scalar multiplication by λ, which maps B X (r) onto B X (|λ|r),

• the normalized norm predicate • /r, which maps B X (r) onto the interval [0, 1],

• the normalized distance predicate on B X (r) defined by d(x, y) = x -y /(2r) (as x -y ∈ B X (2r)). Notice that with the normalized norm and distance, all symbols are 1-Lipschitz, meaning that the identity function δ(ǫ) = ǫ is a modulus of uniform continuity for each and every one of them.

Other ways of regarding Banach space as metric structures are discussed in Section 3 of [BU] and in Section 4 [Ben].

If X and Y are Banach spaces and T : X → Y is a Banach space operator, we denote by (X, Y, T ) the structure that includes, in addition to the Banach space structure of X and the Banach space structure on Y , in separate sorts, the operator T as a family of functions between the appropriate sorts, i.e., from B X (r) to B Y (s) if s ≥ T r. If T is nonzero, the function δ(ǫ) = ǫ/ T is a modulus of uniform continuity for T .

Proposition 5.1. Let X, Y, X, Ŷ be Banach spaces and let T : X → Y and T : X → Ŷ be bounded linear operators such that (X, Y, T ) ≡ ( X, Ŷ , T ). Then T is surjective if and only if T is surjective.

Proof. For a real number r ≥ 0, let B X (r) and B Y (r) denote the closed balls of radius r around 0 in X and Y , respectively. The proof of the Open Mapping Theorem shows that T : X → Y is surjective if and only if the following holds: for every ǫ > 0 there exists δ(ǫ) > 0 such that ∀y ∈ B Y (δ(ǫ)) ∃x ∈ B X (1) ( T (x) -y ≤ ǫ ).

We can assume that δ(ǫ) < 1 for ǫ < 1. Thus, T is surjective if and only if for every ǫ with 0 < ǫ < 1 we have ϕ (X,Y,T ) ǫ = 0, where ϕ ǫ is the following finitary sentence (the where for each n < ω, a n is the interpretation of c n , b n is the interpretation of d n , and a * 0 is the interpretation of c * 0 . By (i), we have ( X, Y, T ) ≺ ( X 1 , Y 1 , T 1 ), so, in particular, by Proposition 5.1, T 1 is surjective. Now we iterate the preceding process to find for each ordinal α with 0 < α < ω 1 a separable structure

( X α , Y α , T α , a n , b n , a * i | n < ω, i < α ) such that if 0 < α < β < ω 1 , • ( X α , Y α , T α , a n , b n , a * i | n < ω, i < α ) ≺ ( X β , Y β , T β , a n , b n , a * i | n < ω, i < α ) • a * i ∈ X α for i < α • a *
i = 1 and a * i -a * j = 1 for i < j < α • The linear span of {b n | n < ω} is a dense subset of T α (X α ). The theorem then follows by taking X = α<ω 1 X α , Ŷ = α<ω 1 Y α , and T = α<ω 1 T α .

5.4

First author partially supported by NSF grant DMS-0500172.

(Or, if one wishes to be pedantic, replace T (x) -y -. ǫ with 1 2 T (x) -y -. ǫ 2 .) Hence, if (X, Y, T ) ≡ ( X, Ŷ , T ) and T is surjective, T is surjective too.

5.1

The authors are grateful to William B. Johnson for pointing out that Proposition 5.1 is given by the proof of the Open Mapping Theorem.

All the Banach spaces mentioned henceforth will be infinite dimensional.

The Separable Quotient Problem is perhaps the most prominent open problem in nonseparable Banach space theory. The question is whether for every nonseparable Banach space X there exist a separable Banach space Y and a surjective operator T : X → Y . Let T : X → Y be a Banach space operator and consider the structure (X, Y, T ) (the sorts of this structure are X and Y ). In this section we use Corollary 4.7 to prove that if T : X → Y is surjective and has infinite dimensional kernel, then there exists an operator T : X → Ŷ such that (i) (X, Y, T ) ≡ ( X, Ŷ , T ), (ii) X has density character ω 1 , (iii) Ŷ is separable. It follows from (i) and Proposition 5.1 that T is surjective.

Lemma 5.2. Suppose that X is a Banach space and Y is a closed proper subspace of X. Then there exists a non-zero linear functional f : X → R whose restriction to Y is zero. Up to multiplication by a scalar we may further assume that f = 1.

Proof. This is a well-known application of the Hahn-Banach theorem; the proof can be found in a textbook, e.g., [FHH + 01].

5.2

Lemma 5.3. If X is a Banach space of density character κ, there exists a family (x i ) i<κ in X such that x i = 1 for every i < κ and x i -x j ≥ 1 for i < j < κ.

Proof. The construction of (x i ) i<κ is inductive. Fix j < κ and suppose that constructed x i is defined for i < j. Let Y be the closed linear span of {x i | i < j}, which is a proper closed subspace of X. By Lemma 5.2, take f : X → R such that f (x) = 0 for every x ∈ Y and f = 1. Let now x j be an element of the unit sphere of X such that |f (x)| = f = 1. Then, if y ∈ Y , we have x j -y ≥ |f (x j ) -f (y)| = 1; in particular, x j -x i ≥ 1 for i < j.

5.3

Theorem 5.4. For every surjective operator T : X → Y with infinite dimensional kernel there exists an operator T : X → Ŷ such that

• (X, Y, T ) ≡ ( X, Ŷ , T ),

• X has density character ω 1 ,

• Ŷ is separable.

Furthermore, if D is a given countable subset of X, the structure ( X, Ŷ , T ) can be chosen with the following property: there exists a separable subspace X 0 of X such that D ⊆ X 0 and if T 0 denotes the restriction of T to X 0 ,

• (X 0 , T 0 (X 0 ), T 0 ) ≺ (X, Y, T ),

• (X 0 , T 0 (X 0 ), T 0 ) ≺ ( X, Ŷ , T ).

Proof. By the Löwenheim-Skolem Theorem [HI02, page 47], there exists a separable subspace X 0 of X such that if T 0 denotes the restriction of T to X 0 and Y 0 = T 0 (X 0 ),

(Note that X 0 can be taken so that it contains any given countable subset of X.) Let A be a countable dense subset of X 0 and consider the structure

Let L be the signature that results from expanding the signature of ( X, Y, T, a | a ∈ A ) with new constant symbols c 0 , c 1 , . . . and c * 0 of sort B X (1) as well as new constant symbols d 0 , d 1 , . . . and of sort B Y (1).

Let us introduce some temporary terminology. If ϕ is an L-sentence, an L-structure M satisfies the inequality ϕ < r if ϕ M < r. An inequality ϕ < r will be called finitary if the formula ϕ is finitary.

Let Γ consist of the following inequalities (the variable x in (vii) is of sort B Y (1)): (i) All the finitary inequalities satisfied by the structure ( X 0 , Y 0 , T, a | a ∈ A ) (ii) ¬ c n < ǫ (i.e., c n > 1 -ǫ) and ¬ d n < ǫ, for every n < ω and every rational ǫ > 0. (iii) ¬ 1 2 c m -c n < 1 2 + ǫ (i.e., c n -c m > 1 -2ǫ) and ¬ 1 2 d m -d n < 1 2 + ǫ, for every pair m, n with m < n < ω and every rational ǫ > 0. (iv) ¬ c * 0 < ǫ, for every rational ǫ > 0. (v) ¬ 1 2 c * 0 -c n < 1 2 + ǫ, for every n < ω and every rational ǫ > 0. (vi) T (c ω ) < ǫ, for every rational ǫ > 0. (vii) For every rational ǫ > 0, the inequality

Here 1 n+1 • is just the normalized norm predicate on the sort of T (x)-i<n r i d i , and (n + 1) • ϕ is defined in general as ϕ ∔ • • • ∔ ϕ n + 1 times. Lemma 5.3 ensures that the hypotheses of Corollary 4.7 are satisfied with Σ = L ω,ω . Thus by Corollary 4.7, Γ has a separable model ( X 1 , Y 1 , T 1 , a, a n , b n , a * 0 | a ∈ A, n < ω ),