arXiv subjects

Zoltan A. Kocsis

Publications and source records attributed to Zoltan A. Kocsis.

11 recordsLinked to original sources

arXiv2026

Two applications of the point-free coderivative

We present two new applications of Simmons' point-free Cantor-Bendixson coderivative operator in intuitionistic logic. First, we use it to give a simplified proof of the recent result of Xu and Ye that the free Heyting algebra on two generators does not occur as the Heyting algebra of subterminal objects in any elementary topos. Then we use it to prove that complete Heyting algebra semantics is not strongly complete for intuitionistic second-order propositional logic: semantic consequence from an arbitrary set of assumptions does not coincide with ordinary syntactic consequence.

math.LO↗

arXiv2026

Distributive lattices in o-minimal structures

We investigate distributive lattices and Heyting algebras definable in o-minimal structures. We give a complete description of one-dimensional distributive lattices definable in o-minimal structures expanding a real-closed field, and prove a definable analogue of Birkhoff representation. As applications, we obtain a sharp lower bound on the dimension of definable Heyting algebras which contain infinite free subalgebras, and determine all one-variable equations in the language of Heyting algebras whose solution set can constitute a maximal-dimension proper subset of an infinite algebra.

math.LO↗

arXiv2025

The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

We report on the Equational Theories Project (ETP), an online collaborative pilot project to explore new ways to collaborate in mathematics with machine assistance. The project successfully determined all 22 028 942 edges of the implication graph between the 4694 simplest equational laws on magmas, by a combination of human-generated and automated proofs, all validated by the formal proof assistant language Lean. As a result of this project, several new constructions of magmas satisfying specific laws were discovered, and several auxiliary questions were also addressed, such as the effect of restricting attention to finite magmas.

math.RA↗

arXiv2025

Structured Decompositions: Structural and Algorithmic Compositionality

We introduce structured decompositions, category-theoretic structures which simultaneously generalize notions from graph theory (including treewidth, layered treewidth, co-treewidth, graph decomposition width, tree independence number, hypergraph treewidth and H-treewidth), geometric group theory (specifically Bass-Serre theory), and dynamical systems (e.g. hybrid dynamical systems). We define width functors, which provide a compositional way to analyze and relate different structural complexity measures, and establish a general duality between decompositions and completions of objects.

math.CT↗

arXiv2025

Proof-theoretic methods in quantifier-free definability

We introduce a proof-theoretic approach to showing nondefinability of second-order intuitionistic connectives by quantifier-free schemata. We apply the method to prove that Taranovsky's "realizability disjunction" connective does not admit a quantifier-free definition, and use it to obtain new results and more nuanced information about the nondefinability of Kreisel's and Połacik's unary connectives. The finitary and combinatorial nature of our method makes it resilient to changes in metatheory, and suitable even for settings with axioms that are explicitly incompatible with classical logic. Furthermore, the problem-specific subproofs arising from this approach can be readily transcribed into univalent type theory and verified using the Agda proof assistant.

math.LO↗

arXiv2024

Apartness relations between propositions

We classify all apartness relations definable in propositional logics extending intuitionistic logic using Heyting algebra semantics. We show that every Heyting algebra which contains a non-trivial apartness term satisfies the weak law of excluded middle, and every Heyting algebra which contains a tight apartness term is in fact a Boolean algebra. This answers a question of E. Rijke regarding the correct notion of apartness for propositions, and yields a short classification of apartness terms that can occur in a Heyting algebra. We also show that Martin-Löf Type Theory is not able to construct non-trivial apartness relations between propositions.

math.LO↗

arXiv2024

Degree of Satisfiability in Heyting Algebras

Given a finite structure $M$ and property $p$, it is a natural to study the degree of satisfiability of $p$ in $M$; i.e. to ask: what is the probability that uniformly randomly chosen elements in $M$ satisfy $p$? In group theory, a well-known result of Gustafson states that the equation $xy=yx$ has a finite satisfiability gap: its degree of satisfiability is either $1$ (in Abelian groups) or no larger than $\frac{5}{8}$. Degree of satisfiability has proven useful in the study of (finite and infinite) group-like and ring-like algebraic structures, but finite satisfiability gap questions have not been considered in lattice-like, order-theoretic settings yet. Here we investigate degree of satisfiability questions in the context of Heyting algebras and intuitionistic logic. We classify all equations in one free variable with respect to finite satisfiability gap, and determine which common principles of classical logic in multiple free variables have finite satisfiability gap. In particular we prove that, in a finite non-Boolean Heyting algebra, the probability that a randomly chosen element satisfies $x \vee \neg x = \top$ is no larger than $\frac{2}{3}$. Finally, we generalize our results to infinite Heyting algebras, and present their applications to point-set topology, black-box algebras, and the philosophy of logic.

