This paper deals with axiomatization problems for varieties of residuated meet semilattice-ordered monoids. An internal characterization of the finitely subdirectly irreducible RSs is proved, and it is used to investigate the varieties of RSs within which the finitely based subvarieties are closed under finite joins. It is shown that a variety has this closure property if its finitely subdirectly irreducible members form an elementary class. A syntactic characterization of this hypothesis is proved, and examples are discussed.

We show that the variety of residuated lattices is generated by its finite simple members, improving upon a finite model property result of Okada and Terui. The reasoning is a blend of proof-theoretic and algebraic arguments.

We exhibit a construction which produces for every Turing machine T with two halting states μ 0 and μ -1 , an algebra B(T) (finite and of finite type) with the property that the variety generated by B(T) is residually large if T halts in state μ -1 , while if T halts in state μ 0 then this variety is residually bounded by a finite cardinal.

In this paper we prove that, for n > 1, the n-generated free algebra in any locally finite subvariety of HoRA can be written in a unique nontrivial way as Ł2 × A′, where A′ is a directly indecomposable algebra in . More precisely, we prove that the unique nontrivial pair of factor congruences of is given by the filters and , where the element is recursively defined from the term introduced by W. H. Cornish. As an additional result (...) we obtain a characterization of minimal irreducible filters of in terms of its coatoms. (shrink)

We give a definition, in the ring language, of Zp inside Qp and of Fp[[t]] inside Fp), which works uniformly for all p and all finite field extensions of these fields, and in many other Henselian valued fields as well. The formula can be taken existential-universal in the ring language, and in fact existential in a modification of the language of Macintyre. Furthermore, we show the negative result that in the language of rings there does not exist a uniform (...) definition by an existential formula and neither by a universal formula for the valuation rings of all the finite extensions of a given Henselian valued field. We also show that there is no existential formula of the ring language defining Zp inside Qp uniformly for all p. For any fixed finite extension of Qp, we give an existential formula and a universal formula in the ring language which define the valuation ring. (shrink)

Given a pseudovariety [MATHEMATICAL SCRIPT CAPITAL C], it is proved that a residually-[MATHEMATICAL SCRIPT CAPITAL C] superstable group G has a finite seriesG0 ⊴ G1 ⊴ · · · ⊴ Gn = Gsuch that G0 is solvable and each factor Gi +1/Gi is in [MATHEMATICAL SCRIPT CAPITAL C] . In particular, a residually finite superstable group is solvable-by-finite, and if it is ω -stable, then it is nilpotent-by-finite. Given a finitely generated group G, we (...) show that if G is ω -stable and satisfies some residual properties , then G is finite. (shrink)

We study ultraproducts of finite residue rings \ where \ is a non-principal ultrafilter. We find sufficient conditions of the ultrafilter \ to determine if the resulting ultraproduct \ has simple, NIP, \ but not simple nor NIP, or \ theory, noting that all these four cases occur.

In this paper, we show that the finite model property fails for certain non‐integral semilinear substructural logics including Metcalfe and Montagna's uninorm logic and involutive uninorm logic, and a suitable extension of Metcalfe, Olivetti and Gabbay's pseudo‐uninorm logic. Algebraically, the results show that certain classes of bounded residuated lattices that are generated as varieties by their linearly ordered members are not generated as varieties by their finite members.

We introduce a new product bilattice con- struction that generalizes the well-known one for interlaced bilattices and others that were developed more recently, allowing to obtain a bilattice with two residuated pairs as a certain kind of power of an arbitrary residuated lattice. We prove that the class of bilattices thus obtained is a variety, give a finite axiomatization for it and characterize the congruences of its members in terms of those of their lat- tice factors. Finally, we show (...) how to employ our product construction to define first-order definable classes of bi- lattices corresponding to any first-order definable subclass of residuated lattices. (shrink)

We look at lower semilattice-ordered residuated semigroups and, in particular, the representable ones, i.e., those that are isomorphic to algebras of binary relations. We will evaluate expressions in representable algebras and give finite axiomatizations for several notions of validity. These results will be applied in the context of substructural logics.

