X-Logic is the confluence of ideas for the semantic web (from a previous incarnation of the project), with ideas offering a Carneadean resolution of "the problem" of radical scepticism, involving methodological pluralism and a technique which we call "epistemic retreat".

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

Some aspects of the architecture are explored using formal models, usually models written in languages supported by ProofPower (HOL or Z or set theory in HOL).

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

First, we take scepticism to be the repudiation of dogma, and hence characterised by an open mind. Second we note that scepticism, and its child positivism are continually vitiated by falling into negative dogma, of varying degrees of subtlety. Then note that the pyrrhonean rejection of opinion is itself a form of dogma, as is the desire to establish equipollence (a balance of evidence on each side) for all claims is also a form of negative dogma.

Open mindedness is best realised by recognising appearances, not merely sensory impressions but also our intuitions about what lies behind the. That we should gather evidence about the status of any conjecture, and present the evidence impartially. Conflicting theories can simultaneously be entertained along these lines, no choice need be made between them until some application demands it, and such choices need not always go the same way. We do not need to know which (if any) of our empirical hypotheses are true, we need only to decide on a case by case basis which are likely to give the best predictions for that application.

We want to be able to chose between different models of aspects of reality, whichever are best for the problem at hand. We therefore want science to make available comparative information, rather than prejudging by selecting just one model as "true". If science proceded in this way, then a the knowledge thus recorded would not ba a set of theories or facts deemed true, but a mass of comparative data. This epistemological perspective therefore has an impact on the way in which knowledge is represented and stored.

"Epistemic retreat" is the term we use for the retreat from asserting truth or falsity to asserting the results of various comparative measures. The difference is simplest represented in purely logical matters, where instead of recording the truth of some mathematical theorem, we record that it has been proven in some specific deductive system, and that the proof was checked by a particular proof checker.

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 an early simple model in Isabelle HOL covering (in a rather crude way) the following aspects:

1. the use of assurance marks
2. documents as propositions
3. programs as inference rules
4. languages as i/o specifications

It is out of date to the extent that it is not processable by current versions of Isabelle, but remains the most complete formal model of X-Logic.

This is my current working document and is a muddle! I set out to rework the previous material in Isabelle using ProofPower HOL + set theory, but I didn't get very far. I have recently resumed work on the formal modelling intending to model first an enhanced system of assurance tags. However, since the new system involves lattice theory, I have some work to do on that, which I am putting, pro-tem in Miscellanea. The lattice theory demands other prerequisites, material on equivalence relations, lifting operations over quotients, and I am now succumbing to the temptation to dabble in universal algebra, since much of the machinery I require seems independent of the particular kinds of algebras I am concerned with. So we can expect slow progress on formal models for X-Logic.