```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> <353f854d-c04b-4ae0-9915-897859d3b...@y8g2000prd.googlegroups.com>,>  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, butdiscovered; including as "other" disparate objects in any of a largenumber of "different" forms. The most notable examples of this, like Iexplained in my last replay, fall under the Curry-Howardcorrespondence, where we first learned that what we had been callingproofs all along are actually one and the same as what we were alsocalling the terms of the typed Lambda calculus. The most prominentcase, of course, is the classical proof of the tautology   I: A => Afrom 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 tomake 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 mustalways be of the form A => A.Modus Ponens corresponds to function application. Application in theLambda calculus is written by juxtaposition, with grouping to the left(e.g. uvw means (uv)w, or (u of v) of w). Consequently, the entireproof 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 theconvention, commonly used in text and computer implementations of thelambda calculus of writing the lambda as \), and you have thefollowing beta-equivalences   SKK = (\xyz.xz(yz)) K K =_beta (\yz.Kz(yz)) =_beta \z.Kz(Kz)and   Kz(Kz) = (\xy.x)z(Kz) =_beta (\y.z)(Kz) =_bet zso that (by the zeta rule)   \z.Kz(Kz) =_beta \z.zwhich is just the combinator I = \z.z. So the proof is just thecombinator I.For references, the expansions of a, b and c requires for consistencywith Steps 1-5 are (and must be):a = A => ((B => A) => A)b = A => (B => A)c = A => Awhere B is arbitrary (the arbitrariness of B is closely linked to thefact that *ALL* typed lambda terms SKx, for all x, yield I, since SKand KI are eta-equivalent and SKx = KIx = I).The key difference between a creation and discovery is that a creationis the mark and work of a single individual and is unique to thatindividual. A discovery is where a million different people keepbumping 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 noresemblance to anything having anything to do with proofs orcomputation (example: a dialog strategy in what is known as DialogLogic, or a standardized legislative maneuver under a formalizedparliamentary procedure).
```