2021/05/14 by Samuel Balco, Giuseppe Greco, Balco, Samuel +9
Computer Science · #03B10 #03B35 #03B45 #03B47 #03F03 #03F05 #03F07 #03G05 #03G10 #03G15 #03G30 #06A06 #06A11 #06D10 #06D50 #06E15 #Advanced Algebra and Logic #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2105.06877
openalex publication_date 2021/05/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We introduce a proper display calculus for first-order logic, of which we prove soundness, completeness, conservativity, subformula property and cut elimination via a Belnap-style metatheorem. All inference rules are closed under uniform substitution and are without side conditions.