The Experts below are selected from a list of 960 Experts worldwide ranked by ideXlab platform

Simon Kramer - One of the best experts on this subject based on the ideXlab platform.

  • logic of negation complete interactive proofs formal theory of epistemic deciders
    Electronic Notes in Theoretical Computer Science, 2014
    Co-Authors: Simon Kramer
    Abstract:

    We produce a decidable classical normal modal logic of internalised negation-complete and thus disjunctive non-monotonic interactive proofs (LDiiP) from an existing logical counterpart of non-monotonic or instant interactive proofs (LiiP). LDiiP internalises agent-centric proof theories that are negation-complete (maximal) and consistent (and hence strictly weaker than, for example, Peano Arithmetic) and enjoy the Disjunction Property (like Intuitionistic Logic). In other words, internalised proof theories are ultrafilters and all internalised proof goals are definite in the sense of being either provable or disprovable to an agent by means of disjunctive internalised proofs (thus also called epistemic deciders). Still, LDiiP itself is classical (monotonic, non-constructive), negation-incomplete, and does not have the Disjunction Property. The price to pay for the negation completeness of our interactive proofs is their non-monotonicity and non-communality (for singleton agent communities only). As a normal modal logic, LDiiP enjoys a standard Kripke-semantics, which we justify by invoking the Axiom of Choice on [email protected]?s and then construct in terms of a concrete oracle-computable function. [email protected]?s agent-centric internalised notion of proof can also be viewed as a negation-complete disjunctive explicit refinement of standard KD45-belief, and yields a disjunctive but negation-incomplete explicit refinement of S4-provability.

  • Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer)∗
    2014
    Co-Authors: Simon Kramer
    Abstract:

    We produce a decidable super-intuitionistic normal modal logic of in-ternalised 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 communica-tion 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 knew my proof then CM would persistently and also disjunctively know that my proof goal is true. So intuitionistic interactive proofs effect a lasting transfer of disjunctive propositional knowledge (dis-junctively knowable facts) in the communication medium of multi-agent distributed systems via the transmission of certain individual knowledge (knowable intuitionistic proofs). Our (necessarily) CM-centred notion of proof is also a disjunctive explicit refinement of KD45-belief, and yields also such a refinement of standard S5-knowledge. Monotonicity but not communality is a commonality of LiP, LIiP, and their internalised no-tions of proof. As a side-effect, we offer a short internalised proof of the Disjunction Property of Intuitionistic Logic (originally proved by Gödel)

  • Logic of Negation-Complete Interactive Proofs∗ (Formal Theory of Epistemic Deciders)
    2012
    Co-Authors: Simon Kramer
    Abstract:

    We produce a decidable classical normal modal logic of internalised negation-complete or disjunctive non-monotonic interactive proofs (LDiiP) from an existing logical counterpart of non-monotonic or instant interac-tive proofs (LiiP). LDiiP internalises agent-centric proof theories that are negation-complete (maximal) and consistent (and hence strictly weaker than, for example, Peano Arithmetic) and enjoy the Disjunction Property (like Intuitionistic Logic). In other words, internalised proof theories are ultrafilters and all internalised proof goals are definite in the sense of be-ing either provable or disprovable to an agent by means of disjunctive internalised proofs (thus also called epistemic deciders). Still, LDiiP it-self is classical (monotonic, non-constructive), negation-incomplete, and does not have the Disjunction Property. The price to pay for the nega-tion completeness of our interactive proofs is their non-monotonicity and non-communality (for singleton agent communities only). As a normal modal logic, LDiiP enjoys a standard Kripke-semantics, which we justify by invoking the Axiom of Choice on LiiP’s and then construct in terms of a concrete oracle-computable function. Our agent-centric notion of proof is a negation-complete disjunctive explicit refinement of standard KD45-belief, and also yields a disjunctive but negation-incomplete explicit refinement of standard S5-knowledge

