math.LO

arXiv:2406.04936v5 Announce Type: replace-cross Abstract: We explore a kind of first-order predicate logic with intended semantics in the reals. Compared to other approaches in the literature, we work predominantly in the multiplicative reals $[0,\infty]$, showing they support three generations of connectives, that we call non-linear, linear additive, and linear multiplicative. Means and harmonic means emerge as natural candidates for bounded existential and universal quantifiers, and in fact we see they behave as expected in relation to the other logical connectives. We explain this fact through the well-known fact that min/max and arithmetic mean/harmonic mean sit at opposite ends of a spectrum, that of p-means. We give syntax and semantics for this quantitative predicate logic, and as example applications, we show how softmax is the quantitative semantics of argmax, and R\'enyi entropy/Hill numbers are additive/multiplicative semantics of the same formula. Indeed, the additive reals also fit into the story by exploiting the Napierian duality $-\log \dashv 1/\exp$, which highlights a formal distinction between 'additive' and 'multiplicative' quantities. Finally, we describe two attempts at a categorical semantics via enriched hyperdoctrines. We discuss why hyperdoctrines are in fact probably inadequate for this kind of logic.

arXiv:2404.01670v3 Announce Type: replace-cross Abstract: In the product $L_1\times L_2$ of two Kripke complete consistent logics, local tabularity of $L_1$ and $L_2$ is necessary for local tabularity of $L_1\times L_2$. However, it is not sufficient: the product of two locally tabular logics may not be locally tabular. We provide extra semantic and axiomatic conditions that give criteria of local tabularity of the product of two locally tabular logics, and apply them to identify new families of locally tabular products. We show that the product of two locally tabular logics may lack the product finite model property. We give an axiomatic criterion of local tabularity for all extensions of $S4.1 [ 2 ]\times S5$. Finally, we describe a new prelocally tabular extension of $S{4}\times S{5}$.

arXiv:2501.11768v1 Announce Type: cross Abstract: This paper develops the model theory of normal modal logics based on partial "possibilities" instead of total "worlds," following Humberstone (1981) instead of Kripke (1963). Possibility semantics can be seen as extending to modal logic the semantics for classical logic used in weak forcing in set theory, or as semanticizing a negative translation of classical modal logic into intuitionistic modal logic. Thus, possibility frames are based on posets with accessibility relations, like intuitionistic modal frames, but with the constraint that the interpretation of every formula is a regular open set in the Alexandrov topology on the poset. The standard world frames for modal logic are the special case of possibility frames wherein the poset is discrete. We develop the beginnings of duality theory, definability/correspondence theory, and completeness theory for possibility frames.

arXiv:2501.11799v1 Announce Type: new Abstract: In a multi-agent system, one may choose to govern the behaviour of an agent by imposing norms, which act as guidelines for how agents should act either all of the time or in given situations. However, imposing multiple norms on one or more agents may result in situations where these norms conflict over how the agent should behave. In any system with normative conflicts (such as safe reinforcement models or systems which monitor safety protocols), one must decide which norms should be followed such that the most important and most relevant norms are maintained. We introduce a new method for resolving normative conflicts through argumentation and graph colouring which is compatible with a variety of normative conflict resolution policies. We prove that this method always creates an admissible set of arguments under argumentation semantics, meaning that it produces coherent outputs. We also introduce more robust variants of this method, each building upon their predecessor to create a superior output, and we include further mathematical proof of their coherence. Our most advanced variant uses the existing concept of curtailment, where one norm may supersede another without fully eliminating it. The methods we introduce are all compatible with various pre-existing policies for resolving normative conflicts. Empirical evaluations are also performed to compare our algorithms to each other and to others in existing literature.

arXiv:2501.07332v1 Announce Type: cross Abstract: In ``Monk Algebras and Ramsey Theory,'' \emph{J. Log. Algebr. Methods Program.} (2022), Kramer and Maddux prove various representability results in furtherance of the goal of finding the smallest weakly representable but not representable relation algebra. They also pose many open problems. In the present paper, we address problems and issues raised by Kramer and Maddux. In particular, we prove that their Proposition 7 does not generalize, and we answer Problem 1.1 in the negative: relation algebra $1311_{1316}$ is not representable. Thus $1311_{1316}$ is a good candidate for the smallest weakly representable but not representable relation algebra. Finally, we give the first known finite cyclic group representations for relation algebras $31_{37}$, $32_{65}$, $1306_{1314}$, and $1314_{1316}$.

