Syntax-Independent Logic Infrastructure

Title:	Syntax-Independent Logic Infrastructure
Authors:	Andrei Popescu (a /dot/ popescu /at/ mdx /dot/ ac /dot/ uk) and Dmitriy Traytel
Submission date:	2020-09-16
Abstract:	We formalize a notion of logic whose terms and formulas are kept abstract. In particular, logical connectives, substitution, free variables, and provability are not defined, but characterized by their general properties as locale assumptions. Based on this abstract characterization, we develop further reusable reasoning infrastructure. For example, we define parallel substitution (along with proving its characterizing theorems) from single-point substitution. Similarly, we develop a natural deduction style proof system starting from the abstract Hilbert-style one. These one-time efforts benefit different concrete logics satisfying our locales' assumptions. We instantiate the syntax-independent logic infrastructure to Robinson arithmetic (also known as Q) in the AFP entry Robinson_Arithmetic and to hereditarily finite set theory in the AFP entries Goedel_HFSet_Semantic and Goedel_HFSet_Semanticless, which are part of our formalization of Gödel's Incompleteness Theorems described in our CADE-27 paper A Formally Verified Abstract Account of Gödel's Incompleteness Theorems.
BibTeX:	@article{Syntax_Independent_Logic-AFP, author = {Andrei Popescu and Dmitriy Traytel}, title = {Syntax-Independent Logic Infrastructure}, journal = {Archive of Formal Proofs}, month = sep, year = 2020, note = {\url{http://isa-afp.org/entries/Syntax_Independent_Logic.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Used by:	Goedel_Incompleteness, Robinson_Arithmetic
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document

Browse theories

Download this entry