Work with ProofPower in LaTeX/PDF (aka: THE SHED)
Overview
 This directory contains a collection of fragments of work using ProofPower in LaTeX documents converted to PDF for viewing. They are mainly philosophically motivated, but doing anything formally requires a lot of purely technical infrastructure, and so the philosophical connection may not be obvious. Listed in roughly inverse chronological order of document creation, left column most recent.
 Presentations Some presentations, given or in preparation, Introduction to Work in Progress A description of the problems I am working on and an index to the documents in which that work is progressing. Formal Architectural Modelling Some notes on methods for formal verification of system architecture in the context of Model Based Systems Engineering. Unicode Characters in ProofPower through Lualatex This document serves to establish what characters render like in utf8 ProofPower documents prepared using lualatex. Infinitary Induction in HOL This paper explores some ideas for providing general support in HOL for structures defined by transfinite induction, by exploiting a strong infinity axiom expressed in terms of a well-ordering on a new type of "'a ordinals". Illative Combinatory Logic Another approach to illative combinatory logic, based this time on the hol4 example on pure combinatory logic. Mainly an attempt to understand why that example is so much simpler than my own efforts. Axiomatic Method An exploration of axiomatic method using ProofPower. Iterative Foundational Ontologies A broad discussion of ontologies for mathematics and abstract semantics. Formal Semantics and Deductive Methods A discussion of formal semantics and semantic embedding. Pluralities and Sets This is a formal exploration with ProofPower of a topic addressed by {\O}ystein Linnebo in a paper under the same title. Meaning, Modality and Metaphysics A partly formal discussion of modal concepts leading to a discussion of certain kinds of metaphysics. Model Theory and Universal Algebra (II) This is a second exploratory approach to Universal Algebra. More Miscellanea This theory is for miscellanea which depend upon well-founded set theory with urelements (GSU). It also has misc1 as a parent. A Higher Order Theory of Well-Founded Sets (with Urelements) This is a modification of the pure set theory GS to admit urelements. An Illative Lambda-Calculus This is an approach to illative lambda-calculi via construction of an infinitary calculus in a well-founded set theory. Abstract Models for Concrete Constructions Some preliminary explorative modelling of electronic circuits. Equivalences, Quotients, Universal Algebra and Lattice Theory This is a limited development of universal algebra and lattice theory for the purposes of X-Logic. Higher Order Logic At present this document is a (small) mess pot of explorations of how one might go about presentation of Church's Simple Theory of Types and ultimately ProofPower HOL using Standard ML and/or ProofPower HOL. I am interested both in exposing exactly what Church said, comparing the details of his system with those of ProofPower HOL and discussing the reasons for the differences, but also I am looking for an interesting and digestible way of presenting ProofPower HOL to philosophers or other groups without much IT background. Its doubtful that all these objectives are compatible, and so far my attempts have not been in the least impressive, but I probably will keep picking at it and may eventually come up with something useful. Grice on Vacuous Names Formal analysis (using Higher Order Logic with ProofPower) and commentary on Grice's system Q (G, $G_{HP}$) first presented in his paper \emph{Vacuous Names}. The Proposition A place to play formally with the concept of proposition. This actually started as a formal look at some of Harvey Friedman's ideas, particularly his concept calculus but also BRT theory, and I think somehow I got the idea that the relevance of this to me was something to do with propositions. Anyway, it hasn't really got anywhere. The Logic and Metaphysics of Leibniz Formal models of aspects of the Logic and Metaphysics of Gottfried Wilhelm Leibniz. Pure Type Systems and HOL-Omega in ProofPower The abstract syntax and semantics of Pure Type Systems and HOL-Omega in a formal higher-order theory of well-founded sets. Russell and Wittgenstein, Logic and Metaphysics Formal models of aspects of the Tractatus Logico-Philosophicus and Russell's philosophy of Logical Atomism. Analyses of Analysis: Part II - Introduction The introductory chapter to the second part of Analyses of Analysis. Aristotle's Logic and Metaphysics Formalisation in higher order logic of parts of Aristotle's logic and metaphysics. Infinitary First Order Set Theory The abstract syntax and semantics of an infinitary first order set theory. Infinitarily Definable Sets This is my third approach to set theory conceived as a maximal consistent theory of comprehension. It differs from the previous attempt (in t024) by simplification of the treatment of infinitary logic, allowing only a single binary relation. More Miscellanea (misc1, misc2) This theory is for miscellanea which cannot be put in theory rbjmisc'' because of dependencies on other theories. It consists primarily of things required in the documents on non well-founded set theories, but not specific to that work, which make use of galactic set theory or fixed point theory. Since I moved my non-well-founded foundational work back from set theory to combinatory logic using version of well-founded set theory with urelements it has been necessary to replicate those definitions required which depend upon well-founded set theory in the context of this other version of well founded set theory. For that reason this document is in the process of being restructured as three theories, one of material which does not depend on the well founded set theory, and one for materials dependent respectively on each of the two versions of well-founded set theory. These are the theories misc1, misc2 and misc3. Infinitarily Definable Non-Well-Founded Sets This paper is my second approach to set theory conceived as a maximal consistent theory of set comprehension. The principle innovation in this version is to simplify the syntax by removing comprehension, so that the syntactic category of term is no longer required.
 A Higher Order Theory of Well-Founded Sets An axiomatic development in ProofPower-HOL of a higher order theory of well-founded sets. This is similar to a higher order ZFC strengthened by the assertion that every set is a member of some other set which is a (standard) model of ZFC. Surreal Geometric Analysis This document is an exploration into formalisation of geometric algebra and analysis using surreal numbers instead of real numbers. Set Theory as Consistent Infinitary Comprehension This paper is concerned with set theory conceived as a maximal consistent theory of set comprehension. This is interpreted by looking for large subdomains of a notation for infinitary comprehension, and the theory is developed from such interpretations. PolySet Theory This document is concerned with the specification of an interpretation of the first order language of set theory. The purpose of this is to provide an ontological basis for foundation systems suitable for the formal derivation of mathematics. The ontology is to include the pure well-founded sets of rank up to some arbitrary large cardinal together with the graphs of the polymorphic functions definable in a polymorphic functional language such as ML, and the categories corresponding to abstract mathematical concepts. The interpretation is constructed by defining names'' or representatives'' for the sets in the domain of discourse by transfinite inductive definition in the context of a suitably large collection of pure well-founded sets. A membership relation and a equality congruence are then defined simultaneously over this domain, so that the domain of the new intepretation is a collection of equivalence classes of these representatives. Relative to a natural semantic for the names, the definitions of these is not well-founded, and special measures are required to obtain a fixed point for the defining functional. These include choice of a suitable boolean algebra of truth values for the defined relations, and the location of a suitable subdomain of the representatives. NFU and NF in ProofPower-HOL Three formalisations in {\Product-HOL} are undertaken of NFU and NF. One is based on Hailperin's axioms. Another tries to follow Quine's original formulation by expressing stratified comprehension as a single higher-order axiom (axiom schemes are not supported by {\Product}. The last is a finite axiomatisation based on one originating with Holmes. The Category of Categories Explorations into the possibility of contructing non-well-founded foundations systems which are ontologically category theoretic and include a category of all categories. Category Theory Formalisation of some of the concepts of category theory in {\ProductHOL}. X-Logic Models Formal models of various aspects of X-Logic in Z An Introduction to ProofPower An introductory illustrated description of ProofPower (not progressed far enough to be useful). The Story of ProofPower History and rationale of the development of ProofPower. Z in HOL - the story of ProofPower An analysis of the ideas behind the engineering of a proof tool to support the Z specification language by semantic embedding into HOL. From the ideas of Leibniz via the creation of the new academic disciplines, first of Mathematical Logic and then of Computer Science, we trace the roots of one small step in the mechanisation of reason. Backward Chaining This document provides facilities for automatic reasoning based on backward chaining. They are intended to be similar in capability to refutation proof procedures such as resolution or semantic tableau, but in order to fit in better with interactive proof in ProofPower are not refutation oriented. The main target is a backchaining facility which searches for a proof of the conclusion of the current goal from premises and rules drawn from the assumptions and elsewhere. Unifying and Antiunifying Type and Term Nets Theorem proving in ProofPower is heavily based on rewriting which is supported by term nets which partially match the rewriting rules against target terms. To provide a higher level of automation using unification, closer to the power of modern predicate calculus automation present in other implementations of HOL term nets which unify rather than match, and which also produce antiunifiers have been considered here. This is mainly design, and though there is a very crude implementation, this is for evaluation only and would not deliver reasonable performance. Miscellaneous Tactics Several structures providing tactics, tacticals, etc. for theories, forward chaining, backward chaining, theory trawling et.al. Well-orderings and Well-foundedness This document consists of two parts. The first is a theory of well-orderings prepared by Rob Arthan for possible inclusion in the ProofPower theory of ordered sets. The second is material on well-foundedness, mainly consisting in the proof of the recursion theorem which is needed for consistency proofs of definitions by transfinite recursion respecting (if that's the right term) some well founded relationship. Illustrations of (Co-)Inductive Definitions This document provides examples of the use of the facilities provided in t007.doc. Inductive and Co-inductive Definitions in ProofPower Systematic facilities for a range of different kinds of inductive and co-inductive definitions of sets and types in ProofPower HOL. Miscellanea This document contains things used by my other theories which do not particularly belong in them. Definitions or theorems which arguably belong in a theory already produced by someone else. Well Founded Relations and Recursion Fixed points, well founded relations and a recursion theorem. Membership Structures A queer way of doing set theory in HOL (together with some queer reasons for doing it that way). Differential Geometry The theory of real vector spaces, norms and derivatives of functions between normed vector spaces as required for formal modelling of some physical theories. The Formalisation of Physics This document provides an example illustrating a method of formalising physical theories, together with a discussion of some aspects of {\it semantic positivism}. Metaphysical Positivism Formal models of aspects of Metaphysical Positivism source tarball (rbj.src.tgz) If you have ProofPower and some extra mathematical theories available from the Lemma1 web site then this tarball can be used to rerun (and tamper with if you like) the material in all these documents.

$Id: indexhead.xml,v 1.6 2013/02/01 09:02:00 rbj Exp$