arXiv:2303.09287v5 Announce Type: replace Abstract: We introduce semitopology, a generalisation of point-set topology that removes the restriction that intersections of open sets need necessarily be open. The intuition is that points represent participants in a decentralised system, and open sets represent collections of participants that collectively have the authority to collaborate to update their local state; we call this an actionable coalition. Examples of actionable coalition include: majority stakes in proof-of-stake blockchains; communicating peers in peer-to-peer networks; and even pedestrians working together to not bump into one another in the street. Where actionable coalitions exist, they have in common that: collaborations are local (updating the states of the participants in the coalition, but not immediately those of the whole system); collaborations are voluntary (up to and including breaking rules); participants may be heterogeneous in their computing power or in their goals (not all pedestrians want to go to the same place); participants can choose with whom to collaborate; and they are not assumed subject to permission or synchronisation by a central authority. We develop a topology-flavoured mathematics that goes some way to explaining how and why these complex decentralised systems can exhibit order, and gives us new ways to understand existing practical implementations.

arXiv:2402.02829v2 Announce Type: replace Abstract: Craig interpolation is a fundamental property of classical and non-classic logics with a plethora of applications from philosophical logic to computer-aided verification. The question of which interpolants can be obtained from an interpolation algorithm is of profound importance. Motivated by this question, we initiate the study of completeness properties of interpolation algorithms. An interpolation algorithm $\mathcal{I}$ is \emph{complete} if, for every semantically possible interpolant $C$ of an implication $A \to B$, there is a proof $P$ of $A \to B$ such that $C$ is logically equivalent to $\mathcal{I}(P)$. We establish incompleteness and different kinds of completeness results for several standard algorithms for resolution and the sequent calculus for propositional, modal, and first-order logic.

arXiv:2501.03789v1 Announce Type: cross Abstract: We present a dichotomy for structures $A$ that are preserved by primitive actions of $S_{\omega} = \text{Sym}({\mathbb N})$: either such a structure interprets all finite structures primitively positively, or it is of a very simple form and in particular has a binary polymorphism $f$ and an automorphism $\alpha$ satisfying $f(x,y) = \alpha(f(y,x))$. It is a consequence of our results that the constraint satisfaction problem for $A$ is in P or NP-complete. To prove our result, we study the first-order reducts of the Johnson graph $J(k)$, for $k \geq 2$, whose automorphism group $G$ equals the action of $S_{\omega}$ on the set $V$ of $k$-element subsets of $\mathbb N$. We use the fact that $J(k)$ has a finitely bounded homogeneous Ramsey expansion and that $G$ is a maximal closed subgroup of $\text{Sym}(V)$.

arXiv:2501.03297v1 Announce Type: cross Abstract: I deal with two approaches to proof-theoretic semantics: one based on argument structures and justifications, which I call reducibility semantics, and one based on consequence among (sets of) formulas over atomic bases, called base semantics. The latter splits in turn into a standard reading, and a variant of it put forward by Sandqvist. I prove some results which, when suitable conditions are met, permit one to shift from one approach to the other, and I draw some of the consequences of these results relative to the issue of completeness of (recursive) logical systems with respect to proof-theoretic notions of validity. This will lead me to focus on a notion of base-completeness, which I will discuss with reference to known completeness results for intuitionistic logic. The general interest of the proposed approach stems from the fact that reducibility semantics can be understood as a labelling of base semantics with proof-objects typed on (sets of) formulas for which a base semantics consequence relation holds, and which witness this very fact. Vice versa, base semantics can be understood as a type-abstraction of a reducibility semantics consequence relation obtained by removing the witness of the fact that this relation holds, and by just focusing on the input and output type of the relevant proof-object.

