Related papers: Constructive Combinatorics of Dickson's Lemma

We study the reverse mathematics of the principle stating that, for every property of finite character, every set has a maximal subset satisfying the property. In the context of set theory, this variant of Tukey's lemma is equivalent to the…

In this paper we study projective algebras in varieties of (bounded) commutative integral residuated lattices from an algebraic (as opposed to categorical) point of view. In particular we use a well-established construction in residuated…

For a Dickson pair $(q,n)$ we show that $ \big \lbrace \frac{q^k-1}{q-1}, 1 \leq k < n \big \rbrace $ forms a finite complete set of different residues modulo $n$. We also study the construction of a finite Dickson nearfield that arises…

In this paper a new mathematical procedure is presented for combining different pieces of evidence which are represented in the interval form to reflect our knowledge about the truth of a hypothesis. Evidences may be correlated to each…

The differential equations with piecewise constant argument (DEPCAs, for short) is a class of hybrid dynamical systems (combining continuous and discrete). In this paper, under the assumption that the nonlinear term is partially unbounded,…

Cantor's diagonal method is traditionally used to prove the uncountability of the set of all infinite binary sequences. This paper analyzes the expressive limits of this method. It is shown that under any constructive application --…

We use reverse mathematics to analyze "iterated jump" versions of the following four principles: the atomic model theorem with subenumerable types (AST), the diagonally noncomputable principle (DNR), weak weak K\H{o}nig's lemma (WWKL), and…

We use fast-growing finite and infinite sequences of natural numbers and more complicated constructs to define models of hypercomputation and interpret non-arithmetic predicates, with the strongest extensions reaching full second order…

Existence of long arithmetic progression in sumsets and subset sums has been studied extensively in the field of additive combinatorics. These additive combinatorics results play a central role in the recent progress of fundamental problems…

We describe a new class of positive linear discrete-time switching systems for which the problems of stability or stabilizability can be resolved constructively. This class generalizes the class of systems with independently switching state…

We provide a Kingman-like Theorem for arbitrary finite measures and a version of Birkhoff's Theorem for bounded observable. As an application, we show that Birkhoff's limit exists for some continuous observable, in an example of Bowen.

We use G\"odel's Dialectica interpretation to analyse Nash-Williams' elegant but non-constructive "minimal bad sequence" proof of Higman's Lemma. The result is a concise constructive proof of the lemma (for arbitrary decidable…

The unified correspondence theory for distributive lattice expansion logics (DLE-logics) is specialized to strict implication logics. As a consequence of a general semantic consevativity result, a wide range of strict implication logics can…

We define constructive truth for arithmetic and for intuitionistic analysis, and investigate its properties. We also prove that the set of constructively true (first order) arithmetical statements is Pi-1-2 and Sigma-1-2 hard, and we…

In this paper, we consider iterative propositional calculi, which are finite sets of propositional formulas together with the rules of modus ponens and weak substitution (when formula being substituted must be already inferred). We…

In this paper, we introduce a general family of sequent-style calculi over the modal language and its fragments to capture the essence of all constructively acceptable systems. Calling these calculi \emph{constructive}, we show that any…

We give an unified framework to solve rough differential equations. Based on flows, our approach unifies the former ones developed by Davie, Friz-Victoir and Bailleul. The main idea is to build a flow from the iterated product of an almost…

We uncover a close relationship between combinatorial and syntactic proofs for first-order logic (without equality). Whereas syntactic proofs are formalized in a deductive proof system based on inference rules, a combinatorial proof is a…

The Lovasz Local Lemma [EL75] is a powerful tool to prove the existence of combinatorial objects meeting a prescribed collection of criteria. The technique can directly be applied to the satisfiability problem, yielding that a k-CNF formula…

We generalize the validity criterion for the infinitary proof system of the multiplicative additive linear logic with fixed points. Our criterion is designed to take into account axioms and cuts. We show that it is sound and enjoys the cut…