We give a proof of the finite model property of some fragments of commutative and noncommutative linear logic: the Lambek calculus, BCI, BCK and their enrichments, MALL and Cyclic MALL. We essentially simplify the method used in [4] for proving fmp of BCI and the Lambek ca culus and in [5] for proving fmp of MALL. Our construction of finite models also differs from that used in Lafont [8] in his proof of fmp of MALL.

The typical rules for truth-trees for first-order logic without functions can fail to generate finite branches for formulas that have finite models–the rule set fails to have the finite tree property. In 1984 Boolos showed that a new rule set proposed by Burgess does have this property. In this paper we address a similar problem with the typical rule set for first-order logic with identity and functions, proposing a new rule set that does have the (...) finite tree property. (shrink)

It is standard to think that in Spinoza’s system, all things are necessary and in no sense contingent. However, in his classic book, Spinoza’s Metaphysics, published in 1969, Edwin Curley argues based on the proposition 28 of the first part of the Ethics that Spinoza endorses necessitarianism of only a modest kind, according to which when it comes to finite modes, there is a sense in which they are contingent. In this paper, I revisit Curley’s argument. Commentators have responded (...) to Curley’s argument, showing that Spinoza’s remarks on infinite modes entail that finite modes can in no sense be contingent. But this alone falls short of dispelling Curley’s misgivings about the standard interpretation, for it remains unexplained why Curley is wrong in thinking that the proposition 28 supports his moderate necessitarian interpretation. In defense of the standard interpretation, I bolster the usual response to Curley in greater detail than has been done in the literature and explain why, pace Curley, the proposition 28 plays no evidential role in support of Curley’s interpretation. (shrink)

The finite model property (FMP) in weakly transitive tense logics is explored. Let \(\mathbb {S}=[\textsf{wK}_t\textsf{4}, \textsf{K}_t\textsf{4}]\) be the interval of tense logics between \(\textsf{wK}_t\textsf{4}\) and \(\textsf{K}_t\textsf{4}\). We introduce the modal formula \(\textrm{t}_0^n\) for each \(n\ge 1\). Within the class of all weakly transitive frames, \(\textrm{t}_0^n\) defines the class of all frames in which every cluster has at most _n_ irreflexive points. For each \(n\ge 1\), we define the interval \(\mathbb {S}_n=[\textsf{wK}_t\textsf{4T}_0^{n+1}, \textsf{wK}_t\textsf{4T}_0^{n}]\) which is a subset of \(\mathbb {S}\). (...) There are \(2^{\aleph _0}\) logics in \(\mathbb {S}_n\) lacking the FMP, and there are \(2^{\aleph _0}\) logics in \(\mathbb {S}_n\) having the FMP. Then we explore the FMP in finitely alternative tense logics \(L_{n,m}=L\oplus \{\textrm{Alt}_n^F, \textrm{Alt}_m^P\}\) with \(n,m\ge 0\) and \(L\in \mathbb {S}\). For all \(k\ge 0\) and \(n,m\ge 1\), we define intervals \(\mathbb {F}^k_{n,m}\), \(\mathbb {P}^k_{n,m}\) and \(\mathbb {S}^k_{n,m}\) of tense logics. The number of logics lacking the FMP in them is either 0 or \(2^{\aleph _0}\), and the number of logics having the FMP in them is either finite or \(2^{\aleph _0}\). (shrink)

Our investigation is concerned with the finite model property with respect to admissible rules. We establish general sufficient conditions for absence of fmp w. r. t. admissibility which are applicable to modal logics containing K4: Theorem 3.1 says that no logic λ containing K4 with the co-cover property and of width > 2 has fmp w. r. t. admissibility. Surprisingly many, if not to say all, important modal logics of width > 2 are within the scope of (...) this theorem–K4 itself, S4, GL, K4.1, K4.2, S4.1, S4.2, GL.2, etc. Thus the situation is completely opposite to the case of the ordinary fmp–the absolute majority of important logics have fmp, but not with respect to admissibility. As regards logics of width ≤ 2, there exists a zone for fmp w. r. t. admissibility. It is shown that all modal logics A of width ≤ 2 extending S4 which are not sub-logics of three special tabular logics have fmp w.r.t. admissibility. (shrink)

MIPC is a well-known intuitionistic modal logic of Prior and Bull . It is shown that every normal intuitionistic modal logic L over MIPC has the finite model property whenever L is Kripke-complete and universal.

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.

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.

The logics considered here are the propositional Linear Logic and propositional Intuitionistic Linear Logic extended by a knotted structural rule: γ, xn → y / γ, xm → y. 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. (shrink)

