Displaying similar documents to “Some decidable theories with finitely many covers which are decidable and algorithmically found”

Construction of sentences with specific interpretability properties

A. Stern (1993)

Fundamenta Mathematicae

Similarity:

The Rowland Institute for Science, 100 Cambridge Parkway, Cambridge, Massachusetts 02142, U.S.A. A construction is presented for generating sentences that satisfy a recursively enumerable set of interpretability properties. This construction is then used to prove three previously announced results concerning the lattice of local interpretability types of theories (also known as the Lattice of Chapters).

Strong completeness of the Lambek Calculus with respect to Relational Semantics

Szabolcs Mikulás (1993)

Banach Center Publications

Similarity:

In [vB88], Johan van Benthem introduces Relational Semantics (RelSem for short), and states Soundness Theorem for Lambek Calculus (LC) w.r.t. RelSem. After doing this, he writes: "it would be very interesting to have the converse too", i.e., to have Completeness Theorem. The same question is in [vB91, p. 235]. In the following, we state Strong Completeness Theorems for different versions of LC.

Order with successors is not interprétable in RCF

S. Świerczkowski (1993)

Fundamenta Mathematicae

Similarity:

Using the monotonicity theorem of L. van den Dries for RCF-definable real functions, and a further result of that author about RCF-definable equivalence relations on ℝ, we show that the theory of order with successors is not interpretable in the theory RCF. This confirms a conjecture by J. Mycielski, P. Pudlák and A. Stern.

Mizar Analysis of Algorithms: Algorithms over Integers

Grzegorz Bancerek (2008)

Formalized Mathematics

Similarity:

This paper is a continuation of [5] and concerns if-while algebras over integers. In these algebras the only elementary instructions are assignment instructions. The instruction assigns to a (program) variable a value which is calculated for the current state according to some arithmetic expression. The expression may include variables, constants, and a limited number of arithmetic operations. States are functions from a given set of locations into integers. A variable is a function...

Compactness and Löwenheim-Skolem properties in categories of pre-institutions

Antonino Salibra, Giuseppe Scollo (1993)

Banach Center Publications

Similarity:

The abstract model-theoretic concepts of compactness and Löwenheim-Skolem properties are investigated in the "softer" framework of pre-institutions [18]. Two compactness results are presented in this paper: a more informative reformulation of the compactness theorem for pre-institution transformations, and a theorem on natural equivalences with an abstract form of the first-order pre-institution. These results rely on notions of compact transformation, which are introduced as arrow-oriented...

Transition of Consistency and Satisfiability under Language Extensions

Julian J. Schlöder, Peter Koepke (2012)

Formalized Mathematics

Similarity:

This article is the first in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [17] for uncountably large languages. We follow the proof given in [18]. The present article contains the techniques required to expand formal languages. We prove that consistent or satisfiable theories retain these properties under changes to the language they are formulated in.