- Submit
-
Browse
- All Categories
- Metaphysics and Epistemology
- Value Theory
- Science, Logic, and Mathematics
- Science, Logic, and Mathematics
- Logic and Philosophy of Logic
- Philosophy of Biology
- Philosophy of Cognitive Science
- Philosophy of Computing and Information
- Philosophy of Mathematics
- Philosophy of Physical Science
- Philosophy of Social Science
- Philosophy of Probability
- General Philosophy of Science
- Philosophy of Science, Misc
- History of Western Philosophy
- Philosophical Traditions
- Philosophy, Misc
- Other Academic Areas
- More
Switch to: References
Citations of:
Syntactic cut-elimination for common knowledge
Annals of Pure and Applied Logic 160 (1):82-95 (2009)
Add citations
You must login to add citations.
|
|
|
For some modal fixed point logics, there are deductive systems that enjoy syntactic cut-elimination. An early example is the system in Pliuskevicius [15] for LTL. More recent examples are the systems by the authors of this paper for the logic of common knowledge [5] and by Hill and Poggiolesi for PDL[8], which are based on a form of deep inference. These logics can be seen as fragments of the modal mu-calculus. Here we are interested in how far this approach can (...) |
|
|
The article deals with infinitary modal logic. We first discuss the difficulties related to the development of a satisfactory proof theory and then we show how to overcome these problems by introducing a labelled sequent calculus which is sound and complete with respect to Kripke semantics. We establish the structural properties of the system, namely admissibility of the structural rules and of the cut rule. Finally, we show how to embed common knowledge in the infinitary calculus and we discuss first-order (...) |
|
|
We study the proof-theoretic relationship between two deductive systems for the modal mu-calculus. First we recall an infinitary system which contains an omega rule allowing to derive the truth of a greatest fixed point from the truth of each of its (infinitely many) approximations. Then we recall a second infinitary calculus which is based on non-well-founded trees. In this system proofs are finitely branching but may contain infinite branches as long as some greatest fixed point is unfolded infinitely often along (...) |
|
|
The paper offers a formalization of reasoning about distributed multi-agent systems. The presented propositional probabilistic temporal epistemic logic |$\textbf {PTEL}$| is developed in full detail: syntax, semantics, soundness and strong completeness theorems. As an example, we prove consistency of the blockchain protocol with respect to the given set of axioms expressed in the formal language of the logic. We explain how to extend |$\textbf {PTEL}$| to axiomatize the corresponding first-order logic. |
|
|
We study a propositional probabilistic temporal epistemic logic |$\textbf {PTEL}$| with both future and past temporal operators, with non-rigid set of agents and the operators for agents’ knowledge and for common knowledge and with probabilities defined on the sets of runs and on the sets of possible worlds. A semantics is given by a class |${\scriptsize{\rm Mod}}$| of Kripke-like models with possible worlds. We prove decidability of |$\textbf {PTEL}$| by showing that checking satisfiability of a formula in |${\scriptsize{\rm Mod}}$| is (...) |
|
|
A non-effective cut-elimination proof for modal mu-calculus has been given by G. Jäger, M. Kretz and T. Studer. Later an effective proof has been given for a subsystem M 1 with non-iterated fixpoints and positive endsequents. Using a new device we give an effective cut-elimination proof for M 1 without restriction to positive sequents. |
|
|
Hilbert arithmetic in a wide sense, including Hilbert arithmetic in a narrow sense consisting by two dual and anti-isometric Peano arithmetics, on the one hand, and the qubit Hilbert space (originating for the standard separable complex Hilbert space of quantum mechanics), on the other hand, allows for an arithmetic version of Gentzen’s cut elimination and quantum measurement to be described uniformy as two processes occurring accordingly in those two branches. A philosophical reflection also justifying that unity by quantum neo-Pythagoreanism links (...) |
PhilPapers logo by Andrea Andrews and Meghan Driscoll.
This site uses cookies and Google Analytics (see our terms & conditions for details regarding the privacy implications). Use of this site is subject to terms & conditions.
All rights reserved by The PhilPapers Foundation
Server: philpapers-web-5ff6c685cb-pqwqt uwo