Recently Lafont [6] showed the finite model property for the multiplicative additive fragment of linear logic (MALL) and for affine logic (LLW), i.e., linear logic with weakening. In this paper, we shall prove the finite model property for intuitionistic versions of those, i.e. intuitionistic MALL (which we call IMALL), and intuitionistic LLW (which we call ILLW). In addition, we shall show the finite model property for contractive linear logic (LLC), i.e., linear logic with contraction, (...) and for its intuitionistic version (ILLC). The finite model property for related substructural logics also follow by our method. In particular, we shall show that the property holds for all of FL and GL - -systems except FL c and GL - c of Ono [11], that will settle the open problems stated in Ono [12]. (shrink)

A cutset of H is a subset of ∪ H which meets every element of H.H has the finite cutset property if every cutset of H contains a finite one. We study this notion, and in particular how it is related to the compactness of H for the natural topology. MSC: 04A20, 54D30.

This paper proposes a semantic description of the linear step-like temporal multi-agent logic with the universal modality \(\mathcal{LTK}.sl_U\) based on the idea of non-reflexive non-transitive nature of time. We proved a finite model property and projective unification for this logic.

Recently Lafont [6] showed the finite model property for the multiplicative additive fragment of linear logic and for affine logic, i.e., linear logic with weakening. In this paper, we shall prove the finite model property for intuitionistic versions of those, i.e. intuitionistic MALL, and intuitionistic LLW. In addition, we shall show the finite model property for contractive linear logic, i.e., linear logic with contraction, and for its intuitionistic version. The finite model property (...) for related substructural logics also follow by our method. In particular, we shall show that the property holds for all of FL and GL$^-$-systems except FL$_c$ and GL$^-_c$ of Ono [11], that will settle the open problems stated in Ono [12]. (shrink)

There are many aspects of the Ethics that seem to suggest, or perhaps even require the possibility of deducing finite modes from the infinite substance. Nonetheless, as many have noted even during Spinoza’s own time, it is far from clear that such a deduction can be successfully performed. In this chapter I argue that the expectation of a top-down deduction is unwarranted, and that interestingly enough, it is not only unwarranted with regard to Spinoza but with regard to Descartes (...) as well. I show this by pointing to the crucial role confusion plays for both, noting that our epistemic journey to clear and distinct or adequate knowledge begins with confusion, and that this trajectory is one of emending initially confused ideas. This shows that epistemically a bottom-up trajectory necessarily precedes a top-down one. My claim, however, goes beyond this point regarding the order of discovery. I argue that the state of confusion presupposes a plurality of finite modes, in Spinoza’s case, and substances and modes in Descartes’s. Confusion, I claim, amounts to an inadequate perception of an amalgam of ideas of a real plurality of things. Recognizing the metaphysical ground of confusion along with its central epistemic role brings to light the artificiality, and indeed ultimately the impossibility of a top-down deduction which is divorced from a preceding bottom-up analysis. (shrink)

The tangle modality is a propositional connective that extends basic modal logic to a language that is expressively equivalent over certain classes of finite frames to the bisimulation-invariant fragments of both first-order and monadic second-order logic. This paper axiomatises several logics with tangle, including some that have the universal modality, and shows that they have the finite model property for Kripke frame semantics. The logics are specified by a variety of conditions on their validating frames, including local (...) and global connectedness properties. Some of the results have been used to obtain completeness theorems for interpretations of tangled modal logics in topological spaces. (shrink)

We prove, by a probabilistic argument, that a class of ω-categorical structures, on which algebraic closure defines a pregeometry, has the finite submodel property. This class includes any expansion of a pure set or of a vector space, projective space or affine space over a finite field such that the new relations are sufficiently independent of each other and over the original structure. In particular, the random graph belongs to this class, since it is a sufficiently independent (...) expansion of an infinite set, with no structure. The class also contains structures for which the pregeometry given by algebraic closure is non-trivial. (shrink)

A central difficulty in the way of understanding Spinoza's metaphysical system is that of reconciling two apparently contradictory theories of the causation of finite modes found in his Ethics. The easiest way to present the problem is to place these two accounts side by side.A. All things which follow from the absolute nature of any attribute of God must forever exist, and must be infinite; that is to say, through that attribute they are eternal and infinite. A thing which (...) has been determined to any action was necessarily so determined by God. Together, these propositions entail that God is a necessary and sufficient condition for the occurrence of any action, and that anything so determined is eternal and infinite. Compare these implications with the following.B. An individual thing or a thing which is finite and has determinate existence cannot exist nor be determined to action unless it be determined to existence and action by another cause which is also finite and has a determinate existence; and again this cause cannot exist nor be determined to action unless by another cause which is also finite and determined to existence and action, and so on, ad infinitum. (shrink)

We argue that the simplicity condition on a probability function on sentences of a predicate language L that it takes only finitely many values on the sentences of any finite sublanguage of L can be viewed as rational. We then go on to investigate consequences of this condition, linking it to the model theoretic notion of quantifier elimination.

