
SyntaxIndependent
Logic
Infrastructure
Title: 
SyntaxIndependent Logic Infrastructure 
Authors:

Andrei Popescu and
Dmitriy Traytel

Submission date: 
20200916 
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 singlepoint
substitution. Similarly, we develop a natural deduction style proof
system starting from the abstract Hilbertstyle one. These onetime
efforts benefit different concrete logics satisfying our locales'
assumptions. We instantiate the syntaxindependent 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 CADE27 paper A
Formally Verified Abstract Account of GĂ¶del's Incompleteness
Theorems. 
BibTeX: 
@article{Syntax_Independent_LogicAFP,
author = {Andrei Popescu and Dmitriy Traytel},
title = {SyntaxIndependent Logic Infrastructure},
journal = {Archive of Formal Proofs},
month = sep,
year = 2020,
note = {\url{https://isaafp.org/entries/Syntax_Independent_Logic.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Used by: 
Goedel_Incompleteness, Robinson_Arithmetic 
