首页/论文/2012.08309

arXiv 2012.083092020-12math.LO

A note on the intuitionistic logic of false belief

Tomasz Witczak

备注：: Initial report on the question of intuitionistic logic of false belief

英文摘要：

In this paper we analyse logic of false belief in intuitionistic setting. This logic, studied in its classical version by Steinsvold, Fan, Gilbert and Venturi, describes the following situation: a formula F is not satisfied in a given world, but we still believe in it (or we think that it should be accepted). Another interpretations are also possible: e.g. that we do not accept F but it is imposed on us by a kind of council or advisory board. From the mathematical point of view, the idea is expressed by an adequate form of modal operator W which is interpreted in relational frames with neighborhoods. We discuss monotonicity of forcing, soundness, completeness and several other issues. We present also some simple systems in which confirmation of previously accepted formula is modelled.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Curry-Howard-Lambek Correspondence for Intuitionistic Belief

This paper introduces a natural deduction calculus for intuitionistic logic of belief $\mathsf{IEL}^{-}$ which is easily turned into a modal $λ$-calculus giving a computational semantics for deductions in $\mathsf{IEL}^{-}$. By using that interpretation, it is also proved that $\mathsf{IEL}^{-}$ has good proof-theoretic properties. The correspondence between deductions and typed terms is then extended to a categorical semantics for identity of proofs in $\mathsf{IEL}^{-}$ showing the general structure of such a modality for belief in an intuitionistic framework.

2020-12-15cs.LOmath.LO

An analytic calculus for intuitionistic belief

Intuitionistic belief has been axiomatized by Artemov and Protopopescu as an extension of intuitionistic propositional logic by means of the distributivity scheme K, and of co-reflection $A\rightarrow\Box A$. This way, belief is interpreted as a result of verification, and it fits an extended Brouwer-Heyting-Kolmogorov interpretation for intuitionistic propositional logic with an epistemic modality. In the present paper, structural properties of a natural deduction system $\mathsf{IEL}^{-}$ for intuitionistic belief are investigated. The focus is on the analyticity of the calculus, so that the…

2021-06-27cs.LOmath.LO

Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic

In their seminal paper Artemov and Protopopescu provide Hilbert formal systems, Brower-Heyting-Kolmogorov and Kripke semantics for the logics of intuitionistic belief and knowledge. Subsequently Krupski has proved that the logic of intuitionistic knowledge is PSPACE-complete and Su and Sano have provided calculi enjoying the subformula property. This paper continues the investigations around to sequent calculi for Intuitionistic Epistemic Logics by providing sequent calculi that have the subformula property and that are terminating in linear depth. Our calculi allow us to design a procedure th…

2021-03-04math.LO

An Arithmetical Interpretation of Verification and Intuitionistic Knowledge

Intuitionistic epistemic logic introduces an epistemic operator, which reflects the intended BHK semantics of intuitionism, to intuitionistic logic. The fundamental assumption concerning intuitionistic knowledge and belief is that it is the product of verification. The BHK interpretation of intuitionistic logic has a precise formulation in the Logic of Proofs and its arithmetical semantics. We show here that this interpretation can be extended to the notion of verification upon which intuitionistic knowledge is based, thereby providing the systems of intuitionistic epistemic logic extended by …

2016-01-12math.LO

Intuitionistic Epistemic Logic

