De Rijke introduced a unary interpretability logic $$\textbf{il}$$, and proved that $$\textbf{il}$$ is the unary counterpart of the binary interpretability logic $$\textbf{IL}$$. In this paper, we find the unary counterparts of the sublogics of $$\textbf{IL}$$.

A unary algebra is an algebraic system A = , where ƒ 0 ,…,ƒ n are unary operations on A and n ∈ ω. In the paper we develop the theory of effective unary algebras. We investigate well-known questions of constructive model theory with respect to the class of unary algebras. In the paper we construct unary algebras with a finite number of recursive isomorphism types. We give the notions of program, uniform, and algebraic dimensions (...) of models, and then we investigate these notions on unary algebras. We find connections between algebraic and effective properties of r.e. representable unary algebras. We also deal with finitely generated r.e. unary algebras. We show the connections between trees and unary algebras. Our interests also concern recursive automorphisms groups, r.e. subalgebra and congruence lattices of effective unary algebras. (shrink)

We shall investigate certain statements concerning the rigidity of unary functions which have connections with forms of the axiom of choice.

In this article, we study some new characterizations of primitive recursive functions based on restricted forms of primitive recursion, improving the pioneering work of R. M. Robinson and M. D. Gladstone. We reduce certain recursion schemes (mixed/pure iteration without parameters) and we characterize one-argument primitive recursive functions as the closure under substitution and iteration of certain optimal sets.

In this paper (except in Section 5) all quantifiers are assumedto be so called simple unaryquantifiers, and all models are assumedto be finite. We give a necessary and sufficientcondition for a quantifier to be definablein terms of monotone quantifiers. For amonotone quantifier we give a necessaryand sufficient condition for beingdefinable in terms of a given set of bounded monotonequantifiers. Finally, we give a necessaryand sufficient condition for a monotonequantifier to be definable in terms of agiven monotone quantifier.Our analysis shows that (...) the quantifierat least one half and its relatives behavedifferently than other monotone quantifiers. (shrink)

It is well known that most is not first-order definable, and that the proof is in Barwise and Cooper’s 1981 paper. Actually, Barwise and Cooper present two theorems that bear on the issue. Their theorem C12 says that, for any pair of one-place predicates A and B, there is no sentence of classical predicate logic that is true iff ‘Most A are B’ is. (I assume that ‘Most A are B’ means that more than half of the A’s are B, (...) but the only thing that matters is that most is proportional.) Barwise and Cooper’s C13 states that the foregoing result remains valid when classical logic is enriched with a unary quantifier Q so defined that Qx(Ax) is true iff more than half of the entities in the domain of quantification are A’s. (shrink)

It was shown in the previous work of the author that one can avoid the paradox of minimal logic { ϕ , ¬ ϕ } ¬ ψ defining the negation operator via reduction not a constant of absurdity, but to a unary operator of absurdity. In the present article we study in details what does it mean that negation in a logical system can be represented via an absurdity or contradiction operator. We distinguish different sorts of such presentations. Finally, (...) we consider the possibility to represent the negation via absurdity and contradiction operators in such well known systems of paraconsistent logic as D.Batens's logic CLuN and Sette's logic P 1. (shrink)

Iterative characterizations of computable unary functions are useful patterns for the definition of programming languages based on iterative constructs. The features of such a characterization depend on the pairing producing it: this paper offers an infinite class of pairings involving very nice features.

The set of unary functions of complexity classes defined by using bounded primitive recursion is inductively characterized by means of bounded iteration. Elementary unary functions, linear space computable unary functions and polynomial space computable unary functions are then inductively characterized using only composition and bounded iteration.

We determine precisely those locally finite varieties of unary algebras of finite type which, when augmented by a ternary discriminator, generate a variety with a decidable theory.

Standard unary modal logic and binary modal logic, i.e. modal logic with one binary operator, are shown to be definitional extensions of one another when an additional axiom |$U$| is added to the basic axiomatization of the binary side. This is a strengthening of our previous results. It follows that all unary modal logics extending Classical Modal Logic, in other words all unary modal logics with a neighborhood semantics, can equivalently be seen as binary modal logics. This (...) in particular applies to standard modal logics, which can be given simple natural axiomatizations in binary form. We illustrate this in the logic K. We call such logics binary expansions of the unary modal logics. There are many more such binary expansions than the ones given by the axiom |$U$|⁠. We initiate an investigation of the properties of these expansions and in particular of the maximal binary expansions of a logic. Our results directly imply that all sub- and superintuitionistic logics with a standard modal companion also have binary modal companions. The latter also applies to the weak subintuitionistic logic WF of our previous papers. This logic doesn’t seem to have a unary modal companion. (shrink)

