Synthetic Philosophy and Deductive Engineering
This document outlines methods for writing formal specifications for the SPaDE project using ProofPower HOL. It clarifies the intended role for such specifications, identifies the context in which those specifications are to be written and seeks to provide the best possible links into the documentation with which agents must be familiar to undertake the specifications successfully.
It is presented in the following parts:
SPaDE is intended to be a reflexive project, rooted in essentially the same logical system as ProofPower HOL. It is intended to support “deductive engineering”, using reflexive methods, as a service for LLMs using the MCP protocol.
That service has two main components. The first is the management of knowledge repositories suitable for storing and organizing declarative knowledge. The second is support for logical inference in the context of bodies of declarative knowledge, in the form of focal deductive intelligence.
The reflexive nature of the project involves the optimisation of deduction by reasoning about the system. It includes the verification of derived rules of inference, which may then be executed directly within the system. This is a form of self-improvement which is to be baked into SPaDE from the outset. The formal work which is done using ProofPower prior to the establishment of SPaDE capabilities, will, as soon as is practical be migrated into SPaDE native knowledge repositories, as the SPaDE system takes over those responsibilities initially satisfied by ProofPower and github.
The HOL specifications are needed before that functionality is in place, and to ensure the integrity and coherence of the specifications we need something to process them. ProofPower HOL has been chosen to fulfill that role, which is part of a complex bootstrap operation necessary to get SPaDE off the ground.
A single task description will normally suffice for the entire development of a HOL theory, though this will usually be undertaken in multiple stages.
Those stages will be reflected in successive sections of the specification document itself, and the task description will be progressivelyupdated to identify the section to be addressed by each successive stage in accomplishing the task. So most of the detailed description of the work will be provided by early stages in the task and will be held in the specification document itself rather than the task description.
The execution of each section of a theory may also be broken into parts. They would be:
A SPaDE specification is a markdown document. The SPaDE make files strip the formal text from the markdown and prepare it for processing by ProofPower. ProofPower checks that the script is well-formed.
The HOL specification is embedded in the sml using HOL paragraphs and some sml procedure calls. Theorems are proven using sml scripts, usually achieving a goal oriented proof approach by the use of the ProofPower goal package. The development of such proofs is usually an interactive process, and provision is therefore made for agents to interact with ProofPower when an assigment requires theorems to be proven, and also when introducing new type definitions or for establishing the consistency of some constant specifications.
In general, error free processing of a complete specification document will be a strong indication of its syntactic and logical correctness, and a code review will not be necessary until this is accomplished.
A theory is opened with new_SPaDE_theory, defined in tlcd002.md:
new_SPaDE_theory ("theory_name", "parent", []);
The procedure opens the parent, removes any previous version of the theory, and creates it. Further parents are the third argument. The name is brief and suggestive of the theory’s role. Naming and the theory listings are in ampd012.md.
spc001.pp–spc005.pp in the ProofPower source src/hol are reference for the language and the deductive system. None of them is kept intact. The deductive system remains that of those documents, written so that an inference rule can be executed. A rule shown to be sound can then be run. HOL4, Isabelle, and Lean may be read as exemplars. New architectural HOL is this ProofPower HOL in markdown.
The first specification is the theory of T-expressions, in terms of which all architectural specifications are expressed, and which underpins both the specific metatheory of HOL and its representation in SPaDE repositories, as well as providing a more general basis for the representation of abstract syntax and other data structures.
[This is implemented in the SPaDE native repository using byte-sequences which are packed in building complex structures by conversion to and from null-terminated byte-sequences as described in the section on packing in krdd004.md.]
The foundational logical system of SPaDE is substantially similar in the substance if not in form to that of ProofPower HOL.
The relevant context falls under the following headings:
In writing the specifications it is necessary to be aware that the system we are trying to deliver is not the same as ProofPower HOL, even though the logical system is almost identical (as an abstraction).
There are three principal points of divergence.
The first, concerns the reflexive aspects of SPaDE, which demand a new inference rule which allows functions shown to be logically sound to be applied directly in deriving further conclusions within the system. This intended to make no difference to the theorems which are provable, but simply to shorten proofs.
To make the reasoning about the deductive system efficient, the provision for literal constants is modified to provide convenient support for term literals via an encoding of abstract syntax into byte sequences.
The third point of divergence concerns the claim to universality for declarative languge of the HOL specification language. The alleged universality attaches not to the bare HOL logical system, but rather to something which SPaDE calls a “universal foundational institution”. This is not the place to explain that concept, but its consequence for the SPaDE logical system is a preference for strong infinity principles, effectively large cardinal axioms. So the SPaDE variant of HOL will come with strong infinity axioms.
It is likely that it will be advantageous to provide special extracts of the ProofPower documentation focussing on those aspects which are needed for the specification work required in SPaDE, but this has not yet been done and so a selection of the existing documents is cited here pro-tem. It may be that an early task will involve creating such extracts, which can then be referenced in subsequent tasks.
There are multiple sources of documentation for ProofPower HOL, so I will provide references to the full range of available materials, together and also identify a compact subset which may be sufficient for most purposes.
The most comprehensive resource is the ProofPower repository at github.com/robarthn/pp. The build of ProofPower creates the documentation as PDF files but for many purposes it may be more instructive to refer to source files. SPaDEs use of ProofPower is on the utf8 branch which differs from the main branch in using utf8 character coding throughout.
The SPaDE development environment contains a clone of the utf8 branch of the ProofPower repository, which has been built and therefore contains the executables and the PDF documentation.
The documentation is also available online at:
https://www.lemma-one.com/ProofPower/doc/doc.html
Only a few of the ProofPower manuals are relevant to SPaDE.
The relevant documents are:
The following documents are linked to online copies at lemma-one.com in versions not quite the same as those which are build by the SPaDE development environment from the utf8 branch of the ProofPower repository. Developers can access the latter at $PPDIR/bld/doc.
SPaDE uses a minimal part of the ProofPower HOL theory hierarchy in its specifications. This is important to minimise the complexity of reflexive features of SPaDE.
SPaDE specifications are children of SPaDEroot (tlcd002.md), or of a theory which descends from it. SPaDEroot is opened on rbjmisc, from retro/np. The present context is the ancestry of rbjmisc together with SPaDEroot. Transition to minimal context is eventually intended, but is not a short term priority. That reduction is deferred in tlcd002.md.
It will therefore be helpful to agents contributing to the SPaDE specifications to be aware of what is available in rbjmisc, SPaDEroot, the ancestry of basic_hol.
The ancestry of basic_hol is documented in the ProofPower HOL reference manual usr029. A more compact presentation of the ancestors of basic_hol may be found in HTML at :https://www.rbjones.com/rbjpub/pp/pptheories.html
It may however be instructive for agents seeking to contribute specifications to refer to the source file which create the theories. These source files are located in the src directory of the ProofPower repository and the directory SPaDE/repo/np.
The names of the relevant files are as follows:
| Theory name | Source files |
|---|---|
| min | imp006.pp |
| log, init, misc | dtd023.pp, imp023.pp |
| pair | dtd023.pp, imp023.pp |
| list | dtd039.pp, imp039.pp |
| char | dtd040.pp, imp040.pp |
| rbjmisc | t006.pp, t010.pp |
The following formal specifications of ProofPower HOL and the HOL proof system are particularly relevant since some of these specifications will be rewritten for SPaDE, with the intention that there is no substantive change to the deductive system.
There is also a philosophical narrative (in SPaDE’s Synthetic Philosophy) concerning the universality of a foundational institution, closely related to this logical system, the precise formal articulation of which will involve an account of the semantics.
The source files are available in the development environment at $PPDIR/src/hol/
The theories created by these files are also available in the spade.polydb ProofPower database.
There are some eccentricities in the character set used by ProofPower which may not be as easily identified by the documentation as is desirable.
Since it is based on a pure lambda calculus, all variable binding in ProofPower HOL is done by applying a function to a lambda abstraction, but in the concrete syntax, the lambda is replaced by the name of the relevant function.
In the most common example, universal quantification, the function is called ∀ which is followed by the variables being bound and the character ⦁ not ..
For instance, the expression ⌜∀x⦁ P(x)⌝ is syntactic sugar for applying the ∀ function to the lambda abstraction ⌜λx⦁ P(x)⌝.
Note that when supplying a HOL term in an SML script “term quotes” (⌜⌝), sometimes known as “quine corners” must be used to delimit the term, not conventional quotation marks.
Another point to note is that when constants are defined in specification paragraphs, e.g. that introduced by ⓈHOLCONST, the vertical lines on the left should be formed using the character “│” rather than a conventional vertical bar “ |
”. |
In a HOL specification (the version we are using) arbitrary UNICODE characters may be used (though some configuration may be required). Commonly used non-ascii symbols include:
Greek Letters
Γ Δ Θ Λ Ξ Π Σ Υ Φ Ψ Ω
α β γ δ ε ζ η θ ι κ λ μ ν ξ π ρ σ τ υ φ χ ψ ω
Logic: ∧ ∨ ¬ ∀ ∃ ⦁ × ≤ ≠ ≥ ∈ ∉ ⇔ ⇒
Set symbols: 𝔹 ℂ 𝔽 ℕ ℙ ℚ ℝ 𝕊 𝕌 ℤ ⊆ ∅ ⊂ ∩ ⋂ ∪ ⋃ ⊖
Arrows: → ⤖ ⤕ ⇻ ↔ ⤀ ⇸ ↣ ↦ ↠ ⤔
Formal Text Brackets: ⌜ ⌝ ⓣ ⓜ ⓩ Ⓢ ■ ┌ └ ╒ ├
Padding symbols │ ─ ═ Index Brackets ⦏ ⦎
Bracketing symbols: ⟨ ⟩ ⟦ ⟧ ⦇ ⦈
Subscription and Superscription: ⋎ ⋏ ↗ ↘ ↕ Underlining: ⨽ ⨼
Relation, Sequence and Bag Symbols: ⩥ ▷ ⩤ ◁ ⁀ ↾ ↿ ⊕ ⊎ ⨾ ∘
Miscellaneous: ⊢ ⦂ ≜ ⊥ ⊖
In writing HOL specifications for ProofPower constant definitions (which include all types of term), are introduced using a ⓈHOLCONST specification paragraph. These allow a freedom of expression similar to the paragraphs in the specification language Z, which does not require specifications to be conservative. But ProofPower HOL does require definitions to be conservative, non-conservative extensions must be introduced by explicit axioms.
In enforcing this constraint ProofPower will attemp to prove automatically that an extensions is conservative, by demonstrating that there already is a function available with the required characteristics. Thus, if asked to intoduce a constant C such that P(C) ProofPower will attempt to prove that ⌜∃x⦁ P(x)⌝.
If it cannot do so, then the specification is made with a caveat which makes consistency provable, but will have to be discarged before the constant can be shown to have the required property. This works fine, but makes theory listings more obscure. SPaDEroot provides a mechanism to undertake a consistency proof which is beyond the automatic prover before the specification is introduced, yielding a conservative extension with a clearer theory listing. It is nevertheless generally preferable to present the specification in a form which can be proven automatically, without requiring the additional consistency proof mechanism. This is particularly important, for example, when the definition is recursive, because manual proofs of consistency are a lot harder than casting the definition in a form that can be automatically verified. Examples of such definitions can be found in the theory LIST.
There is also a proof requirement to be discharged before introducing a new type constructor, which is done by identifying set of objects which represent the new type (and will be in bijection with the new type) and which must be shown to be non-empty since HOL types are required to be non-empty.