SearcharxivSearch

arXiv subjects

Sean Walsh

Publications and source records attributed to Sean Walsh.

18 recordsLinked to original sources

The generalized quantifiers of natural language are predicatively definable

This paper studies the definability of natural language generalized quantifiers. The semantics of generalized quantifiers are provided by a collection of subsets of the underlying domain. However, the generalized quantifiers appearing in natural language are definable either by first-order quantification or by cardinality notions. This paper provides an explanation for this observed phenomenon. The explanation is that the famous constraints of domain independence and conservativity, when extended to Henkin models, suffice to ensure low-level definability, namely $\Delta^1_1$-definability or at least $\Sigma^1_1$-definability; and in most cases this definability can be made to be bounded. This is basically a consequence of Feferman's Preservation Theorem, which Marker has provided a short model-theoretic proof of. Further, we verify that the paradigmatic cardinality quantifiers are indeed $\Delta^1_1$-definable for a reasonable choice of background theory. Finally, in many other cases, we show that this definability can be lowered to first-order definability.

math.LO

Algorithmic randomness and the weak merging of computable probability measures

We characterize Martin-L\"of randomness and Schnorr randomness in terms of the merging of opinions, along the lines of the Blackwell-Dubins Theorem. After setting up a general framework for defining notions of merging randomness, we focus on finite horizon events, that is, on weak merging in the sense of Kalai-Lehrer. In contrast to Blackwell-Dubins and Kalai-Lehrer, we consider not only the total variational distance but also the Hellinger distance and the Kullback-Leibler divergence. Our main result is a characterization of Martin-L\"of randomness and Schnorr randomness in terms of weak merging and the summable Kullback-Leibler divergence. The main proof idea is that the Kullback-Leibler divergence between $\mu$ and $\nu$, at a given stage of the learning process, is exactly the incremental growth, at that stage, of the predictable process of the Doob decomposition of the $\nu$-submartingale $L(\sigma)=-\ln \frac{\mu(\sigma)}{\nu(\sigma)}$. These characterizations of algorithmic randomness notions in terms of the Kullback-Leibler divergence can be viewed as global analogues of Vovk's theorem on what transpires locally with individual Martin-L\"of $\mu$- and $\nu$-random points and the Hellinger distance between $\mu,\nu$.

math.LO

Schnorr Randomness and Effective Bayesian Consistency and Inconsistency