Hoop residuation algebras are the {, 1}-subreducts of hoops; they include Hilbert algebras and the {, 1}-reducts of MV-algebras (also known as Wajsberg algebras). The paper investigates the structure and cardinality of finitely generated free algebras in varieties of k-potent hoop residuation algebras. The assumption of k-potency guarantees local finiteness of the varieties considered. It is shown that the free algebra on n generators in any of these varieties can be represented as a union of n subalgebras, each of which (...) is a copy of the {, 1}-reduct of the same finite MV-algebra, i.e., of the same finite product of linearly ordered (simple) algebras. The cardinality of the product can be determined in principle, and an inclusion-exclusion type argument yields the cardinality of the free algebra. The methods are illustrated by applying them to various cases, both known (varieties generated by a finite linearly ordered Hilbert algebra) and new (residuation reducts of MV-algebras and of hoops). (shrink)

It is proved that the variety of relevant disjunction lattices has the finite embeddability property. It follows that Avron's relevance logic RMImin has a strong form of the finite model property, so it has a solvable deducibility problem. This strengthens Avron's result that RMImin is decidable.

The aim of this paper is to show that the implicational fragment BKof the intuitionistic propositional calculus (IPC) without the rules of exchange and contraction has the finite model property with respect to the quasivariety of left residuation algebras (its equivalent algebraic semantics). It follows that the variety generated by all left residuation algebras is generated by the finite left residuation algebras. We also establish that BKhas the finite model property with respect to a class of structures (...) that constitute a Kripke-style relational semantics for it. The results settle a question of Ono and Komori [OK85]. (shrink)

We show that the equational theory of representable lattice-ordered residuated semigroups is not finitely axiomatizable. We apply this result to the problem of completeness of substructural logics.

We show that the equational theory of representable lower semilattice-ordered residuated semigroups is finitely based. We survey related results.

We investigate the provability of some properties of abelian groups and quadratic residues in variants of bounded arithmetic. Specifically, we show that the structure theorem for finite abelian groups is provable in S22 + iWPHP, and use it to derive Fermat's little theorem and Euler's criterion for the Legendre symbol in S22 + iWPHP extended by the pigeonhole principle PHP. We prove the quadratic reciprocity theorem in the arithmetic theories T20 + Count2 and I Δ0 + Count2 with modulo-2 (...) counting principles. (shrink)

A quasivariety of algebras has the joint embedding property (JEP) if and only if it is generated by a single algebra A. It is structurally complete if and only if the free ℵ0‐generated algebra in can serve as A. A consequence of this demand, called ‘passive structural completeness’ (PSC), is that the nontrivial members of all satisfy the same existential positive sentences. We prove that if is PSC then it still has the JEP, and if it has the JEP and (...) its nontrivial members lack trivial subalgebras, then its relatively simple members all belong to the universal class generated by one of them. Under these conditions, if is relatively semisimple then it is generated by one ‐simple algebra. We also prove that a quasivariety of finite type, with a finite nontrivial member, is PSC if and only if its nontrivial members have a common retract. The theory is then applied to the variety of De Morgan monoids, where we isolate the sub(quasi)varieties that are PSC and those that have the JEP, while throwing fresh light on those that are structurally complete. The results illuminate the extension lattices of intuitionistic and relevance logics. (shrink)

Over the past 50 years, Nelson algebras have been extensively studied by distinguished scholars as the algebraic counterpart of Nelson's constructive logic with strong negation. Despite these studies, a comprehensive survey of the topic is currently lacking, and the theory of Nelson algebras remains largely unknown to most logicians. This paper aims to fill this gap by focussing on the essential developments in the field over the past two decades. Additionally, we explore generalisations of Nelson algebras, such as N4-lattices which (...) correspond to the paraconsistent version of Nelson's logic, as well as their applications to other areas of interest to logicians, such as duality and rough set theory. A general representation theorem states that each Nelson algebra is isomorphic to a subalgebra of a rough set-based Nelson algebra induced by a quasiorder. Furthermore, a formula is a theorem of Nelson logic if and only if it is valid in every finite Nelson algebra induced by a quasiorder. (shrink)

