### 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.

### License

BSD License

### Topics

- Logic/Proof theory

### Session Syntax_Independent_Logic

- Prelim
- Syntax
- Deduction
- Natural_Deduction
- Pseudo_Term
- Standard_Model
- Syntax_Arith
- Deduction_Q

### Used by

- An Abstract Formalization of Gödel’s Incompleteness Theorems
- Robinson Arithmetic

## Cite

×

Syntax_Independent_Logic-AFP

    @article{Syntax_Independent_Logic-AFP,
      author  = {Andrei Popescu and Dmitriy Traytel},
      title   = {Syntax-Independent Logic Infrastructure},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Syntax_Independent_Logic.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Sep 18, 2020 : Isabelle2020