For a cardinal of the form $κ=\beth_κ$, Shelah's logic $L^1_κ$ has a characterisation as the maximal logic above $\bigcup_{λ<κ} L_{λ, ω}$ satisfying Strong Undefinability of Well Order (SUDWO). SUDWO is a strengthening of the Undefinability of Well Order (UDWO). We prove that if $κ$ is singular of countable cofinality, Karp's chain logic \cite{Karpintroduceschain} is above $L^1_κ$, while it is already known that it satisfies UDWO and Interpolation. Moreover, we show that in these circumstances, the chain logic is -- in a sense -- maximal among logics with chain models to satisfy UDWO. We then show that the chain logic gives a partial solution to Problem 1.4. from Shelah's \cite{Sh797}, which asked whether for $κ$ singular of countable cofinality there was a logic strictly between $ L_{κ^+, ω}$ and $L_{κ^+, κ^+}$ having Interpolation. We show that modulo accepting as the upper bound a model class of $L_{κ, κ}$, Karp's chain logic satisfies the required properties. In addition, we show that this chain logic is not $κ$-compact, a question that we have asked on various occasions. We contribue to the further development of chain logic by proving the Union Lemma and identifying the chain-independent fragment of the logic, showing that it still has considerable expressive power. In conclusion, we have shown that the simply defined chain logic emulates the logic $L^1_κ$ in satisfying Interpolation, undefinability of well-order and maximality with respect to it, and the Union Lemma. In addition it has a Completeness Theorem.
We point out a gap in Shelah's proof of the following result: $\mathbf{Claim}$ Let $K$ be an abstract elementary class categorical in unboundedly many cardinals. Then there exists a cardinal $λ$ such that whenever $M, N \in K$ have size at least $λ$, $M \le N$ if and only if $M \preceq_{L_{\infty, \text{LS} (K)^+}} N$. The importance of the claim lies in the following theorem, implicit in Shelah's work: $\mathbf{Theorem}$ Assume the claim. Let $K$ be an abstract elementary class categorical in unboundedly many cardinals. Then the class of $λ$ such that: 1) $K$ is categorical in $λ$; 2) $K$ has…
We generalize the Hart-Shelah example \cite{HaSh:323} to higher infinitary logics. We build, for each natural number $k\geq 2$ and for each infinite cardinal $λ$, a sentence $ψ_k^λ$ of the logic $L_{(2^λ)^+,ω}$ that (modulo mild set theoretical hypotheses around $λ$ and assuming $2^λ< λ^{+m}$) is categorical in $λ^+,\dots,λ^{+k-1}$ but not in $\beth_{k+1}(λ)^+$ (or beyond); we study the dimensional encoding of combinatorics involved in the construction of this sentence and study various model-theoretic properties of the resulting abstract elementary class ${\mathcal K}^*(λ,k)=(Mod(ψ_k^λ),\prec…
We study propositional and first-order Gödel logics over infinitary languages which are motivated semantically by corresponding interpretations into the unit interval [0,1]. We provide infinitary Hilbert-style calculi for the particular (propositional and first-order) cases with con-/disjunctions of countable length and prove corresponding completeness theorems by extending the usual Lindenbaum-Tarski construction to the infinitary case for a respective algebraic semantics via complete linear Heyting algebras. We provide infinitary hypersequent calculi and prove corresponding cut-elimination t…
We describe an infinitary logic for metric structures which is analogous to $L_{ω_1, ω}$. We show that this logic is capable of expressing several concepts from analysis that cannot be expressed in finitary continuous logic. Using topological methods, we prove an omitting types theorem for countable fragments of our infinitary logic. We use omitting types to prove a two-cardinal theorem, which yields a strengthening of a result of Ben Yaacov and Iovino concerning separable quotients of Banach spaces.
We prove completeness, interpolation and omitting types for certain predicate topological logics that properly extend the first order case. We aslo count the non isomorphic topological models of a countable theory
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 …
We consider model-theoretic properties related to the expressive power of three analogues of $L_{ω_1, ω}$ for metric structures. We give an example showing that one of these infinitary logics is strictly more expressive than the other two, but also show that all three have the same elementary equivalence relation for complete separable metric structures. We then prove that a continuous function on a complete separable metric structure is automorphism invariant if and only if it is definable in the more expressive logic. Several of our results are related to the existence of Scott sentences for…
The logic L^1_θintroduced in [Sh:797]; it is the maximal logic below L_theta theta in which a well ordering is not definable. We investigate it for theta a compact cardinal. We prove it satisfies several parallel of classical theorems on first order logic, strengthening the thesis that it is a natural logic. In particular, two models are L^1_theta-equivalent iff for some omega-sequence of theta-complete ultrafilters, the iterated ultra-powers by it of those two models are isomorphic.
Analogues of Scott's isomorphism theorem, Karp's theorem as well as results on lack of compactness and strong completeness are established for infinitary propositional relevant logics. An "interpolation theorem" (of a particular sort introduced by Barwise and van Benthem) for the infinitary quantificational boolean logic $L_{\infty ω}$ holds. This yields a preservation result characterizing the expressive power of infinitary relevant languages with absurdity using the model-theoretic relation of relevant directed bisimulation as well as a Beth definability property.
We introduce a realisability semantics for infinitary intuitionistic set theory that is based on Ordinal Turing Machines (OTMs). We show that our notion of OTM-realisability is sound with respect to certain systems of infinitary intuitionistic logic, and that all axioms of infinitary Kripke-Platek set theory are realised. Finally, we use a variant of our notion of realisability to show that the propositional admissible rules of (finitary) intuitionistic Kripke-Platek set theory are exactly the admissible rules of intuitionistic propositional logic.
Ordinary infinitary languages L_{lambda, kappa} satisfy the Interpolation Theorem only in the case lambda <= {aleph_1}, kappa = {aleph_0}, this include first order logic of course. There are also some pairs of such logics satifying interpolation, e.g. (L_{lambda^+,{aleph_0}}, L_{(2^lambda)^+, lambda^+}) . Does this come from an intermidiate logic satisfying it? Is it nice? unique? We define for kappa = beth_kappa a new logic L^1_kappa such that L_{kappa omega}< L^1_kappa LL_{kappa kappa} and L^1_kappa is very nice; in particular satisfies the Interpolation Theorem. Moreover, L^1_kappa has a mo…
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.
We study different representation theorems for various reducts of Heyting polyadic algebras. Superamalgamation is proved for several (natural reducts) and our results are compared to the finitizability problem in classical algebraic logic dealing with cylindric and polyadic (Boolean algebras). We also prove several new neat embedding theorems, and obtain that the class of representable algebras based on (a generalized) Kripke semantics coincide with the class of algebras having the neat embedding property, that is those algebras that are subneat reducts of algebras having $ω$ extra dimensions.
We present a unified categorical treatment of completeness theorems for several classical and intuitionistic infinitary logics with a proposed axiomatization. This provides new completeness theorems and subsumes previous ones by Gödel, Kripke, Beth, Karp, Joyal, Makkai and Fourman/Grayson. As an application we prove, using large cardinals assumptions, the disjunction and existence properties for infinitary intuitionistic first-order logics.
Let K^0_lambda be the class of structures < lambda,<,A>, where A subseteq lambda is disjoint from a club, and let K^1_lambda be the class of structures < lambda,<,A>, where A subseteq lambda contains a club. We prove that if lambda = lambda^{< kappa} is regular, then no sentence of L_{lambda^+ kappa} separates K^0_lambda and K^1_lambda. On the other hand, we prove that if lambda = mu^+, mu = mu^{< mu}, and a forcing axiom holds (and aleph_1^L= aleph_1 if mu = aleph_0), then there is a sentence of L_{lambda lambda} which separates K^0_lambda and K^1_lambda .
Given a weakly compact cardinal $κ$, we give an axiomatization of intuitionistic first-order logic over $\mathcal{L}_{κ^+, κ}$ and prove it is sound and complete with respect to Kripke models. As a consequence we get the disjunction and existence properties for that logic. This generalizes the work of Nadel for intuitionistic logic over $\mathcal{L}_{ω_1, ω}$. When $κ$ is a regular cardinal such that $κ^{<κ}=κ$, we deduce, by an easy modification of the proof, a complete axiomatization of intuitionistic first-order logic over $\mathcal{L}_{κ^+, κ, κ}$, the language with disjunctions of at most…
We extend Łukasiewicz logic obtaining the infinitary logic $\mathcal{IR}Ł$ whose models are algebras $C(X,[0,1])$, where $X$ is a basically disconnected compact Hausdorff space. Equivalently, our models are unit intervals in $σ$-complete Riesz spaces with strong unit. The Lindenbaum-Tarski algebra of $\mathcal{IR}Ł$ is, up to isomorphism, an algebra of $[0,1]$-valued Borel functions. Finally, our system enjoys standard completeness with respect to the real interval $[0,1]$.
We introduce infinitary action logic with exponentiation -- that is, the multiplicative-additive Lambek calculus extended with Kleene star and with a family of subexponential modalities, which allows some of the structural rules (contraction, weakening, permutation). The logic is presented in the form of an infinitary sequent calculus. We prove cut elimination and, in the case where at least one subexponential allows non-local contraction, establish exact complexity boundaries in two senses. First, we show that the derivability problem for this logic is $Π_1^1$-complete. Second, we show that t…
We study first-order as well as infinitary logics extended with quantifiers closed upwards under embeddings. In particular, we show that if a chain of quasi-homogeneous structures is sufficiently long then a given formula of such a logic is eventually equivalent to a quantifier-free formula in that chain. We use this fact to produce a number of undefinability results for logics with embedding-closed quantifiers. In the final section we introduce an Ehrenfeucht-Fraïssé game that characterizes the $L$-equivalence between structures, where $L$ is the infinitary logic $L_{\infty ω}$ extended with …
We investigate the extent of second order characterizable structures by extending Shelah's Main Gap dichotomy to second order logic. For this end we consider a countable complete first order theory T. We show that all sufficiently large models of T have a characterization up to isomorphism in the extension of second order logic obtained by adding a little bit of infinitary logic if and only if T is shallow superstable with NDOP and NOTOP. Our result relies on cardinal arithmetic assumptions. Under weaker assumptions we get consistency results or alternatively results about second order logic w…
Action logic is the algebraic logic (inequational theory) of residuated Kleene lattices. This logic involves Kleene star, axiomatized by an induction scheme. For a stronger system which uses an $ω$-rule instead (infinitary action logic) Buszkowski and Palka (2007) have proved $Π_1^0$-completeness (thus, undecidability). Decidability of action logic itself was an open question, raised by D. Kozen in 1994. In this article, we show that it is undecidable, more precisely, $Σ_1^0$-complete. We also prove the same complexity results for all recursively enumerable logics between action logic and infi…
Given a regular cardinal $κ$ such that $κ^{<κ}=κ$ (e.g., if the Generalized Continuum Hypothesis holds), we develop a proof system for classical infinitary logic that includes heterogeneous quantification (i.e., infinite alternate sequences of quantifiers) within the language $\mathcal{L}_{κ^+, κ}$, where there are conjunctions and disjunctions of at most $κ$ any formulas and quantification (including the heterogeneous one) is applied to less than $κ$ many variables. This type of quantification is interpreted in $\mathcal{S}et$ using the usual second-order formulation in terms of strategies fo…
Circular proofs, introduced by Daniyar Shamkanov, are proofs in which assumptions are allowed that are not axioms but do appear at least twice along a branch. Shamkanov has shown that a formula belongs to the provability logic GL exactly if it has a circular proof in the modal logic K4. Shamkanov uses Tait style proof systems and infinitary proofs. In this paper we prove the same result but then for sequent calculi and without the detour via infinitary systems. We also obtain a mild generalisation of the result, implying that its intuitionistic analogue holds as well.
Institute of Computer Science, Czech Academy of Sciences（捷克科学院计算机研究所）；Department of Algebra, Faculty of Mathematics and Physics, Charles University（查理大学数学物理学院代数系）；Department of Information Engineering and Mathematics, University of Siena（锡耶纳大学信息与工程数学系）
The logic $\mathcal L^1_κ$ was introduced by Shelah in [3]. In [4], he proved that for a strongly compact cardinal $κ$, it admits the following algebraic characterization: two structures are $\mathcal L^1_κ$-equivalent if and only if they have isomorphic iterated ultrapowers via $κ$-complete ultrafilters. We give a presentation of the logic $\mathcal L^1_κ$ and a simplified and slightly modified proof of this result.
In this note, we show that the first-order logic IK$^ω$ is sound with regard to the models obtained from continuum-valued Łukasiewicz-models for first-order languages by treating the quantifiers as infinitary strong disjunction/conjunction rather than infinitary weak disjunction/conjunction. Moreover, we show that these models cannot be used to provide a new consistency proof for the theory of truth IKT$^ω$ obtained by expanding IK$^ω$ with transparent truth because the models are inconsistent with transparent truth. Finally, we show that whether or not this inconsistency can be reproduced in …
Considering a particular case of a problem posed by Saharon Shelah, we prove that the automorphism group of an infinitely generated free nilpotent group N first-order interprets the full second-order theory of the set rank(N) in the empty language.
A modified realisability interpretation of infinitary logic is formalised and proved sound in constructive type theory (CTT). The logic considered subsumes first order logic. The interpretation makes it possible to extract programs with simplified types and to incorporate and reason about them in CTT.
Ehrenfeucht-Fraisse games are very useful in studying separation and equivalence results in logic. The standard finite Ehrenfeucht-Fraisse game characterizes equivalence in first order logic. The standard Ehrenfeucht-Fraisse game in infinitary logic characterizes equivalence in $L_{\inftyω}$. The logic $L_{ω_1ω}$ is the extension of first order logic with countable conjunctions and disjunctions. There was no Ehrenfeucht-Fraisse game for $L_{ω_1ω}$ in the literature. In this paper we develop an Ehrenfeucht-Fraisse Game for $L_{ω_1ω}$. This game is based on a game for propositional and first ord…
The Stone-Weierstrass Theorem for compact Hausdorff spaces is a basic result of functional analysis with far-reaching consequences. We introduce an equational logic $\vDash_Δ$ associated with an infinitary variety $Δ$ and show that the Stone-Weierstrass Theorem is a consequence of the Beth definability property of $\vDash_Δ$, stating that every implicit definition can be made explicit. Further, we define an infinitary propositional logic $\vdash_Δ$ by means of a Hilbert-style calculus and prove a strong completeness result whereby the semantic notion of consequence associated with $\vdash_Δ$ c…
We prove preservation theorems for $\mathcal{L}_{ω_1, G}$, the countable fragment of Vaught's closed game logic. These are direct generalizations of the theorems of Łoś-Tarski (resp. Lyndon) on sentences of $\mathcal{L}_{ω_1, ω}$ preserved by substructures (resp. homomorphic images). The solution, in $ZFC$, only uses general features and can be extended to several variants of other strong first-order logic that do not satisfy the interpolation theorem; instead, the results on infinitary definability are used. This solves an open problem dating back to 1977. Another consequence of our approach …
In this paper, we explain how the connection between higher-order model-checking and linear logic recently exhibited by the authors leads to a new and conceptually enlightening proof of the selection problem originally established by Carayol and Serre using collapsible pushdown automata. The main idea is to start from an infinitary and colored relational semantics of the lambdaY-calculus already formulated, and to replace it by its finitary counterpart based on finite prime-algebraic lattices. Given a higher-order recursion scheme G, the finiteness of its interpretation in the model enables us…
This paper is part of a program initiated by Saharon Shelah to extend the model theory of first order logic to the non-elementary setting of abstract elementary classes (AECs). An abstract elementary class is a semantic generalization of the class of models of a complete first order theory with the elementary substructure relation. We examine the symmetry property of splitting (previously isolated by the first author) in AECs with amalgamation that satisfy a local definition of superstability. The key results are a downward transfer of symmetry and a deduction of symmetry from failure of the o…
In 1969, Per Lindstrom proved his celebrated theorem characterising the first-order logic and established criteria for the first-order definability of formal theories for discrete structures. K. J. Barwise, S. Shelah, J. Vaananen and others extended Lindstrom's characterizability program to classes of infinitary logic systems, including a recent paper by M. Dzamonja and J. Vaananen on Karp's chain logic, which satisfies interpolation, undefinability of well-order, and is maximal in the class of logic systems with these properties. The novelty of the chain logic is in its new definition of sati…
Let ϕbe a first order formula and M be a countable model. ϕ^M denotes the set of all assignments that satisfy ϕin M. Let M, N be countable models. A formula ϕdistinguishes these models if |ϕ^M|\neq |ϕ^N|. We show that the number of distinguishable countable models for a complete countable first order theory, satisfies the Glimm Effross dichotomy, hence also Vaught's conjecture. The proof in the presence of equality is fairly easy, though we need infinite conjunctions to implement it and somewhat heavy theorems from descriptive set theory. However, the case without equality seems to be much mor…
We investigate properties of the formula $p \to \Box p$ in the basic modal logic K. We show that K satisfies an infinitary weaker variant of the rule of margins $ϕ\to \Boxϕ/ ϕ, \negϕ$, and as a consequence, we obtain various negative results about admissibility and unification in K. We describe a complete set of unifiers (i.e., substitutions making the formula provable) of $p \to \Box p$, and use it to establish that K has the worst possible unification type: nullary. In well-behaved transitive modal logics, admissibility and unification can be analyzed in terms of projective formulas, introdu…