For odd and for even involutive, commutative residuated chains a representation theorem is presented in this paper by means of direct systems of abelian o-groups equipped with further structure. This generalizes the corresponding result of J. M. Dunnabout finite Sugihara monoids.

Given a positive universal formula in the language of residuated lattices, we construct a recursive basis of equations for a variety, such that a subdirectly irreducible residuated lattice is in the variety exactly when it satisfies the positive universal formula. We use this correspondence to prove, among other things, that the join of two finitely based varieties of commutative residuated lattices is also finitely based. This implies that the intersection of two finitely axiomatized substructural logics over FL + is also (...) finitely axiomatized. Finally, we give examples of cases where the join of two varieties is their Cartesian product. (shrink)

We solve several open problems on the cardinality of atoms in the subvariety lattice of residuated lattices and FL-algebras [4, Problems 17—19, pp. 437]. Namely, we prove that the subvariety lattice of residuated lattices contains continuum many 4-potent commutative representable atoms. Analogous results apply also to atoms in the subvariety lattice of FL i -algebras and FL o -algebras. On the other hand, we show that the subvariety lattice of residuated lattices contains only five 3-potent commutative representable atoms and two (...) integral commutative representable atoms. Inspired by the construction of atoms, we are also able to prove that the variety of integral commutative representable residuated lattices is generated by its 1-generated finite members. (shrink)

We present numerous natural algebraic examples without the so-called Canonical Base Property (CBP). We prove that every commutative unitary ring of finite Morley rank without finite-index proper ideals satisfies the CBP if and only if it is a field, a ring of positive characteristic or a finite direct product of these. In addition, we construct a CM-trivial commutative local ring with a finite residue field without the CBP. Furthermore, we also show that finite-dimensional non-associative algebras (...) over an algebraically closed field of characteristic [Formula: see text] give rise to triangular rings without the CBP. This also applies to Baudisch’s [Formula: see text]-step nilpotent Lie algebras, which yields the existence of a [Formula: see text]-step nilpotent group of finite Morley rank whose theory, in the pure language of groups, is CM-trivial and does not satisfy the CBP. (shrink)

Hahn’s embedding theorem asserts that linearly ordered abelian groups embed in some lexicographic product of real groups. Hahn’s theorem is generalized to a class of residuated semigroups in this paper, namely, to odd involutive commutative residuated chains which possess only finitely many idempotent elements. To this end, the partial lexicographic product construction is introduced to construct new odd involutive commutative residuated lattices from a pair of odd involutive commutative residuated lattices, and a representation theorem for odd involutive commutative residuated chains (...) which possess only finitely many idempotent elements, by means of linearly ordered abelian groups and the partial lexicographic product construction is presented. (shrink)

We construct a family $\fancyscript{F}$ , indexed by five integer parameters, of finite monogenerated left-distributive (LD) groupoids with the property that every finite monogenerated LD groupoid is a quotient of a member of $\fancyscript{F}$ . The combinatorial abundance of finite monogenerated LD groupoids is encoded in the congruence lattices of the groupoids $\fancyscript{F}$ , which we show to be extremely large.

We consider a modal language over crisp frames and formulas evaluated on a finite MTL-chain (a linearly ordered commutative integral residuated lattice). We first show that the basic modal abstract logic with constants for the values of the MTL-chain is the maximal abstract logic satisfying Compactness, the Tarski Union Property and strong invariance for bisimulations. Finally, we improve this result by replacing the Tarski Union Property by a relativization property.

