.Open Mathematics
. Introduction - Mathematics is More than Logic
Modern mathematics contains a large number of re-usable formal systems complete with declarations, definitions of useful terms, axioms and theorems. For example, each algebra is a pre-fabricated collection of abstract data types. More powerfully, mathematical system talk about the possibilities for new classes and the relationships between different types of classes. Mathematics distils a quintessential language suitable for thinking about complex systems.
This document describes the ways in which mathematics is more than traditional logic:
.See http://www/dick/maths/logic_0_Intro.html
If you want to get to the specific techniques that make mathematics be more than logic, see
.See Algebra
and the sections that follow it.
. Quotations
"A Formal manipulator in mathematics often experiences the discomforting feeling that his pencil surpasses him in intelligence."
.Source Howrad W Eves, "In Mathematical Circles", Boston: Prindel, Weber and Scmidt, 1969, p52. Quoted in Am Math Monthly, V102n5(May 95)p437.
"The realisation began as an academic exercise without reference to personalities; Smiley manoevred the characters like pieces in a puzzle, twisting them this way and that to fit the complex framework of established facts -- and then, in a moment, the pattern had suddenly re-formed with such assurance that it was a game no more"
.Source Le Carre 62, "Call for the Dead", page 149 of "The Incongruous Spy"
. Historical Examples
Mathematicians have tended to use terminology, notation and techniques ahead of accepted logic of their time. Thus Euclid's geometry and Archimedes calculations were not expressed in the dialectic of Plato or the logic and metaphysics of Aristotle. Descartes used algebra (an Arabic invention) and combined it with Pappus's geometric analysis as a way of solving problems [
.See Grabiner 95
] and then published a "Discourse on Method". Pascal is famous for noting that the "heart has its reasons". Similarly Newton was forced to publish results derived with the calculus in the language and logic of Euclid. Maclaurin's defence of Newton's calculus was to show that its results could be derived, in a cumbersome way, from Archimedean and Euclidian methods. Liebnitz's concept of an infinitessimal was not shown to be consistent until 300 years later. The differential and integral calculi were used for a century or so while more rigorous minds attempted to explain why it worked. During the 19th century George Boole attempted to put the laws of logic in mathematical terms ("The Laws of Thought").
At the end of the 19th century, there was aprogram to put mathematics on a formal logical basis culminating in Whitehead and Russel's monumental three volume work "Principia Mathematica"[Whitehead and Russel 64]. I think that this attempt gives experiemntal evidence that mathematics is more complex than most philosophers can handle. The work of Goedel, Church, and Turing together show that any form of mechanical or formal reasoning will be either uninetersting, inconsistent or incomplete. And to this day even the most formal mathematical papers are (to a large extent) written in unformalised language.
In what follows we look at some particular extra-logical features of modern mathematics.
. Algebra
Algebra uses a very useful form of proof where a series of transformations are made to an expression and then a relation is deduced between the start and the end of the series. This is not used by "real" logicians. Recently, David Gries has been championing such "calculational proofs".
In text books the syntax looks like this
.As_is e1 R1 e2
.As_is R2 e3
.As_is R3 e4
.As_is ...
.As_is R[n-1] e[n]
At then of such a chain of relationships we can conclude that the combination
(relational product) of all the relations holds between the first and last
expression:
.As_is e1 (R1; R2; R3; ...) e[n].
or in shorthand:
.As_is e1 ;R e[n]
This inference is valid, since we can show:
(theory_of_relations)|- For e:#expressions, R:#relations, if e1 R1 e2 R2 e3 R3 ... e[n] then e1 (R1; R2; R3; ...) e[n].
Often all the relations and the conclusion are the same transitive relation. The identity relation("=") or logical equivalence("iff") are both very common and useful. The MATHS syntax is in
.See http://www/dick/maths/logic_2_Proofs.html#algebraic_step
There is no general algorithm for proving the equality of two formulae in a general logic with equality formulae [Post...]. There are procedures for converting some sets of equalities into effective and efficient algorithms for testing for equality - eg
.Source Knuth & Bendix "Simple word problems in Universal Algebras" pp263-297 in Cl Probs in Abs Alg Leech 1970.
.Source Nelson G & Oppen 80, G Nelson & D C Oppen, Fast Decision procedures based on congruence closure, J ACM V27(Apr 80)pp356-364.
.Source Smith A 90, Alf Smith, The Knuth-Bendix Completion Algorithm and its Specification in Z, pp195-220 in Nicholls 90.
. Solving Equations
"Solving an equation" is another mathematical process that is not part of traditional logic and is indeed not computable. In many ways Descarte's contribution to mathematics is wide application of a problem solving method that starts:
.As_is Let x be ....
and finishes
.As_is and so x=...
.Source Grabiner 95
Often a formula like `f(x)=a` where `f(x)` is an expression containing `x` as a free variable and `e` is an expression, is
transformed into one like `x=e` and the mathematician concludes "That `e` is the solution to `f(x)=a`".
But this is not always enough because, if there is no `x` such that `f(x)=e`, then assuming that `x` exists lets you deduce any conclusion including that `x=a`. So having derived `x=a` we should check `f(a)=e`.
In general, suppose that `P(x)` is assumed and `x=e` derived. Then you have shown that if an x exists that satisfies P then it must be x:
(1):if for some x( P(x)) then x=e,
In formal terms we have the following theorem - if whenever `x` satisfies `P` it is `e`, then either `e` satisfies `P` or no `x` can satisfy `P`:
(logic)|- if (for all x(if P(x) then x=e)) then ( P(e) or for no x( P(x))),
Or - either there is no way to satisfy P or we have found it.
(logic)|- if (for all x(if P(x) then x=e)) then ( for no x( P(x)) or (for one x(P(x)) and the x(P(x))=e )).
Hence it is valid to infer
(2): e=the x(P(x)) or for no x(P(x))
from
(3): for all x(if P(x) then x=e).
Typically P(e) is assumed to follow, however this step is not always valid. Only by assuming or showing `for some x(Px)` can we safely deduce `P(e)` from `For all x, if P(x) then x=e`.
Thus 'solving an equation' does not guarantee that the solution exists. Of course if a value is deduced and if it satisfies the original properties then we have
(logic)|- if for all x(if P(x) then x=e) then if P(e) then e=the(x||P(x) ).
Hence
(above)|- if for all x(if P(x) then x=e) and P(e) then e=the x(P(x)).
Hence a valid method is to find a possible solution and then verify it.
. Calculational Solutions
Sometimes (ideally) the derivation of the solution is reversible - each step is an `iff-step`. Then solving the equation works because the following formula is true and indicates a valid argument:
(logic)|- if for all x:T( f(x)=a iff x=e) then f(e)=a.
The argument is a classical algebraic or calculational proof that looks like this
.As_is Let{ x:T.
.As_is f(x)= a
.As_is iff e1=e2
.As_is iff e3=e4
.As_is ...
.As_is iff x=e[n]
.As_is } |- f(e[n])=a.
In MATHS we would include labels or explanations to guarantee the above format.
.As_is Let{ (e0): x:T.
.As_is (e1): f(x)= a
.As_is (e2): iff e1=e2
.As_is (e3): iff e3=e4
.As_is ...
.As_is (em): iff x=e[n]
.As_is } |- f(e[n])=a.
. Creative Mathematics
In the past when an expression for x has not been found mathematicians have created new algebras by postulating that a set of equations do have solutions and working out the consequences - ultimately redefining the universe of discourse to include the new types of objects:
for i:Nat0, some x:X(i+x=0) -- leads to signed integers(X:=Int)
for i,j:Int, some x:X(i*x=j) -- leads to rational numbers(X:=Rat)
for a:Rat, some x:X(x*x=a) -- leads to irrationals, and hence the Real numbers
for all a:Real, some x:X(x*x=-1) -- leads to imaginary and complex numbers
.Open Proposed Syntax for Solving Problems
The examples and schema are deceptively simple - a single variable and a single predicate. However by choosing the sufficeintly complex domain of discourse the variable `x` can be a structured variable with hundreds of more or less complex components. Similarly the predicate can be a conjunction of many terms. The MATHS syntax of a `net` is ideal for documenting such complex domains of discourse:
.See http://www/dick/maths/notn_13_Docn_Syntax.html
The following syntax for mathematical problem solving is therefore suggested.
The ideal problem+solution would look like this
.Box
PROBLEM::=following
.Net
Definitions and declarations.
Assumptions.
Goals.
.Close.Net
SOLUTION::=following
.Net
Analysis: Manipulation to give solutions.
Synthesis: Proofs that solutions fit the assumptions.
.Close.Net
.Close.Box
. Examples of solving an equations.
A non-parametric problem:
(ex1): solutions{ x:Real, x^2-7*x+12=0} = {(x=>3),(x=>4)}.
ex1_PROBLEM::=following
.Net
x:Real.
|- (ex1a): x^2-7x+12 =0.
.Close.Net
ex1_SOLUTION::=following
x:Real.
solutions = {(x=>3),(x=>4)}.
proof the x=3 is a solution.
.Let x=3,
(-1, arithmetic)|- x*x = 3 * 3 =9,
(-2, arithmetic)|- 7*x = 7*3=21,
(-1,-2,arithmetic)|- x*x-7*x = -12,
(-1, arithmetic)|- x*x-7*x +12 = 0
(-1)|-$ex1_PROBLEM.
.Close.Let
Proof that x=4 is a solution.
Left as an exercise for the reader.
.Close.Net
Also see
.See ../samples/fish.html
for a simple example.
Example of solving an equation given data/parameters.
(ex2): solve{ x:Real, a*x^2-b*x+c=0} given{a,b,c:Real}
(ex3): = map[a,b,c:Real]{ (-b-sqrt(b^2-4*a*c))/(2*a), (-b+sqrt(b^2-4*a*c))/(2*a)} .
. General form
Solving_Equations::=Net{
For Documentation D, solutions{D}::=$Net{D}.
For Documentation D1,D2, solve D1 given D2::=map[p:$D2](solutions(D1)).
}=::Solving_Equations.
.Close Proposed Syntax for Solving Problems
. Benign Confusion and Abuses of Notation
Mathematical texts and papers over the years demonstrate that there is no harm in less than rigorous syntax. Bourbaki calls these "Abuses of notation". For example - An unbound variable in a proposition is automatically assumed to be unversally quantified to some local default type.
There are two common and contradictory idioms used to talk about algebras in text books:
The typical definition is
`An Monoid M is a triple of a set S, with an operation + and unit 0, ...`
but the typical way this is used is like this
`X is a Monoid with operation * and unit 1`
meaning
`The triple (X, *, 1) is a Monoid.`
In general the name of a set of tpls is used as a name for the type of the first element - this seems to be a harmless piece of overloading, which we formalize as follows:-
If the first declaration in a set of documentation is for a variable of type `Sets`:
xyz::=$XYZ
where
XYZ::=Net{x:Sets, y:Y,z:Z...}
Then
`xyz` can be used as follows:
.As_is (x=>X, y=>b, z=>c ...) : xyz -- declares variables(X,b,c,...)
.As_is (X, b, c, ...) :xyz -- declares same variables
.As_is X : xyz(y=>b, z=>c, ...) -- declares an X (Given b,c,...)
.As_is X : xyz(b, c, ...),
.As_is X : xyz, -- declares (x=>X, y=>y, z=>z,...) : $XYZ
Further we allow sets in both these forms:
|- xyz(y=>b, z=b, ...) = {X:Type||(x=>X, y=>b, z=>c ... )in XYZ}
|- xyz(b, c, ...) = {X:Type||(x=>X, y=>b, z=>c ... )in XYZ}
Thus since Monoid::=$Net{X:Sets, op:associative(X), unit:units(X,op)} we can write
(X=>Nat0, op=>(+), unit=>0) in Monoid
or
Monoid(X=>Nat0, op=>(+), unit=>0)
or
Nat0 in Monoid(op=>(+), unit=>0)
or
Nat0:Monoid((+), 0)
A piece of documentation can define a name to be a tpl of declared terms, then all the terms can be substituted implicitly. Suppose we have
XYZ::=Net{ x:X, y:Y,z:Z,
a::=...
P...
N::=(x,y,z)
}=::XYZ.
then we can write
Use XYZ and N=(u,v,w)
as equivalent to
.As_is u::X, v::Y,w::Z
.As_is a::=...
.As_is P...
.As_is N::=(x,y,z), N=(u,v,w)
is equivalent to
.As_is u::X, v::Y,w::Z
.As_is a::=...
.As_is P...
.As_is x=u, y=v, z=w,
.As_is N::=(x,y,z)
. Analogies
A common method for a tough problem is to map it into one of a set of
simpler probelms, solve that one and map the solution back to the original
problem domain. This is very helpful in tackling tough problems. A well chosen
map will transform a tough problem into one that can be solved more easily
and then mapped back into a solution to the tough problem. For example
the Logarithm map developed by Napier. Here is the simplest form
the logarithms to base 2.
.As_is Original Relation Transformed
.As_is 128 * 4 = 2^7*2^2
.As_is 7+2 = 9
.As_is Solve
.As_is 9
.As_is 2^9 =
.As_is 512
The general form of logarithm to base `b` is:
.As_is Numbers Greater than Zero <-> Numbers
.As_is 1 <-> 0
.As_is b <-> 1
.As_is Multiplication <-> Addition
.As_is Division <-> Subtraction
.As_is Exponentiation <-> Multiplication
.As_is Roots <-> Division
.As_is Less_than <-> Less_than
.As_is Unequal <-> Unequal
More advanced maps are the Laplace and Fourier transforms. A
computer proffessional also understands intuitively that decimal numbers
and binary numbers are transforms of each other that preserves the
arithmetic of the underlying numbers.
In other words a complicated domain can sometimes be transformed into
asimpler one without destroying the essence or structure of the
original domain. For this process to be worthwhile there must be an easy way
to transfer expressions and values across the map. Typically a set of
tables are prepared (not an easy task) that can be searched quickly and
easily. However for this to be valid the map must preserve
the structure of the domain.
. Structure Preserving Mappings
Structure preservation is at the heart being able to solve problems by
.See Analogies
One of the ways of distinguishing a logician from a mathematician is that (by and large) a logcian is most interested in a single set of axioms whereas the mathematicain is concerned with the relationship between two or more sets axiom systems. One of the commonest echniques and ideas of the twentieth century scene has been the study of sets of maps that transmit or preserve the structure of the objects that they connect.
The very word 'map' indicates an object that reflects in a grossly reduced and simplified some of the properties of the real world. The properties are those that are useful to the owner of the map - lengths are to scale, directions similar, and colors on paper refect something about what is in the equivalent places in the real world - blue often means - a place of wetness, for example. Thus a map guides its user in the real world with out being the real world.
In general a structure preserving mapping is called a 'morphism'. They come in a wide variety of flavors. Some standard flavors will be found in
.See http://www/dick/maths/math_11_STANDARD.html
The Grand Unified Theory of all systems and morphisms is called Category Theory. Some have called this "general abstract nonsense" but it turns out that category theory provides a common language and approach to any logistic system. Category theory is the ultimate map - it guides its user in a world of abstract structures.
.Close
. See Also
theory_of_relations::=http://www.csci.csusb.edu/dick/maths/logic_40_Relations.html.
logic::=http://www.csci.csusb.edu/dick/maths/logic_2_Proofs.html
.Close Mathematics