In this paper we consider an approach where both propositions and the accessibility relation are infinitely many-valued over Gödel algebras. In particular, we consider separately the $\Box $-fragment and the $\Diamond $-fragment of our Gödel modal logic and prove that both logics are complete with respect to the class of models with values in the linear Hetying algebra [0,1]. In addition, we show that the first fragment is uniquely determined by the class of models having crisp accessibility relation but it has not the finite model property. On the contrary, the second fragment is not characterized by crisp accessibility models alone but it has the finite model property. Finally, we show that the approach can be extended to include finitely many rational truth-values à la Pavelka.
We show that the standard Gödel modal logics, as initially introduced by Caicedo and Rodriguez in \cite{CR2009,CR2010}, are not realized by the basic Gödel justification logics although being related by the forgetful projection.
We study abstract versions of Gödel's second incompleteness theorem and formulate generalizations of Löb's derivability conditions that work for logics weaker than the classical one. We isolate the role of contraction rule in Gödel's theorem and give a (toy) example of a system based on modal logic without contraction invalidating Gödel's argument.
We study an extension of \g propositional logic whose corresponding algebra is an ordered Abelian group. Then we expand the ideas to first-order case of this logic.
We study public announcement operators in the context of standard Gödel modal logic as introduced by Caicedo and Rodriguez. Over that base logic, admitting a natural semantics over [0,1]-valued generalizations of modal Kripke models, we exhibit three possible semantic interpretations of the public announcement operator, all equivalent in a classical setting, and show that these logics are all different in terms of expressive strength. We provide partial completeness results for these logics via Hilbert-style calculi.
Gödel modal logics can be seen as extenions of intutionistic modal logics with the prelinearity axiom. In this paper we focus on the algebraic and relational semantics for Gödel modal logics that leverages on the duality between finite Gödel algebras and finite forests, i.e. finite posets whose principal downsets are totally ordered. We consider different subvarieties of the basic variety of Gödel algebras with two modal operators (GAOs for short) and their corresponding classes of forest frames, either with one or two accessibility relations. These relational structures can be considered as p…
In this paper we continue the study of the variety $\mathbb{MG}$ of monadic Gödel algebras. These algebras are the equivalent algebraic semantics of the S5-modal expansion of Gödel logic, which is equivalent to the one-variable monadic fragment of first-order Gödel logic. We show three families of locally finite subvarieties of $\mathbb{MG}$ and give their equational bases. We also introduce a topological duality for monadic Gödel algebras and, as an application of this representation theorem, we characterize congruences and give characterizations of the locally finite subvarieties mentioned a…
Assuming the existence of suitable large cardinals, we show it is consistent that the Provability logic $\mathbf{GL}$ is complete with respect to the filter sequence of normal measures. This result answers a question of Andreas Blass from 1990 and a related question of Beklemishev and Joosten.
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…
This report first shows the equivalence bewteen several formulations of classical logic in intuitionistic logic (tertium non datur, reductio ad absurdum, Pierce's law). Then it establishes the correctness of the Gödel-Kolmogorov translation, whose restriction to the propositional case is due to Glivenko. This translation maps a formula $F$ of first order logic to a formula $F^{\lnot\lnot}$ in such a way that $F$ is provable in classical logic if and only if $F^{\lnot\lnot}$ is provable in intuitionistic logic. All formal proofs are presented in natural deduction. These questions are well-known…
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…
In this paper we consider the modal logic with both Box and Diamond arising fromKripke models with a crisp accessibility and whose propositions are valued over the stan-dard Godel algebra [0,1]G. We provide an axiomatic system extending the one from [3]for models with a valued accessibility with Dunn axiom from positive modal logics, andshow it is strongly complete with respect to the intended semantics. The axiomatizationsof the most usual frame restrictions are given too. We also prove that in the studied logicit is not possible to get Box as an abbreviation of Diamond, nor vice-versa, showi…
We introduce a~paraconsistent modal logic $\mathbf{K}\mathsf{G}^2$, based on Gödel logic with coimplication (bi-Gödel logic) expanded with a De Morgan negation $\neg$. We use the logic to formalise reasoning with graded, incomplete and inconsistent information. Semantics of $\mathbf{K}\mathsf{G}^2$ is two-dimensional: we interpret $\mathbf{K}\mathsf{G}^2$ on crisp frames with two valuations $v_1$ and $v_2$, connected via $\neg$, that assign to each formula two values from the real-valued interval $[0,1]$. The first (resp., second) valuation encodes the positive (resp., negative) information th…
Justification logics are special kinds of modal logics which provide a framework for reasoning about epistemic justifications. For this, they extend classical boolean propositional logic by a family of necessity-style modal operators "t:", indexed over t by a corresponding set of justification terms, which thus explicitly encode the justification for the necessity assertion in the syntax. With these operators, one can therefore not only reason about modal effects on propositions but also about dynamics inside the justifications themselves. We replace this classical boolean base with Gödel logi…
FCEyN - UBA（布宜诺斯艾利斯大学理学院与自然科学院）；University of Bern（伯尔尼大学）；IIIA - CSIC（西班牙国家研究委员会人工智能研究所）
In this paper, we provide simplified semantics for the logic K45(G), i.e. the many-valued Godel counterpart of the classical modal logic K45. More precisely, we characterize K45(G) as the set of valid formulae of the class of possibilistic Godel Kripke Frames <W,π> where W is a non-empty set of worlds and π: W \to [0, 1] is a possibility distribution on W.
An edited version is given of the text of Gödel's unpublished manuscript of the notes for a course in basic logic he delivered at the University of Notre Dame in 1939. Gödel's notes deal with what is today considered as important logical problems par excellence, completeness, decidability, independence of axioms, and with natural deduction too, which was all still a novelty at the time the course was delivered. Full of regards towards beginners, the notes are not excessively formalistic. Gödel presumably intended them just for himself, and they are full of abbreviations. This together with som…
This is an examination, a commentary, of links between some philosophical views ascribed to Gödel and general proof theory. In these views deduction is of central concern not only in predicate logic, but in set theory too, understood from an infinitistic ideal perspective. It is inquired whether this centrality of deduction could also be kept in the intensional logic of concepts whose building Gödel seems to have taken as the main task of logic for the future.
We further develop the paraconsistent Gödel modal logic. In this paper, we consider its version endowed with Kripke semantics on $[0,1]$-valued frames with two fuzzy relations $R^+$ and $R^-$ (degrees of trust in assertions and denials) and two valuations $v_1$ and $v_2$ (support of truth and support of falsity) linked with a De Morgan negation $\neg$. We demonstrate that it \emph{does not} extend Gödel modal logic and that $\Box$ and $\lozenge$ are not interdefinable. We also show that several important classes of frames are $\birelKGsquare$ definable (in particular, crisp, mono-relational, a…
Completeness and Incompleteness for Expanding Gödel-Löb Logics
School of Mathematics, Institute for Research in Fundamental Sciences (IPM)（基础科学研究所数学学院）；Department of Philosophy, University of Barcelona（巴塞罗那大学哲学系）；Centre de Recerca Matemàtica（数学研究中心）
Intuitionistic Propositional Logic is proved to be an infinitely many valued logic by Kurt Gödel (1932), and it is proved by Stanisław Jaśkowski (1936) to be a countably many valued logic. In this paper, we provide alternative proofs for these theorems by using models of Saul Kripke (1959). Gödel's proof gave rise to an intermediate propositional logic (between intuitionistic and classical), that is known nowadays as Gödel or the Gödel-Dummet Logic, and is studied by fuzzy logicians as well. We also provide some results on the inter-definablility of propositional connectives in this logic.
Valuations in Gödel Logic, and the Euler Characteristic
使用V. Klee和G.- C. Rota在六十年代，我们定义了哥德尔逻辑中公式的欧拉特征（在无穷多个真值上）。然后，我们证明了编码的信息的欧拉特征是经典的，即符合类似的概念定义的布尔逻辑。在此基础上，我们定义了公式$φ$的欧拉特征线的多值版本，并证明了它们确实提供了关于$φ$在哥德尔逻辑中的逻辑状态的信息。具体地说，我们的第一个主要结果表明，多值欧拉特征是分离的多值重言式从非重言式的不变量。此外，我们提供了这些广义特征的线性结构的初步调查。我们的第二个主要结果是多值特征的集合形成了一个线性独立集在实向量空间中的所有赋值的哥德尔逻辑在许多命题变量。
A new viewpoint of the Gödel's incompleteness theorem be given in this article which reveals the deep relationship between the logic and computation. Upon the results of these studies, an algorithm be given which shows how to search a proof of statement in first order logic from finite concrete examples, and an approach be proposed to improve searching mathematical proof by neural network.
Three variants of Kurt Gödel's ontological argument, proposed by Dana Scott, C. Anthony Anderson and Melvin Fitting, are encoded and rigorously assessed on the computer. In contrast to Scott's version of Gödel's argument the two variants contributed by Anderson and Fitting avoid modal collapse. Although they appear quite different on a cursory reading they are in fact closely related. This has been revealed in the computer-supported formal analysis presented in this article. Key to our formal analysis is the utilization of suitably adapted notions of (modal) ultrafilters, and a careful distinc…
In 1932, Gödel proved that there is no finite semantics for intuitionistic logic. We consider all fragments of intuitionistic logic and check in each case whether a finite semantics exists. We may fulfill a didactic goal, as little logic and algebra are presupposed.
An approach to universal (meta-)logical reasoning in classical higher-order logic is employed to explore and study simplifications of Kurt Gödel's modal ontological argument. Some argument premises are modified, others are dropped, modal collapse is avoided and validity is shown already in weak modal logics K and T. Key to the gained simplifications of Gödel's original theory is the exploitation of a link to the notions of filter and ultrafilter from topology. The paper illustrates how modern knowledge representation and reasoning technology for quantified non-classical logics can contribute n…
Gödel-McKinsey-Tarski and (not quite) Blok-Esakia for Heyting-Lewis Implication
School of Computing The Australian National University（澳大利亚国立大学计算机学院）；Chair For Theoretical Computer Science FAU Erlangen-Nuremberg（埃尔朗根-纽伦堡大学理论计算机科学教席）
The Gödel translation provides an embedding of the intuitionistic logic $\mathsf{IPC}$ into the modal logic $\mathsf{Grz}$, which then embeds into the modal logic $\mathsf{GL}$ via the splitting translation. Combined with Solovay's theorem that $\mathsf{GL}$ is the modal logic of the provability predicate of Peano Arithmetic $\mathsf{PA}$, both $\mathsf{IPC}$ and $\mathsf{Grz}$ admit arithmetical interpretations. When attempting to 'lift' these results to the monadic extensions $\mathsf{MIPC}$, $\mathsf{MGrz}$, and $\mathsf{MGL}$ of these logics, the same techniques no longer work. Following a…
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 introduce a syntactic translation of Goedel's System T parametrized by a weak notion of a monad, and prove a corresponding fundamental theorem of logical relation. Our translation structurally corresponds to Gentzen's negative translation of classical logic. By instantiating the monad and the logical relation, we reveal the well-known properties and structures of T-definable functionals including majorizability, continuity and bar recursion. Our development has been formalized in the Agda proof assistant.
We introduce two-dimensional logics based on Łukasiewicz and Gödel logics to formalize paraconsistent fuzzy reasoning. The logics are interpreted on matrices, where the common underlying structure is the bi-lattice (twisted) product of the $[0,1]$ interval. The first (resp.\ second) coordinate encodes the positive (resp.\ negative) information one has about a statement. We propose constraint tableaux that provide a modular framework to address their completeness and complexity.
