From: Lawrence Paulson <email@example.com>
I’m delighted to announce a new entry by Andrei Popescu and Dmitriy Traytel:
Syntax-Independent Logic Infrastructure
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.
And built upon that, four additional entries:
An Abstract Formalization of Gödel's Incompleteness Theorems
From Abstract to Concrete Gödel's Incompleteness Theorems—Part I
From Abstract to Concrete Gödel's Incompleteness Theorems—Part II
An impressive body of work!
Last updated: Dec 08 2021 at 10:22 UTC