When [Formula: see text] is a finite field, [J. Becker, J. Denef and L. Lipshitz, Further remarks on the elementary theory of formal power series rings, in Model Theory of Algebra and Arithmetic, Proceedings Karpacz, Poland, Lecture Notes in Mathematics, Vol. 834 (Springer, Berlin, 1979)] observed that the total residue map [Formula: see text], which picks out the constant term of the Laurent series, is definable in the language of rings with a parameter for [Formula: see text]. Driven by (...) this observation, we study the theory [Formula: see text] of valued fields equipped with a linear form [Formula: see text] which restricts to the residue map on the valuation ring. We prove that [Formula: see text] does not admit a model companion. In addition, we show that [Formula: see text] is undecidable whenever [Formula: see text] is an infinite field. As a consequence, we get that [Formula: see text] is undecidable, where [Formula: see text] maps [Formula: see text] to its complex residue at [Formula: see text]. (shrink)

We prove the Finite Model Property (FMP) for Distributive Full Lambek Calculus ( DFL ) whose algebraic semantics is the class of distributive residuated lattices ( DRL ). The problem was left open in [8, 5]. We use the method of nuclei and quasi–embedding in the style of [10, 1].

The article presents proofs of the context freeness of a family of typelogical grammars, namely all grammars that are based on a uni- ormultimodal logic of pure residuation, possibly enriched with thestructural rules of Permutation and Expansion for binary modes.

Dynamic algebras combine the classes of Boolean (B 0) and regular (R ; *) algebras into a single finitely axiomatized variety (B R ) resembling an R-module with scalar multiplication . The basic result is that * is reflexive transitive closure, contrary to the intuition that this concept should require quantifiers for its definition. Using this result we give several examples of dynamic algebras arising naturally in connection with additive functions, binary relations, state trajectories, languages, and flowcharts. The main result (...) is that free dynamic algebras are residually finite (i.e. factor as a subdirect product of finite dynamic algebras), important because finite separable dynamic algebras are isomorphic to Kripke structures. Applications include a new completeness proof for the Segerberg axiomatization of prepositional dynamic logic, and yet another notion of regular algebra. (shrink)

We prove that any torsion-free, residually finite relatively free group of infinite rank is not \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\aleph_1}$$\end{document} -homogeneous. This generalizes Sklinos’ result that a free group of infinite rank is not \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\aleph_1}$$\end{document} -homogeneous, and, in particular, gives a new simple proof of that result.

In this paper we prove that the equational class generated by bounded BCK-algebras is the variety generated by the class of finite simple bounded BCK-algebras. To obtain these results we prove that every simple algebra in the equational class generated by bounded BCK-algebras is also a relatively simple bounded BCK-algebra. Moreover, we show that every simple bounded BCK-algebra can be embedded into a simple integral commutative bounded residuated lattice. We extend our main results to some richer subreducts of the (...) class of integral commutative bounded residuated lattices and to the involutive case. (shrink)

All known structural extensions of the substructural logic $\textbf{FL}_{\textbf{e}}$, the Full Lambek calculus with exchange/commutativity (corresponding to subvarieties of commutative residuated lattices axiomatized by $\{\vee, \cdot, 1\}$ -equations), have decidable theoremhood; in particular all the ones defined by knotted axioms enjoy strong decidability properties (such as the finite embeddability property). We provide infinitely many such extensions that have undecidable theoremhood, by encoding machines with undecidable halting problem. An even bigger class of extensions is shown to have undecidable deducibility problem (...) (the corresponding varieties of residuated lattices have undecidable word problem); actually with very few exceptions, such as the knotted axioms and the other prespinal axioms, we prove that undecidability is ubiquitous. Known undecidability results for non-commutative extensions use an encoding that fails in the presence of commutativity, so and-branching counter machines are employed. Even these machines provide encodings that fail to capture proper extensions of commutativity, therefore we introduce a new variant that works on an exponential scale. The correctness of the encoding is established by employing the theory of residuated frames. (shrink)

