Cut-Elimination

Preamble This document presents the complete axiom system of L×-the formal language in which {1=1×1.} is a well-formed formula. L× is not a revision of Zermelo-Fraenkel set theory. It operates at a level prior to all axiomatic systems: the level at which the primitives that make formal systems possible are themselves derived rather than assumed. L× extends the identity language L= by introducing the correspondence operator (×), the terminal marker (.), and the axioms that govern them. The axioms are presented in eight groups, ordered by logical priority. Group A governs identity-first as inherited from L= and then as extended by L×. Groups B through H introduce conditions that L= cannot provide: correspondence, closure, the fixed point, deviation, return, logical order, and the pre-systematic status of the law itself. Every axiom is stated in three parts: the formal statement, the precise explanation of what it establishes, and why it is required. No axiom is introduced without logical necessity. No term is used without prior definition. Three appendices follow the main axiom system. Appendix A provides step-by-step derivation examples, including the formal derivation chains establishing Theorem A7 and Theorem C2 from Axiom A8 (Derivations 4 and 5). Appendix B constructs a minimal model satisfying all 24 axioms, establishing that L× is formally interpretable. Appendix C addresses consistency, the formal justification of Axiom H1, the resolution of the C2/ A7 independence question (C.4), and the independence proofs for Axioms B1, D1, and D2 (C.5).

In this paper we give a semantic proof of cut-elimination for ICTT. ICTT is an intuitionistic formulation of Church's theory of types defined by Miller, Scedrov, Nadathur and Pfenning in the late 1980s. It is the basis for the *prolog programming language. Our approach, extending techniques of Takahashi, Andrews and tableaux machinery of Fitting, Smullyan, Nerode and Shore, is to prove a completeness theorem for the cut-free fragment, and show, semantically, that cut is a derived rule. The technique used allows us to extract a generalization of the Takahashi-Sch"utte lemma on extending semivaluations in impredicative systems. We strengthen Andrews ' notion of Hintikka sets to intuitionistic logic in a way that also defines tableau-provability for intuitionistic type theory. We develop a corresponding model theory for ICTT and, after giving a completeness theorem without using cut we then show, using cut, how to establish completeness of more conventional term models. ...

We introduce Complementary Measurement of Inconsistency (CMI), a formal framework for studying inconsistent or undecidable mathematical structures by measurement into locally consistent branches. The central methodological distinction is that an inconsistent source is not treated as a single classical theory from which arbitrary conclusions may be inferred. Instead, it is treated as a repository of possible supports. A measurement selects a finite locally consistent support and produces a branch-typed theory. Distinct branches may validate complementary conclusions, such as P and ¬P , but no fusion rule permits these conclusions to be conjoined inside a single untyped theory. We define the predicative fragment CMI <Γ0 (B), where branch generation is ranked by ordinal notations below the Feferman-Schuette ordinal Γ 0. The main theorem is a relative consistency result: PRA + TI Γ0 + Con(B) ⊢ Con(CMI <Γ0 (B)). The proof proceeds by transfinite induction up to Γ 0 on the branch rank. The induction invariant states that every branch of rank below α is locally consistent. Measurement preserves consistency because each child branch is generated only from a certified finite consistent support, and the branch-type discipline prevents cross-branch explosion. The theorem does not assert that all complementary branches may be jointly conjoined, nor does it provide an internal self-consistency proof for a sufficiently strong CMI theory.

It is well-known that typability, type inhabitation and type inference are undecidable in the Girard-Reynolds polymorphic system F. It has recently been proven that type inhabitation remains undecidable even in the predicative fragment of system F in which all universal instantiations have an atomic witness (system Fat). In this paper we analyze typability and type inference in Curry style variants of system Fat and show that typability is decidable and that there is an algorithm for type inference which is capable of dealing with non-redundancy constraints.

