Jaykov Foukzon
In 1942 Haskell B.Curry presented what is now called Curry paradox which can be found in a logic independently of its stand on negation.In recent years there has been a revitalised interest in non-classical solutions to the semantic paradoxes. In this article the non-classical resolution of Curry's Paradox and Shaw-Kwei paradox without rejection any contraction postulate is proposed.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Intuitionistic first-order logic extended with a restricted form of Markov's principle is constructive and admits a Curry-Howard correspondence, as shown by Herbelin. We provide a simpler proof of that result and then we study intuitionistic first-order logic extended with unrestricted Markov's principle. Starting from classical natural deduction, we restrict the excluded middle and we obtain a natural deduction system and a parallel Curry-Howard isomorphism for the logic. We show that proof terms for existentially quantified formulas reduce to a list of individual terms representing all possi…
We add to intuitionistic logic infinitely many classical disjunctive tautologies and use the Curry--Howard correspondence to obtain typed concurrent $λ$-calculi; each of them features a specific communication mechanism, including broadcasting and cyclic message-exchange, and enhanced expressive power with respect to the $λ$-calculus. Moreover they all implement forms of code mobility. Our results provide a first concurrent computational interpretation for many propositional intermediate logics, classical logic included.
This reports introduces a novel sound and complete semantics for first order intuitionistic logic, in the framework of category theory and by the computational interpretation of the logic based on the so-called Curry-Howard isomorphism. Aside, a sound and complete semantics for the corresponding lambda-calculus is derived, too. This semantics extends, in a way, the more traditional meanings given by Heyting categories, the topos-theoretic interpretation, and Kripke models. The feature which justifies the introduction of this novel semantics is the fact that it is 'point-free', i.e., there is n…
This paper provides a proof that Tennant's logical system entails a paradox that is called Core logic paradox, in reference to the new name given by Tennant to his intuitionistic relevant logic.
Justification Logic of the Lambda Calculus
研究λ演算的证明逻辑，通过引入一种逻辑，其模态证明项为类型化λ项，能同时推理计算与证明。给出公理系统、自然演绎系统及Curry-Howard解释，还构建相继式演算并证明切割消去，得到归一化结果。
This paper sets out a predicative response to the Russell-Myhill paradox of propositions within the framework of Church's intensional logic. A predicative response places restrictions on the full comprehension schema, which asserts that every formula determines a higher-order entity. In addition to motivating the restriction on the comprehension schema from intuitions about the stability of reference, this paper contains a consistency proof for the predicative response to the Russell-Myhill paradox. The models used to establish this consistency also model other axioms of Church's intensional l…
Set theoretical paradoxes have a common root -- lack of understanding of why some multitudes are not sets. Why some multitudes of objects of thought cannot themselves be objects of thought? Moreover, it is a logical truth that such multitudes do exist. However we do not understand this logical truth so well as we understand, for example, the logical truth $\forall x \ x=x$. In this paper, we formulate a logical truth which we call the productivity principle. Bertrand Rusell was the first one to formulate this principle, but in a restricted form and with a different purpose. The principle expli…
Non-contractive logics, Paradoxes, and Multiplicative Quantifiers
本文研究规避悖论的非收缩逻辑，比较加法量词系统与Grišin集合论，分析乘法量词与真规则不相容的根源，并通过消去无穷切割规则证明无真乘法量词逻辑的相容性。
In game theory, the notion of a player's beliefs about the game players' beliefs about other players' beliefs arises naturally. In this paper, we present a non-self-referential paradox in epistemic game theory which shows that completely modeling players' epistemic beliefs and assumptions is impossible. Furthermore, we introduce an interactive temporal assumption logic to give an appropriate formalization of the new paradox. Formalizing the new paradox in this logic shows that there is no complete interactive temporal assumption model.
Stability and Paradox in Algorithmic Logic
无类型的逻辑系统被设计为一致地处理自引用的重要实例。一些相容的无类型系统也具有允许一般抽象或理解原则的特征，这导致了朴素集合论中的悖论。由于无类型系统具有这些特征，并且避免了在某些上下文中被认为是不自然的类型层次结构，因此它们有可能在数学的数学基础、类理论（产生比目前在集合论和范畴论中使用的更丰富的类概念）、属性理论、自然语言语义学、真值理论和理论计算机科学中发挥重要作用。显然，无类型系统必须在某种程度上偏离经典逻辑，但对于使用哪种无类型系统，以及应该允许哪些偏离经典逻辑，几乎没有达成一致。我们研究无类型逻辑的方法是研究一个自然发生的无类型系统，我们相信它在某种意义上是最终证明有用的系统的原型。本文所研究的逻辑称为算法逻辑，涉及到某些涉及算法的基本语句以及这些语句之间的算法推理规则。本文研究算法逻辑的命题性质。未来的论文将表明，算法逻辑具有一般的抽象原则。
In this note we study the effect of adding fixed points to justification logics. We introduce two extensions of justification logics: extensions by fixed point (or diagonal) operators, and extensions by least fixed points. The former is a justification version of Smorynski's Diagonalization Operator Logic, and the latter is a justification version of Kozen's modal $μ$-calculus. We also introduce fixed point extensions of Fitting's quantified logic of proofs, and formalize the Knower Paradox and the Surprise Test Paradox in these extensions. By interpreting a surprise statement as a statement f…
We present a calculus providing a Curry-Howard correspondence to classical logic represented in the sequent calculus with explicit structural rules, namely weakening and contraction. These structural rules introduce explicit erasure and duplication of terms, respectively. We present a type system for which we prove the type-preservation under reduction. A mutual relation with classical calculus featuring implicit structural rules has been studied in detail. From this analysis we derive strong normalisation property.
An observer-based approach to the sorites paradox and the logic derived from that
本文提出了一种基于观察者和时间依赖的三值逻辑方法，用于解决Sorites矛盾问题。
Logical systems with classical negation and means for sentential or propositional self-reference involve, in some way, paradoxical statements such as the liar. However, the paradox disappears if one replaces classical by an appropriate non-classical negation such as a paraconsistent one (no paradox arises if the liar is both true and false). We consider a non-Fregean logic which is a revised and extended version (Lewitzka 2012) of Epsilon-T-Logic originally introduced by (Straeter 1992) as a logic with a total truth predicate and propositional quantifiers. Self-reference is achieved by means o…
Turning the Liar paradox into a metatheorem of Basic logic
我们表明，自指可以形式化的基本逻辑的手段，通过新的连接词@，称为“纠缠”。事实上，连接词@的非恒等性是一个元定理，它说明一个自纠缠的句子失去了它自己的同一性。这就防止了在相应的元语言中出现自我指涉悖论。在这种情况下，我们引入了一个广义的自指定义，这是需要处理的乘法连接子结构逻辑。
The aim of this paper is to provide a logic-based conceptual analysis of the twin paradox (TwP) theorem within a first-order logic framework. A geometrical characterization of TwP and its variants is given. It is shown that TwP is not logically equivalent to the assumption of the slowing down of moving clocks, and the lack of TwP is not logically equivalent to the Newtonian assumption of absolute time. The logical connection between TwP and a symmetry axiom of special relativity is also studied.
Paradoxes are interesting puzzles in philosophy and mathematics, and they could be even more fascinating, when turned into proofs and theorems. For example, Liar's paradox can be translated into a propositional tautology, and Barber's paradox turns into a first-order tautology. Russell's paradox, which collapsed Frege's foundational framework, is now a classical theorem in set theory, implying that no set of all sets can exist. Paradoxes can be used in proofs of some other theorems; Liar's paradox has been used in the classical proof of Tarski's theorem on the undefinability of truth in suffic…
Here, by introducing a version of Unexpected hanging paradox first we try to open a new way and a new explanation for paradoxes, similar to liar paradox. Also, we will show that we have a semantic situation which no syntactical logical system could support it. Finally, we propose a claim in the subject of axiomatizibility. Based on this claim, having an axiomatic system for Computability Theory is not possible. In fact, the same argument shows that many other theories are non-axiomatizable. (Dare to say: General Theories of Physics and Mathematics).
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…
Predicate and Set Bundles in Multi-valued Logic
本文提出基于谓词丛的多值逻辑新模型，定义相关真值度与运算，研究集合丛并解决模态逻辑的必然性/可能性问题及连锁悖论。
Theoremizing Yablo's Paradox
本研究针对“所有悖论均源于循环/自指/对角线论证”的观点，将Yablo悖论的多个变体形式化，在线性时序逻辑（LTL）中证明相关定理，首次把Yablo悖论转化为数理逻辑领域的新定理。
Gödel-McKinsey-Tarski and (not quite) Blok-Esakia for Heyting-Lewis Implication
本文研究了海廷-刘易斯逻辑的语义和转换方法，通过框架语义和代数解释的对偶性，建立其与经典模态逻辑的关系，并证明了该逻辑的可判定性。
The investigations on higher-order type theories and on the related notion of parametric polymorphism constitute the technical counterpart of the old foundational problem of the circularity (or impredicativity) of second and higher order logic. However, the epistemological significance of such investigations, and of their often non trivial results, has not received much attention in the contemporary foundational debate. The results recalled in this paper suggest that the question of the circularity of second order logic cannot be reduced to the simple assessment of a vicious circle. Through a …
Foundations of real analysis and computability theory in non-Aristotelian finitary logic
本文概述了最近提出的非阿斯特丽德有限逻辑（NAFL）的实分析和可计算性理论的新范式。NAFL（NRA）中的构造性实分析是通过将欧几里德几何中的图解概念翻译成NAFL版本的皮亚诺算术（NPA）的扩展（NPAR）来完成的。这样的翻译是可能的，因为NPA证明了存在每一个可以用NPA语言定义的自然数的无限真类。NPAR中不允许无限集合，并且禁止对适当类进行量化;因此康托的对角线方法在NRA中不能合法地公式化，并且对于任何实数的集合（“超类”）都没有“基数”。经典实分析的许多有用的方面，如牛顿和莱布尼茨的微积分，在NRA中是合理的。但悖论，如芝诺的运动悖论和巴拿赫-塔斯基悖论，解决，因为NRA只承认封闭的实数超类，特别是，开放/半开区间的实数是不允许的。NAFL版本的可计算性理论（NCT）拒绝了图灵关于停机问题的不可判定性的论证，并允许超计算。NCT的重要潜在应用是在量子和自主计算领域。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。