*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] 2 new AFP entries*From*: Gerwin Klein <Gerwin.Klein at nicta.com.au>*Date*: Mon, 18 Nov 2013 02:53:25 +0000*Accept-language*: en-AU, en-US*Thread-index*: AQHO5AlaguvrbqY2UU63HYitN63QHg==*Thread-topic*: 2 new AFP entries

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.

- Previous by Date: [isabelle] "Semantics of Proofs and Certified Mathematics", IHP trimester (second call for starting school and workshop registration)
- Next by Date: [isabelle] 0::'a
- Previous by Thread: [isabelle] "Semantics of Proofs and Certified Mathematics", IHP trimester (second call for starting school and workshop registration)
- Next by Thread: [isabelle] 0::'a
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list