Foundations of Analytics
Overview
Foundation systems for formal analysis play the same role as logical foundations for mathematics but are aimed at a broader range of applications.
Our preferred starting point is the formalisation of set theory in Higher Order Logic. This provides a universal semantic foundation for X-Logic, and a suitable framework for further formal foundational experiments.
Some experiments in foundation systems intended to deliver pragmatic features like polymorhphism and structured name-spaces without rocking the boat.
The identification of functions with well-founded graphs is both fruitful and cumbersome. Is it possible to reconcile this classical framework with a more liberal notion of "rule"?
Formal foundation systems are normally associated with fixed sets of rules and axioms. For X-Logic, liberalisation is proposed, yielding a closer relationship between proof and computation.
The attempt to define semantics formally leads either to infinite regress or to meta-circular semantics. We propose the latter.
Introduction
Abstract and Concrete Semantics
In our theory of knowledge we propose the factorisation of semantics into a formalisable abstract semantics and an informal concrete semantics
Higher Order Set Theory
Set theory has been fundamental to mathematics throughout the twentieth century. We propose for it a broader foundational role in formal analytics.
Introduction
Universal Semantic Foundations
We define a universal semantic foundation system as one which can be used to give an abstract semantics to any coherent language, and argue that Higher Order Set Theory is one (among many).
The formalisation of ZFC in ProofPower HOL and its applications.
Galactic Set Theory and some applications.
Well-Founded Systems
Some experiments in foundation systems intended to deliver pragmatic features like polymorhphism and structured name-spaces without rocking the boat.
Reflexive Foundations
The identification of functions with well-founded graphs is both fruitful and cumbersome. Is it possible to reconcile this classical framework with a more liberal notion of "rule"?
Proof and Computation
Formal foundation systems are normally associated with fixed sets of rules and axioms. For X-Logic, liberalisation is proposed, yielding a closer relationship between proof and computation.
Where the Buck Stops
The attempt to define semantics formally leads either to infinite regress or to meta-circular semantics. We propose the latter.

up quick index © RBJ

$Id: foundAnaly.xml,v 1.1.1.1 2000/12/04 17:22:18 rbjones Exp $