Mathematical Philosophy for Formal Analysis

Overview:

  • Logicism repaired
  • Formalism asset-stripped
  • Constructivism sidestepped
  • Lakatos and Social Constructivism rejected
logicism re-affirmed
logicism through analyticity, ontological liberalism
formalism in collusion with semantics, Gödel fully assimilated.
constructivism: the role of intuition and the importance of computation recognised, weak logics spurned
Lakatos, Social Constructivism: historical tales appreciated, pedagogical lessons absorbed, relativistic tendency rejected
A New Mathematics We advocate expanding mathematics to encompass all complex analytic truths.
New Tools Mathematicians should be teaching computers to do maths proper.

logicism re-affirmed:

see also: logicism
  • mathematics is analytic
  • Ayer's defence adopted
  • analytic truths semantically reducible to set theory
  • incompletely formalisable

Mathematics is Analytic: since mathematical truths follow from the definitions of the abstract entities involved
Abstract Ontology is arbitrary, with the limits of consistency
Set Theory (WF) Suffices: as a semantic foundation WF is rich enough to define all coherent abstract concepts
Conservative Extension Preferred: as a more abstract alternative to definitions
Inherited Incompleteness: theories developed using definitions in set theory may inherit incomplete formalisability
Incompleteness Not A Problem: available formalisations are good enough

formalism:

  • no easy answers on consistency, but Gödel's results yield a ranking
  • no substitute for semantic intuitions, but formality greatly aids precision
failure of Hilbert's program results in the need for strong foundation systems
Gödel incompleteness results prevent formality from wholly supplanting intuitive semantics
Questions of Consistency are now much better understood and are not a practical problem
Formal Descriptions, in practice, greatly improve the semantic precision of our languages
Hilbert's Ontological Liberalism, following Hilbert's lead we are content to work with any abstract ontology of whose consistency we are reasonably confident; set theory will do

constructivism:

see: Carnap's Syntactical Method
  • the role of intuition and the importance of computation recognised
  • weak logics spurned
Intuition is Vital, but my intuitions don't don't make me an intuitionist
Classical Logic OK, the soundness proofs are good enough for me (intuitionistic logic is OK as well)
effective analysis is important, but can be worked out with classical logics
Truth is not Proof the distinction is important, especially in the light of the incompleteness results
Types as Propositions, is a clever but not a good idea
Weak Foundations, are better than inconsistent ones, but not as good as strong ones ceteris paribus

Lakatos, Social Constructivism:

historical tales appreciated, pedagogical lessons absorbed, relativistic tendency rejected
Lakatos mimics Popper, trying to do for mathematics what Popper did for empirical science. Unfortunately though they may be sociologically similar, there are major epistemological differences.
Mathematical Truth Objective: notwithstanding Lakatos
history may be a poor guide either to what will be or what should be. Formal Analysis is a proposal for how things might be done.
Improvements in Presentation desirable, as Lakatos suggests. Presentation should fit purposes and nature of target audience.
Structure and Detail of Mathematics Engineered: Formal Analysis is a proposal for extensive re-engineering.
Truth Remains Absolute, the creativity of mathematicians does not make the truth of mathematical conjectures discretionary.

A New Mathematics:

We advocate expanding mathematics to encompass all complex analytic truths.
Mathematics is too narrowly conceived, anything which is too easy, or too hard for the wrong reasons, doesn't count as mathematics. So a fair amount of what non-mathematicians think of as mathematics doesn't figure in the maths department. This includes most things that people do with computers.
Frege said: Mathematics is Analytic
We say: Analytic is Mathematics!
With computers to do the drudgery, no analytic problem solving should be beyond mathematics. Stop giving ground to "Computer Science" Hackers
Re-Engineer Mathematics, mathematics should be completely re-engineered anticipating a future when mathematics will be done by computers, and often about computers.
Mechanise Mathematics the re-engineering should be a mechanisation. Proofs formal, machine checked, and often machine discovered. Methods resulting from the theory should be efficiently executable by the machine.
The Deliverable Should be Software not journal pages.

New Tools:

Mathematicians should be teaching computers to do maths proper.
delivering capability, in the future, mathematicians will not deliver theorems to a tiny auidience of other mathematicians, they will deliver capability at the work/play station.
theories to models the application of mathematics is through the building of mathematical models, mathematics developed in the right context will translate directly into new modelling capability
the mathematical environment, to a first cut a hybrid of mathematica and a good proof tool, will have formal precision and extensive mathematical libraries, which provide the machine with the capability not only to undertake mathematical computations to arbitrary known accuracy, but symbolic manipulations and abstract reasoning with superhuman speed and reliability.
making the tools: the major part of the creativity in creating the mathematical environment which will deliver future mathematics to its users is mathematical, those aspects which we would today think of as software engineering will be thought of in the future as just some of the mathematicians tools of the trade, not a different trade.


up Quick Index © RBJ created 1997/12/29 modified 1997/12/29