Deductive Support for Science and Engineering

Logical Foundations Deduction can establish only necessary or analytic propositions, and must be conducted in a consistent logical framework. The most general and powerful logical context permitting consistent deduction is a formal foundation system such as a formal axiomatisation of classical set theory. My preferred foundation is a polymorphic higher order set theory with a liberal conservative extension principle and a reflection rule implemented following the LCF paradigm. Scientific Inference Scientific theories are not isolated contingent claims, but are part of coherent mathematical models which are introduced by conservative extension in just the same way as any other mathematical theory. Multiple incompatible models (e.g. general relativity and quantum mechanics) can be introduced in this way without logical inconsistency. The tools of formalised and mechanised mathematics can be applied to determining how these models behave either in particular or in more generally specified circumstances.

Formalised Mathematics Mathematics can be formalised on our logical foundations using conservative extensions which define the required mathematical concepts. Mathematical theories can then be derived in the extended contexts. Proficient functionality will be achieved by coding up practical methods. The reflection rule will permit these coded methods to be used for logical inference. Deferment of proof will be possible on a top-down principle of proficiency before rigour. Engineering Logic Models defined and evaluated by Scientific Inference are applied in Engineering Logic to evaluate by mathematical modelling proposed engineering designs. Design automation is realisable by coding up algorithms for this purpose in just the same way as more general mathematical methods are coded up. Ultimately, hand coded algorithms are displaced by machine generated alogorithms as Artificial Intelligence emerges.

© created 1996/10/8 modified 1996/12/31