ProofPower and its use at RBJones.com
Overview
This page provides information about ProofPower and the various formal theories developed at RBJones.com using ProofPower.
This page provides some information about ProofPower.
Galactic Set Theory and some applications. "Galactic" set theory is basically a higher-order set theory in which every set is a member of a "galaxy" and every galaxy is a model of ZFC. (galaxies are what Grothendieck called "universes", which is obviously a misnomer, you can't have more than one universe can you?)
In this document I prove the Knaster-Tarski fixedpoint theorem in a general formulation for HOL.
Some material concerning transitive and well-founded relations and the recursion theorem.
Formal definitions are given of the concepts analytic and demonstrative and it is proven that under these definitions the two concepts are coextensive. This is done twice using two slightly different models, the first very simple but with perhaps an unconvincing treatment of analyticity, the second a little more complex and hopefully a little more convincing.
A strong axiom of infinity is asserted to enable conservative development of classical set theory and its metatheory, and other foundational work for which a strong metalanguage is convenient.
This directory contains a collection of fragments of work using ProofPower in LaTeX documents converted to PDF for viewing. They are mainly philosophically motivated.
ProofPower
This page provides some information about ProofPower.
ProofPower and its Logic
ProofPower is a specification and proof development and checking tool developed by ICL and now owned by Lemma-1. It is an intellectual descendent of Cambridge HOL, and implements in Standard ML following the LCF paradigm, proof support for exactly the same polymorphic higher order logic as that in Cambridge HOL.
Links to listings of some of the theories which come with ProofPower, with brief descriptions. These are the ones used by the theories at RBJones.com, though at present I am not able to convert them all into HTML.
Freek Wiedijk is tracking progress on automated proofs of a list of "100 greatest theorems". This page lists the statements of the theorems on the list that have been proved in ProofPower.
ProofPower uses an extended character set so that logic and mathematics comes out a bit nicer. This page has some tables showing how these render in HTML.
This document contains extra sml procedures for use with ProofPower to support the methods adopted at X-Logic.org.
Strong Infinity Axioms
A strong axiom of infinity is asserted to enable conservative development of classical set theory and its metatheory, and other foundational work for which a strong metalanguage is convenient.
Introduction
A new "si" theory is created as a child of "hol" and an axiom of strong infinity is asserted of type IND. Probably
Proof Context
This is a place holder.
GST in HOL
Galactic Set Theory and some applications. "Galactic" set theory is basically a higher-order set theory in which every set is a member of a "galaxy" and every galaxy is a model of ZFC. (galaxies are what Grothendieck called "universes", which is obviously a misnomer, you can't have more than one universe can you?)
This document is an overview of and conclusion to the work in which Galactic set theory is developed, creating the theory gst which should be cited as ancestor by applications of GST and a proof context suitable for applications.
This document creates a theory of pure concrete categories and functors. The theory contains a set of theorems which might serve as an independent axiomatisation of the theory.
A simple model of semantics and soundness for X-Logic.
A theory of fixed points
In this document I prove the Knaster-Tarski fixedpoint theorem in a general formulation for HOL.
Introduction
A new "fixp" theory is created as a child of "hol".
Definitions
Definition of the notion of a bounded monotonic function and of least and greatest fixed points.
Least Fixed Points
Proofs that "lfp" gives a fixed point and that it is the least fixed point.
Greatest Fixed Points
Proofs that "gfp" gives a fixed point and that it is the greatest fixed point.
Inductive Definitions
Taking a closure of constructors for an inductive datatype definition.
Well-Foundedness and Recursion
Some material concerning transitive and well-founded relations and the recursion theorem.
This is the theory of transitive and well founded relations as sets (using ProofPower's SET type constructor).
Most ProofPower relations are properties not sets, so the theory of this kind of well-foundedness is developed here.
This is a proof of the recursion theorem for well-founded recursive definitions. It is modelled on Tobias Nipkow's proof for Isabelle HOL and uses relations modelled with ProofPower HOL's SET type constructor.
This document contains the proof of a recursion theorem asserting the existence of a fixed point for any functional which "respects" some well-founded relation.
Analyticity and Deduction
Formal definitions are given of the concepts analytic and demonstrative and it is proven that under these definitions the two concepts are coextensive. This is done twice using two slightly different models, the first very simple but with perhaps an unconvincing treatment of analyticity, the second a little more complex and hopefully a little more convincing.
Introduction
The motivation for these models and the correspondence of the defined concepts with prior usage is discussed, and the models compared.
Model 1
In this model the notion of analyticity in some language is effectively taken as primitive, by defining a semantics as an analyticity predicate. Language generic notions of analytic and demonstrative are then defined and shown to be coextensive.
Model 2
An improved model of semantics is now adopted, permitting a more informative definition of analyticity and a stronger soundness predicate for the deductive systems, more closely matching usual practice in soundness proofs.
Model 3
The treatment of the deductive system is refined by modelling a deductive system as an immediate derivability relation.

up quick index © RBJ

privacy policy

Created:2002/12/24

$Id: index.xml,v 1.8 2006/10/22 13:38:39 rbj01 Exp $

V