Related papers: Semantic A-translation and Super-consistency entai…
We give a simple and direct proof that super-consistency implies the cut elimination property in deduction modulo. This proof can be seen as a simplification of the proof that super-consistency implies proof normalization. It also takes…
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…
We consider cut-elimination in the sequent calculus for classical first-order logic. It is well known that this system, in its most general form, is neither confluent nor strongly normalizing. In this work we take a coarser (and…
Any set of truth-functional connectives has sequent calculus rules that can be generated systematically from the truth tables of the connectives. Such a sequent calculus gives rise to a multi-conclusion natural deduction system and to a…
The goal of this note is to compare two notions, one coming from the theory of rewrite systems and the other from proof theory: confluence and cut elimination. We show that to each rewrite system on terms, we can associate a logical system:…
Non-classical negations may fail to be contradictory-forming operators in more than one way, and they often fail also to respect fundamental meta-logical properties such as the replacement property. Such drawbacks are witnessed by intricate…
Cut-elimination is the bedrock of proof theory with a multitude of applications from computational interpretations to proof analysis. It is also the starting point for important meta-theoretical investigations including decidability,…
We focus on the persistence principle over weak interpretability logic. Our object of study is the logic obtained by adding the persistence principle to weak interpretability logic from several perspectives. Firstly, we prove that this…
We present some hypersequent calculi for all systems of the classical cube and their extensions with axioms $T$, $P$, $D$, and, for every $n\geq 1$, rule $RD^+_n$. The calculi are internal as they only employ the language of the logic, plus…
This paper explores the connection between two central results in the proof theory of classical logic: Gentzen's cut-elimination for the sequent calculus and Herbrands "fundamental theorem". Starting from Miller's expansion-tree-proofs, a…
In the context of natural deduction for propositional classical logic, with classicality given by the inference rule reductio ad absurdum, we investigate the De Morgan translation of disjunction in terms of negation and conjunction. Once…
Herbrand's theorem is one of the most fundamental insights in logic. From the syntactic point of view, it suggests a compact representation of proofs in classical first- and higher-order logic by recording the information of which instances…
We present a syntactic cut-elimination procedure for the alternation-free fragment of the modal mu-calculus. Cut reduction is carried out within a cyclic proof system, where proofs are finitely branching but may be non-wellfounded. The…
We extend the notion of Heyting algebra to a notion of truth values algebra and prove that a theory is consistent if and only if it has a B-valued model for some non trivial truth values algebra B. A theory that has a B-valued model for all…
This paper defines a sound and complete semantic criterion, based on reducibility candidates, for strong normalization of theories expressed in minimal deduction modulo \`a la Curry. The use of Curry-style proof-terms allows to build this…
We show how to express intuitionistic Zermelo set theory in deduction modulo (i.e. by replacing its axioms by rewrite rules) in such a way that the corresponding notion of proof enjoys the normalization property. To do so, we first rephrase…
In this note we will show how to get consistency for first order classical logic, in a purely syntactic way, without going through cut elimination. The procedure is very simple and it uses the calculus of structures in an essential way. It…
Cut-elimination theorems constitute one of the most important classes of theorems of proof theory. Since Gentzen's proof of the cut-elimination theorem for the system $\mathbf{LK}$, several other proofs have been proposed. Even though the…
Self-modification is often taken as constitutive of artificial superintelligence (SI), yet modification is a relative action requiring a supplement outside the operation. When self-modification extends to this supplement, the classical…
We give a direct, purely arithmetical and elementary proof of the strong normalization of the cut-elimination procedure for full (i.e. in presence of all the usual connectives) classical natural deduction.