My Current HOL Algorithm

The following is equivalent in strength to HOL Light. Continues this post.

• As an extension of the notion of term (defined here), add the notation of polymorphically typed lambda calculus, an equality predicate, and the choice operator (I'll call it epsilon-- it's a function that takes predicates and forms a term that represents an arbitrary satisfier of the predicate, if one exists; otherwise, it just represents an arbitrary term).
• Take terms with boolean type as a drop-in replacement for atomic statements in that design. (It may seem strange to use them to replace atomic statements, since they are compound statements, but bear with me. Rules will correspond to valid sequents, rather than to compound statements in the logic.)
• Use lambda-calculus unification as a drop-in replacement for first-order unification. This includes normalization; we could either store the normal forms of statements in the KB or let the unification algorithm normalize on the spot, depending on whether space efficiency of the KB or time efficiency of the unifier is a bigger concern.
• Implement equational reasoning. Fundamentally, we treat an equality statement which has a given truth value, T, as if it represented two rules with that truth value: one justifying inferences in each direction, substituting one term for another. These rules cannot be stated as FOL rules, however, since they represent substitution of terms within larger statements. Nonetheless, the same basic propagation scheme for the truth values will work. In addition to the 2 pseudo-rules for each equality statement, we treat the system as knowing A=A for all terms A. Knuth-Bendix completion should be implemented eventually, which allows us to ignore one of the two inference directions for each equality statement without losing anything. Ultimately, I believe this means equational reasoning can be implemented as an extension to the normalization step of the unification algorithm (but I could be wrong here).
• Finally, we also need one hypothetical reasoning rule: if assuming A implies B with truth calue TV1, and assuming B implies A with truth value TV2, then A=B with truth value (& TV1 TV2) for an appropriate &-formula. Rather than implementing this as one complicated hypothetical reasoning step, it seems to me that the most convenient way would be to implement rule-level reasoning in general (ie, a query can be a rule, rules can be combined with other rules to produce new rules, etc) and then add this as a way of recording high-probability mutual implication.

That's all, folks!

PS:

In addition to the above reasoning system, for HOL Light, we also need the axiom of choice and the axiom of infinity. (The axiom of extensionality is covered by normalization.) Both of these axioms are very much "mathematical" in nature, and it isn't clear whether they are needed for more common-sense reasoning. (My suspicion is that they would emerge in other forms, ie, in coding the KB we'd encode something like these plus much more.)