We present a new Curry-Howard correspondence for classical first-order natural deduction. We add to the lambda calculus an operator which represents, from the viewpoint of programming, a mechanism for raising and catching multiple exceptions, and from the viewpoint of logic, the excluded middle over arbitrary prenex formulas. The machinery will allow to extend the idea of learning -originally developed in Arithmetic -to pure logic. We prove that our typed calculus is strongly normalizing and show that proof terms for simply existential statements reduce to a list of individual terms forming an Herbrand disjunction. A by-product of our approach is a natural-deduction proof and a computational interpretation of Herbrand's Theorem.

Nominal logic is a theory of names and binding based on the primitive concepts of freshness and swapping, with a self-dual N-(or "new")-quantifier, originally presented as a Hilbert-style axiom system extending first-order logic. We present a sequent calculus for nominal logic called Fresh Logic, or FL, admitting cut-elimination. We use FL to provide a proof-theoretic foundation for nominal logic programming and show how to interpret F Oλ ∇ , another logic with a self-dual quantifier, within FL.

In this paper we make some observations about Natural Deduction derivations (Prawitz, 1965, van Dalen, 1986, Bell and Machover, 1977). We assume the reader is familiar with it and with proof-theory in general. Our development will be simple, even simple-minded, and concrete. However, it will also be evident that general ideas motivate our examples, and we think both our specific

In informal mathematical usage we often reason using languages with binding. We usually find ourselves placing capture-avoidance constraints on where variables can and cannot occur free. We describe a logical derivation system which allows a direct formalisation of such assertions, along with a direct formalisation of their constraints. We base our logic on equality, probably the simplest available judgement form. In spite of this, we can axiomatise systems of logic and computation such as first-order logic or the lambda-calculus in a very direct and natural way. We investigate the theory of derivations, prove a suitable semantics sound and complete, and discuss existing and future research.

We present a generalisation of first-order unification to the practically important case of equations between terms involving binding operations. A substitution of terms for variables solves such an equation if it makes the equated terms «-equivalent, i.e. equal up to renaming bound names. For the applications we have in mind, we must consider the simple, textual form of substitution in which names occurring in terms may be captured within the scope of binders upon substitution. We are able to take a "nominal" approach to binding in which bound entities are explicitly named (rather than using nameless, de Bruijn-style representations) and yet get a version of this form of substitution that respects «-equivalence and possesses good algorithmic properties. We achieve this by adapting two existing ideas. The first one is terms involving explicit substitutions of names for names, except that here we only use explicit permutations (bijective substitutions). The second one is that the unification algorithm should solve not only equational problems, but also problems about the freshness of names for terms. There is a simple generalisation of classical first-order unification problems to this setting which retains the latter's pleasant properties: unification problems involving «-equivalence and freshness are decidable; and solvable problems possess most general solutions.

The modal logic S4 can be used via a Curry-Howard style correspondence to obtain a λcalculus. Modal (boxed) types are intuitively interpreted as 'closed syntax of the calculus'. This λ-calculus is called modal type theory-this is the basic case of a more general contextual modal type theory, or CMTT. CMTT has never been given a denotational semantics in which modal types are given denotation as closed syntax. We show how this can indeed be done, with a twist. We also use the denotation to prove some properties of the system.

Nominal rewriting is based on the observation that if we add support for -equivalence to first-order syntax using the nominal-set approach, then systems with binding, including higher-order reduction schemes such as -calculus ÿ-reduction, can be smoothly represented. Nominal rewriting maintains a strict distinction between variables of the object-language (atoms) and of the meta-language (variables or unknowns). Atoms may be bound by a special abstraction operation, but variables cannot be bound, giving the framework a pronounced first-order character, since substitution of terms for variables is not capture-avoiding. We show how good properties of first-order rewriting survive the extension, by giving an efficient rewriting algorithm, a critical pair lemma, and a confluence theorem for orthogonal systems.

