Proof-theoretical analysis of order relations

DOI10.1007/S00153-003-0209-8MaRDI QIDQ701722zbMATH OpenOpenAlexFDO

Authors Sara Negri, Jan von Plato, Thierry Coquand

Publication date 16 December 2004

Published in Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00153-003-0209-8

zbMATH Keywords

decidabilityelementary theory of order relationsentailment relationproof-theoretical analysissequential formulationSzpilrajn's theorem

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Total orders (06A05) Partial orders, general (06A06)

Review text

In a previous work, the first and second author proposed a proof-theoretical treatment of axiomatic systems in a general setting by showing that a wide class of mathematical axioms are convertible into rules of inference added to certain contraction-free sequent calculi so that we can apply several establised methods of proof analysis in sequent calculi. In this paper, the argument is enriched by some developments on duality of mathematical rules and on Harrop theories, and then applied to a concrete analysis of elementary theories of order relations. The main result obtained by the analysis is a conservativity theorem which gives rise to a proof-theoretical version of Szpilrajn's theorem on the extension of a partical order into a linear one. Decidability of the theories of partial and linear order for quantifier-free sequents is also shown by giving terminating methods of proof-search. Finally the third author discusses these results by an alternative approach, featuring the notion of entailment relation introduced by D. Scott.

Recommendations

• Sequent calculus proof theory of intuitionistic apartness and order relations
• scientific article; zbMATH DE number 1795222
• Admissibility of structural rules for extensions of contraction-free sequent calculi
• Computability-theoretic and proof-theoretic aspects of partial and linear orderings
• Proof analysis beyond geometric theories: from rule systems to systems of rules

Cited in

(20)

• Sequent calculi for \(\mathsf{SCI}\)
• Eliminating disjunctions by disjunction elimination
• Sequent calculus proof theory of intuitionistic apartness and order relations
• The Hahn-Banach theorem by disjunction elimination
• A verified decision procedure for orders in Isabelle/HOL
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
• Proof theory and ordinal analysis
• Decision methods for linearly ordered Heyting algebras
• A universal algorithm for Krull's theorem
• The intensional side of algebraic-topological representation theorems
• scientific article; zbMATH DE number 1870412 (Why is no real title available?)
• scientific article; zbMATH DE number 935103 (Why is no real title available?)
• THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY
• An investigation into intuitionistic logic with identity
• Eliminating disjunctions by disjunction elimination
• Proof analysis in intermediate logics
• A general Glivenko-Gödel theorem for nuclei
• Conservation as translation
• Well quasi-orders, better quasi-orders, and monomial ideals
• Proof analysis in modal logic

This page was built for publication: Proof-theoretical analysis of order relations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q701722)