The current literature that attempts to bridge between geometric morphometrics (GMM) and finite element analyses (FEA) of CT-derived data from bones of living animals and fossils appears to lack a sound biotheoretical foundation. To supply the missing rigor, the present article demonstrates a new rhetoric of quantitative inference across the GMM–FEA bridge—a rhetoric bridging form to function when both have been quantified so stringently. The suggested approach is founded on diverse standard textbook examples of the relation between forms and (...) the way strains in them are produced by stresses imposed upon them. One potentially cogent approach to the explanatory purposes driving studies of this class arises from a close scrutiny of the way in which computations in both domains, shape and strain, can be couched as minimizations of a scalar quantity. For GMM, this is ordinary Procrustes shape distance; in FEA, it is the potential energy that is stored in the deformed configuration of the solid form. A hybrid statistical method is introduced requiring that all forms be subjected to the same detailed loading designs (the same “probes”) in a manner careful to accommodate the variations of those same forms before they were stressed. The proper role of GMM is argued to be the construction of regressions for strain energy density on the largest-scale relative warps in order that biological explanations may proceed in terms of the residuals from those regressions: the local residual features of strain energy density. The method, evidently a hierarchical one, might be intuitively apprehended as a geometrical approach to a formal allometric analysis of strain. The essay closes with an exhortation. (shrink)

For arbitrary finite group $G$ and countable Dedekind domain $R$ such that the residue field $R/P$ is finite for every maximal $R$ -ideal $P$ , we show that the localizations at every maximal ideal of two $RG$ -lattices are isomorphic if and only if the two lattices satisfy the same first order sentences. Then we investigate generalizations of the above results to arbitrary $R$ -torsion-free $RG$ -modules and we apply the previous results to show the decidability of the (...) theory of ${\vec Z}C(2)^2$ -lattices. Eventually, we show that ${\vec Z} [i] C(2)^2$ -lattices have undecidable theory. (shrink)

Monoidal t-norm based logic $\mathbf {MTL}$ is the weakest t-norm based residuated fuzzy logic, which is a $[0,1]$ -valued propositional logical system having a t-norm and its residuum as truth function for conjunction and implication. Monadic fuzzy predicate logic $\mathbf {mMTL\forall }$ that consists of the formulas with unary predicates and just one object variable, is the monadic fragment of fuzzy predicate logic $\mathbf {MTL\forall }$, which is indeed the predicate version of monoidal t-norm based logic $\mathbf {MTL}$. The main (...) aim of this paper is to give an algebraic proof of the completeness theorem for monadic fuzzy predicate logic $\mathbf {mMTL\forall }$ and some of its axiomatic extensions. Firstly, we survey the axiomatic system of monadic algebras for t-norm based residuated fuzzy logic and amend some of them, thus showing that the relationships for these monadic algebras completely inherit those for corresponding algebras. Subsequently, using the equivalence between monadic fuzzy predicate logic $\mathbf {mMTL\forall }$ and S5-like fuzzy modal logic $\mathbf {S5(MTL)}$, we prove that the variety of monadic MTL-algebras is actually the equivalent algebraic semantics of the logic $\mathbf {mMTL\forall }$, giving an algebraic proof of the completeness theorem for this logic via functional monadic MTL-algebras. Finally, we further obtain the completeness theorem of some axiomatic extensions for the logic $\mathbf {mMTL\forall }$, and thus give a major application, namely, proving the strong completeness theorem for monadic fuzzy predicate logic based on involutive monoidal t-norm logic $\mathbf {mIMTL\forall }$ via functional representation of finitely subdirectly irreducible monadic IMTL-algebras. (shrink)

A full separation theorem for the derivable rules of intuitionistic linear logic without bounds, 0 and exponentials is proved. Several structural consequences of this theorem for subreducts of (commutative) residuated lattices are obtained. The theorem is then extended to the logic LR+ and its proof is extended to obtain the finite embeddability property for the class of square increasing residuated lattices.

We develop a general algebraic and proof-theoretic study of substructural logics that may lack associativity, along with other structural rules. Our study extends existing work on substructural logics over the full Lambek Calculus [34], Galatos and Ono [18], Galatos et al. [17]). We present a Gentzen-style sequent system that lacks the structural rules of contraction, weakening, exchange and associativity, and can be considered a non-associative formulation of . Moreover, we introduce an equivalent Hilbert-style system and show that the logic associated (...) with and is algebraizable, with the variety of residuated lattice-ordered groupoids with unit serving as its equivalent algebraic semantics. Overcoming technical complications arising from the lack of associativity, we introduce a generalized version of a logical matrix and apply the method of quasicompletions to obtain an algebra and a quasiembedding from the matrix to the algebra. By applying the general result to specific cases, we obtain important logical and algebraic properties, including the cut elimination of and various extensions, the strong separation of , and the finite generation of the variety of residuated lattice-ordered groupoids with unit. (shrink)

