Lindström's Theorem characterizes first order logic as the maximal logic satisfying the Compactness Theorem and the Downward Löwenheim-Skolem Theorem. If we do not assume that logics are closed under negation, there is an obvious extension of first order logic with the two model theoretic properties mentioned, namely existential second order logic. We show that existential second order logic has a whole family of proper extensions satisfying the Compactness Theorem and the Downward Löwenheim-Skolem Theorem. Furthermore, we show that in the context of negationless logics, positive logics, as we call them, there is no strongest extension of first order logic with the Compactness Theorem and the Downward Löwenheim-Skolem Theorem.
Fuchino-Maschio-Sakai~\cite{FuchinoEtAl_DRP_LST} proved that the Löwenheim-Skolem-Tarski (LST) property of Stationary Logic is equivalent to the Diagonal Reflection Principle on internally club sets ($\text{DRP}_{\text{IC}}$) introduced in \cite{DRP}. We prove that the restriction of the LST property to (downward) reflection of $Π^1_1$ formulas, which we call the $Π^1_1 \! \! \downarrow$-LST property, is equivalent to the \emph{internal} version of DRP from \cite{Cox_RP_IS}. Combined with results from \cite{Cox_RP_IS}, this shows that the $Π^1_1 \! \! \downarrow$-LST Property for Stationary Lo…
Continuing [Fuchino, Ottenbreit and Sakai[9, 10]] and [Fuchino and Ottenbreit[11]], we further study reflection principles in connection with the Löwenheim-Skolem Theorems of stationary logics. In this paper, we mainly analyze the situations in the models obtained by mixed support iteration of a supercompact length and then collapsing another supercompact cardinal to make it $(2^{\aleph_0})^+$. We show, among other things, that the reflection down to $< 2^{\aleph_0}$ of the non-metrizability of topological spaces with small character is independent from the reflection properties studied in [Fu…
Continuing the previous paper, we study the Strong Downward Löwenheim-Skolem Theorems (SDLSs) of the stationary logic and their variations. It has been shown that the SDLS for the ordinary stationary logic with weak second-order parameters down to $<\aleph_2$ is equivalent to the conjunction of CH and Cox's Diagonal Reflection Principle for internally clubness. We show that the SDLS for the stationary logic without weak second-order parameters down to $<2^{\aleph_0}$ implies that the size of the continuum is $\aleph_2$. In contrast, an internal interpretation of the stationary logic can satisf…
Lindström theorem obviously fails as a characterization of $\mathcal{L}_{ωω}^{-} $, first-order logic without identity. In this note we provide a fix: we show that $\mathcal{L}_{ωω}^{-} $ is \emph{maximal} among abstract logics satisfying a weak form of the isomorphism property (suitable for identity-free languages and studied in \cite{Casa}), 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 avai…
We show that a strong form of the so called Lindstrom's Theorem fails to generalize to extensions of L_{kappa,omega} and L_{kappa,kappa}: For weakly compact kappa there is no strongest extension of L_{kappa,omega} with the (kappa,kappa)-compactness property and the Lowenheim-Skolem theorem down to kappa. With an additional set-theoretic assumption, there is no strongest extension of L_{kappa,kappa} with the (kappa,kappa)-compactness property and the Lowenheim-Skolem theorem down to <kappa.
Bagaria and Väänänen developed a framework for studying the large cardinal strength of downwards Löwenheim-Skolem theorems and related set theoretic reflection properties. The main tool was the notion of symbiosis, originally introduced by the third author. Symbiosis provides a way of relating model theoretic properties of strong logics to definability in set theory. In this paper we continue the systematic investigation of symbiosis and apply it to upwards Löwenheim-Skolem theorems and reflection principles. To achieve this, we need to adapt the notion of symbiosis to a new form, called bound…
Skolem (1956) studied the germs at infinity of the smallest class of real valued functions on the positive real line containing the constant $1$, the identity function $x$, and such that whenever $f$ and $g$ are in the set, $f+g,fg$ and $f^g$ are in the set. This set of germs is well ordered and Skolem conjectured that its order type is epsilon-zero. Van den Dries and Levitz (1984) computed the order type of the fragment below $2^{2^x}$. Here we prove that the set of asymptotic classes within any archimedean class of Skolem functions has order type $ω$. As a consequence we obtain, for each pos…
Elimination of a single Skolem function in pure logic increases the length of proofs only linearly. The result is shown for derivations with cuts that are free for the Skolem function in a sequent calculus with strong locality property.
This is a set of 288 questions written for a Moore-style course in Mathematical Logic. I have used these (or some variation) four times in a beginning graduate course. Topics covered are: propositional logic axioms of ZFC wellorderings and equivalents of AC ordinal and cardinal arithmetic first order logic, and the compactness theorem Lowenheim-Skolem theorems Turing machines, Church's Thesis completeness theorem and first incompleteness theorem undecidable theories second incompleteness theorem
This paper develops a general methodology to connect propositional and first-order interpolation. In fact, the existence of suitable skolemizations and of Herbrand expansions together with a propositional interpolant suffice to construct a first-order interpolant. This methodology is realized for lattice-based finitely-valued logics, the top element representing true. It is shown that interpolation is decidable for these logics.
In this paper (propositional) probability logic ($PL$) is investigated from model theoretic point of view. First of all, the ultraproduct construction is adapted for $σ$-additive probability models, and subsequently when this class of models is considered it is shown that the compactness property holds with respect to a fragment of $PL$ called basic probability logic ($BPL$). On the other hand, when dealing with finitely-additive probability models, one may extend the compactness property for a larger fragment of probability logic, namely positive probability logic ($PPL$). We finally prove th…
In this paper we investigate the consequences and consistency of the downward Löwenheim-Skolem theorem for extension of the first order logic by the Magidor-Malitz quantifier. We derive some combinatorial results and improve the known upper bound for the consistency of Chang's Conjecture at successor of singular cardinals.
In the the present contribution, we prove an Omitting Types Theorem (OTT) for an arbitrary fragment of hybriddynamic first-order logic with rigid symbols (i.e. symbols with fixed interpretations across worlds) closed under negation and retrieve. The logical framework can be regarded as a parameter and it is instantiated by some well-known hybrid and/or dynamic logics from the literature. We develop a forcing technique and then we study a forcing property based on local satisfiability, which lead to a refined proof of the OTT. For uncountable signatures, the result requires compactness, while f…
Informally speaking, the categoricity of an axiom system means that its non-logical symbols have only one possible interpretation that renders the axioms true. Although non-categoricity has become ubiquitous in the second half of the 20th century whether one looks at number theory, geometry or analysis, the first axiomatizations of such mathematical theories by Dedekind, Hilbert, Huntington, Peano and Veblen were indeed categorical. A common resolution of the difference between the earlier categorical axiomatizations and the more modern non-categorical axiomatizations is that the latter derive…
The paper studies admissibility of multiple-conclusion rules in the positive logics. Using modification of a method used by M.~Wajsberg in the proof of the separation theorem, it is shown that the problem of admissibility in positive logics is equivalent to the problem of admissibility in intermediate logics defined by positive additional axioms.
We study the basic properties of a dual "spectral" topology on positive type spaces of h-inductive theories and its essential connection to infinitary logic. The topology is Hausdorff, has the Baire property, and its compactness characterises positive model completeness; it also has a basis of clopen sets and is described by the formulas of geometric logic. The "geometric types" are closed in the type spaces under all the operations of infinitary logic, and we introduce a positive analogue of existentially universal structures, through which we interpret the full first order logic in positive …
With the aim of developing the concepts of positive logic and in response to a question that was asked by Poizat in one of his articles, I wrote this article. The main topic is the study of compactness in the extension as a compact structure. they are based on a fundamental characterization of the compactness, which was given by Itai Ben Yacov and Poizat in section Basis of positive logic.
Proof-theoretic methods are developed for subsystems of Johansson's logic obtained by extending the positive fragment of intuitionistic logic with weak negations. These methods are exploited to establish properties of the logical systems. In particular, cut-free complete sequent calculi are introduced and used to provide a proof of the fact that the systems satisfy the Craig interpolation property. Alternative versions of the calculi are later obtained by means of an appropriate loop-checking history mechanism. Termination of the new calculi is proved, and used to conclude that the considered …
In this paper we extend of the notion of algebraically closed given in the case of groups and skew fields to an arbitrary h-inductive theory. The main subject of this paper is the study of the notion of positive algebraic closedness and its relationship with the notion of positive closedness and the amalgamation property.
A strictly formal, set-theoretical treatment of classical first-order logic is given. Since this is done with the goal of a concrete Mizar formalization of basic results (Lindenbaum lemma; Henkin, satisfiability, completeness and Lowenheim-Skolem theorems) in mind, it turns into a systematic pursue of simplification: we give up the notions of free occurrence, of derivation tree, and study what inference rules are strictly needed to prove the mentioned results. Afterwards, we discuss details of the actual Mizar implementation, and give general techniques developed therein.
We deal with the fragment of modal logic consisting of implications of formulas built up from the variables and the constant `true' by conjunction and diamonds only. The weaker language allows one to interpret the diamonds as the uniform reflection schemata in arithmetic, possibly of unrestricted logical complexity. We formulate an arithmetically complete calculus with modalities labeled by natural numbers and ω, where ωcorresponds to the full uniform reflection schema, whereas n<ωcorresponds to its restriction to arithmetical Π_{n+1}-formulas. This calculus is shown to be complete w.r.t. a su…
An important dividing line in the class of unstable theories is being NSOP$_1$, which is more general than being simple. In NSOP$_1$ theories forking independence may not be as well-behaved as in stable or simple theories, so it is replaced by another independence notion, called Kim-independence. We generalise Kim-independence over models in NSOP$_1$ theories to positive logic -- a proper generalisation of first-order logic where negation is not built in, but can be added as desired. For example, an important application is that we can add hyperimaginary sorts to a positive theory to get anoth…
Frobenius Galois expansions of substructural logics:Algebraization, Kalman equivalence and positive cone semantics
School of Science, Xi’an Petroleum University（西安石油大学理学院）；School of Mathematics and Data Science, Shaanxi University of Science and Technology（陕西科技大学数学与数据科学学院）；School of Science, Xi Hang University（西航大学理学院）
We study the amalgamation property in positive logic. We give some connections between the amalgamation property and Robinson theories, model-complete theories and the Hausdorff property.
We establish a natural translation from word rewriting systems to strictly positive polymodal logics. Thereby, the latter can be considered as a generalization of the former. As a corollary we obtain examples of undecidable strictly positive normal modal logics. The translation has its counterpart on the level of proofs: we formulate a natural deep inference proof system for strictly positive logics generalizing derivations in word rewriting systems. We also formulate some open questions related to the theory of modal companions of superintuitionistic logics that was initiated by L.L. Maximova…
We characterise non-distributive positive logic as the fragment of a single-sorted first-order language that is preserved by a new notion of simulation called a meet-simulation. Meet-simulations distinguish themselves from simulations because they relate pairs of states from one model to single states from another. En route to this result we use a more traditional notion of simulations and prove a Hennessy-Milner style theorem for it, using an analogue of modal saturation called meet-compactness.
We reformulate Hrushovski's definability patterns from the setting of first order logic to the setting of positive logic. Given an h-universal theory T we put two structures on the type spaces of models of T in two languages, \mathcal{L} and \mathcal{L}_π. It turns out that for sufficiently saturated models, the corresponding h-universal theories \mathcal{T} and \mathcal{T}_π are independent of the model. We show that there is a canonical model \mathcal{J} of \mathcal{T}, and in many interesting cases there is an analogous canonical model \mathcal{J}_π of \mathcal{T}_π, both of which embed int…
We construct a 2-equivalence $\mathfrak{CohTheory}^\text{op} \simeq \mathfrak{TypeSpaceFunc}$. Here $\mathfrak{CohTheory}$ is the 2-category of positive theories and $\mathfrak{TypeSpaceFunc}$ is the 2-category of type space functors. We give a precise definition of interpretations for positive logic, which will be the 1-cells in $\mathfrak{CohTheory}$. The 2-cells are definable homomorphisms. The 2-equivalence restricts to a duality of categories, making precise the philosophy that a theory is `the same' as the collection of its type spaces (i.e. its type space functor). In characterising tho…
This paper presents rules of inference for a binary quantifier $I$ for the formalisation of sentences containing definite descriptions within intuitionist positive free logic. $I$ binds one variable and forms a formula from two formulas. $Ix[F, G]$ means `The $F$ is $G$'. The system is shown to have desirable proof-theoretic properties: it is proved that deductions in it can be brought into normal form. The discussion is rounded up by comparisons between the approach to the formalisation of definite descriptions recommended here and the more usual approach that uses a term-forming operator $ι$…
We study FO+, a fragment of first-order logic on finite words, where monadic predicates can only appear positively. We show that there is a FO-definable language that is monotone in monadic predicates but not definable in FO+. This provides a simple proof that Lyndon's preservation theorem fails on finite structures. We additionally show that given a regular language, it is undecidable whether it is definable in FO+.
We introduce the framework of AECats (abstract elementary categories), generalising both the category of models of some first-order theory and the category of subsets of models. Any AEC and any compact abstract theory ("cat", as introduced by Ben-Yaacov) forms an AECat. In particular, we find applications in positive logic and continuous logic: the category of (subsets of) models of a positive or continuous theory is an AECat. The Kim-Pillay theorem for first-order logic characterises simple theories by the properties dividing independence has. We prove a version of the Kim-Pillay theorem for …
Inclusion logic is a variant of dependence logic that was shown to have the same expressive power as positive greatest fixed-point logic. Inclusion logic is not axiomatizable in full, but its first-order consequences can be axiomatized. In this paper, we provide such an explicit partial axiomatization by introducing a system of natural deduction for inclusion logic that is sound and complete for first-order consequences in inclusion logic.
Locality is a property of logics, based on Hanf's and Gaifman's theorems, and that was shown to be very useful in the context of finite model theory. In this paper I present a homotopic variation for locality, namely a Quillen model category-based framework for locality under k-logical equivalence, for every primitive-positive sentence of quantifier-rank k.
A model checking computation checks whether a given logical sentence is true in a given finite structure. Provenance analysis abstracts from such a computation mathematical information on how the result depends on the atomic data that describe the structure. In database theory, provenance analysis by interpretations in commutative semirings has been rather succesful for positive query languages (such a unions of conjunctive queries, positive relational algebra, or datalog). However, it did not really offer an adequate treatment of negation or missing information. Here we propose a new approach…
