Date: Sep 4, 2011 5:35 AM
Author: Rock Brentwood
Subject: Re: Why Math Works: Is math invented or discovered?
On Aug 22, 1:23 am, Virgil <vir...@ligriv.com> wrote:
> In article
> Graham Cooper <grahamcoop...@gmail.com> wrote:
> > 90% of sci.math taken for granted fundamental formula are INVENTED.
> > Real Mathematics is discovered!
> Whether that is true or not, proofs of it are invented.
Proofs are, themselves, mathematical objects and are not invented, but
discovered; including as "other" disparate objects in any of a large
number of "different" forms. The most notable examples of this, like I
explained in my last replay, fall under the Curry-Howard
correspondence, where we first learned that what we had been calling
proofs all along are actually one and the same as what we were also
calling the terms of the typed Lambda calculus. The most prominent
case, of course, is the classical proof of the tautology
I: A => A
from the axions
S: (A => (B => C)) => ((A => B) => (A => C))
K: A -> (B => A)
which proceeds by the well-known route
Step 1: An instance of S, which we'll abbreviate a => (b => c),
where a and b are both instances of K and c has a suitable form to
make a => (b => c) an instance of S.
Step 2: The axiom K: a
Step 3: Modus Ponens applied to 1 and 2 to yield b => c
Step 4: The axiom K: b
Step 5: Modus Ponens applied to 3 and 4 to yield c, which must
always be of the form A => A.
Modus Ponens corresponds to function application. Application in the
Lambda calculus is written by juxtaposition, with grouping to the left
(e.g. uvw means (uv)w, or (u of v) of w). Consequently, the entire
proof is simply the the lambda-term SKK.
The steps are: step 1, write down S, step 2, write down the first K,
step 3, write it after so to get SK, step 4 write down the second K,
step 5, write it after SK to get SKK.
In the Lambda calculus S = \xyz.xz(yz), K = \xy.x (with the
convention, commonly used in text and computer implementations of the
lambda calculus of writing the lambda as \), and you have the
SKK = (\xyz.xz(yz)) K K =_beta (\yz.Kz(yz)) =_beta \z.Kz(Kz)
Kz(Kz) = (\xy.x)z(Kz) =_beta (\y.z)(Kz) =_bet z
so that (by the zeta rule)
\z.Kz(Kz) =_beta \z.z
which is just the combinator I = \z.z. So the proof is just the
For references, the expansions of a, b and c requires for consistency
with Steps 1-5 are (and must be):
a = A => ((B => A) => A)
b = A => (B => A)
c = A => A
where B is arbitrary (the arbitrariness of B is closely linked to the
fact that *ALL* typed lambda terms SKx, for all x, yield I, since SK
and KI are eta-equivalent and SKx = KIx = I).
The key difference between a creation and discovery is that a creation
is the mark and work of a single individual and is unique to that
individual. A discovery is where a million different people keep
bumping into the same thing from a million different directions. Here,
it's the thing known variously as "combinator", "lambda term", "proof"
and also known under numerous other guises that may bear little or no
resemblance to anything having anything to do with proofs or
computation (example: a dialog strategy in what is known as Dialog
Logic, or a standardized legislative maneuver under a formalized