We extend the characterization of extremal valued fields given in [2] to the missing case of valued fields of mixed characteristic with perfect residue field. This leads to a complete characterization of the tame valued fields that are extremal. The key to the proof is a model theoretic result about tame valued fields in mixed characteristic. Further, we prove that in an extremal valued field of finitep-degree, the images of all additive polynomials have the optimal approximation property. This fact can (...) be used to improve the axiom system that is suggested in [8] for the elementary theory of Laurent series fields over finite fields. Finally we give examples that demonstrate the problems we are facing when we try to characterize the extremal valued fields with imperfect residue fields. To this end, we describe several ways of constructing extremal valued fields; in particular, we show that in every ℵ1saturated valued field the valuation is a composition of extremal valuations of rank 1. (shrink)

A full separation theorem for the derivable rules of intuitionistic linear logic without bounds, 0 and exponentials is proved. Several structural consequences of this theorem for subreducts of (commutative) residuated lattices are obtained. The theorem is then extended to the logic LR+ and its proof is extended to obtain the finite embeddability property for the class of square increasing residuated lattices.

In this paper we prove that the equational class generated by bounded BCK-algebras is the variety generated by the class of finite simple bounded BCK-algebras. To obtain these results we prove that every simple algebra in the equational class generated by bounded BCK-algebras is also a relatively simple bounded BCK-algebra. Moreover, we show that every simple bounded BCK-algebra can be embedded into a simple integral commutative bounded residuated lattice. We extend our main results to some richer subreducts of the (...) class of integral commutative bounded residuated lattices and to the involutive case. (© 2007 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim). (shrink)

Action logic of Pratt [21] can be presented as Full Lambek Calculus FL [14, 17] enriched with Kleene star *; it is equivalent to the equational theory of residuated Kleene algebras (lattices). Some results on axiom systems, complexity and models of this logic were obtained in [4, 3, 18]. Here we prove a stronger form of *-elimination for the logic of *-continuous action lattices and the –completeness of the equational theories of action lattices of subsets of a finite monoid (...) and action lattices of binary relations on a finite universe. We also discuss possible applications in linguistics. (shrink)

The Soul is considered, both for religions and philosophy, to be the immaterial aspect or essence of a human being, conferring individuality and humanity, often considered to be synonymous with the mind or the self. For most theologies, the Soul is further defined as that part of the individual, which partakes of divinity and transcends the body in different explanations. But, regardless of the philosophical background in which a specific theology gives the transcendence of the soul as the source of (...) its everlasting essence – often considered to survive the death of the body –, it is always appraised as a higher existence for which all should fight for. In this regard, all religious beliefs assert that there are many unseen battles aiming to take hold of the human soul, either between divinity and evil, or between worlds, or even between the body and the soul itself. These unseen battles over the human soul raging in the whole world made it the central item of the entire universe, both for the visible and the unseen worlds, an item of which whoever takes possession will also become the ruler of the universe. Through this philosophy, the value of the soul became abysmal, incommensurable, and without resemblance. The point for making such a broad overview of the soul in religious beliefs is the question of whether we can build an interfaith discourse based on the religions’ most debated and valuable issue, soul? Regardless of the variety of religious beliefs on what seems to be the soul, there is always a residual consideration in them that makes the soul more important than the body. This universal impression is due to another belief or instead need of believing that above and beyond this seen, palpable, finite life and the world should exist another one, infinite, transcendent, and available all the same after here. This variety stretches from the minimum impact that soul has on the body, as being the superior essence that inhabitants and enlivens the matter, to the highest impact in which soul has nothing to do with matter[1] and is only ephemeral linked to it, but its existence is not at all limited, defined or depended on the matter [2], or even placed to the extreme, as the very life of the matter thus this seen universe is merely a thought in the soul/mind [3]. In this extensive variety of soul overviews, the emphasis of the soul’s importance gives an inverse significance to the body/matter, from being everything that matters to a thin, dwindle item that has no existence at all outside consciousness. (shrink)