This essay argues that Spinoza believed that each finite mode is absolutely necessitated by God's nature and is causally necessitated by the laws of nature in conjunction with other finite modes. A geometrical analogy from Part 2 of the Ethics is employed in order to give a more suggestive account of the ways in which all things are necessary, according to Spinoza.

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)

Spinoza’s rejection of Aristotelian final causation seems to create a difficulty for his account of individuation. If causation is indeed blind, how do finite modes come to assume complex, differentiated forms? And why do we find in nature a great regularity of such forms? Several recent commentators have proposed that Spinoza maintains something of the Aristotelian conception of causation where the formal essences of individuals guide the process of individuation toward certain desirable outcomes. But this sort of approach introduces (...) other difficulties that threaten to undermine Spinoza’s naturalistic framework and his ontology of immanence. This paper outlines a mechanistic and probabilistic account of individuation whereby modes are individuated by entering into relations that increase their mutual power of enduring. Together with conatus as the principle of individuation, this mechanistic account suffices to explain the individuation of finite bodies without introducing additional kinds of causation into Spinoza’s philosophy. (shrink)

We prove the finite model property (fmp) for BCI and BCI with additive conjunction, which answers some open questions in Meyer and Ono [11]. We also obtain similar results for some restricted versions of these systems in the style of the Lambek calculus [10, 3]. The key tool is the method of barriers which was earlier introduced by the author to prove fmp for the product-free Lambek calculus [2] and the commutative product-free Lambek calculus [4].

Tense logics in the bimodal propositional language are investigated with respect to the Finite Model Property. In order to prove positive results techniques from investigations of modal logics above K4 are extended to tense logic. General negative results show the limits of the transfer.

In this article, I present a semantically natural conservative extension of Urquhart’s positive semilattice logic with a sort of constructive negation. A subscripted sequent calculus is given for this logic and proofs of its soundness and completeness are sketched. It is shown that the logic lacks the finite model property. I discuss certain questions Urquhart has raised concerning the decision problem for the positive semilattice logic in the context of this logic and pose some problems for further research.

An old conjecture of modal logics states that every splitting of the major systems K4, S4, G and Grz has the finite model property. In this paper we will prove that all iterated splittings of G have fmp, whereas in the other cases we will give explicit counterexamples. We also introduce a proof technique which will give a positive answer for large classes of splitting frames. The proof works by establishing a rather strong property of these splitting (...) frames namely that they preserve the finite model property in the following sense. Whenever an extension Λ has fmp so does the splitting Λ/f of Λ by f. Although we will also see that this method has its limitations because there are frames lacking this property, it has several desirable side effects. For example, properties such as compactness, decidability and others can be shown to be preserved in a similar way and effective bounds for the size of models can be given. Moreover, all methods and proofs are constructive. (shrink)

There are two known general results on the finite model property of commutators [L0,L1]. If L is finitely axiomatizable by modal formulas having universal Horn first-order correspondents, then both [L,K] and [L,S5] are determined by classes of frames that admit filtration, and so they have the fmp. On the negative side, if both L0 and L1 are determined by transitive frames and have frames of arbitrarily large depth, then [L0,L1] does not have the fmp. In this paper we (...) show that commutators with a “weakly connected” component often lack the fmp. Our results imply that the above positive result does not generalize to universally axiomatizable component logics, and even commutators without “transitive” components such as [K3,K] can lack the fmp. We also generalize the above negative result to cases where one of the component logics has frames of depth one only, such as [S4.3,S5] and the decidable product logic S4.3×S5. We also show cases when already half of commutativity is enough to force infinite frames. (shrink)

The first example of an intuitively meaningful propositional logic without the finite model property, and still the simplest one in the literature. The question of its decidability appears still to be open.

The first example of an intuitively meaningful propositional logic without the finite model property, and still the simplest one in the literature. The question of its decidability appears still to be open.

Spinoza’s bold claim that there exists only a single infinite substance entails that finite things pose a deep challenge: How can Spinoza account for their finitude and their plurality? Taking finite bodies as a test case for finite modes in general I articulate the necessary conditions for the existence of finite things. The key to my argument is the recognition that Spinoza’s account of finite bodies reflects both Cartesian and Hobbesian influences. This recognition leads to (...) the surprising realization there must be more to finite bodies than their finitude, a claim that goes well beyond the basic substance-monism claim, namely, that anything that is, is in God. This leads to the conclusion, which may seem paradoxical, that finite bodies have both an infinite as well as a finite aspect to them. Finite bodies, I argue, both actively partially determine all the other finite bodies, thereby partially causing their existence insofar as they are finite, as well as are determined by the totality of other bodies. I articulate precisely what this infinite aspect is and how it is distinct from the general substance-monism dictum. (shrink)