arXiv:2501.00496v1 Announce Type: cross Abstract: This work studies the proof theory of left (right) skew monoidal closed categories and skew monoidal bi-closed categories from the perspective of non-associative Lambek calculus. Skew monoidal closed categories represent a relaxed version of monoidal closed categories, where the structural laws are not invertible; instead, they are natural transformations with a specific orientation. Uustalu et al. used sequents with stoup (the leftmost position of an antecedent that can be either empty or a single formula) to deductively model left skew monoidal closed categories, yielding results regarding proof identities and categorical coherence. However, their syntax does not work well when modeling right skew monoidal closed and skew monoidal bi-closed categories. We solve the problem by constructing cut-free sequent calculi for left skew monoidal closed and skew monoidal bi-closed categories, reminiscent of non-associative Lambek calculus, with trees as antecedents. Each calculus is respectively equivalent to the sequent calculus with stoup (for left skew monoidal categories) and the axiomatic calculus (for skew monoidal bi-closed categories). Moreover, we prove that the latter calculus is sound and complete with respect to its relational models. We also prove a correspondence between frame conditions and structural laws, providing an algebraic way to understand the relationship between the left and right skew monoidal (closed) categories.

arXiv:2405.13398v3 Announce Type: replace-cross Abstract: Epistemic logic is known as a 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 taking the product of individual knowledge structures and the set of 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 two main results; one is that this logic can embed the standard epistemic logic, and the other is that there is a proof system of tableau calculus that works in finite time. We also discuss various sentences and inferences that this logic can express.

arXiv:2501.00451v1 Announce Type: new Abstract: We demonstrate that techniques of Weihrauch complexity can be used to get easy and elegant proofs of known and new results on initial value problems. Our main result is that solving continuous initial value problems is Weihrauch equivalent to weak K\H{o}nig's lemma, even if only solutions with maximal domains of existence are considered. This result simultaneously generalizes negative and positive results by Aberth and by Collins and Gra\c{c}a, respectively. It can also be seen as a uniform version of a Theorem of Simpson. Beyond known techniques we exploit for the proof that weak K\H{o}nig's lemma is closed under infinite loops. One corollary of our main result is that solutions with maximal domain of existence of continuous initial value problems can be computed non-deterministically, and for computable instances there are always solutions that are low as points in the function space. Another corollary is that in the case that there is a fixed finite number of solutions, these solutions are all computable for computable instances and they can be found uniformly in a finite mind-change computation.

arXiv:2412.07592v2 Announce Type: replace-cross Abstract: We study the complexity of deterministic and probabilistic inversions of partial computable functions on the reals.

arXiv:2209.11229v3 Announce Type: replace Abstract: The notions of bounded-size and quasibounded-size decompositions with bounded treedepth base classes are central to the structural theory of graph sparsity introduced by two of the authors years ago, and provide a characterization of both classes with bounded expansions and nowhere dense classes. Strong connections of this theory with model theory led to considering first-order transductions, which are logically defined graph transformations, and to initiate a comparative study of combinatorial and model theoretical properties of graph classes, with an emphasis on the model theoretical notions of dependence (or NIP) and stability. In this paper, we first prove that every hereditary class with quasibounded-size decompositions with dependent (resp.\ stable) base classes is itself dependent (resp.\ stable). This result is obtained in a more general study of ``decomposition horizons'', which are class properties compatible with quasibounded-size decompositions. We deduce that hereditary classes with quasibounded-size decompositions with bounded shrubdepth base classes are stable. In the second part of the paper, we prove the converse. Thus, we characterize stable hereditary classes of graphs as those hereditary classes that admit quasibounded-size decompositions with bounded shrubdepth base classes. This result is obtained by proving that every hereditary stable class of graphs admits almost nowhere dense quasi-bush representations, thus answering positively a conjecture of Dreier et al. These results have several consequences. For example, we show that every graph $G$ in a stable, hereditary class of graphs $\mathscr C$ has a clique or a stable set of size $\Omega_{\mathscr C,\epsilon}(|G|^{1/2-\epsilon})$, for every $\epsilon>0$, which is tight in the sense that it cannot be improved to $\Omega_{\mathscr C}(|G|^{1/2})$.

arXiv:2311.01184v2 Announce Type: replace Abstract: We investigate the correspondence between the time and space recognition complexity of languages. For this purpose, we will code the long-continued computations of deterministic two-tape Turing machines by the relatively short-length quantified Boolean formulae. The modified Meyer and Stockmeyer method will appreciably be used for this simulation. It will be proved using this modeling that the complexity classes Deterministic Exponential Time and Deterministic Polynomial Space coincide. It will also be proven that any language recognized in polynomial time can be recognized in almost logarithmic space. Furthermore, this allows us slightly to improve the early founded lower complexity bound of decidable theories that are nontrivial relative to some equivalence relation (this relation may be equality) -- each of these theories is consistent with the formula, which asserts that there are two non-equivalent elements. Keywords: computational complexity, the coding of computations through formulae, exponential time, polynomial space, the lower complexity bound of the language recognition