Kramer Simon - One of the best experts on this subject based on the ideXlab platform.

  • Logic of Negation-Complete Interactive Proofs (Formal Theory of Epistemic Deciders)
    Published by Elsevier B.V., 2014
    Co-Authors: Kramer Simon
    Abstract:

    AbstractWe produce a decidable classical normal modal logic of internalised negation-complete and thus disjunctive non-monotonic interactive proofs (LDiiP) from an existing logical counterpart of non-monotonic or instant interactive proofs (LiiP). LDiiP internalises agent-centric proof theories that are negation-complete (maximal) and consistent (and hence strictly weaker than, for example, Peano Arithmetic) and enjoy the Disjunction Property (like Intuitionistic Logic). In other words, internalised proof theories are ultrafilters and all internalised proof goals are definite in the sense of being either provable or disprovable to an agent by means of disjunctive internalised proofs (thus also called epistemic deciders). Still, LDiiP itself is classical (monotonic, non-constructive), negation-incomplete, and does not have the Disjunction Property. The price to pay for the negation completeness of our interactive proofs is their non-monotonicity and non-communality (for singleton agent communities only). As a normal modal logic, LDiiP enjoys a standard Kripke-semantics, which we justify by invoking the Axiom of Choice on LiiPʼs and then construct in terms of a concrete oracle-computable function. LDiiPʼs agent-centric internalised notion of proof can also be viewed as a negation-complete disjunctive explicit refinement of standard KD45-belief, and yields a disjunctive but negation-incomplete explicit refinement of S4-provability

  • Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer)
    'Association for Computing Machinery (ACM)', 2014
    Co-Authors: Kramer Simon
    Abstract:

    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 knew my proof then CM would persistently and also disjunctively know that my proof goal is true. So intuitionistic interactive proofs effect a lasting transfer of disjunctive propositional knowledge (disjunctively knowable facts) in the communication medium of multi-agent distributed systems via the transmission of certain individual knowledge (knowable intuitionistic proofs). Our (necessarily) CM-centred notion of proof is also a disjunctive explicit refinement of KD45-belief, and yields also such a refinement of standard S5-knowledge. Monotonicity but not communality is a commonality of LiP, LIiP, and their internalised notions of proof. As a side-effect, we offer a short internalised proof of the Disjunction Property of Intuitionistic Logic (originally proved by Goedel).Comment: continuation of arXiv:1201.3667; extended start of Section 1 and 2.1; extended paragraph after Fact 1; dropped the N-rule as primitive and proved it derivable; other, non-intuitionistic family members: arXiv:1208.1842, arXiv:1208.591

  • Logic of Negation-Complete Interactive Proofs (Formal Theory of Epistemic Deciders)
    'Elsevier BV', 2013
    Co-Authors: Kramer Simon
    Abstract:

    We produce a decidable classical normal modal logic of internalised negation-complete and thus disjunctive non-monotonic interactive proofs (LDiiP) from an existing logical counterpart of non-monotonic or instant interactive proofs (LiiP). LDiiP internalises agent-centric proof theories that are negation-complete (maximal) and consistent (and hence strictly weaker than, for example, Peano Arithmetic) and enjoy the Disjunction Property (like Intuitionistic Logic). In other words, internalised proof theories are ultrafilters and all internalised proof goals are definite in the sense of being either provable or disprovable to an agent by means of disjunctive internalised proofs (thus also called epistemic deciders). Still, LDiiP itself is classical (monotonic, non-constructive), negation-incomplete, and does not have the Disjunction Property. The price to pay for the negation completeness of our interactive proofs is their non-monotonicity and non-communality (for singleton agent communities only). As a normal modal logic, LDiiP enjoys a standard Kripke-semantics, which we justify by invoking the Axiom of Choice on LiiP's and then construct in terms of a concrete oracle-computable function. LDiiP's agent-centric internalised notion of proof can also be viewed as a negation-complete disjunctive explicit refinement of standard KD45-belief, and yields a disjunctive but negation-incomplete explicit refinement of S4-provability.Comment: Expanded Introduction. Added Footnote 4. Corrected Corollary 3 and 4. Continuation of arXiv:1208.184