There is a long tradition of reading Spinoza as committed, perhaps unwillingly, to the non-reality of finite modes. While acknowledging that Spinoza does seem to rely on the reality of modes in certain places, Michael Della Rocca has called attention to what he labels an “idealist strand.” As a concluding remark in “Steps Toward Eleaticism in Spinoza's Philosophy of Action,” he claims that faced with these two conflicting strands, which are genuinely to be found in the text, it is (...) better to note both rather than artificially imposing a unity on the text. In this paper, I suggest that one need not admit two conflicting strands in Spinoza, on the one hand, nor arbitrarily disregard one strand, on the other. Rather, I argue for a unified view that diagnoses what gives rise to both seemingly conflicting strands. The key to this enterprise is recognizing that finite modes, paradoxically seeming perhaps at first, are not wholly finite. That is, a finite mode is determined by the totality of finite modes—wherein lies its finite aspect, but at the same time, and equally, partially actively determines this totality—wherein lies its infinite aspect. (shrink)

$\underline{\text{Saturation is} -\text{transferable in} T}$ if and only if there is an expansion T$_1$ of T with $\mid T_1 \mid$ = $\mid T \mid$ such that if M is a $\mu$-saturated model of T$_1$ and $\mid M \mid \geq \kappa$ then the reduct M $\mid L$ is $\kappa$-saturated. We characterize theories which are superstable without f.c.p., or without f.c.p. as, respectively those where saturation is - transferable or, \lambda$)-transferable for all $\lambda$. Further if for some $\mu \geq \mid T \mid, (...) 2^\mu > \mu^+$, stability is equivalent to for all $\mu \geq \mid T \mid$, saturation is - transferable. (shrink)

Some passages throughout Spinoza’s body of works suggest that an attribute in its absolute nature provides a sufficient condition for all of its modes, including the finite ones. Other passages suggest that an attribute in its absolute nature fails to provide a sufficient condition for its finite modes. My aim is to dispel this apparent tension. I argue that all finite modes are ultimately entailed by the absolute nature of their attribute. Furthermore, I explain how the Spinozistic (...) positions that appear incompatible with this view are in fact compatible. As I see it, we should read those passages where Spinoza says that no finite mode ultimately follows from the absolute nature of its attribute as saying merely that no finite mode ultimately follows in one-by-one fashion, independent of an infinite series of other modes, from the absolute nature of its attribute. (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].

We study a class of 0-categorical simple structures such that every M in has uncomplicated forking behavior and such that definable relations in M which do not cause forking are independent in a sense that is made precise; we call structures in independent. The SU-rank of such M may be n for any natural number n>0. The most well-known unstable member of is the random graph, which has SU-rank one. The main result is that for every strongly independent structure M (...) in , if a sentence φ is true in M then φ is true in a finite substructure of M. The same conclusion holds for every structure in with SU-rank one; so in this case the word ‘strongly’ can be removed. A probability theoretic argument is involved and it requires sufficient independence between relations which do not cause forking. A stable structure M belongs to if and only if it is 0-categorical, 0-stable and every definable strictly minimal subset of is indiscernible. (shrink)

We show that the loosely guarded and packed fragments of first-order logic have the finite model property. We use a construction of Herwig and Hrushovski. We point out some consequences in temporal predicate logic and algebraic logic.

$\underline{\text{Saturation is} (\mu, \kappa)-\text{transferable in} T}$ if and only if there is an expansion T 1 of T with ∣ T 1 ∣ = ∣ T ∣ such that if M is a μ-saturated model of T 1 and ∣ M ∣ ≥ κ then the reduct M ∣ L(T) is κ-saturated. We characterize theories which are superstable without f.c.p., or without f.c.p. as, respectively those where saturation is (ℵ 0 , λ)- transferable or (κ (T), λ)-transferable for all λ. (...) Further if for some $\mu \geq \mid T \mid, 2^\mu > \mu^+$ , stability is equivalent to for all μ ≥ ∣ T ∣, saturation is (μ, 2 μ )- transferable. (shrink)

In this paper a unified framework for dealing with a broad family of propositional multimodal logics is developed. The key tools for presentation of the logics are the notions of closure relation operation and monotonous relation operation. The two classes of logics: FiRe-logics (finitely reducible logics) and LaFiRe-logics (FiRe-logics with local agreement of accessibility relations) are introduced within the proposed framework. Further classes of logics can be handled indirectly by means of suitable translations. It is shown that the logics from (...) these classes have the finite model property with respect to the class of -formulae, i.e. each -formula has a -model iff it has a finite -model. Roughly speaking, a -formula is logically equivalent to a formula in negative normal form without occurrences of modal operators with necessity force. In the proof we introduce a substantial modification of Claudio Cerrato's filtration technique that has been originally designed for graded modal logics. The main core of the proof consists in building adequate restrictions of models while preserving the semantics of the operators used to build terms indexing the modal operators. (shrink)