Abstract

Was the QED project for the formalisation of mathematics too ambitious? Leibniz, whose conception of a universal language and calculus of reasoning preceded QED by 300 years, would have thought it faint-hearted, the two most difficult problems in realising his grander vision having been resolved by the revolution in modern logic and the invention of the electronic digital computer.

“X-Logic” is a contemporary interpretation of Leibniz’s project. Like the original, it is a multi-disciplinary enterprise, straddling the boundaries between philosophy, logic, computing, and science.

In this talk after introducing Leibniz and his project, I will enumerate some philosophical principles endemic to the Cambridge Automated Reasoning Group (implicit in the methods and/or explicit in some of the publications of the ARG ). Some consequences of these philosophical principles for an architecture for globally distributed, linguistically pluralistic, automated deduction will then be considered, making use of a formal model in Isabelle-HOL.

At this level inference takes place between documents, which are understood as complex propositions, and may be in any language which has a well-defined abstract semantics. The notion of proof is generalised to encompass all correct computation relative to program specifications expressed in terms of the languages of documents. Assurance of the truth of propositions thus proven is managed by the qualification of judgements with a list of those authorities upon whose infallibility certainty in the content of the judgement rests.

A central concern is the articulation of a notion of soundness appropriate to this context. A manner of resolving the foundational problem of semantic regress, and that of a final resort on matters of consistency. will be touched upon.