math.LO↗

arXiv2022

Spined categories: generalizing tree-width beyond graphs

Tree-width is an invaluable tool for computational problems on graphs. But often one would like to compute on other kinds of objects (e.g. decorated graphs or even algebraic structures) where there is no known tree-width analogue. Here we define an abstract analogue of tree-width which provides a uniform definition of various tree-width-like invariants including graph tree-width, hypergraph tree-width, complemented tree-width and even new constructions such as the tree-width of modular quotients. We obtain this generalization by developing a general theory of categories that admit abstract analogues of both tree decompositions and tree-width; we call these pseudo-chordal completions and the triangulation functor respectively.

math.CO↗

arXiv2021

Treewidth via Spined Categories (extended abstract)

Treewidth is a well-known graph invariant with multiple interesting applications in combinatorics. On the practical side, many NP-complete problems are polynomial-time (sometimes even linear-time) solvable on graphs of bounded treewidth. On the theoretical side, treewidth played an essential role in the proof of the celebrated Robertson-Seymour graph minor theorem. While defining treewidth-like invariants on graphs and treewidth analogues on other sorts of combinatorial objects (incl. hypergraphs, digraphs) has been a fruitful avenue of research, a direct, categorial description capturing multiple treewidth-like invariants is yet to emerge. Here we report on our recent work on spined categories (arXiv:2104.01841): categories equipped with extra structure that permits the definition of a functorial analogue of treewidth, the triangulation functor. The usual notion of treewidth is recovered as a special case, the triangulation functor of a spined category with graphs as objects and graph monomorphisms as arrows. The usual notion of treewidth for hypergraphs arises as the triangulation functor of a similar category of hypergraphs.

math.CT↗

arXiv2020

Degree of satisfiability of some special equations

A well-known theorem of Gustafson states that in a non-Abelian group the degree of satisfiability of $xy=yx$, i.e. the probability that two uniformly randomly chosen group elements $x,y$ obey the equation $xy=yx$, is no larger than $\frac{5}{8}$. The seminal work of Antolin, Martino and Ventura (arXiv:1511.07269) on generalizing the degree of satisfiability to finitely generated groups led to renewed interest in Gustafson-style properties of other equations. Positive results have recently been obtained for the 2-Engel and metabelian identities (arXiv:1809.02997). Here we show that the degree of satisfiability of the equations $xy^2=y^2x$, $xy^3=y^3x$ and $xy=yx^{-1}$ is either 1, or no larger than $1-\varepsilon$ for some positive constant $\varepsilon$. Using the Antolin-Martino-Ventura formalism, we introduce criteria to identify which equations hold in a finite index subgroup precisely if they have positive degree of satisfiability. We deduce that the equations $xy=yx^{-1}$ and $xy^2=y^2x$ do not have this property.

math.GR↗

arXiv2017

Dependency Injection for Programming by Optimization

Programming by Optimization tools perform automatic software configuration according to the specification supplied by a software developer. Developers specify design spaces for program components, and the onerous task of determining which configuration best suits a given use case is determined using automated analysis tools and optimization heuristics. However, in current approaches to Programming by Optimization, design space specification and exploration relies on external configuration algorithms, executable wrappers and fragile, preprocessed programming language extensions. Here we show that the architectural pattern of Dependency Injection provides a superior alternative to the traditional Programming by Optimization pipeline. We demonstrate that configuration tools based on Dependency Injection fit naturally into the software development process, while requiring less overhead than current wrapper-based mechanisms. Furthermore, the structural correspondence between Dependency Injection and context-free grammars yields a new class of evolutionary metaheuristics for automated algorithm configuration. We found that the new heuristics significantly outperform existing configuration algorithms on many problems of interest (in one case by two orders of magnitude). We anticipate that these developments will make Programming by Optimization immediately applicable to a large number of enterprise software projects.

cs.AI↗