The finite embeddability property for some noncommutative knotted extensions of FL

Mapping Intimacies ◽

10.29007/vqt7 ◽

2018 ◽

Author(s):

Riquelmi Cardona

Keyword(s):

Residuated Lattices ◽

Finite Model ◽

Structural Rule ◽

Model Property ◽

Finite Model Property ◽

Finite Embeddability Property ◽

Commutativity Property ◽

Weaker Conditions ◽

Full Algebra

We consider the knotted structural rule xm≤xn for n different than m and m greater or equal than 1. Previously van Alten proved that commutative residuated lattices that satisfy the knotted rule have the finite embeddability property (FEP). Namely, every finite partial subalgebra of an algebra in the class can be embedded into a finite full algebra in the class. In our work we replace the commutativity property by some slightly weaker conditions. Particularly, we prove the FEP for the variety of residuated lattices that satisfy the equation xyx=x2y and the knotted rule. Furthermore, we investigate some generalizations of this noncommutative property by working with equations that allow us to move variables. We also note that the FEP implies the finite model property. Hence the logics modeled by these residuated lattices are decidable.

Download Full-text

The finite model property for knotted extensions of propositional linear logic

Journal of Symbolic Logic ◽

10.2178/jsl/1107298511 ◽

2005 ◽

Vol 70 (1) ◽

pp. 84-98 ◽

Cited By ~ 9

Author(s):

C. J. van Alten

Keyword(s):

Linear Logic ◽

Finite Model ◽

Algebraic Semantics ◽

Structural Rule ◽

Model Property ◽

Algebraic Models ◽

Finite Model Property ◽

Finite Embeddability Property ◽

Full Algebra ◽

Intuitionistic Linear Logic

AbstractThe logics considered here are the propositional Linear Logic and propositional Intuitionistic Linear Logic extended by a knotted structural rule: . It is proved that the class of algebraic models for such a logic has the finite embeddability property, meaning that every finite partial subalgebra of an algebra in the class can be embedded into a finite full algebra in the class. It follows that each such logic has the finite model property with respect to its algebraic semantics and hence that the logic is decidable.

Download Full-text

The finite embeddability property for noncommutative knotted extensions of RL

International Journal of Algebra and Computation ◽

10.1142/s0218196715500010 ◽

2015 ◽

Vol 25 (03) ◽

pp. 349-379 ◽

Cited By ~ 1

Author(s):

R. Cardona ◽

N. Galatos

Keyword(s):

Classical Logic ◽

Proof Theory ◽

Mathematical Linguistics ◽

Residuated Lattices ◽

Automata Theory ◽

Finite Model ◽

Algebraic Proof ◽

Model Property ◽

Finite Model Property ◽

Finite Embeddability Property

The finite embeddability property (FEP) for knotted extensions of residuated lattices holds under the assumption of commutativity, but fails in the general case. We identify weaker forms of the commutativity identity which ensure that the FEP holds. The results have applications outside of order algebra to non-classical logic, establishing the strong finite model property (SFMP) and the decidability for deductions, as well as to mathematical linguistics and automata theory, providing new conditions for recognizability of languages. Our proofs make use of residuated frames, developed in the context of algebraic proof theory.

Download Full-text

Canonical rules

Journal of Symbolic Logic ◽

10.2178/jsl/1254748686 ◽

2009 ◽

Vol 74 (4) ◽

pp. 1171-1205 ◽

Cited By ~ 16

Author(s):

Emil Jeřábek

Keyword(s):

Alternative Proof ◽

Finite Model ◽

Consequence Relations ◽

Model Property ◽

Finite Model Property ◽

Admissible Rules ◽

Superintuitionistic Logics ◽

Canonical Formulas ◽

Global Consequence

AbstractWe develop canonical rules capable of axiomatizing all systems of multiple-conclusion rules over K4 or IPC, by extension of the method of canonical formulas by Zakharyaschev [37]. We use the framework to give an alternative proof of the known analysis of admissible rules in basic transitive logics, which additionally yields the following dichotomy: any canonical rule is either admissible in the logic, or it is equivalent to an assumption-free rule. Other applications of canonical rules include a generalization of the Blok–Esakia theorem and the theory of modal companions to systems of multiple-conclusion rules or (unitary structural global) consequence relations, and a characterization of splittings in the lattices of consequence relations over monomodal or superintuitionistic logics with the finite model property.

Download Full-text

On the Modal μ-Calculus Over Finite Symmetric Graphs

