Logic
See recent articles
- [1] arXiv:2407.13082 [pdf, html, other]
-
Title: An $\mathrm{NSOP}_{1}$ theory without the existence axiomComments: 12 pagesSubjects: Logic (math.LO)
Answering a question of Dobrowolski, Kim and Ramsey, we find an $\mathrm{NSOP}_{1}$ theory that does not satisfy the existence axiom.
- [2] arXiv:2407.13287 [pdf, html, other]
-
Title: On the Logical and Algebraic Aspects of Reasoning with Formal ContextsComments: 30 pagesSubjects: Logic (math.LO)
A formal context consists of objects, properties, and the incidence relation between them. Various notions of concepts defined with respect to formal contexts and their associated algebraic structures have been studied extensively, including formal concepts in formal concept analysis (FCA), rough concepts arising from rough set theory (RST), and semiconcepts and protoconcepts for dealing with negation. While all these kinds of concepts are associated with lattices, semiconcepts and protoconcepts additionally yield an ordered algebraic structure, called double Boolean algebras. As the name suggests, a double Boolean algebra contains two underlying Boolean algebras.
In this paper, we investigate logical and algebraic aspects of the representation and reasoning about different concepts with respect to formal contexts. We present two-sorted modal logic systems \textbf{KB} and \textbf{KF} for the representation and reasoning of rough concepts and formal concepts respectively. Then, in order to represent and reason about both formal and rough concepts in a single framework, these two logics are unified into a two-sorted Boolean modal logic \textbf{BM}, in which semiconcepts and protoconcepts are also expressible. Based on the logical representation of semiconcepts and protoconcepts, we prove the characterization of double Boolean algebras in terms of their underlying Boolean algebras. Finally, we also discuss the possibilities of extending our logical systems for the representation and reasoning of more fine-grained information in formal contexts. - [3] arXiv:2407.13344 [pdf, other]
-
Title: Extremal models and direct integrals in affine logicComments: 133 pagesSubjects: Logic (math.LO); Functional Analysis (math.FA)
Affine logic is a fragment of continuous logic, introduced by Bagheri, in which only affine functions are allowed as connectives. This has the effect of endowing type spaces with the structure of compact convex sets. We study extremal models of affine theories (those that only realize extreme types), and the ways and conditions under which all models can be described from the extremal ones.
We introduce and develop the general theory of measurable fields of metric structures and their direct integrals. One of our main results is an extremal decomposition theorem for models of simplicial theories, that is, affine theories whose type spaces form Choquet simplices. We prove that every model of a simplicial theory can be (uniquely) decomposed as a direct integral of extremal models. This generalizes known decomposition results (ergodic decomposition, tracial von Neumann factor decomposition), and moreover, holds without any separability hypothesis.
Two extreme kinds of simplicial theories are Bauer theories, whose extreme types form a closed set, and Poulsen theories, whose extreme types form a dense set. We show that Keisler randomizations of continuous theories are, essentially, the same thing as affine Bauer theories. We establish a dichotomy result: a complete simplicial theory is either Bauer or Poulsen.
As part of our analysis, we adapt many results and tools from continuous logic to the affine or extremal contexts (definability, saturation, type isolation, categoricity, etc.). We also provide a detailed study of the relations between continuous logic and affine logic.
Finally, we present several examples of simplicial theories arising from theories in discrete logic, Hilbert spaces, probability measure-preserving systems, and tracial von Neumann algebras. - [4] arXiv:2407.13504 [pdf, html, other]
-
Title: Relative leftmost path principles and omega-model reflections of transfinite inductionsComments: 13 pagesSubjects: Logic (math.LO)
In this paper, we show that the omega-model reflection of $\Pi^1_{n+1}$ transfinite induction is equivalent to Towsner's $\Sigma^0_n$ relative leftmost path principle $\Sigma^0_n\mathsf{LPP}$ over $\mathsf{RCA}_0$ for $n > 1$. As a consequence, we have that $\Sigma^0_{n+1}\mathsf{LPP}$ relative leftmost path principle is strictly stronger than $\Sigma^0_{n}\mathsf{LPP}$.
- [5] arXiv:2407.13619 [pdf, html, other]
-
Title: A tree rewriting system for the Reflection CalculusSubjects: Logic (math.LO)
The $Reflection$ $Calculus$ ($\mathcal{\mathbf{RC}}$) is the fragment of the polymodal logic $\mathcal{\mathbf{GLP}}$ in the language $L^+$ whose formulas are built up from $\top$ and propositional variables using conjunction and diamond modalities. $\mathcal{\mathbf{RC}}$ is complete with respect to the arithmetical interpretation that associates modalities with reflection principles and has various applications in proof theory, specifically ordinal analysis.
We present ${\sf TRC}$, a tree rewriting system that is adequate and complete with respect to $\mathcal{\mathbf{RC}}$, designed to simulate $\mathcal{\mathbf{RC}}$ derivations. ${\sf TRC}$ is based on a given correspondence between formulas of $L^{+}$ and modal trees ${\sf Tree}^{\Diamond}$. Modal trees are presented as an inductive type allowing precise positioning and transformations which give rise to the formal definition of rewriting rules and facilitates formalization in proof assistants. Furthermore, we provide a rewrite normalization theorem for systematic rule application. The normalization of the rewriting process enhances proof search efficiency and facilitates implementation.
By providing ${\sf TRC}$ as an efficient provability tool for $\mathcal{\mathbf{RC}}$, we aim to help on the study of various aspects of the logic such as the subformula property and rule admissibility. - [6] arXiv:2407.13624 [pdf, html, other]
-
Title: Model-theoretic $K_1$ of free modules over PIDsComments: 18 pagesSubjects: Logic (math.LO); K-Theory and Homology (math.KT)
Motivated by Krajiček and Scanlon's definition of the Grothendieck ring $K_0(M)$ of a first-order structure $M$, we introduce the definition of $K$-groups $K_n(M)$ for $n\geq0$ via Quillen's $S^{-1}S$ construction. We provide a recipe for the computation of $K_1(M_R)$, where $M_R$ is a free module over a PID $R$, subject to the knowledge of the abelianizations of the general linear groups $GL_n(R)$. As a consequence, we provide explicit computations of $K_1(M_R)$ when $R$ belongs to a large class of Euclidean domains that includes fields with at least $3$ elements and polynomial rings over fields with characteristic $0$. We also show that the algebraic $K_1$ of a PID $R$ embeds into $K_1(R_R)$.
New submissions for Friday, 19 July 2024 (showing 6 of 6 entries )
- [7] arXiv:2407.13448 (cross-list from math.CT) [pdf, html, other]
-
Title: Pure maps are strict monomorphismsSubjects: Category Theory (math.CT); Logic (math.LO)
We prove that $i)$ if $\mathcal{A}$ is $\lambda $-accessible and it is axiomatizable in (finitary) coherent logic then $\lambda $-pure maps are strict monomorphisms and $ii)$ if there is a proper class of strongly compact cardinals and $\mathcal{A}$ is $\lambda $-accessible then for some $\mu \vartriangleright \lambda $ every $\mu $-pure map is a strict monomorphism.
- [8] arXiv:2407.13600 (cross-list from math.GR) [pdf, html, other]
-
Title: Spherically orderable groupsSubjects: Group Theory (math.GR); Logic (math.LO)
We introduce and study the class of spherically ordered groups. The notions of spherically ordered groups and their spectra of spherical orderability are introduced. Values of these spectra are found for a series of natural groups.
Cross submissions for Friday, 19 July 2024 (showing 2 of 2 entries )
- [9] arXiv:2010.09499 (replaced) [pdf, other]
-
Title: Computable classifications of continuous, transducer, and regular functionsSubjects: Logic (math.LO)
We develop a systematic algorithmic framework that unites global and local classification problems using index sets. We prove that the classification problem for continuous (binary) regular functions among almost everywhere linear, pointwise linear-time Lipschitz functions is $\Sigma^0_2$-complete. We show that a function $f\colon [0,1] \rightarrow \mathbb{R}$ is (binary) transducer if and only if it is continuous regular. As one of many consequences, our $\Sigma^0_2$-completeness result covers the class of transducer functions as well. Finally, we show that the Banach space $C[0,1]$ of real-valued continuous functions admits an arithmetical classification among separable Banach spaces. Our proofs combine methods of abstract computability theory, automata theory, and functional analysis.
- [10] arXiv:2302.04251 (replaced) [pdf, html, other]
-
Title: Definability of continuous isomorphisms of groups definable in o-minimal expansions of the real fieldSubjects: Logic (math.LO)
In this paper, we study the relation between the category of real Lie groups and that of groups definable in o-minimal expansions of the real field (which we will refer to as "definable groups"). It is known (\cite{Pi88}) that any group definable in an o-minimal expansion of the real field is a Lie group, and in \cite{COP} a complete characterization of when a Lie group has a "definable group" which is \emph{Lie isomorphic} to it was given. We continue the analysis by explaining when a Lie homomorphism between definable groups is a definable isomorphism.
Among other things, we prove that in any o-minimal expansion $\mathcal R$ of the real field we can add a function symbol for any Lie isomorphism between definable groups to the language of $\mathcal R$ preserving o-minimality, and that any definable group $G$ can be endowed with an analytic manifold structure definable in $\mathcal R_{\text{Pfaff}}$ that makes it an analytic group. - [11] arXiv:2312.13024 (replaced) [pdf, html, other]
-
Title: Univalent Material Set TheorySubjects: Logic (math.LO)
Homotopy type theory (HoTT) can be seen as a generalisation of structural set theory, in the sense that 0-types represent structural sets within the more general notion of types. For material set theory, we also have concrete models as 0-types in HoTT, but this does not currently have any generalisation to higher types. The aim of this paper is to give such a generalisation of material set theory to higher type levels within homotopy type theory. This is achieved by generalising the construction of the type of iterative sets. At level 1, this gives a connection between groupoids and multisets.
More specifically, we define the notion of an $\in$-structure as a type with an extensional binary type family and generalise the axioms of constructive set theory to higher type levels. Once an $\in$-structure is given, its elements can be seen as representing types in the ambient type theory.
The theory has an alternative, coalgebraic formulation, in terms of coalgebras for a certain hierarchy of functors, $P^n$, which generalises the powerset functor from sub-types to covering spaces and $n$-connected maps in general. The coalgebras which furthermore are fixed-points of their respective functors in the hierarchy are shown to model the axioms given in the first part.
As concrete examples of models for the theory developed we construct the initial algebras of the $P^n$ functors. In addition to being an example of initial algebras of non-polynomial functors, this construction allows one to start with a univalent universe and get a hierarchy of $\in$-structures which gives a stratified $\in$-structure representation of that universe. These types are moreover $n$-type universes of $n$-types which contain all the usual types an type formers. - [12] arXiv:2405.04338 (replaced) [pdf, html, other]
-
Title: The computational content of multidimensional discontinuitySubjects: Logic (math.LO)
The Weihrauch degrees are a tool to gauge the computational difficulty of mathematical problems. Often, what makes these problems hard is their discontinuity. We look at discontinuity in its purest form, that is, at otherwise constant functions that make a single discontinuous step along each dimension of their underlying space. This is an extension of previous work of Kihara, Pauly, Westrick from a single dimension to multiple dimensions. Among other results, we obtain strict hierarchies in the Weihrauch degrees, one of which orders mathematical problems by the richness of the truth-tables determining how discontinuous steps influence the output.
- [13] arXiv:2405.13398 (replaced) [pdf, html, other]
-
Title: Agent-Knowledge Logic for Alternative Epistemic LogicComments: 16 pages, 3 figures, preprint of NCL'24Subjects: Logic (math.LO)
Epistemic logic is known as logic that captures the knowledge and beliefs of agents and has undergone various developments since Hintikka (1962). In this paper, we propose a new logic called agent-knowledge logic by multiplying the individual knowledge structure with the relationships among agents. This logic is based on the Facebook logic proposed by Seligman et al. (2011) and the Logic of Hide and Seek Game proposed by Li et al. (2021). We show that this logic can embed the epistemic logic we know well. We also discuss various sentences and inferences that this logic can express.
- [14] arXiv:2301.13116 (replaced) [pdf, html, other]
-
Title: Big Ramsey Degrees and Infinite LanguagesComments: 26 pagesSubjects: Combinatorics (math.CO); Discrete Mathematics (cs.DM); Logic (math.LO)
This paper investigates big Ramsey degrees of unrestricted relational structures in (possibly) infinite languages. Despite significant progress in the study of big Ramsey degrees, the big Ramsey degrees of many classes of structures with finite small Ramsey degrees are still not well understood. We show that if there are only finitely many relations of every arity greater than one, then unrestricted relational structures have finite big Ramsey degrees, and give some evidence that this is tight. This is the first time finiteness of big Ramsey degrees has been established for a random structure in an infinite language. Our results represent an important step towards a better understanding of big Ramsey degrees for structures with relations of arity greater than two.
- [15] arXiv:2407.06952 (replaced) [pdf, html, other]
-
Title: Domain theory in univalent foundations I: Directed complete posets and Scott's $D_\infty$Comments: Based on Ch. 3 and Sec. 5.1 of the author's PhD thesis (arXiv:2301.12405). v3: Updated AcknowledgementsSubjects: Logic in Computer Science (cs.LO); Logic (math.LO)
We develop domain theory in constructive and predicative univalent foundations (also known as homotopy type theory). That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. Our work is constructive in the sense that we do not rely on excluded middle or the axiom of (countable) choice. Domain theory studies so-called directed complete posets (dcpos) and Scott continuous maps between them and has applications in a variety of fields, such as programming language semantics, higher-type computability and topology. A common approach to deal with size issues in a predicative foundation is to work with information systems, abstract bases or formal topologies rather than dcpos, and approximable relations rather than Scott continuous functions. In our type-theoretic approach, we instead accept that dcpos may be large and work with type universes to account for this. A priori one might expect that iterative constructions of dcpos may result in a need for ever-increasing universes and are predicatively impossible. We show, through a careful tracking of type universe parameters, that such constructions can be carried out in a predicative setting. In particular, we give a predicative reconstruction of Scott's $D_\infty$ model of the untyped $\lambda$-calculus. Our work is formalised in the Agda proof assistant and its ability to infer universe levels has been invaluable for our purposes.
- [16] arXiv:2407.06956 (replaced) [pdf, html, other]
-
Title: Domain theory in univalent foundations II: Continuous and algebraic domainsComments: Based on Ch. 4 of the author's PhD thesis (arXiv:2301.12405). v3: Updated AcknowledgementsSubjects: Logic in Computer Science (cs.LO); Logic (math.LO)
We develop the theory of continuous and algebraic domains in constructive and predicative univalent foundations, building upon our earlier work on basic domain theory in this setting. That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. Our work is constructive in the sense that we do not rely on excluded middle or the axiom of (countable) choice. To deal with size issues and give a predicatively suitable definition of continuity of a dcpo, we follow Johnstone and Joyal's work on continuous categories. Adhering to the univalent perspective, we explicitly distinguish between data and property. To ensure that being continuous is a property of a dcpo, we turn to the propositional truncation, although we explain that some care is needed to avoid needing the axiom of choice. We also adapt the notion of a domain-theoretic basis to the predicative setting by imposing suitable smallness conditions, analogous to the categorical concept of an accessible category. All our running examples of continuous dcpos are then actually examples of dcpos with small bases which we show to be well behaved predicatively. In particular, such dcpos are exactly those presented by small ideals. As an application of the theory, we show that Scott's $D_\infty$ model of the untyped $\lambda$-calculus is an example of an algebraic dcpo with a small basis. Our work is formalised in the Agda proof assistant and its ability to infer universe levels has been invaluable for our purposes.