Danko Ilik
We propose an extension of minimal intuitionistic predicate logic, based on delimited control operators, that can derive the predicate-logic version of the Double-negation Shift schema, while preserving the disjunction and existence properties.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
First, we reconstruct Wim Veldman's result that Open Induction on Cantor space can be derived from Double-negation Shift and Markov's Principle. In doing this, we notice that one has to use a countable choice axiom in the proof and that Markov's Principle is replaceable by slightly strengthening the Double-negation Shift schema. We show that this strengthened version of Double-negation Shift can nonetheless be derived in a constructive intermediate logic based on delimited control operators, extended with axioms for higher-type Heyting Arithmetic. We formalize the argument and thus obtain a pr…
We show which implicational relations hold between the three principles ex falso sequitur quodlibet, tertium non datur, and double negation elimination, on the basis of minimal logic.
Double negation stable h-propositions in cubical sets
研究在立方集模型中双重否定稳定h命题的分类器构造，通过该构造得出一些相对一致性结果，如特定分类器在立方集与元理论中的存在关系、添加戴德金实数不改变一致性强度及构造带扩展丘奇论题的同伦类型理论模型。
This paper considers a generalisation of selection functions over an arbitrary strong monad $T$, as functionals of type $J^T_R X = (X \to R) \to T X$. It is assumed throughout that $R$ is a $T$-algebra. We show that $J^T_R$ is also a strong monad, and that it embeds into the continuation monad $K_R X = (X \to R) \to R$. We use this to derive that the explicitly controlled product of $T$-selection functions is definable from the explicitly controlled product of quantifiers, and hence from Spector's bar recursion. We then prove several properties of this product in the special case when $T$ is t…
The definition of negation has to be referred to the totality of a theory and at last to what is defined as the organization of a scientific theory; in other words, the definition of negation is of a structural kind, rather than of an objective kind or a subjective kind. The paper starts by remarking that the ancient Greek word for truth was aletheia, which is a double negation, i.e. unveiling. Not before the 1968 the double negation law was re-evaluated, since it was recognized that its failure represents more appropriately than the failure of of excluded middle law the borderline between cla…
Pocrims and suitable specialisations thereof are structures that provide the natural algebraic semantics for a minimal affine logic and its extensions. Hoops comprise a special class of pocrims that provide algebraic semantics for what we view as an intuitionistic analogue of the classical multi-valued Łukasiewicz logic. We present some contributions to the theory of these algebraic structures. We give a new proof that the class of hoops is a variety. We use a new indirect method to establish several important identities in the theory of hoops: in particular, we prove that the double negation …
When is double negation Scott continuous?
针对T₀空间X的开集框架L，研究双重否定核的Scott连续性，证明其与X的离散性、有限性等价，推广结果到所有布尔核，给出X清醒且T₁的无点刻画。
Strong negation in the theory of computable functionals TCF
本文在可计算泛函理论 TCF 中同时定义公式和谓词的强否定，证明爆炸原理与双重否定消去律，引入紧致公式，并通过案例研究说明该定义的自然性及其对 Bishop 式构造性数学的适用性。
A class of models is presented, in the form of continuation monads polymorphic for first-order individuals, that is sound and complete for minimal intuitionistic predicate logic. The proofs of soundness and completeness are constructive and the computational content of their composition is, in particular, a $β$-normalisation-by-evaluation program for simply typed lambda calculus with sum types. Although the inspiration comes from Danvy's type-directed partial evaluator for the same lambda calculus, the there essential use of delimited control operators (i.e. computational effects) is avoided. …
In this paper, a short survey about the concepts underlying general logics is given. In particular, a novel rigorous definition of a fuzzy negation as an operation acting on a lattice to render it into a fuzzy logic is presented. According to this definition, a fuzzy negation satisfies the weak double negation condition, requiring double negation to be expansive, the antitony condition, being equivalent to the disjunctive De Morgan law and thus warranting compatibility of negation with the lattice operations, and the Boolean boundary condition stating that the universal bounds of the lattice a…
By a De Morgan algebra is meant a bounded poset equipped with an antitone involution considered as negation. Such an algebra can be considered as an algebraic axiomatization of a propositional logic satisfying the double negation law. Our aim is to introduce the so-called tense operators in every De Morgan algebra for to get an algebraic counterpart of a tense logic with negation satisfying the double negation law which need not be Boolean. Following the standard construction of tense operators $G$ and $H$ by a frame we solve the following question: if a dynamic De Morgan algebra is given, how…
We define a new topos, the Herbrand topos, inspired by the modified realizability topos and our earlier work on Herbrand realizability. We also introduce the category of Herbrand assemblies and characterise these as the double-negation-separated objects in the Herbrand topos. In addition, we show that the category of sets is included as the category of double-negation-sheaves and prove that the inclusion functor preserves and reflects validity of first-order formulas.
A Guide to Krivine Realizability for Set Theory
本文介绍Krivine对传统可实现性方法的扩展，通过一类模型元素名称给出其可实现性理论的改进形式化，并探讨该方法与直觉主义可实现性、双重否定翻译及力迫理论的关联。
Four negations and the spectral presheaf
本文提出双准直觉逻辑和阿奇乌林逻辑，通过正交补定义谱预叠上的两种否定运算，并证明其与相关代数的正确性与完备性，同时反驳了谱预叠作为相关逻辑模型的可能性。
The multi-valued logic of Łukasiewicz is a substructural logic that has been widely studied and has many interesting properties. It is classical, in the sense that it admits the axiom schema of double negation, [DNE]. However, our understanding of Łukasiewicz logic can be improved by separating its classical and intuitionistic aspects. The intuitionistic aspect of Łukasiewicz logic is captured in an axiom schema, [CWC], which asserts the commutativity of a weak form of conjunction. This is equivalent to a very restricted form of contraction. We show how Łukasiewicz Logic can be viewed both as …
Intuitionistic logic, in which the double negation law not-not-P = P fails, is dominant in categorical logic, notably in topos theory. This paper follows a different direction in which double negation does hold. The algebraic notions of effect algebra/module that emerged in theoretical physics form the cornerstone. It is shown that under mild conditions on a category, its maps of the form X -> 1+1 carry such effect module structure, and can be used as predicates. Predicates are identified in many different situations, and capture for instance ordinary subsets, fuzzy predicates in a probabilist…
The so-called paradoxes of material implication have motivated the development of many non-classical logics over the years \cite{aA75,nB77,aA89,gP89,sH96}. In this note, we investigate some of these paradoxes and classify them, over minimal logic. We provide proofs of equivalence and semantic models separating the paradoxes where appropriate. A number of equivalent groups arise, all of which collapse with unrestricted use of double negation elimination. Interestingly, the principle \emph{ex falso quodlibet}, and several weaker principles, turn out to be distinguishable, giving perhaps supporti…
A non-distributive two-sorted hypersequent calculus \textbf{PDBL} and its modal extension \textbf{MPDBL} are proposed for the classes of pure double Boolean algebras and pure double Boolean algebras with operators respectively. A relational semantics for \textbf{PDBL} is next proposed, where any formula is interpreted as a semiconcept of a context. For \textbf{MPDBL}, the relational semantics is based on Kripke contexts, and a formula is interpreted as a semiconcept of the underlying context. The systems are shown to be sound and complete with respect to the relational semantics. Adding approp…
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…
The minimum classical extension S$^{+g}$ of a classically sound theory S based on intuitionistic logic, defined by adding to S the Gentzen negative interpretations of its mathematical axioms, contains a faithful translation S$^g$ of the classical version S + (--A -> A) of S. S$^g$ may be called the classical content of S. First and second order intuitionistic arithmetic contain their classical contents, but intuitionistic recursive analysis cannot prove the negative interpretation of its quantifier-free countable choice axiom. Variants of Kuroda's double negation shift principle (including the…
Caracterización semántico-deductiva de la lógica doble LD y los gráficos existenciales Gamma-LD
本文提出双重命题逻辑LD及其可能世界语义，证明其一致性、有效性与完备性，并展示其解决说谎者悖论的能力，同时以Gamma-LD存在图刻画该逻辑。
In a 1985 commentary to his collected works, Kolmogorov remarked that his 1932 paper "was written in hope that with time, the logic of solution of problems [i.e., intuitionistic logic] will become a permanent part of a [standard] course of logic. A unified logical apparatus was intended to be created, which would deal with objects of two types - propositions and problems." We construct such a formal system, as well as its predicate version QHC, which is a conservative extension of both the intuitionistic predicate calculus QH and the classical predicate calculus QC. The only new connectives ? …
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。