The permutation model of set theory with atoms (FM-sets), devised by Fraenkel and Mostowski in the 1930s, supports notions of 'name-abstraction' and 'fresh name' that provide a new way to represent, compute with, and reason about the syntax of formal systems involving variable-binding operations. Inductively defined FM-sets involving the name-abstraction set former (together with Cartesian product and disjoint union) can correctly encode syntax modulo renaming of bound variables. In this way, the standard theory of algebraic data types can be extended to encompass signatures involving binding operators. In particular, there is an associated notion of structural recursion for defining syntax-manipulating functions (such as capture avoiding substitution, set of free variables, etc.) and a notion of proof by structural induction, both of which remain pleasingly close to informal practice in computer science.

Nominal rewriting introduced a novel method of specifying rewriting on syntax-with-binding. We extend this treatment of rewriting with hierarchy of variables representing increasingly 'meta-level' variables, e.g. in hierarchical nominal term rewriting the meta-level unknowns (representing unknown terms) in a rewrite rule can be 'folded into' the syntax itself (and rewritten). To the extent that rewriting is a mathematical metaframework for logic and computation, and nominal rewriting is a framework with native support for binders, hierarchical nominal term rewriting is a meta-to-the-omega level framework for logic and computation with binders.

A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures.

Sharing graphs are an implementation of linear logic proofnets in such a way that their reduction never duplicate a redex. In their usual formulations, proof-nets present a problem of coherence: if the proof-net N reduces by standard cutelimination to N' , then, by reducing the sharing graph of N we do not obtain the sharing graph of N' . We solve this problem by changing the way the information is coded into sharing graphs and introducing a new reduction rule (absorption). The rewriting system is confluent and terminating. The proof of this fact exploits an algebraic semantics for sharing graphs.

We study the problem of local and asynchronous computation in the context of multiplicative exponential linear logic (MELL) proof nets. The main novelty i s in a complete set of rewriting rules for cut-elimination in presence of weakening (which requires garbage collection). The proposed reduction system is strongly normalizing and con uent.

A uniform construction for sequent calculi for finite-valued first-order logics with distribution quantifiers is exhibited. Completeness, cut-elimination and midsequent theorems are established. As an application, an analog of Herbrand&#39;s theorem for the four-valued knowledge-representation logic of Belnap and Ginsberg is presented. It is indicated how this theorem can be used for reasoning about knowledge bases with incomplete and inconsistent information.

In the analytic calculus Ê ½ for Gödel logic has been introduced. Ê ½ operates on "sequents of relations". We show constructively how to eliminate cuts from Ê ½ -derivations. The version of the cut rule we consider allows to derive other forms of cut as well as a rule corresponding to the "communication rule" of Avron's hypersequent calculus for ½ . Moreover, we give an ex- plicit description of all the axioms of Ê ½ and prove their completeness.

