[FOM] 614: Adventures in Formalization 1 - a suggested framework

[Arnon Avron]

On Mon, Sep 14, 2015 at 01:43:28PM -0400, Harvey Friedman wrote:

> ...
> 
> It doesn't help matters if nobody (outside the Theorem Prover
> community) can, or can even want to, read the actual statements.
> 
> REST ASSURED, this can be largely fixed. I started up an effort along
> these lines, furthered by others, and I think now things have gone
> somewhat further, but I don't know the latest:
> 
> (with S. Kieffer, J. Avigad), A language for mathematical knowledge
> management, in: Computer Reconstruction of the Body of Mathematics,
> ed. A. Grabowski, A. Naumowicz, Studies in Logic, Grammar and
> Rhetoric, p. 51-66, 2009.
 
> ...

> 
> I envision a large system and various important weaker subsystems.
> Since to much math can be done in systems much weaker than ZFC, this
> should be reflected in the choice of Gold Standards. There should be a
> few major Gold Standards ranging from Finite Set Theory to full blown
> ZFC.

If I may, I would like in connection to these issues to call the
attention of the community to a paper of mine which suggests
and develops a framework which I believe could be rather useful
for these tasks. It is "A Framework for Formalizing Set 
Theories Based on the Use of Static Set Terms", and was published
in a festschrift in honor of B. Trakhtenbrot called
"Pillars of Computer Science" (LNCS 4800, Springer, 2008, pp. 87--106).
Its abstract is enclosed below (the paper is available
from my homepage too).

Arnon Avron

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We present a new unified framework for formalizations of axiomatic 
set theories of different strength, from rudimentary set theory to 
full ZF. It allows the use of set terms, but provides a *static* check of
their validity.  Like the inconsistent ``ideal calculus" for set theory,
it is essentially based on just two
set-theoretical principles: extensionality and
comprehension (to which we optionally add $\in$-induction and/or
the axiom of choice).  Comprehension is formulated as:
$x\in\{x\mid\psi\}\leftrightarrow\psi$, where $\{x\mid\psi\}$
is a legal set term of the theory. For it being one $\psi$ should be *safe*
with respect to $\{x\}$, where safety is a relation between formulas 
and finite sets of variables.  The various systems we consider differ 
from each other mainly with respect to the safety relations they 
employ. These relations are all defined purely syntactically (using 
an induction on the logical structure of formulas).  The basic one
is based on the safety relation which implicitly underlies
commercial query languages for relational database systems (like SQL).

Our framework makes it possible to reduce all extensions by definitions 
to abbreviations. Hence it is very convenient for mechanical 
manipulations and for interactive theorem proving. It also provides 
a unified treatment of comprehension axioms and of absoluteness 
properties of formulas.