Hannes Leitgeb - One of the best experts on this subject based on the ideXlab platform.

  • HYPE: A System of Hyperintensional Logic (with an Application to Semantic Paradoxes)
    Journal of Philosophical Logic, 2019
    Co-Authors: Hannes Leitgeb
    Abstract:

    This article introduces, studies, and applies a new system of logic which is called ‘HYPE’. In HYPE, formulas are evaluated at states that may exhibit truth value gaps (partiality) and truth value gluts (overdeterminedness). Simple and natural semantic rules for negation and the conditional operator are formulated based on an incompatibility relation and a partial fusion operation on states. The semantics is worked out in formal and philosophical detail, and a sound and complete axiomatization is provided both for the propositional and the predicate logic of the system. The propositional logic of HYPE is shown to contain first-degree entailment, to have the Finite Model Property, to be decidable, to have the Disjunction Property, and to extend intuitionistic propositional logic conservatively when intuitionistic negation is defined appropriately by HYPE’s logical connectives. Furthermore, HYPE’s first-order logic is a conservative extension of intuitionistic logic with the Constant Domain Axiom, when intuitionistic negation is again defined appropriately. The system allows for simple model constructions and intuitive Euler-Venn-like diagrams, and its logical structure matches structures well-known from ordinary mathematics, such as from optimization theory, combinatorics, and graph theory. HYPE may also be used as a general logical framework in which different systems of logic can be studied, compared, and combined. In particular, HYPE is found to relate in interesting ways to classical logic and various systems of relevance and paraconsistent logic, many-valued logic, and truthmaker semantics. On the philosophical side, if used as a logic for theories of type-free truth, HYPE is shown to address semantic paradoxes such as the Liar Paradox by extending non-classical fixed-point interpretations of truth by a conditional as well-behaved as that of intuitionistic logic. Finally, HYPE may be used as a background system for modal operators that create hyperintensional contexts, though the details of this application need to be left to follow-up work.

Michael Rathjen - One of the best experts on this subject based on the ideXlab platform.

  • Metamathematical Properties of Intuitionistic Set Theories with Choice Principles
    2009
    Co-Authors: Michael Rathjen
    Abstract:

    This paper is concerned with metamathematical properties of intuitionistic set theories with choice principles. It is proved that the Disjunction Property, the numerical existence Property, Church’s rule, and several other metamathematical properties hold true for Constructive Zermelo-Fraenkel Set Theory and full Intuitionistic Zermelo-Fraenkel augmented by any combination of the principles of Countable Choice, Dependent Choices and the Presentation Axiom. Also Markov’s principle may be added. Moreover, these properties hold effectively. For instance from a proof of a statement ∀n ∈ ω ∃m ∈ ω ϕ(n, m) one can effectively construct an index e of a recursive function such that ∀n ∈ ω ϕ(n, {e}(n)) is provable. Thus we have an explicit method of witness and program extraction from proofs involving choice principles. As for the proof technique, this paper is a continuation of [32]. [32] introduced a selfvalidating semantics for CZF that combines realizability for extensional set theory and truth

  • Metamathematical Properties of Intuitionistic Set Theories with Choice Principles
    New Computational Paradigms, 2008
    Co-Authors: Michael Rathjen
    Abstract:

    This paper is concerned with metamathematical properties of intuitionistic set theories with choice principles. It is proved that the Disjunction Property, the numerical existence Property, Church’s rule, and several other metamathematical properties hold true for constructive Zermelo–Fraenkel Set Theory and full intuitionistic Zermelo–Fraenkel augmented by any combination of the principles of countable choice, dependent choices, and the presentation axiom. Also Markov’s principle may be added.

Tadeusz Litak - One of the best experts on this subject based on the ideXlab platform.

  • Some notes on the superintuitionistic logic of chequered subsets
    2015
    Co-Authors: Tadeusz Litak
    Abstract:

    We are going to investigate the superintuitionistic analogue of the modal logic of chequered subsets of R ∞ introduced by van Benthem et al. [2] It will be observed that this logic possesses the Disjunction Property, contains the Scott axiom, fails to contain the Kreisel-Putnam axiom and is not structurally complete. We will prove that it is a sublogic of the Medvedev logic ML. In recent years, there seems to be growing interest in modal logics determined by various topological spaces and particular families of their subsets. Bezhanishvili et al. [3] improved on a classical result by McKinsey and Tarski that S4 is complete with respect to the real line by showing that it is actually enough to consider only countable unions of convex subsets. On the other hand, Aiello et al. [1] proved that the modal logic determined by finite unions of convex subsets of R is a very strong tabular extension of Grz complete with respect to the 2-fork Kripke frame F1. F1 = 〈W1, R1 〉 is the first frame in Figure 1; W1 = {w0, w−, w+}, all points are R1-reflexive, w0 R1-sees all the other points. Van Benthem et al. [2] investigated logics determined by finite unions of products of convex subsets of R in Rα (where α ∈ N ∪ {∞}); such subsets were called chequered. It was established that for α = n, the modal logic in question corresponds to the logic determined by Fn = Fn−1 × F, the order being the standard product order. In case of α =∞, the respective modal logic is determined by infinite sequence of frames {Fn}n≥1. It is, however, worth recalling that there exists another, simpler lan-guage well-tailored for describing topological spaces: it is the language o