Search

This paper enriches a pre-existing decision algorithm, which in its turn augmented a fragment of Tarski’s elementary algebra with one-argument real functions endowed with continuous first derivative. In its present (still quantifier-free) version, our decidable language embodies addition of functions; the issue we address is the one of satisfiability. As regards real numbers, individual variables and constructs designating the basic arithmetic operations are available, along with comparison relators. As regards functions, we have another sort of variables, out of which compound terms are formed by means of constructs designating addition and—outermostly—differentiation. An array of predicates designate various relationships between functions, as well as function properties, that may hold over intervals of the real line; those are: function comparisons, strict and non-strict monotonicity / convexity / concavity, comparisons between the derivative of a function and a real term. With respect to results announced in earlier papers of the same stream, a significant effort went into designing the family of interpolating functions so that it could meet the new constraints stemming from the presence of function addition (along with differentiation) among the constructs of our fragment of mathematical analysis.

We recently undertook an investigation aimed at identifying small fragments of set theory (which in most cases are sublanguages of Multi-Level Syllogistic) endowed with polynomial-time satisfiability decision tests, potentially useful for automated proof verification. Leaving out of consideration the membership relator ∈ for the time being, in this note we provide a complete taxonomy of the polynomial and the NP-complete fragments involving, besides variables intended to range over the von Neumann set-universe, the Boolean operators ∪, ∩, , the Boolean relators ⊆, /⊆, =, /=, and the predicates ‘· = ∅’ and ‘Disj(·, ·)’, meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’, along with their opposites ‘· /= ∅’ and ‘¬Disj(·, ·)’.

The Davis-Putnam-Robinson theorem showed that every partially computable m-ary function f(a_1, . . . , a_m) = c on the natural numbers can be specified by means of an exponential Diophantine formula involving, along with parameters a_1, . . . , a_m, c, some number k of existentially quantified variables. Yuri Matiyasevich improved this theorem in two ways: on the one hand, he proved that the same goal can be achieved with no recourse to exponentiation and, thereby, he provided a negative answer to Hilbert's 10th problem; on the other hand, he showed how to construct an exponential Diophantine equation specifying f which, once a_1, . . . , a_m have been fixed, is solved by at most one tuple of values for the remaining variables. This latter property is called single-foldness. Whether there exists a single- (or, at worst, finite-)fold polynomial Diophantine representation of any partially computable function on the natural numbers is as yet an open problem. This work surveys relevant results on this subject and tries to draw a route towards a hoped-for positive answer to the finite-fold-ness issue.

A translation is proposed of conjunctions of literals of the forms x = y z, x /= y z, and x ∈ y, where x, y, z stand for variables ranging over the von Neumann universe of sets, into unquantified Boolean formulae of a rather simple conjunctive normal form. The formulae in the target language involve variables ranging over a Boolean field of sets, along with a difference operator and relators designating equality, non-disjointness and inclusion. Moreover, the result of each translation is a conjunction of literals of the forms x = y z, x /= y z and of implications whose antecedents are isolated literals and whose consequents are either inclusions (strict or non-strict) between variables, or equalities between variables. Besides reflecting a simple and natural semantics, which ensures satisfiability-preservation, the proposed translation has quadratic algorithmic time-complexity, and bridges two languages both of which are known to have an NP-complete satisfiability problem.

We enrich a pre-existing decision algorithm, which in its turn augmented a fragment of Tarski’s elementary algebra with one-argument functions enjoying significant properties such as continuity and differentiability. We also pave the way to further enrichments, embodying symbols to designate certain operations on functions such as pointwise addition.

Inspired by some recent revisitations of the Cantor-Bernstein theorem, in particular its formalizations in ZF carried out via the proof assistant AProS by W. Sieg and P. Walsh, we are carrying out the proof of a related graph-theoretical proposition. Our development is assisted by the proof checker ÆtnaNova, and our proof pattern is drawn from Halmos’s classic ‘Naive set theory’. This case-study illustrates the flexibility of a proof environment rooted in Set Theory, which can be bent with equal ease toward declarative and procedural styles of proof.

This paper introduces formative processes, composed by transitive partitions. Given a family F of sets, a formative process ending in the Venn partition Sigma of F is shown to exist. Sufficient criteria are also singled out for a transitive partition to model (via a function from set variables to unions of sets in the partition) all set-literals modeled by Sigma . On the basis of such criteria a procedure is designed that mimics a given formative process by another where sets have finite rank bounded by C(|Sigma|), with C a specific computable function. As a by-product, one of the core results on decidability in computable set theory is rediscovered, namely the one that regards the satisfiability of unquantified set-theoretic formulae involving Boolean operators, the singleton-former, and the powerset operator. The method described (which is able to exhibit a set-solution when the answer is affirmative) can be extended to solve the satisfiability problem for broader fragments of set theory.