Finite methods in 1-order formalisms

DOI10.1016/S0168-0072(01)00054-9zbMath0992.03067OpenAlexW2023390377MaRDI QIDQ5957909

L. N. Gordeev

Publication date: 16 September 2002

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(01)00054-9

zbMATH Keywords

arithmeticsequent calculusDialectica interpretationrelation algebrasset theoryinductioncut-eliminationterm rewritingfinite variable logicinfinite supply of individual variables admitted in 1-order deductionsinfinite-branching rules in sequent calculiinfinityproof searchrecursive functions

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Grammars and rewriting systems (68Q42) Structure of proofs (03F07) Cylindric and polyadic algebras; relation algebras (03G15) General logic (03Bxx)

Uses Software

• ARA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Cylindric algebras. Part II
• Computability. Recursive and programmable functions
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• The Neat Embedding Problem and the Number of Variables Required in Proofs
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Finitary Algebraic Logic
• Nonfinite axiomatizability results for cylindric and relation algebras
• Variable compactness in 1-order logic
• A set of axioms for logic