Mathematica Slovaca ◽

10.1515/ms-2015-0052 ◽

2015 ◽

Vol 65 (4) ◽

Author(s):

Giovanna D’Agostino ◽

Giacomo Lenzi

Keyword(s):

Lower Bound ◽

Upper Bound ◽

Satisfiability Problem ◽

Finite Model ◽

Model Property ◽

Finite Model Property ◽

Symmetric Graphs ◽

Trivial Consequence

AbstractIn this paper we consider the alternation hierarchy of the modal μ-calculus over finite symmetric graphs and show that in this class the hierarchy is infinite. The μ-calculus over the symmetric class does not enjoy the finite model property, hence this result is not a trivial consequence of the strictness of the hierarchy over symmetric graphs. We also find a lower bound and an upper bound for the satisfiability problem of the μ-calculus over finite symmetric graphs.

Download Full-text

Finite model property for five modal calculi in the neighbourhood of $S3$.

Notre Dame Journal of Formal Logic ◽

10.1305/ndjfl/1093894152 ◽

1971 ◽

Vol 12 (1) ◽

pp. 69-74 ◽

Cited By ~ 1

Author(s):

Anjan Shukla

Keyword(s):

Finite Model ◽

Model Property ◽

Finite Model Property

Download Full-text

On simple, weak and strong models of propositional calculi

Mathematical Proceedings of the Cambridge Philosophical Society ◽

10.1017/s030500410004771x ◽

1973 ◽

Vol 74 (1) ◽

pp. 1-9 ◽

Cited By ~ 2

Author(s):

Ronald Harrop

Keyword(s):

Simple Model ◽

Propositional Calculus ◽

Finite Model ◽

Model Property ◽

Finite Model Property ◽

Finite Structure ◽

Propositional Calculi ◽

Simple Models

In this paper we will be concerned primarily with weak, strong and simple models of a propositional calculus, simple models being structures of a certain type in which all provable formulae of the calculus are valid. It is shown that the finite model property defined in terms of simple models holds for all calculi. This leads to a new proof of the fact that there is no general effective method for testing, given a finite structure and a calculus, whether or not the structure is a simple model of the calculus.

Download Full-text

On the Decidability of Intuitionistic Tense Logic without Disjunction

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence ◽

10.24963/ijcai.2020/249 ◽

2020 ◽

Author(s):

Fei Liang ◽

Zhe Lin

Keyword(s):

Proof Theory ◽

Tense Logic ◽

Heyting Algebras ◽

Finite Model ◽

Algebraic Proof ◽

Model Property ◽

Algebraic Models ◽

Finite Axiomatizability ◽

Finite Model Property ◽

Modal Operators

Implicative semi-lattices (also known as Brouwerian semi-lattices) are a generalization of Heyting algebras, and have been already well studied both from a logical and an algebraic perspective. In this paper, we consider the variety ISt of the expansions of implicative semi-lattices with tense modal operators, which are algebraic models of the disjunction-free fragment of intuitionistic tense logic. Using methods from algebraic proof theory, we show that the logic of tense implicative semi-lattices has the finite model property. Combining with the finite axiomatizability of the logic, it follows that the logic is decidable.

Download Full-text

Small substructures and decidability issues for first-order logic with two variables

Journal of Symbolic Logic ◽

10.2178/jsl/1344862160 ◽

2012 ◽

Vol 77 (3) ◽

pp. 729-765 ◽

Cited By ~ 11

Author(s):

Emanuel Kieroński ◽

Martin Otto

Keyword(s):

Order Logic ◽

First Order Logic ◽

Equivalence Relations ◽

Finite Model ◽

Model Property ◽

Finite Model Property ◽

First Order ◽

Surrounding Structure ◽

Small Model ◽

Exponential Size

AbstractWe study first-order logic with two variables FO2 and establish a small substructure property. Similar to the small model property for FO2 we obtain an exponential size bound on embedded substructures, relative to a fixed surrounding structure that may be infinite. We apply this technique to analyse the satisfiability problem for FO2 under constraints that require several binary relations to be interpreted as equivalence relations. With a single equivalence relation, FO2 has the finite model property and is complete for non-deterministic exponential time, just as for plain FO2. With two equivalence relations, FO2 does not have the finite model property, but is shown to be decidable via a construction of regular models that admit finite descriptions even though they may necessarily be infinite. For three or more equivalence relations, FO2 is undecidable.

Download Full-text