Benoît Jubin
We give a normal five-valued truth-table proving independence of one of the axioms in Robinson's set of axioms for propositional calculus from 1968, answering a question raised in his article, where he uses a non-normal truth-table. We also give a normal four-valued truth-table proving independence of one of the other axioms, where he uses a normal five-valued truth-table.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
In this paper, we construct an undecidable 3-variable superintuitionistic propositional calculus, i.e., a finitely axiomatizable extension of the intuitionistic propositional calculus with axioms containing only 3 variables. Since there are no 2-variable superintuitionistic propositional calculi, this is the minimal possible number of variables.
We give sound and complete Hilbert-style axiomatizations for propositional dependence logic (PD), modal dependence logic (MDL), and extended modal dependence logic (EMDL) by extending existing axiomatizations for propositional logic and modal logic. In addition, we give novel labeled tableau calculi for PD, MDL, and EMDL. We prove soundness, completeness and termination for each of the labeled calculi.
In this paper we explore the following question: how weak can a logic be for Rosser's essential undecidability result to be provable for a weak arithmetical theory? It is well known that Robinson's Q is essentially undecidable in intuitionistic logic, and P. Hajek proved it in the fuzzy logic BL for Grzegorczyk's variant of Q which interprets the arithmetic operations as non-total non-functional relations. We present a proof of essential undecidability in a much weaker substructural logic and for a much weaker arithmetic theory, a version of Robinson's R (with arithmetic operations also interp…
In this paper we consider propositional calculi, which are finitely axiomatizable extensions of intuitionistic implicational propositional calculus together with the rules of modus ponens and substitution. We give a proof of undecidability of the following problem for these calculi: whether a given finite set of propositional formulas constitutes an adequate axiom system for a fixed propositional calculus. Moreover, we prove the same for the following restriction of this problem: whether a given finite set of theorems of a fixed propositional calculus derives all theorems of this calculus. The…
We study $Q$-tableaux and axiom systems that they engender, producing a new proof that the Implicational Propositional Calculus is complete.
In 1988, Ivlev proposed four-valued non-deterministic semantics for modal logics in which the alethic T axiom holds good. Unfortunately, no completeness was proved. In previous work, we proved completeness for some Ivlev systems and extended his hierarchy, proposing weaker six-valued systems in which the T axiom was replaced by the deontic D axiom. Here, we eliminate both axioms, proposing even weaker systems with eight values. Besides, we prove completeness for those new systems. It is natural to ask if a characterization by finite ordinary (deterministic) logical matrices would be possible f…
Nontrivial single axiom schemata and their quasi-nontriviality of Leśniewski-Ishimoto's propositional ontology $\bf L_1$
本文介绍了Leśniewski-Ishimoto命题本体论$\bf L_1$自1995年发现的非平凡单一公理模式($\mathrm{A_{M8}}$)的研究进展，提出了非平凡性与准非平凡性标准，给出了多个简化公理模式及其性质，并提出了若干非平凡单一公理模式的猜想。
In this paper, we consider iterative propositional calculi, which are finite sets of propositional formulas together with the rules of modus ponens and weak substitution (when formula being substituted must be already inferred). We construct an undecidable iterative propositional calculus using axioms in 3 variables. Particulary, we show that the general problem of derivability for these calculi is undecidable.
Cieśliński asked whether compositional truth theory with the additional axiom that all propositional tautologies are true is conservative over Peano Arithmetic. We provide a partial answer to this question, showing that if we additionally assume that truth predicate agrees with arithmetical truth on quantifier-free sentences, the resulting theory is as strong as $Δ_0$-induction for the compositional truth predicate, hence non-conservative. On the other hand, it can be shown with a routine argument that the principle of quantifier-free correctness is itself conservative.
Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
本文借助同伦类型理论与带属性范畴，通过上下文间典范同伦等价证明外延类型理论对带命题计算公理的依赖类型理论具有保守性。
Quantified propositional Goedel logics
证明了基于真值集V-up = {1 - 1/n：n >= 1} u {1}的量化命题Goedel-Dummett逻辑G-up是可判定的.这一结果是由Buechi的理论S1 S得到的。基于量词消去的另一种证明也被给出，它给出了G-up作为所有有限值量化命题Goedel逻辑的交集的公理化和特征化.
Orthologic with Axioms
本文研究带公理的正交逻辑，通过限制相继式至多含两个公式的证明系统建立广义切消与三次时间可判定算法，并提出有效命题正交逻辑及其可靠完备系统。
Kalmár-style constructive completeness proofs for classical positive propositional calculi
本文通过改编 Kalmár 完备性证明方法，构造性地证明了多个经典正命题演算（含 Peirce 律）的完备性，并利用定义析取等技巧简化了相关演算的完备性推导。
It is a consequence of existing literature that least and greatest fixed-points of monotone polynomials on Heyting algebras-that is, the alge- braic models of the Intuitionistic Propositional Calculus-always exist, even when these algebras are not complete as lattices. The reason is that these extremal fixed-points are definable by formulas of the IPC. Consequently, the $μ$-calculus based on intuitionistic logic is trivial, every $μ$-formula being equiv- alent to a fixed-point free formula. We give in this paper an axiomatization of least and greatest fixed-points of formulas, and an algorithm…
It is a consequence of existing literature that least and greatest fixed-points of monotone polynomials on Heyting algebras-that is, the algebraic models of the Intuitionistic Propositional Calculus-always exist, even when these algebras are not complete as lattices. The reason is that these extremal fixed-points are definable by formulas of the IPC. Consequently, the $μ$-calculus based on intuitionistic logic is trivial, every $μ$-formula being equivalent to a fixed-point free formula. We give in this paper an axiomatization of least and greatest fixed-points of formulas, and an algorithm to …
Non-iterative normal modal logics are defined by axioms of modal degree 1. In this paper we use calculations with normal forms to determine the set of all possible non-iterative normal modal logics, unimodal propositional extensions of K. To characterize them, we construct the complete set (lattice) of such logics and we provide the generic specification of their axioms and their semantics.
Cirquent calculus is a new proof-theoretic and semantic approach introduced for the needs of computability logic by G.Japaridze, who also showed that, through cirquent calculus, one can capture, refine and generalize independence-friendly (IF) logic. Specifically, the approach allows us to account for independence from propositional connectives in the same spirit as the traditional IF logic accounts for independence from quantifiers. Japaridze's treatment of IF logic, however, was purely semantical, and no deductive system was proposed. The present paper constructs a formal system sound and co…
This paper investigates formal logics for reasoning about determinacy and independence. Propositional Dependence Logic D and Propositional Independence Logic I are recently developed logical systems, based on team semantics, that provide a framework for such reasoning tasks. We introduce two new logics L_D and L_I, based on Kripke semantics, and propose them as alternatives for D and I, respectively. We analyze the relative expressive powers of these four logics and discuss the way these systems relate to natural language. We argue that L_D and L_I naturally resolve a range of interpretational…
A propositional cirquent calculus for computability logic
本文提出CL18公理化系统，用于可计算性逻辑的基本命题片段，并证明其相对于该逻辑博弈语义的可靠性与完备性。
PBNF-transform as a formulation of Propositional Calculus, I
本文提出PBNF变换作为命题演算的公式化方法，通过多项式家族实现逻辑连接词的几何化表示，简化了计算方法。
In this paper we investigate certain systems of propositional intuitionistic modal logic defined semantically in terms of neighborhood structures. We discuss various restrictions imposed on those frames but our constant approach is to discard superset axiom. Such assumption allows us to think about specific modalities $Δ, \nabla$ and new functor $\rightsquigarrow$ depending on the notion of maximal neighborhood. We show how it is possible to treat our models as bi-relational ones. We prove soundness and completeness of proposed axiomatization by means of canonical model. Moreover, we show that…
We show that for $Π_2$-properties of second or third order arithmetic as formalized in appropriate natural signatures the apparently weaker notion of forcibility overlaps with the standard notion of consistency (assuming large cardinal axioms). Among such $Π_2$-properties we mention: the negation of the Continuum hypothesis, Souslin Hypothesis, the negation of Whitehead's conjecture on free groups, the non-existence of outer automorphisms for the Calkin algebra, etc... In particular this gives an a posteriori explanation of the success forcing (and forcing axioms) met in producing models of su…
Generating proof systems for three-valued propositional logics
本文说明了如何利用 3-标号演算和 Set-Set Hilbert 风格演算，通过生成和精简子过程，为三值逻辑矩阵定义的逻辑自动生成有限公理化，并证明了两者在单演矩阵下可相互转换。
We study propositional logical systems arising from the language of Johansson's minimal logic and obtained by weakening the requirements for the negation operator. We present their semantics as a variant of neighbourhood semantics. We use duality and completeness results to show that there are uncountably many subminimal logics. We also give model-theoretic and algebraic definitions of filtration for minimal logic and show that they are dual to each other. These constructions ensure that the propositional minimal logic has the finite model property. Finally, we define and investigate bi-modal …
This paper aims to give an epistemic interpretation to the tensor disjunction in dependence logic, through a rather surprising connection to the so-called weak disjunction in Medvedev's early work on intermediate logic under the Brouwer-Heyting-Kolmogorov (BHK)-interpretation. We expose this connection in the setting of inquisitive logic with tensor disjunction discussed by Ciardelli and Barbero (2019}, but from an epistemic perspective. More specifically, we translate the propositional formulae of inquisitive logic with tensor into modal formulae in a powerful epistemic language of "knowing h…
By a well-known result of Kotlarski, Krajewski, and Lachlan (1981), first-order Peano arithmetic $PA$ can be conservatively extended to the theory $CT^{-}[PA]$ of a truth predicate satisfying compositional axioms, i.e., axioms stating that the truth predicate is correct on atomic formulae and commutes with all the propositional connectives and quantifiers. This results motivates the general question of determining natural axioms concerning the truth predicate that can be added to $CT^{-}[PA]$ while maintaining conservativity over $PA$. Our main result shows that conservativity fails even for t…
Marginalia to a Theorem of Asperó and Schindler
本文通过博弈论刻画了添加无穷命题公式模型的偏序条件，并利用该条件为 Asperó–Schindler 定理（$\mathsf{MM}^{++}$ 蕴含 Woodin 公理 $(*)$）提供了新证明。
We examine Paul Halmos' comments on category theory, Dedekind cuts, devil worship, logic, and Robinson's infinitesimals. Halmos' scepticism about category theory derives from his philosophical position of naive set-theoretic realism. In the words of an MAA biography, Halmos thought that mathematics is "certainty" and "architecture" yet 20th century logic teaches us is that mathematics is full of uncertainty or more precisely incompleteness. If the term architecture meant to imply that mathematics is one great solid castle, then modern logic tends to teach us the opposite lession, namely that t…
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…
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。