A new method for obtaining lower bounds on the computational complexity of logical theories is presented. It extends widely used techniques for proving the undecidability of theories by interpreting models of a theory already known to be undecidable. New inseparability results related to the well known inseparability result of Trakhtenbrot and Vaught are the foundation of the method. Their use yields hereditary lower bounds . By means of interpretations lower bounds can be transferred from one theory to another. Complicated machine (...) codings are replaced by much simpler definability considerations, viz., the kinds of binary relations definable with short formulas on large finite sets. Numerous examples are given, including new proofs of essentially all previously known lower bounds for theories, and lower bounds for various theories of finite trees, which turn out to be particularly useful. (shrink)

In a recent paper, Montagna proved the undecidability of the first-order theory of diagonalisable algebras. This result is here refined — the set of finitely refutable sentences is shown effectively inseparable from the set of theorems. The proof is quite simple.

It has been shown recently that monodic first-order temporal logic without functional symbols but with equality is incomplete, i.e., the set of the valid formulae of this logic is not recursively enumerable. In this paper we show that an even simpler fragment consisting of monodic monadic two-variable formulae is not recursively enumerable.

The relation between logic and philosophy of science, often taken for granted, is in fact problematic. Although current fashionable criticisms of the usefulness of logic are usually mistaken, there are indeed difficulties which should be taken seriously — having to do, amongst other things, with different scientific mentalities in the two disciplines (section 1). Nevertheless, logic is, or should be, a vital part of the theory of science. To make this clear, the bulk of this paper is devoted to the (...) key notion of a scientific theory in a logical perspective. First, various formal explications of this notion are reviewed (section 2), then their further logical theory is discussed (section 3). In the absence of grand inspiring programs like those of Klein in mathematics or Hilbert in metamathematics, this preparatory ground-work is the best one can do here. The paper ends on a philosophical note, discussing applicability and merits of the formal approach to the study of science (section 4). (shrink)

The relation between logic and philosophy of science, often taken for granted, is in fact problematic. Although current fashionable criticisms of the usefulness of logic are usually mistaken, there are indeed difficulties which should be taken seriously -- having to do, amongst other things, with different "scientific mentalities" in the two disciplines. Nevertheless, logic is, or should be, a vital part of the theory of science. To make this clear, the bulk of this paper is devoted to the key notion (...) of a "scientific theory" in a logical perspective. First, various formal explications of this notion are reviewed, then their further logical theory is discussed. In the absence of grand inspiring programs like those of Klein in mathematics or Hilbert in metamathematics, this preparatory ground-work is the best one can do here. The paper ends on a philosophical note, discussing applicability and merits of the formal approach to the study of science. (shrink)

Lindström’s theorem obviously fails as a characterization of first-order logic without identity ( $\mathcal {L}_{\omega \omega }^{-} $ ). In this note, we provide a fix: we show that $\mathcal {L}_{\omega \omega }^{-} $ is a maximal abstract logic satisfying a weak form of the isomorphism property (suitable for identity-free languages and studied in [11]), the Löwenheim–Skolem property, and compactness. Furthermore, we show that compactness can be replaced by being recursively enumerable for validity under certain conditions. In the proofs, we (...) use a form of strong upwards Löwenheim–Skolem theorem not available in the framework with identity. (shrink)

In 1950, B.A. Trakhtenbrot showed that the set of first-order tautologies associated to finite models is not recursively enumerable. In 1999, P. Hájek generalized this result to the first-order versions of Łukasiewicz, Gödel and Product logics, w.r.t. their standard algebras. In this paper we extend the analysis to the first-order versions of axiomatic extensions of MTL. Our main result is the following. Let \ be a class of MTL-chains. Then the set of all first-order tautologies associated to the finite models (...) over chains in \, fTAUT\, is \ -hard. Let TAUT\ be the set of propositional tautologies of \. If TAUT\ is decidable, we have that fTAUT\ is in \. We have similar results also if we expand the language with the Δ operator. (shrink)

We say that a first order sentence A defines a graph G if A is true on G but false on any graph non-isomorphic to G. Let L ) denote the minimum length of such a sentence. We define the succinctness function s ) to be the minimum L ) over all graphs on n vertices.We prove that s and q may be so small that for no general recursive function f we can have f)≥n for all n. However, for (...) the function q*=maxi≤nq, which is the least nondecreasing function bounding q from above, we have q*=)log*n, where log*n equals the minimum number of iterations of the binary logarithm sufficient to lower n to 1 or below.We show an upper bound qshrink)

In this paper, we investigate the Lindenbaum algebra ℒ of the theory T fin = Th of the class M fin of all finite models of a finite rich signature. We prove that this algebra is an atomic Boolean algebra while its Gödel numeration γ is a [Formula: see text]-numeration. Moreover, the quotient algebra /ℱ, γ/ℱ) modulo the Fréchet ideal ℱ is a [Formula: see text]-algebra, which is universal over the class of all [Formula: see text] Boolean algebras. These conditions (...) characterize uniquely the algebra ℒ; moreover, these conditions characterize up to recursive isomorphism the numerated Boolean quotient algebra /ℱ, γ/ℱ). These results extend the work of Trakhtenbrot [17] and Vaught [18] on the first order theory of the class of all finite models of a finite rich signature. (shrink)