We study Doob's Consistency Theorem and Freedman's Inconsistency Theorem from the vantage point of computable probability and algorithmic randomness. We show that the Schnorr random elements of the parameter space are computably consistent, when there is a map from the sample space to the parameter space satisfying many of the same properties as limiting relative frequencies. We show that the generic inconsistency in Freedman's Theorem is effectively generic, which implies the existence of computable parameters which are not computably consistent. Taken together, this work provides a computability-theoretic solution to Diaconis and Freedman's problem of ``know[ing] for which [parameters] the rule [Bayes' rule] is consistent'', and it strengthens recent similar results of Takahashi on Martin-L\"of randomness in Cantor space.

math.LO

Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic

A system $\boldsymbol\lambda_{\theta}$ is developed that combines modal logic and simply-typed lambda calculus, and that generalizes the system studied by Montague and Gallin. Whereas Montague and Gallin worked with Church's simple theory of types, the system $\boldsymbol\lambda_{\theta}$ is developed in the typed base theory most commonly used today, namely the simply-typed lambda calculus. Further, the system $\boldsymbol\lambda_{\theta}$ is controlled by a parameter $\theta$ which allows more options for state types and state variables than is present in Montague and Gallin. A main goal of the paper is to establish some basic metatheory of $\boldsymbol\lambda_{\theta}$: (i) an Andrews-like characterization of its models in terms of combinatory logic is given, and this combinatory logic involves a $\mathsf{BCKW}$-like basis rather than an $\mathsf{SKI}$-like basis and (ii) semantic conservation and expressibility results relating $\boldsymbol\lambda_{\theta}$ to the maximal system $\boldsymbol\lambda_{\omega}$ are proven. Similar results are proven for the relation between $\boldsymbol\lambda_{\omega}$ and $\boldsymbol\lambda$, the corresponding ordinary simply-typed lambda calculus. This answers a question of Zimmermann in the semantics of the simply typed setting. In a companion paper this is extended to Church's simple theory of types. We further develop a partial correspondence between a pure combinatory logic centered on the $\mathsf{BCKW}$-like basis and the weak deductive system for $\boldsymbol\lambda_{\omega}$ wherein $\beta$-reduction is not allowed under a lambda abstract, and we use this to show partial deductive conservation between the maximal system $\boldsymbol\lambda_{\omega}$ and the intermediary systems $\boldsymbol\lambda_{\theta}$.

cs.LO

Algorithmic Randomness, Effective Disintegrations, and Rates of Convergence to the Truth

L\'evy's Upward Theorem says that the conditional expectation of an integrable random variable converges with probability one to its true value with increasing information. In this paper, we use methods from effective probability theory to characterise the probability one set along which convergence to the truth occurs, and the rate at which the convergence occurs. We work within the setting of computable probability measures defined on computable Polish spaces and introduce a new general theory of effective disintegrations. We use this machinery to prove our main results, which (1) identify the points along which certain classes of effective random variables converge to the truth in terms of certain classes of algorithmically random points, and which further (2) identify when computable rates of convergence exist. Our convergence results significantly generalize earlier results within a unifying novel abstract framework, and there are no precursors of our results on computable rates of convergence. Finally, we make a case for the importance of our work for the foundations of Bayesian probability theory.

math.LO

Data Harmonisation for Information Fusion in Digital Healthcare: A State-of-the-Art Systematic Review, Meta-Analysis and Future Research Directions

Removing the bias and variance of multicentre data has always been a challenge in large scale digital healthcare studies, which requires the ability to integrate clinical features extracted from data acquired by different scanners and protocols to improve stability and robustness. Previous studies have described various computational approaches to fuse single modality multicentre datasets. However, these surveys rarely focused on evaluation metrics and lacked a checklist for computational data harmonisation studies. In this systematic review, we summarise the computational data harmonisation approaches for multi-modality data in the digital healthcare field, including harmonisation strategies and evaluation metrics based on different theories. In addition, a comprehensive checklist that summarises common practices for data harmonisation studies is proposed to guide researchers to report their research findings more effectively. Last but not least, flowcharts presenting possible ways for methodology and metric selection are proposed and the limitations of different methods have been surveyed for future research.

cs.AI

Federated Learning for Multi-Center Imaging Diagnostics: A Study in Cardiovascular Disease

Deep learning models can enable accurate and efficient disease diagnosis, but have thus far been hampered by the data scarcity present in the medical world. Automated diagnosis studies have been constrained by underpowered single-center datasets, and although some results have shown promise, their generalizability to other institutions remains questionable as the data heterogeneity between institutions is not taken into account. By allowing models to be trained in a distributed manner that preserves patients' privacy, federated learning promises to alleviate these issues, by enabling diligent multi-center studies. We present the first federated learning study on the modality of cardiovascular magnetic resonance (CMR) and use four centers derived from subsets of the M\&M and ACDC datasets, focusing on the diagnosis of hypertrophic cardiomyopathy (HCM). We adapt a 3D-CNN network pretrained on action recognition and explore two different ways of incorporating shape prior information to the model, and four different data augmentation set-ups, systematically analyzing their impact on the different collaborative learning choices. We show that despite the small size of data (180 subjects derived from four centers), the privacy preserving federated learning achieves promising results that are competitive with traditional centralized learning. We further find that federatively trained models exhibit increased robustness and are more sensitive to domain shift effects.

eess.IV

Improving 3D Object Detection for Pedestrians with Virtual Multi-View Synthesis Orientation Estimation

Accurately estimating the orientation of pedestrians is an important and challenging task for autonomous driving because this information is essential for tracking and predicting pedestrian behavior. This paper presents a flexible Virtual Multi-View Synthesis module that can be adopted into 3D object detection methods to improve orientation estimation. The module uses a multi-step process to acquire the fine-grained semantic information required for accurate orientation estimation. First, the scene's point cloud is densified using a structure preserving depth completion algorithm and each point is colorized using its corresponding RGB pixel. Next, virtual cameras are placed around each object in the densified point cloud to generate novel viewpoints, which preserve the object's appearance. We show that this module greatly improves the orientation estimation on the challenging pedestrian class on the KITTI benchmark. When used with the open-source 3D detector AVOD-FPN, we outperform all other published methods on the pedestrian Orientation, 3D, and Bird's Eye View benchmarks.

cs.CV

Leveraging Pre-Trained 3D Object Detection Models For Fast Ground Truth Generation

Training 3D object detectors for autonomous driving has been limited to small datasets due to the effort required to generate annotations. Reducing both task complexity and the amount of task switching done by annotators is key to reducing the effort and time required to generate 3D bounding box annotations. This paper introduces a novel ground truth generation method that combines human supervision with pretrained neural networks to generate per-instance 3D point cloud segmentation, 3D bounding boxes, and class annotations. The annotators provide object anchor clicks which behave as a seed to generate instance segmentation results in 3D. The points belonging to each instance are then used to regress object centroids, bounding box dimensions, and object orientation. Our proposed annotation scheme requires 30x lower human annotation time. We use the KITTI 3D object detection dataset to evaluate the efficiency and the quality of our annotation scheme. We also test the the proposed scheme on previously unseen data from the Autonomoose self-driving vehicle to demonstrate generalization capabilities of the network.

cs.LG

The Prehistory of the Subsystems of Second-Order Arithmetic

This paper presents a systematic study of the prehistory of the traditional subsystems of second-order arithmetic that feature prominently in the reverse mathematics program of Friedman and Simpson. We look in particular at: (i) the long arc from Poincaré to Feferman as concerns arithmetic definability and provability, (ii) the interplay between finitism and the formalization of analysis in the lecture notes and publications of Hilbert and Bernays, (iii) the uncertainty as to the constructive status of principles equivalent to Weak König's Lemma, and (iv) the large-scale intellectual backdrop to arithmetical transfinite recursion in descriptive set theory and its effectivization by Borel, Lusin, Addison, and others.

math.HO

Definability Aspects of the Denjoy Integral

The Denjoy integral is an integral that extends the Lebesgue integral and can integrate any derivative. In this paper, it is shown that the graph of the indefinite Denjoy integral $f\mapsto \int_a^x f$ is a coanalytic non-Borel relation on the product space $M[a,b]\times C[a,b]$, where $M[a,b]$ is the Polish space of real-valued measurable functions on $[a,b]$ and where $C[a,b]$ is the Polish space of real-valued continuous functions on $[a,b]$. Using the same methods, it is also shown that the class of indefinite Denjoy integrals, called $ACG_{\ast}[a,b]$, is a coanalytic but not Borel subclass of the space $C[a,b]$, thus answering a question posed by Dougherty and Kechris. Some basic model theory of the associated spaces of integrable functions is also studied. Here the main result is that, when viewed as an $\mathbb{R}[X]$-module with the indeterminate $X$ being interpreted as the indefinite integral, the space of continuous functions on the interval $[a,b]$ is elementarily equivalent to the Lebesgue-integrable and Denjoy-integrable functions on this interval, and each is stable but not superstable, and that they all have a common decidable theory when viewed as $\mathbb{Q}[X]$-modules.

math.LO

Realizability Semantics for Quantified Modal Logic: Generalizing Flagg's 1985 Construction

A semantics for quantified modal logic is presented that is based on Kleene's notion of realizability. This semantics generalizes Flagg's 1985 construction of a model of a modal version of Church's Thesis and first-order arithmetic. While the bulk of the paper is devoted to developing the details of the semantics, to illustrate the scope of this approach, we show that the construction produces (i) a model of a modal version of Church's Thesis and a variant of a modal set theory due to Goodman and Scedrov, (ii) a model of a modal version of Troelstra's generalized continuity principle together with a fragment of second-order arithmetic, and (iii) a model based on Scott's graph model (for the untyped lambda calculus) which witnesses the failure of the stability of non-identity.

math.LO

Structure and Categoricity: Determinacy of Reference and Truth-Value in the Philosophy of Mathematics

This article surveys recent literature by Parsons, McGee, Shapiro and others on the significance of categoricity arguments in the philosophy of mathematics. After discussing whether categoricity arguments are sufficient to secure reference to mathematical structures up to isomorphism, we assess what exactly is achieved by recent `internal' renditions of the famous categoricity arguments for arithmetic and set theory.

math.HO

The Strength of Abstraction with Predicative Comprehension

Frege's theorem says that second-order Peano arithmetic is interpretable in Hume's Principle and full impredicative comprehension. Hume's Principle is one example of an abstraction principle, while another paradigmatic example is Basic Law V from Frege's Grundgesetze. In this paper we study the strength of abstraction principles in the presence of predicative restrictions on the comprehension schema, and in particular we study a predicative Fregean theory which contains all the abstraction principles whose underlying equivalence relations can be proven to be equivalence relations in a weak background second-order logic. We show that this predicative Fregean theory interprets second-order Peano arithmetic.

math.LO

Fragments of Frege's Grundgesetze and Gödel's Constructible Universe

Frege's Grundgesetze was one of the 19th century forerunners to contemporary set theory which was plagued by the Russell paradox. In recent years, it has been shown that subsystems of the Grundgesetze formed by restricting the comprehension schema are consistent. One aim of this paper is to ascertain how much set theory can be developed within these consistent fragments of the Grundgesetze, and our main theorem shows that there is a model of a fragment of the Grundgesetze which defines a model of all the axioms of Zermelo-Fraenkel set theory with the exception of the power set axiom. The proof of this result appeals to Gödel's constructible universe of sets, which Gödel famously used to show the relative consistency of the continuum hypothesis. More specifically, our proofs appeal to Kripke and Platek's idea of the projectum within the constructible universe as well as to a weak version of uniformization (which does not involve knowledge of Jensen's fine structure theory). The axioms of the Grundgesetze are examples of abstraction principles, and the other primary aim of this paper is to articulate a sufficient condition for the consistency of abstraction principles with limited amounts of comprehension. As an application, we resolve an analogue of the joint consistency problem in the predicative setting.

math.LO

Predicativity, the Russell-Myhill Paradox, and Church's Intensional Logic

This paper sets out a predicative response to the Russell-Myhill paradox of propositions within the framework of Church's intensional logic. A predicative response places restrictions on the full comprehension schema, which asserts that every formula determines a higher-order entity. In addition to motivating the restriction on the comprehension schema from intuitions about the stability of reference, this paper contains a consistency proof for the predicative response to the Russell-Myhill paradox. The models used to establish this consistency also model other axioms of Church's intensional logic that have been criticized by Parsons and Klement: this, it turns out, is due to resources which also permit an interpretation of a fragment of Gallin's intensional logic. Finally, the relation between the predicative response to the Russell-Myhill paradox of propositions and the Russell paradox of sets is discussed, and it is shown that the predicative conception of set induced by this predicative intensional logic allows one to respond to the Wehmeier problem of many non-extensions.

math.LO

Relative Categoricity and Abstraction Principles

Many recent writers in the philosophy of mathematics have put great weight on the relative categoricity of the traditional axiomatizations of our foundational theories of arithmetic and set theory (\cite{Parsons1990a}, \cite{Parsons2008} §{49}, \cite{McGee1997aa}, \cite{Lavine1999aa}, \cite{Vaananen2014aa}). Another great enterprise in contemporary philosophy of mathematics has been Wright's and Hale's project of founding mathematics on abstraction principles (\cite{Hale2001}, \cite{Cook2007aa}). In \cite{Walsh2012aa}, it was noted that one traditional abstraction principle, namely Hume's Principle, had a certain relative categoricity property, which here we term \emph{natural relative categoricity}. In this paper, we show that most other abstraction principles are \emph{not} naturally relatively categorical, so that there is in fact a large amount of incompatibility between these two recent trends in contemporary philosophy of mathematics. To better understand the precise demands of relative categoricity in the context of abstraction principles, we compare and contrast these constraints to (i) stability-like acceptability criteria on abstraction principles (cf. \cite{Cook2012aa}), (ii) the Tarski-Sher logicality requirements on abstraction principles studied by Antonelli \cite{Antonelli2010aa} and Fine~\cite{Fine2002}, and (iii) supervaluational ideas coming out of Hodes' work \cite{Hodes1984, Hodes1990aa, Hodes1991}.

math.LO

Comparing Hume's Principle, Basic Law V and Peano Arithmetic

This paper presents new constructions of models of Hume's Principle and Basic Law V with restricted amounts of comprehension. The techniques used in these constructions are drawn from hyperarithmetic theory and the model theory of fields, and formalizing these techniques within various subsystems of second-order Peano arithmetic allows one to put upper and lower bounds on the interpretability strength of these theories and hence to compare these theories to the canonical subsystems of second-order arithmetic. The main results of this paper are: (i) there is a consistent extension of the hyperarithmetic fragment of Basic Law V which interprets the hyperarithmetic fragment of second-order Peano arithmetic, and (ii) the hyperarithmetic fragment of Hume's Principle does not interpret the hyperarithmetic fragment of second-order Peano arithmetic, so that in this specific sense there is no predicative version of Frege's Theorem.

math.LO