The design of X-Logic is rooted in philosophy. The whole story is to be found in the philosophy of metaphysical positivism, but here we note the influence of two components of metaphysical positivism, and the features of X-Logic which they have determined. Those influences are of (Pyrrhonean) scepticism and of philosophical positivism.

This is an informal statement of requirements for X-Logic.

Some earlier ideas about X-Logic (previously at X-Logic.org).

Elements of scepticism appear through the history of Greek philosophy, perhaps the most famous example being the scepticism about sensory knowledge illustrated in Plato's allegory of the cave, in which sensory knowledge is likened to the knowledge of the world of a cave dweller whose only source of such knowledge was shadows cast on a wall of the cave.

To a first approximation scepticism can be described as a philosophy of systematic doubt. The word sceptic means, literally in Greek, one who searches, and the skeptics were those who sought true knowledge and therefore found it desirable to reject ill-founded dogma falsely presented as knowledge. Scepticism was made most thorough and systematic by the school started by Pyrrhus of Ellis. According to Sextus Empiricus, who left the most complete accounts of the views of the sceptics, there

It is intended that X-Logic be a framework supporting deductive reasoning in any language which has a well defined propositional semantics. The idea connects with the W3C XML activities, in which generic support for documents on the web is provided by a generalised markup scheme with appropriate metanotations for describing languages and transformations over documents in these languages. The XML activity lacks a full blooded semantic definition capability suitable for X-Logic, so the multilingual aspects of X-Logic are addressed by using the available XML metanotations as far as they go, and adding more powerfull ways of describing the semantics of these notations. Reasoning in X-Logic can then be supported effectively as if by semantic embedding, generic proof capability is realised via the semantic descriptions.

Each proposition in X-Logic is in some language, which provides a logical context. It is asserted to be true if it is demonstrably analytic. Synthetic proposition are addressed by constructing a logical context (as a language definition) which models the relevant aspects of the real world. In such a context the relevant synthetic propositions become analytic, the required facts about the word having been incorporated into the semantics of a language.

In X-Logic inference is not the exclusive province of Proof Tools, any program for which a propositional specification is available can be used to perform inferences. For this purpose a program is understood as a document processor, the input documents being premises to the inference and the output documents being the conclusions. A propositional specification for such a program is an assignment to the input and output documents of languages which have a propositional semantics (i.e. one which tells us which documents in that language are true propositions). The program satisifies such a specification if whenever it is supplied with inputs which are true (with respect to the relevant propositional semantics) it delivers output documents with are also true. It is obvious that any such program implements a sound proof rule.

Though the system is intended to support formal deductive proof, and hence give very high levels of assurance of the truth of its conclusion, it is not intended exclusively for high assurance work. It is intended also (if not primarily) for moderate assurance high functionality applications. The idea is that formality makes possible the use of advanced (and possibly unreliable) algorithms to be used in searching for solutions to problems, because it makes possible reliable independent checking of the adequacy of any putative solution to the problem.

It is intended however, that a well written program which does the job it is intended to do will suffice for inference in this system, so that no greater cost is imposed in implementing new functionality than would be the case outside the X-Logic framework. However, in order that low assurance implementations of inference programs can coexist with the tools based the construction and checking of low level logical proofs without bringing overall assurance levels down to the lowest level, it is required that the system keep track of the assurance with which each result has been obtained. X-Logic is thefore to have some kind of an assurance calculus.

This is a pdf document containingm at present two models.

The first model explored the following ideas:

1. documents as propositions
2. programs as inference rules
3. languages as i/o specifications

The second model is concerned with partial ordering of propositions by assurance.