Re: Godel proved maths inconsistent not incompleteness theorem

On Mar 17, 8:43 am, Alan Smaill <sma...@xxxxxxxxxxxxxxxx> wrote:
Marshall <marshall.spi...@xxxxxxxxx> writes:
On Mar 17, 4:47 am, Alan Smaill <sma...@xxxxxxxxxxxxxxxx> wrote:

Also ignored was my pointer posted earlier to a machine-checked proof
of Tarski's fixed point theorem, and the theory of recursive
functions, both in ZF.

I searched through your recent posting history but couldn't find
these.
Could you please repost the pointer(s)? I'd appreciate it.

www.publications.cl.cam.ac.uk/167/

Paulson, Lawrence C. (1995) Set Theory for Verification: II. Induction
and Recursion. Journal of Automated Reasoning, 15 (2). pp. 167-215.

That page wouldn't load for me, but you gave me enough information
that I could find it on citeseer:

http://citeseer.ist.psu.edu/341657.html


Abstract

A theory of recursive definitions has been mechanized in Isabelle's
Zermelo-Fraenkel (ZF) set theory. The objective is to support the
formalization of particular recursive definitions for use in
verification, semantics proofs and other computational
reasoning. Inductively defined sets are expressed as least
fixedpoints, applying the Knaster-Tarski Theorem over a suitable
set. Recursive functions are defined by well-founded recursion and its
derivatives, such as transfinite recursion. Recursive data structures
are expressed by applying the Knaster-Tarski Theorem to a set, such as
V, that is closed under Cartesian product and disjoint sum. Worked
examples include the transitive closure of a relation, lists,
variable-branching trees and mutually recursive trees and forests. The
Schroder-Bernstein Theorem and the soundness of propositional logic
are proved in Isabelle sessions.


Thanks again! Looks very interesting. Probably most of it will go over
my head, but I'll give it my best shot.


Marshall
.

Relevant Pages

  • Re: Definite description and set abstraction notation - recursive definition?
    ... >> the usual recursive definitions of 'well formed formula' depend on ... > Define the two notions by simultaneous recursion. ... You mentioned 'simultaneous recursion' and that sounds like it might be ... A nasty unique parsing theorem must be proved. ...
    (sci.logic)
  • Re: Binary Tree reposted
    ... Of couse the usual gripe with these nice 'recursive definitions' is that ... basically it's the compiler doing the bookkeeping for you (maintaing stacks ... Personally I'd rather do the bookkeeping myself to be able to catch these ... Recursion is second nature to ...
    (comp.lang.pascal.delphi.misc)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... Recursive functions are defined by well-founded recursion and its ... are expressed by applying the Knaster-Tarski Theorem to a set, ... variable-branching trees and mutually recursive trees and forests. ... "Alan Smaill is a liar when it comes to Mathematical Logic and can't ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... semantics proofs and other computational ... Recursive functions are defined by well-founded recursion and its ... are expressed by applying the Knaster-Tarski Theorem to a set, ... variable-branching trees and mutually recursive trees and forests. ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... semantics proofs and other computational ... Recursive functions are defined by well-founded recursion and its ... are expressed by applying the Knaster-Tarski Theorem to a set, ... variable-branching trees and mutually recursive trees and forests. ...
    (sci.logic)