We outline an intuitionistic view of knowledge which maintains the original Brou\-wer-Heyting-Kolmogorov semantics for intuitionism and is consistent with the well-known approach that intuitionistic knowledge be regarded as the result of verification. We argue that on this view co-reflection $A \rightarrow {\bf{K}} A$ is valid and the factivity of knowledge holds in the form ${\bf{K}} A \rightarrow \neg\neg A$ `known propositions cannot be false'. We show that the traditional form of factivity ${\bf{K}} A \rightarrow A$ is a distinctly classical principle which, like {\it tertium non datur} $A…

2016-01-16math.LO

Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic

A cyclic proof system gives us another way of representing inductive definitions and efficient proof search. In 2011 Brotherston and Simpson conjectured the equivalence between the provability of the classical cyclic proof system and that of the classical system of Martin-Lof's inductive definitions. This paper studies the conjecture for intuitionistic logic. This paper first points out that the countermodel of FOSSACS 2017 paper by the same authors shows the conjecture for intuitionistic logic is false in general. Then this paper shows the conjecture for intuitionistic logic is true under ari…

2017-12-10cs.LOmath.LO

更多相关论文收起更多论文

错误信念与极端无知的逻辑

Logics of False Belief and Radical Ignorance

本文解决了错误信念传递逻辑的公理化开放难题，利用错误信念算子对标准信念算子的“几乎可定义”性找到核心公理，提出统一典范关系证明完备性，并将结果推广到极端无知逻辑。

2024-04-11cs.LOmath.LO

Categorical and Algebraic Aspects of the Intuitionistic Modal Logic $\operatorname{IEL}^{-}$ and its predicate extensions

The system of intuitionistic modal logic ${\bf IEL}^{-}$ was proposed by S. Artemov and T. Protopopescu as the intuitionistic version of belief logic \cite{Artemov}. We construct the modal lambda calculus which is Curry-Howard isomorphic to ${\bf IEL}^{-}$ as the type-theoretical representation of applicative computation widely known in functional programming. We also provide a categorical interpretation of this modal lambda calculus considering coalgebras associated with a monoidal functor on a cartesian closed category. Finally, we study Heyting algebras and locales with corresponding operat…

2020-12-07math.CTmath.LO

An interpolant in predicate Gödel logic

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…

2019-02-12math.LO

直觉主义量子逻辑视角：静态与动态修正算子

Intuitionistic Quantum Logic Perspective: Static and Dynamic Revision Operators

本文结合两种直觉主义量子逻辑框架建立真值赋值，提出与量子系统静态和动态推理模式相对应的静态与动态修正算子，并探讨了它们在自然修正理论框架下对后承关系的共同影响及顺序依赖性。

2024-05-30math.LOquant-ph

Notes on neighborhood semantics for logics of unknown truths and false beliefs

School of Humanities, University of Chinese Academy of Sciences（中国科学院大学人文学院）

In this article, we study logics of unknown truths and false beliefs under neighborhood semantics. We compare the relative expressivity of the two logics. It turns out that they are incomparable over various classes of neighborhood models, and the combination of the two logics are equally expressive as standard modal logic over any class of neighborhood models. We propose morphisms for each logic, which can help us explore the frame definability problem, show a general soundness and completeness result, and generalize some results in the literature. We axiomatize the two logics over various cl…

2020-02-22cs.AImath.LO

Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer)

We produce a decidable super-intuitionistic normal modal logic of internalised intuitionistic (and thus disjunctive and monotonic) interactive proofs (LIiP) from an existing classical counterpart of classical monotonic non-disjunctive interactive proofs (LiP). Intuitionistic interactive proofs effect a durable epistemic impact in the possibly adversarial communication medium CM (which is imagined as a distinguished agent), and only in that, that consists in the permanent induction of the perfect and thus disjunctive knowledge of their proof goal by means of CM's knowledge of the proof: If CM k…

2014-04-08cs.CRcs.LOmath.LO

The Price of Mathematical Scepticism

This paper argues that, insofar as we doubt the bivalence of the Continuum Hypothesis or the truth of the Axiom of Choice, we should also doubt the consistency of third-order arithmetic, both the classical and intuitionistic versions. Underlying this argument is the following philosophical view. Mathematical belief springs from certain intuitions, each of which can be either accepted or doubted in its entirety, but not half-accepted. Therefore, our beliefs about reality, bivalence, choice and consistency should all be aligned.

2022-05-25math.HOmath.LO

Denial Logic

Denial Logic DL, a system of justification logic, is the logic of an agent whose justified beliefs are false, who cannot avow his own propositional attitudes or believe tautologies, but who can believe contradictions. Using Artemov's natural semantics for justification logic JL, in which justifications are interpreted as sets of formulas, we provide an inductive construction of models of DL, and show that DL is sound and complete. Some notions developed for JL, such as constant specifications and the internalization property, are inconsistent with DL. In contrast, we define negative constant s…

2012-09-14math.LO