Modus ponens provides the central theme. There are laws, of the form A→C. A logic L collects such laws. Any datum A provides input to the laws of L. The central ternary relation R relates theories L,T and U, where U consists of all of the outputs C got by applying modus ponens to major premises from L and minor premises from T. Underlying this relation is a modus ponens product operation on theories L and T, whence RLTU iff LTU. (...) These ideas have been expressed, especially with Routley, as worlds semantics for relevant and other substructural logics.Worlds are best demythologized as theories, subject to truth-functional and other constraints. The chief constraint is that theories are taken as closed under logical entailment, which clearly begs the question if we are using the semantics to determine which theory L is Logic itself. Instead we draw the modal logicians’ conclusion—there are many substructural logics, each with its appropriate ternary relational postulates.Each logic L gives rise to a Calculus of L-theories, on which particular candidate logical axioms have the combinatorial properties expected from the well-known Curry–Howard isomorphism . We apply their bubbling lemma, updating the Fools Model of Combinatory Logic at the pure → level for the system BT. We make fusion an explicit connective, proving a combinator correspondence theorem. Having taken relevant → as a left residual for , we explore its right residual mate →r. Finally we concentrate on and prove a finite model property for the classical minimal relevant logic CB, a conservative extension of the minimal positive relevant logic B+. (shrink)

The class of all Artinian local rings of length at most l is ∀ 2 -elementary, axiomatised by a finite set of axioms Art l . We show that its existentially closed models are Gorenstein, of length exactly l and their residue fields are algebraically closed, and, conversely, every existentially closed model is of this form. The theory Got l of all Artinian local Gorenstein rings of length l with algebraically closed residue field is model complete and the theory (...) Art l is companionable, with model-companion Got l. (shrink)

In this paper, some novel analytical and numerical techniques are introduced for solving and analyzing nonlinear second-order ordinary differential equations that are associated to some strongly nonlinear oscillators such as a quadratically damped pendulum equation. Two different analytical approximations are obtained: for the first approximation, the ansatz method with the help of Chebyshev approximate polynomial is employed to derive an approximation in the form of trigonometric functions. For the second analytical approximation, a novel hybrid homotopy with Krylov–Bogoliubov–Mitropolsky method is introduced (...) for the first time for analyzing the evolution equation. For the numerical approximation, both the finite difference method and Galerkin method are presented for analyzing the strong nonlinear quadratically damped pendulum equation that arises in real life, such as nonlinear phenomena in plasma physics, engineering, and so on. Several examples are discussed and compared to the Runge–Kutta numerical approximation to investigate and examine the accuracy of the obtained approximations. Moreover, the accuracy of all obtained approximations is checked by estimating the maximum residual and distance errors. (shrink)

The monoidal t-norm based logic MTL is obtained from Hájek's Basic Fuzzy logic BL by dropping the divisibility condition for the strong (or monoidal) conjunction. Recently, Jenei and Montgana have shown MTL to be standard complete, i.e. complete with respect to the class of residuated lattices in the real unit interval [0,1] defined by left-continuous t-norms and their residua. Its corresponding algebraic semantics is given by pre-linear residuated lattices. In this paper we address the issue of standard and rational completeness (...) (rational completeness meaning completeness with respect to a class of algebras in the rational unit interval [0,1]) of some important axiomatic extensions of MTL corresponding to well-known parallel extensions of BL. Moreover, we investigate varieties of MTL algebras whose linearly ordered countable algebras embed into algebras whose lattice reduct is the real and/or the rational interval [0,1]. These embedding properties are used to investigate finite strong standard and/or rational completeness of the corresponding logics. (shrink)