[FOM] Fwd: [isabelle] 2 new AFP entries

[Serguei Mokhov]

JFYI:


---------- Forwarded message ----------
From: Gerwin Klein <Gerwin.Klein at nicta.com.au>
Date: Sun, Nov 17, 2013 at 9:53 PM
Subject: [isabelle] 2 new AFP entries
To: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>


Two new AFP entries are available from [http://afp.sf.net]:

Gödel's Incompleteness Theorems
by Larry Paulson

Gödel's two incompleteness theorems are formalised, following a
careful presentation by Swierczkowski, in the theory of hereditarily
finite sets. This represents the first ever machine-assisted proof of
the second incompleteness theorem. Compared with traditional
formalisations using Peano arithmetic (see e.g. Boolos), coding is
simpler, with no need to formalise the notion of multiplication (let
alone that of a prime number) in the formalised calculus upon which
the theorem is based. However, other technical problems had to be
solved in order to complete the argument.


The Hereditarily Finite Sets
by Larry Paulson

The theory of hereditarily finite sets is formalised, following the
development of Swierczkowski. An HF set is a finite collection of
other HF sets; they enjoy an induction principle and satisfy all the
axioms of ZF set theory apart from the axiom of infinity, which is
negated. All constructions that are possible in ZF set theory
(Cartesian products, disjoint sums, natural numbers, functions)
without using infinite sets are possible here. The definition of
addition for the HF sets follows Kirby. This development forms the
foundation for the Isabelle proof of Gödel's incompleteness theorems,
which has been formalised separately.


Enjoy,
Gerwin

________________________________

The information in this e-mail may be confidential and subject to
legal professional privilege and/or copyright. National ICT Australia
Limited accepts no liability for any damage caused by this email or
its attachments.



-- 
Serguei Mokhov
http://www.cs.concordia.ca/~mokhov
http://marf.sf.net | http://sf.net/projects/marf