HOL for Knowledge Representation - rbjones/HoLoTruth GitHub Wiki

Here we expand upon that idea. Some prior discussion appears in The Philosophy, here we therefore steer clear of the deeper issues and focus on slightly more practical matters.

The architecture is intended to provide a context for superhuman deductive capabilities. In normal human discourse, in all but the rarified strata of research in pure mathematics, chains of deductive reasoning are short, and are checked by common sense evaluation of their results. Nevertheless in those domains outside of mathematics, such as philosophy, where complex reasoning may be employed, the results are inconclusive, partly because of ambiguities in the context which render different lines of reasoning equally plausible despite their incompatible conclusions.

If we move to a context in which long chains of deduction become routine, then this kind of contextual ambiguity or incoherence will soon be exploited by the derivation of explicit contradictions, rendering all further deduction meaningless. For this reason it is crucial to DA-Hol that the context in which reasoning takes place is unambigous and coherent. It is proposed that this is achieved by the use of abstract HOL for all knowledge representation, in a manner similar to that in which it is normally used in existing HOL theorem provers, i.e. exclusively by conservative extension over the primitive HOL language.

It is a consequence of this that all the truths represented will have a pure interpretation under which they express logical truths (this is sometimes call the broad conception of logical truth, otherwise known as analyticity). This broad notion of logical truth encompasses the truths of mathematics, but not those of empirical science.

Representation of empirical knowledge in science and engineering, or any other subject matter, is made possible in two ways. Firstly, though the possibility of multiple interpretations of the vocabulary in any context. Though all the truths can be interpreted in a pure well-founded set theory, they can also be interpreted in many other ways. When thus interpreted the mechanisms policing conservative extensions will guarantee the existence of an abstract interpretation, and hence the consistency of the resulting theory, but some intended interpretation in which the some of the entities involved are physical entities will permit the language to talk of the real world.

Though the possibility of concrete interpretations does provide one avenue for the use of abstract HOL for the presentation of empirical facts, there are reasons for preferring instead to think in terms of mathematical models which provide useful approximations to the structure of the real world. The main reason is that most scientific theories and engineering theory, uses models which are deliberate simplifications, and therefore, taken literally, are false. The disadvantages of this become lethal if we have two theories each useful, but which are incompatible, e.g. newtonian and relativistic mechanics. So long as we treat these as two logically independent mathematical models then no problems arise in having both of these theories available in some context. But if we were to regard these as both making true claims about the nature of the world we inhabit, then our context would become incoherent, and would no longer provide a basis for sound deductive reasoning.