other hand, is a simple, generic, sequent based theorem prover for propositional nite-valued logics (see [6]). From its very beginning, MUltseq was intended to be a `companion&#x27;to MUltlog. So far, however, MUltseq does not directly use the representation of sequent rules as generated by MUltlog. Moreover (due to lack of funding, personnel and time), further development and maintenance of both system has been stalled for some time now. It is the purpose of this abstract to shortly describe the two systems and the current e orts to integrate them.

The importance of clear concise communication is often overlooked by the typical engineer and scientist. Based on the research findings, the paper emphasises the importance of communication skills in training students for technical and engineering professions. The author provides research findings in analysis of the most common mistakes in preparing PowerPoint slides, and in giving oral presentations. He shows practical outcomes and methodology for proper communication training. The published findings would help teachers of engineering and science subjects to find the way how to implement communication and presentation skills into technical subjects, as well as to increase efficiency of their technical presentations in educational process.

This essay explores the synthesis of Gerhard Gentzen's proof theory with Genrich Altshuller's Theory of Inventive Problem Solving (TRIZ) as a foundational framework for Inventive Mathematical Discovery (IMD). We argue that contemporary AI systems-despite their capacity to verify and formalize proofs-remain fundamentally constrained by their inability to generate novel, non-obvious mathematical conjectures and axiomatic systems. The Gentzen-Altshuller Fusion proposes a meta-methodology that treats unsolved mathematical problems as Technical Contradictions requiring inventive principles for resolution. By integrating structural rigor (Gentzen), heuristic conflict resolution (Altshuller), and constructive validation (Type Theory), we outline an architectural blueprint for next-generation mathematical AI systems capable of genuine discovery. We further situate this framework within broader questions of consciousness, emergence, and coherence in complex systems, suggesting implications that extend beyond mathematics into governance, economics, and fundamental physics.

We present a hypersequent calculus that is sound and complete with respect to the truth-functionally contingent formulas of classical logic. We investigate its structural properties and provide a Gentzen-style cut-elimination procedure. The most notable feature of the calculus is that it jointly satisfies the subformula property and the property of deductive purity, to the effect that only contingent hypersequents occur in formal proofs. Moreover, since the negation of a contingent formula is also contingent, the calculus turns out to be paraconsistent, and since the conjunction of a formula with its own negation is not contingent, the paraconsistency is of the non-adjunctive kind.

We propose an algorithm for constraint solving over hedges and contexts built over individual, sequence, function, and context vari- ables and ∞exible arity symbols, where the admissible bindings of se- quence variables and context variables can be constrained to languages represented by regular hedge or regular context expressions. We identify su-cient syntactic restrictions that enable to solve such constraints by matching techniques, and describe a solving algorithm that is sound and complete.

In this article we provide an intrinsic characterization of the famous Howard-Bachmann ordinal in terms of a natural well-partial-ordering by showing that this ordinal can be realized as a maximal order type of a class of generalized trees with respect to a homeomorphic embeddability relation. We use our calculations to draw some conclusions about some corresponding subsystems of second order arithmetic. All these subsystems deal with versions of light-face Π 1 1 -comprehension.

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] introduced a selfvalidating semantics for CZF that combines realizability for extensional set theory and truth.

The larger project broached here is to look at the generally Π 1 2 sentence " if X is well-ordered then f (X) is well-ordered", where f is a standard proof-theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded ω-models for a particular theory T f whose consistency can be proved by means of a cut elimination theorem in infinitary logic which crucially involves the function f . To illustrate this theme, we prove in this paper that the statement " if X is well-ordered then ε X is wellordered" is equivalent to ACA + 0 . This was first proved by Marcone and Montalban [7] using recursion-theoretic and combinatorial methods. The proof given here is principally proof-theoretic, the main techniques being Schütte's method of proof search (deduction chains) and cut elimination for a (small) fragment of L ω 1 ,ω .

The paper contains proof-theoretic investigations on extensions of Kripke-Platek set theory, KP, which accommodate first order reflection. Ordinal analyses for such theories are obtained by devising cut elimination procedures for infinitary calculi of ramified set theory with Π n reflection rules. This leads to consistency proofs for the theories KP + Π n -reflection using a small amount of arithmetic (PRA) and the well-foundedness of a certain ordinal notation system with respect to primitive recursive descending sequences. Regarding future work, we intend to avail ourselves of these new cut elimination techniques to attain an ordinal analysis of Π 1 2 comprehension by approaching Π 1 2 comprehension through transfinite levels of reflection.

We reconsider Rauszer&#x27;s bi-intuitionistic logic in the framework of the logic for pragmatics: every formula is regarded as expressing an act of assertion or conjecture, where conjunction and implication are assertive and subtraction and disjunction are conjectural. The resulting system of polarized bi-intuitionistic logic (PBL) consists of two fragments, positive intuitionistic logic LJ⊃∩ and its dual LJrg, extended with two negations partially internalizing the duality between LJ⊃∩ and LJrg. Modal interpretations and Kripke&#x27;s semantics over bimodal preordered frames are considered and a Natural Deduction system PBN is sketched for the whole system. A stricter interpretation of the duality and a simpler natural deduction system is obtained when polarized bi-intuitionistic logic is interpreted over S4 rather than bi-modal S4 (a logic called intuitionistic logic for pragmatics of assertions and conjectures ILPAC). The term assignment for the conjectural fragment LJrg exhibit...