The expressive truth functions of two-valued logic have all been identified. This paper begins the task of identifying the expressive truth functions of n-valued logic by characterizing the unary ones. These functions have distinctive algebraic, semantic, and closure-theoretic properties.

Programming practice suggests a notion of general iteration corresponding to the while-do construct. This leads to new characterizations of general computable unary functions usable in computer science.

It is well known that in any nonstandard model of $\mathsf{PA}$ (Peano arithmetic) neither addition nor multiplication is recursive. In this paper we focus on the recursiveness of unary functions and find several pairs of unary functions which cannot be both recursive in the same nonstandard model of $\mathsf{PA}$ (e.g., $\{2x,2x+1\}$, $\{x^2,2x^2\}$, and $\{2^x,3^x\}$). Furthermore, we prove that for any computable injection $f(x)$, there is a nonstandard model of $\mathsf{PA}$ in which $f(x)$ is recursive.

We give a simple proof characterizing the complexity of Presburger arithmetic augmented with additional predicates. We show that Presburger arithmetic with additional predicates is Π 1 1 complete. Adding one unary predicate is enough to get Π 1 1 hardness, while adding more predicates (of any arity) does not make the complexity any worse.

In the first part of this paper (Méndez and Robles 2008) a minimal and an intuitionistic negation is introduced in a wide spectrum of relevance logics extending Routley and Meyer's basic positive logic B+. It is proved that although all these logics have the characteristic paradoxes of consistency, they lack the K rule (and so, the K axiom). Negation is introduced with a propositional falsity constant. The aim of this paper is to build up logics definitionally equivalent to those in (...) the aforementioned paper, negation being now introduced with the unary connective. Relational ternary semantics are provided for the new logics and soundness and completeness results are proved. (shrink)

Consider a language SL having as its primitive signs one or more atomic statements, the two connectives ‘∼’ and ‘&,’ and the two parentheses ‘’; and presume the extra connectives ‘V’ and ‘≡’ defined in the customary manner. With the statements of SL substituting for sets, and the three connectives ‘∼,’ ‘&,’and ‘V’ substituting for the complementation, intersection, and union signs, the constraints that Kolmogorov places in [1] on probability functions come to read:K1. 0 ≤ P,K2. P) = 1,K3. If (...) ⊦ ∼, then P = P + P,K4. If ⊦ A ≡ B, then P = P.2. (shrink)

Vectorization of a class of structures is a natural notion in finite model theory. Roughly speaking, vectorizations allow tuples to be treated similarly to elements of structures. The importance of vectorizations is highlighted by the fact that if the complexity class PTIME corresponds to a logic with reasonable syntax, then it corresponds to a logic generated via vectorizations by a single generalized quantifier (Dawar in J Log Comput 5(2):213–226, 1995). It is somewhat surprising, then, that there have been few systematic (...) studies of the expressive power of vectorizations of various quantifiers. In the present paper, we consider the simplest case: the cardinality quantifiers C S. We show that, in general, the expressive power of the vectorized quantifier logic $${{\rm FO}(\{{\mathsf C}_S^{(n)}\, | \, n \in \mathbb{Z}_+\})}$$ is much greater than the expressive power of the non-vectorized logic FO(C S ). (shrink)

We carry out a study of definability issues in the standard models of Presburger and Skolem arithmetics (henceforth referred to simply as Presburger and Skolem arithmetics, for short, because we only deal with these models, not the theories, thus there is no risk of confusion) supplied with free unary predicates—which are strongly related to definability in the monadic SOA (second-order arithmetic) without × or + , respectively. As a consequence, we obtain a very direct proof for ${\Pi^1_1}$ -completeness of (...) Presburger, and also Skolem, arithmetic with a free unary predicate, generalize it to all ${\Pi^1_n}$ -levels, and give an alternative description of the analytical hierarchy without × or + . Here ‘direct’ means that one explicitly m-reduces the truth of ${\Pi^1_1}$ -formulae in SOA to the truth in the extended structures. Notice that for the case of Presburger arithmetic, the ${\Pi^1_1}$ -completeness was already known, but the proof was indirect and exploited some special ${\Pi^1_1}$ -completeness results on so-called recurrent nondeterministic Turing machines—for these reasons, it was hardly able to shed any light on definability issues or possible generalizations. (shrink)

We prove a local normal form theorem of the Gaifman type for the infinitary logic L∞ωω whose formulas involve arbitrary unary quantifiers but finite quantifier rank. We use a local Ehrenfeucht-Fraïssé type game similar to the one in [9]. A consequence is that every sentence of L∞ωω of quantifier rank n is equivalent to an infinite Boolean combination of sentences of the form ψ, where ψ has counting quantifiers restricted to the -neighborhood of y.

