Some tentative ideas about what this volume might cover.

In keeping with the purpose of the work as a whole, this will be a selective history. In the second half of the twentieth century an enormous variety of logical systems were studied by philosophers. However, the purpose of this history is to explore the ancestry of a point of view from which this diversity of formal systems is of peripheral interest.

The explosion of interest in so called ``non-standard logics'' coincided with the demise of any consensus on any systematic and pervasive role for logic in philosophy of the kind advocated in the first half of the century by philosophers such as Russell and Carnap.

Metaphysical Positivism revives the idea that the systematic exploitation of methods based on logic might be a worthwhile feature of analytic philosophy.

The proximate ancestor of Metaphysical Positivism is Logical Positivism, particularly as represented by the philosophy of Rudolf Carnap. This is seen by many philosophers as having been refuted first by Quine, and then by Kripke.

It is therefore important to present those aspects of Carnap's philosophy which are of greatest relevance to this history, which are his concept of logical truth, his views on semantics, and conception of formal methods for philosophy and science.

Some presentation of Quine's critique of the analytic/synthetic distinction if I can find any useful way of applying the method to these ideas. In this I am handicapped by the low level of credence which I give to his arguments and his alternative position.

Kripke's re-invention of metaphysics, though not to my taste, is at least more promising from the point of view of obtaining interesting models. and it will be of interest to contrast Kripke's conception of metaphysics with the that of Metaphysical Positivism.

This thread will be concerned with tracing the roots of our formal method, its languages logics and supporting software, through the Twentieth Century.

This will involve an account of what we draw from both logicism and formalism, together with something about why intuitionism is largely ignored.

The line of descent of the version of Higher Order Logic will be traced, which goes roughly:

• Russell's Theory of Types
• Ramsey's Simplification
• Church's Lambda Calculus
• Church's Simple Theory of Types
• Milner's Polymorphic Type-System for LCF
• Gordon's Polymorphic HOL
• Set Theory in HOL

The culture of modelling by conservative extension, following Frege's idea that:

Mathematics = Logic + Definitions

The implementation of software support in the form of the HOL proof assistant and ProofPower