Hájek提出的公理系统公理化了基于BL-链的一阶逻辑。本研究通过增加公理$(\u000bforall x ϕ)^2 \leftrightarrow \forall x ϕ^2$以及无穷规则$\frac{ϕ\vee(α\toβ^n):n\in\mathbb{N}}{ϕ\vee(α\toα\\&β)}$来扩展该系统，以获得关于连续t-模的强完全性。
英文摘要：
The axiomatic system introduced by Hájek axiomatizes first-order logic based on BL-chains. In this study, we extend this system with the axiom $(\forall x ϕ)^2 \leftrightarrow \forall x ϕ^2$ and the infinitary rule \[ \frac{ϕ\vee (α\to β^n):n \in \mathbb{N}}{ϕ\vee (α\to α\& β)} \] to achieve strong completeness with respect to continuous t-norms.
Completeness and interpolation for intuitionistic infinitary predicate logic, in connection to finitizing the class of representable Heyting polyadic algebras
It is known that intuitionistic Kripke semantics can be generalized so that it can treat arbitrary propositional connectives characterized by truth functions. We extend this generalized Kripke semantics to first-order logic, and study how the choice of connectives changes the relation between intuitionistic predicate logic and the logic of constant domains in terms of validity of sequents. Our main result gives a simple necessary and sufficient condition for the set of valid sequents in intuitionistic predicate logic to coincide with the set of valid sequents in the logic of constant domains.
In Pure Inductive Logic, the principle of Strong Predicate Exchangeability is a rational principle based on symmetry that sits in between the principles of Predicate Exchangeability and Atom Exchangeability. We will show a de Finetti - style representation theorem for probability functions that satisfy this principle in addition to Unary Language Invariance.
This paper is a contribution to the study of the universal Horn fragment of predicate fuzzy logics, focusing on the proof of the existence of free models of theories of Horn clauses over Rational Pavelka predicate logic. We define the notion of a term structure associated to every consistent theory T over Rational Pavelka predicate logic and we prove that the term models of T are free on the class of all models of T. Finally, it is shown that if T is a set of Horn clauses, the term structure associated to T is a model of T.
A logic satisfies the interpolation property provided that whenever a formula Δ is a consequence of another formula Γ, then this is witnessed by a formula Θ which only refers to the language common to Γ and Δ. That is, the relational (and functional) symbols occurring in Θ occur in both Γ and Δ, Γ has Θ as a consequence, and Θ has Δ as a consequence. Both classical and intuitionistic predicate logic have the interpolation property, but it is a long open problem which intermediate predicate logics enjoy it. In 2013 Mints, Olkhovikov, and Urquhart showed that constant domain intuitionistic logic…
We report on the current status of our on-going project to develop well-behaved hypersequent calculi for intermediate predicate logics, such as the linearity axiom $\mathbf{LIN}\colon\left(φ\toψ\right)\lor\left(ψ\toφ\right)$ and the constant domain axiom $\mathbf{CD}\colon\forall x\left(φ\lorψ\left(x\right)\right)\toφ\lor\forall xψ\left(x\right)$.
In this paper, we investigate Rosser provability predicates whose provability logics are normal modal logics. First, we prove that there exists a Rosser provability predicate whose provability logic is exactly the normal modal logic ${\sf KD}$. Secondly, we introduce a new normal modal logic ${\sf KDR}$ which is a proper extension of ${\sf KD}$, and prove that there exists a Rosser provability predicate whose provability logic includes ${\sf KDR}$.
It is known that not only classical semantics but also intuitionistic Kripke semantics can be generalized so that it can treat arbitrary propositional connectives characterized by truth tables, or truth functions. In our previous work, it has been shown that the set of Kripke-valid propositional sequents and that of classically valid propositional sequents coincide if and only if all available propositional connectives are monotonic. The present paper extend this result to frst-order logic showing that, in the case of predicate logic, the condition that all available propositional connectives …
It is well known that the propositional modal logic $\mathbf{GL}$ of provability satisfies the de Jongh-Sambin fixed-point property. On the other hand, Montagna showed that the predicate modal system $\mathbf{QGL}$, which is the natural variant of $\mathbf{GL}$, loses the fixed-point property. In this paper, we discuss some versions of the fixed-point property for predicate modal logics. First, we prove that several extensions of $\mathbf{QGL}$ including $\mathbf{NQGL}$ do not have the fixed-point property. Secondly, we prove the fixed-point theorem for the logic $\mathbf{QK} + \Box^{n+1} \bot…
Algebraisable versions of predicate topological logic
动机是这样的问题：哪些空间结构可以通过模态逻辑来表征，什么是空间逻辑，如何在模态逻辑中编码不同的几何关系，拓扑逻辑基于拓扑空间而不是Kripke框架提供了用于研究$\sf S4$模态的拓扑语义的汇合的框架。继Sgro的研究和Georgescu的代数研究之后，我们证明了谓词拓扑逻辑和Chang的模态逻辑的各种扩展的一个内插定理和一个省略类型定理。我们的证明是柱形代数分别使用内部算子和盒子的代数寻址展开。然后，我们像抽象代数逻辑一样，研究这两种逻辑的可代数扩展;获得有关其代数对应物的各个子类（这些子类是变种）的合并性质的大量结果。讨论了有限维拓扑柱形代数的原子正则性和完备表示等概念。我们的代数结果的逻辑后果仔细制定了张的谓词模态逻辑和有限版本的无限扩展，通过限制$n$变量，$n$有限的，被视为一个命题多维模态逻辑，和$n$产品的双峰，其框架的形式是$(U, U\times U, R)$其中$R$是一个前序，赋予对角常数。
In this paper, we introduce a proof system $\mathsf{NQGL}$ for a Kripke complete predicate extension of the logic $\mathbf{GL}$, that is, the logic of provability, which is defned by $\mathbf{K}$ and the Löb formula $\Box(\Box p\supset p)\supset\Box p$. $\mathsf{NQGL}$ is a modal extension of Gentzen's sequent calculus $\mathsf{LK}$. Although the propositional fragment of $\mathsf{NQGL}$ axiomatizes $\mathbf{GL}$, it does not have the Löb formula as its axiom. Instead, it has a non-compact rule, that is, a derivation rule with countably many premises. We show that $\mathsf{NQGL}$ enjoys cut ad…
We provide a sound and complete proof system for an extension of Kleene's ternary logic to predicates. The concept of theory is extended with, for each function symbol, a formula that specifies when the function is defined. The notion of "is defined" is extended to terms and formulas via a straightforward recursive algorithm. The "is defined" formulas are constructed so that they themselves are always defined. The completeness proof relies on the Henkin construction. For each formula, precisely one of the formula, its negation, and the negation of its "is defined" formula is true on the constr…
We consider quantified pretransitive Horn modal logic. It is known that such logics are complete with respect to predicate Kripke frames with expanding domains. In this paper we prove that they are also complete with respect to neighbourhood frames with constant domains.
Following G. Mints(Kluwer 2000 and draft 2013), we present terminating and bicomplete proof searches in multi-succedent sequent calculi for intuitionistic propositional logic, fragments of intuitionistic predicate logic and full intuitionistic predicate logic in the spirit of Schuette's schema.
We investigate the relationship between recursive enumerability and elementary frame definability in first-order predicate modal logic. On the one hand, it is well-known that every first-order predicate modal logic complete with respect to an elementary class of Kripke frames, i.e., a class of frames definable by a classical first-order formula, is recursively enumerable. On the other, numerous examples are known of predicate modal logics, based on `natural' propositional modal logics with essentially second-order Kripke semantics, that are either not recursively enumerable or Kripke incomplet…
An algebraic proof is presented for the finite strong standard completeness of involutive uninorm logic with fixed point. The result may provide a first step towards settling the open standard completeness problem for involutive uninorm logic posed in [G. Metcalfe, F. Montagna: Substructural fuzzy logics, J. Symb. Logic, 72, 834-864 (2007)].
We present a completeness result for the implicit fragment of justification stit logic. Although this fragment allows for no strongly complete axiomatization, we show that a restricted form of strong completeness (subsuming weak completeness) is available, as well as deduce a version of restricted compactness property.
We begin the study of categorical logic for continuous model theory. In particular, we 1. introduce the notions of metric logical categories and functors as categorical equivalents of a metric theory and interpretations, 2. prove a continuous version of conceptual completeness showing that $T^\eq$ is the maximal conservative expansion of $T$, and 3. define the concept of a metric pre-topos.
A logic is said to admit an equational completeness theorem when it can be interpreted into the equational consequence relative to some class of algebras. We characterize logics admitting an equational completeness theorem that are either locally tabular or have some tautology. In particular, it is shown that a protoalgebraic logic admits an equational completeness theorem precisely when its has two distinct logically equivalent formulas. While the problem of determining whether a logic admits an equational completeness theorem is shown to be decidable both for logics presented by a finite set…
We present a completeness result for a logical system which combines stit logic and justification logic in order to represent proving activity of the agents. This logic is interpreted over the semantics introduced in earlier publications. We define a Hilbert-style axiomatic system for this logic and show that this system is strongly complete relative to the intended semantics.
In this paper, we present a generalized effective completeness theorem for continuous logic. The primary result is that any continuous theory is satisfied in a structure which admits a presentation of the same Turing degree. It then follows that any decidable theory is satisfied by a computably presentable structure. This modifies and extends previous partial effective completeness theorems for continuous logic given by Calvert and Didehvar, Ghasemloo, and Pourmahdian.
We give a sufficient condition for Kripke completeness of modal logics enriched with the transitive closure modality. More precisely, we show that if a logic admits what we call definable filtration (ADF), then such an expansion of the logic is complete; in addition, has the finite model property, and again ADF. This argument can be iterated, and as an application we obtain the finite model property for PDL-like expansions of logics that ADF.
The problems of logical translation of axiomatizations and the choice of primitive operators have surfaced several times over the years. An early issue was raised by H. Hi{\. z} in the 1950s on the incompleteness of translated calculi. Further pertinent work, some of it touched on here, was done in the 1970s by W. Frank and S. Shapiro, as well as by others in subsequent decades. As we shall see, overlooking such possibilities has led to incorrect claims of completeness being made (e.g. by J. L. Bell and A. B. Slomson as well as J. N. Crossley) for axiomatizations of classical predicate logic o…
Satisfaction relations for proper classes: Applications in logic and set theory
我们开发的理论，部分满意度关系的结构，可能是适当的类，并定义一个满意度谓词适当的结构。我们指出了这个理论作为一阶谓词逻辑和集合论的元理论的发展框架的效用，并利用它证明了对于ZF（Zermelo-Fraenkel集合论）的任何递归可公理化扩张T，存在GB（von Neumann-Bernays-Gödel class theory）的可公理化扩张T'，它是T的保守扩张。我们还证明了一个保守的扩展结果，证明了使用这个谓词来表征地面模型强迫建设。
In this paper, we study the provability logic of intuitionistic theories of arithmetic that prove their own completeness. We prove a completeness theorem for theories equipped with two provability predicates $\Box$ and $\triangle$ that prove the schemes $A\to\triangle A$ and $\Box\triangle S\to\Box S$ for $S\inΣ_1$. Using this theorem, we determine the logic of fast provability for a number of intuitionistic theories. Furthermore, we reprove a theorem previously obtained by M. Ardeshir and S. Mojtaba Mojtahedi determining the $Σ_1$-provability logic of Heyting Arithmetic.
We consider the explicit fragment of the basic justification stit logic introduced in earlier publications. We define a Hilbert-style axiomatic system for this logic and show that this system is strongly complete relative to the intended semantics.
The logics RL, RP, and RG have been obtained by expanding Lukasiewicz logic L, product logic P, and Gödel--Dummett logic G with rational constants. We study the lattices of extensions and structural completeness of these three expansions, obtaining results that stand in contrast to the known situation in L, P, and G. Namely, RL is hereditarily structurally complete. RP is algebraized by the variety of rational product algebras that we show to be Q-universal. We provide a base of admissible rules in RP, show their decidability, and characterize passive structural completeness for extensions of …
We study modal completeness and incompleteness of several sublogics of the interpretability logic $\mathbf{IL}$. We introduce the sublogic $\mathbf{IL}^-$, and prove that $\mathbf{IL}^-$ is sound and complete with respect to Veltman prestructures which are introduced by Visser. Moreover, we prove the modal completeness of twelve logics between $\mathbf{IL}^-$ and $\mathbf{IL}$ with respect to Veltman prestructures. On the other hand, we prove that eight natural sublogics of $\mathbf{IL}$ are modally incomplete. Finally, we prove that these incomplete logics are complete with respect to general…
We study the complexity of predicate logics based on team semantics. We show that the satisfiability problems of two-variable independence logic and inclusion logic are both NEXPTIME-complete. Furthermore, we show that the validity problem of two-variable dependence logic is undecidable, thereby solving an open problem from the team semantics literature. We also briefly analyse the complexity of the Bernays-Schönfinkel-Ramsey prefix classes of dependence logic.
The paper studies the containment companion of a logic $\vdash$. This consists of the consequence relation $\vdash^{r}$ which satisfies all the inferences of $\vdash$, where the variables of the conclusion are \emph{contained} into those of the (set of) premises. In accordance with our previous work on logics of left variable inclusion, we show that a different generalization of the Płonka sum construction, adapted from algebras to logical matrices, allows us to provide a matrix-based semantics for containment logics. In particular, we provide an appropriate completeness theorem for a wide fam…
In this paper we prove that three of the main propositional logics of dependence (including propositional dependence logic and inquisitive logic), none of which is structural, are structurally complete with respect to a class of substitutions under which the logics are closed. We obtain an analogues result with respect to stable substitutions, for the negative variants of some well-known intermediate logics, which are intermediate theories that are closely related to inquisitive logic.