A subset A $\subseteq$ M of a totally ordered structure M is said to be convex, if for any a, b $\in A: [a . A complete theory of first order is weakly o-minimal (M. Dickmann [D]) if any model M is totally ordered by some $\emptyset$ -definable formula and any subset of M which is definable with parameters from M is a finite union of convex sets. We prove here that for any model M of a weakly o-minimal theory (...) T, any expansion M + of M by a family of unary predicates has a weakly o-minimal theory iff the set of all realizations of each predicate is a union of a finite number of convex sets (Theorem 63), that solves the Problem of Cherlin-Macpherson-Marker-Steinhorn [MMS] for the class of weakly o-minimal theories. (shrink)

In many-valued logic the decision of functional completeness is a basic and important problem, and the thorough solution to this problem depends on determining all maximal closed sets in the set of many-valued logic functions. It includes three famous problems, i.e., to determine all maximal closed sets in the set of the total, of the partial and of the unary many-valued logic functions, respectively. The first two problems have been completely solved , and the solution to the third problem (...) boils down to determining all maximal subgroups in the k-degree symmetric group Sk, which is an open problem in the finite group theory. In this paper, all maximal closed sets in the set of unary p-valued logic functions are determined, where p is a prime. (shrink)

Motivated by problems that arise in computing degrees of belief, we consider the problem of computing asymptotic conditional probabilities for first-order sentences. Given first-order sentences φ and θ, we consider the structures with domain {1,..., N} that satisfy θ, and compute the fraction of them in which φ is true. We then consider what happens to this fraction as N gets large. This extends the work on 0-1 laws that considers the limiting probability of first-order sentences, by considering asymptotic conditional (...) probabilities. As shown by Liogon'kii [24], if there is a non-unary predicate symbol in the vocabulary, asymptotic conditional probabilities do not always exist. We extend this result to show that asymptotic conditional probabilities do not always exist for any reasonable notion of limit. Liogon'kii also showed that the problem of deciding whether the limit exists is undecidable. We analyze the complexity of three problems with respect to this limit: deciding whether it is well-defined, whether it exists, and whether it lies in some nontrivial interval. Matching upper and lower bounds are given for all three problems, showing them to be highly undecidable. (shrink)

We prove a local normal form theorem of the Gaifman type for the infinitary logic L∞ωω whose formulas involve arbitrary unary quantifiers but finite quantifier rank. We use a local Ehrenfeucht-Fraïssé type game similar to the one in [9]. A consequence is that every sentence of L∞ωω of quantifier rank n is equivalent to an infinite Boolean combination of sentences of the form ψ, where ψ has counting quantifiers restricted to the -neighborhood of y.

The first-order logical theory Th $({\mathbb{N}},x + 1,F(x))$ is proved to be complete for the class ATIME-ALT $(2^{O(n)},O(n))$ when $F(x) = 2^{x}$ , and the same result holds for $F(x) = c^{x}, x^{c} (c \in {\mathbb{N}}, c \ge 2)$ , and F(x) = tower of x powers of two. The difficult part is the upper bound, which is obtained by using a bounded Ehrenfeucht–Fraïssé game.

We study the class of structures formed by all the polygons over a given monoid, which is equivalent to the study of the varieties in a language containing only unary functions. We collect and amplify previous results concerning their stability and superstability. Then we characterize the regular monoids for which all these polygons are ω-stable; the question about the existence of a non regular monoid with this property is left open.

We define some variations of the Scott rank for countable models and obtain some inequalities involving the ranks. For mono-unary algebras we prove that the game rank of any subtree does not exceed the game rank of the whole model. However, similar questions about linear orders remain unresolved.

We investigate certain statements about factors of unary functions which have connections with weak forms of the axiom of choice. We discuss more extensively the fine structure of Howard and Rubin's Form 314 from [4]. Some of our set-theoretic results have also interesting recursive versions.

Features are unary operators used to build record-like expressions. The resulting term algebras are encountered in linguistic computation and knowledge representation. We present a general description of feature logic and of a slightly restricted version, called record logic. It is shown that every first-order theory can be faithfully interpreted in a record logic with various additional axioms. This fact is used elsewhere [15] to extend a result of Tarski and Givant [14] on expressing first order theories in relation algebra.

In this introduction to the special issue “40 years of FDE”, we offer an overview of the field and put the papers included in the special issue into perspective. More specifically, we first present various semantics and proof systems for FDE, and then survey some expansions of FDE by adding various operators starting with constants. We then turn to unary and binary connectives, which are classified in a systematic manner. First-order FDE is also briefly revisited, and we conclude by (...) listing some open problems for future research. (shrink)