arXiv:2401.01096v2 Announce Type: replace-cross Abstract: We explore the theory of illfounded and cyclic proofs for the propositional {modal $\mu$-calculus}. A fine analysis of {provability} for classical and intuitionistic modal logic provides a novel bridge between finitary, cyclic and illfounded conceptions of proof and re-enforces the importance of two normal form theorems for the logic: guardedness and disjunctiveness.

arXiv:2412.14758v2 Announce Type: replace Abstract: The development of logic has largely been through the 'deductive' paradigm: conclusions are inferred from established premisses. However, the use of logic in the context of both human and machine reasoning is typically through the dual 'reductive' perspective: collections of sufficient premisses are generated from putative conclusions. We call this paradigm, 'reductive logic'. This expression of logic encompass as diverse reasoning activities as proving a formula in a formal system to seeking to meet a friend before noon on Saturday. This paper is a semantical analysis of reductive logic. In particular, we provide mathematical foundations for representing and reasoning about 'reduction operators'. Heuristically, reduction operators may be thought of as `backwards' inference rules. In this paper, we address their mathematical representation, how they are used in the context of reductive reasoning, and, crucially, what makes them 'valid'.

arXiv:2406.10924v2 Announce Type: replace-cross Abstract: We introduce a pebble game extended by backtracking options for one of the two players (called Prover) and reduce the provability of the pigeonhole principle for a generic predicate $R$ in the bounded arithmetic $T^2_2(R)$ to the existence of a particular kind of winning strategy (called oblivious) for Prover in the game. While the unprovability of the said principle in $T^2_2(R)$ is an immediate consequence of a celebrated theorem of Ajtai (which deals with a stronger theory $T_2(R)$), up-to-date no methods working for $T^2_2(R)$ directly (in particular without switching lemma) are known. Although the full analysis of the introduced pebble game is left open, as a first step towards resolving it, we restrict ourselves to a simplified version of the game. In this case, Prover can use only two pebbles and move in an extremely oblivious way. Besides, a series of backtracks can be made only once during a play. Under these assumptions, we show that no strategy of Prover can be winning.

arXiv:2412.16152v1 Announce Type: cross Abstract: This paper proves a homomorphism between extensional formal semantics and distributional vector space semantics, demonstrating structural compatibility. Formal semantics models meaning as reference, using logical structures to map linguistic expressions to truth conditions, while distributional semantics represents meaning through word vectors derived from contextual usage. By constructing injective mappings that preserve semantic relationships, we show that every semantic function in an extensional model corresponds to a compatible vector space operation. This result respects compositionality and extends to function compositions, constant interpretations, and $n$-ary relations. Rather than pursuing unification, we highlight a mathematical foundation for hybrid cognitive models that integrate symbolic and sub-symbolic reasoning and semantics. These findings support multimodal language processing, aligning `meaning as reference' (Frege, Tarski) with `meaning as use' (Wittgenstein, Firth).

arXiv:2102.06673v3 Announce Type: replace Abstract: We investigate the proof complexity of systems based on positive branching programs, i.e. non-deterministic branching programs (NBPs) where, for any 0-transition between two nodes, there is also a 1-transition. Positive NBPs compute monotone Boolean functions, just like negation-free circuits or formulas, but constitute a positive version of (non-uniform) NL, rather than P or NC1, respectively. The proof complexity of NBPs was investigated in previous work by Buss, Das and Knop, using extension variables to represent the dag-structure, over a language of (non-deterministic) decision trees, yielding the system eLNDT. Our system eLNDT+ is obtained by restricting their systems to a positive syntax, similarly to how the 'monotone sequent calculus' MLK is obtained from the usual sequent calculus LK by restricting to negation-free formulas. Our main result is that eLNDT+ polynomially simulates eLNDT over positive sequents. Our proof method is inspired by a similar result for MLK by Atserias, Galesi and Pudl\'ak, that was recently improved to a bona fide polynomial simulation via works of Je\v{r}\'abek and Buss, Kabanets, Kolokolova and Kouck\'y. Along the way we formalise several properties of counting functions within eLNDT+ by polynomial-size proofs and, as a case study, give explicit polynomial-size poofs of the propositional pigeonhole principle.