-
Proof-theoretic methods in quantifier-free definability
Authors:
Zoltan A. Kocsis
Abstract:
We introduce a proof-theoretic method for showing nondefinability of second-order intuitionistic connectives by quantifier-free schemata. We apply the method to confirm 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 connecti…
▽ More
We introduce a proof-theoretic method for showing nondefinability of second-order intuitionistic connectives by quantifier-free schemata. We apply the method to confirm 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 more resilient to changes in metatheory than common semantic approaches, whose robustness tends to waver once we pass to non-classical and especially anti-classical settings. Furthermore, we can easily transcribe the problem-specific subproofs into univalent type theory and check them using the Agda proof assistant.
△ Less
Submitted 5 October, 2023;
originally announced October 2023.
-
Apartness relations between propositions
Authors:
Zoltan A. Kocsis
Abstract:
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 on the correct…
▽ More
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 on 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 either.
△ Less
Submitted 10 September, 2022; v1 submitted 8 September, 2022;
originally announced September 2022.
-
Structured Decompositions: Structural and Algorithmic Compositionality
Authors:
Benjamin Merlin Bumpus,
Zoltan A. Kocsis,
Jade Edenstar Master
Abstract:
We introduce structured decompositions: category-theoretic generalizations of many combinatorial invariants -- including tree-width, layered tree-width, co-tree-width and graph decomposition width -- which have played a central role in the study of structural and algorithmic compositionality in both graph theory and parameterized complexity. Structured decompositions allow us to generalize combina…
▽ More
We introduce structured decompositions: category-theoretic generalizations of many combinatorial invariants -- including tree-width, layered tree-width, co-tree-width and graph decomposition width -- which have played a central role in the study of structural and algorithmic compositionality in both graph theory and parameterized complexity. Structured decompositions allow us to generalize combinatorial invariants to new settings (for example decompositions of matroids) in which they describe algorithmically useful structural compositionality. As an application of our theory we prove an algorithmic meta theorem for the Sub_P-composition problem which, when instantiated in the category of graphs, yields compositional algorithms for NP-hard problems such as: Maximum Bipartite Subgraph, Maximum Planar Subgraph and Longest Path.
△ Less
Submitted 21 March, 2023; v1 submitted 13 July, 2022;
originally announced July 2022.
-
Degree of Satisfiability in Heyting Algebras
Authors:
Benjamin Merlin Bumpus,
Zoltan A. Kocsis
Abstract:
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 la…
▽ More
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.
△ Less
Submitted 4 January, 2024; v1 submitted 21 October, 2021;
originally announced October 2021.
-
Treewidth via Spined Categories (extended abstract)
Authors:
Zoltan A. Kocsis,
Benjamin Merlin Bumpus
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 in…
▽ More
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.
△ Less
Submitted 11 May, 2021;
originally announced May 2021.
-
Spined categories: generalizing tree-width beyond graphs
Authors:
Benjamin Merlin Bumpus,
Zoltan A. Kocsis
Abstract:
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-w…
▽ More
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 develo** 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.
△ Less
Submitted 21 June, 2022; v1 submitted 5 April, 2021;
originally announced April 2021.
-
Degree of satisfiability of some special equations
Authors:
Zoltan A. Kocsis
Abstract:
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 rene…
▽ More
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.
△ Less
Submitted 17 February, 2020; v1 submitted 5 February, 2020;
originally announced February 2020.