>let me try anew
>
>formalism was not created in the twentieth century
>
>nor did it arise spontaneously in the nineteenth century
> or blossom in the eighteenth
>or any such recent history
>
>the fact that language is possible at all
>is the foundations of formalism
> and this goes back hundreds of thousands of years
>
>all language is based on formal negotiations
>exchanging information
>
>the pointing metaphor goes well into our great ape ancestry
> and aparently is found in many animals
>(several pack marine animals to many land animals)
>
>so?
>
>well logic isn't something
> born when they created the word "axiomatic"
>
>the structure of language itself is built of the primitives
> with which all logical calculi are constructed
>
>rigorousness has one valid scientific criteria:
> repeatability
>
>repeatability attractors separate out
> using the dynamics of evolution
> and the thermodynamics of use
>
>words form languages
>
> ***********..^^^^^^^^^^
>
>now flash forward to goldblatt's book "topoi"
>
>if you expect to see axioms as strings
> you may be disappointed
>
>most of the axioms are expressed in strings
> commonly the natural language of english
>but often much informational content is expressed
>in diagrams of directed graphs
>
>now i will make a desperate confession
>
>when i first read goldblatt
> i didn't think it was truly a formalisation
>
>i thought it had too many hand-wavy
> "well-you-know-what-i-mean"s
>to be correctly seen as an axiom system
>
>so i made my own axiom system
>
>but i thought you needed to actually change the symbology
> to reach true rigor
>
>so i actually had four different types of objects
> and four different types of morphisms
>
>rules of formation were diagram productions
>
>i used a named dotted arrow
>
> a
>.....>
>
>to mean forAny morphism a
>
>and i used a named solid arrow
>
> A
>----->
>
>to mean thereExists morphism A
>
>similarly
> i had as negation symbols
> the above arrows with slashes through them
>
>("not for any" and "there does not exist" respectively)
>
>the same partition was used for objects
> a named dot forAny object
> and a named solid circle when thereExists an object
>
>i actually didn't like objects
> so i usually started out with their mappings to identities
>
>so there was a rule i would write
>
> ________________
> | m |
> ________ | a ....> . b |
>| | | ^ .\ |
>| . a | =====> | id_a| . |
>|________| | . m |
> | a |
> |________________|
>
>these diagrams were to be read
> "forAny object a
> thereExists a morphism id_a suchThat
> the given diagram on the right commutes forAny morphism m"
>
>notice how the rule also forms the naming convention
>
>it is assumed in this formalisation
> that symbols can be made to substitute in simple enough way
>so id_a really means that if a were called X
> we really mean id_X
>
>similarly
> this easily included other axioms of category theory
>
>the composition rule was
>
> ______________ ________________
>| | | |
>| a | | a |
>| . | | .\ |
>| . | | . \ m2 o m1 |
>| . | | . \ |
>| .m1 | ===> | .m1 \ |
>| V | | V / |
>| . .....> . | | . ......> . |
>| b m2 c | | b m2 c |
>|______________| |________________|
>
>now
> i had strange desires during this time
>
>like i really thought that no diagrams
> should ever consist of commutative diagrams larger than triangles
>
>in fact
> the composition rule and association make it easy
> to decompose into separate diagrams each triangles
>using a standard "and" interpretation of the collection operation
>so i started calling these diagrams "dox"es
>(as in the root meaning "word")
> and i called contradictory inversions of axioms
> "paradoxes"
>
>e.g.
> b
> .
> m1 \ . m2
> . /
> . ----/----> .
>a c
>
>because there always exists a composition
>
>i went through and translated many of the theorems
>into this new language i created
> and i thought myself so clever and bright
>that i showed this to a professor i knew from the putnam tests
>
>he looked them over
>and then turned and asked me a question i'll never forget
>
>"so what can you do with this?"
>
>well
> it's a formalisation
> and it makes things explicit
> and it shows how a computer might see it
> and...
>
>"but where did you learn the rules in the first place?"
> he said
>
>and i told of the main sources
> all the standards of mac lane and bell and others
>and i felt so happy for myself
> because none of it was taught at the school
>and...
>
>"can your diagrams do anything you didn't learn from the books?"
>
>he got me
>
>because
> well
>no they really couldn't
>
>they were just there to "make rigorous"
> what the books taught
>
>but the books obviously had rigor
>since i was able to repeatably duplicate their theorems
>
>so i swallowed my pride
> which was quite a big gulp in those days
>and confessed that i couldn't explain why i thought it was better
>
>and he said
> and this was a guy i did not regularly respect
>he said
>"don't get lost in aesthetic fetishes"
>
>i went home and reread goldblatt
> which was the only reference i actually owned at the time
>and step by step i looked for the theorems
>
>except for the clearly marked exercises
> they all were very fully detailed
>and i was amazed that my translations
>often amounted to a mechanical transformation
> of explanations often couched in a formal english
>
>i eventually ended up rereading the book
> (for what was like the fourth time)
>working through almost every theorem
>almost as an act of pride
>
>although there were a few places where i finally found
> that some simple arrow chasing steps were not described
>they almost always ended up the same applications
>of basic axiomatic rules like composition
> that were usually well known by then
>
>by the end of this fiasco
>i had come to a very hard conclusion:
>
>i really was stuck on a preference
> that was purely an aesthetic difference
>
>formalisation is a reduction to negotiated primitives
>and this could come in many different forms
>
>suddenly
> the whole foundational scare of the twentieth century
>seemed a silly bravado
>as if the chasm no previous generation had faced
> were a simple linguistic game
> translating ancient paradoxes into new symbologies
>
>fascinating themselves
>
>i understood why many constructivists
> who already recognise those negotiated primitives
>don't commit deeply to formalism
>
>because it often deteriorated
>into religious battles over coding standards
>
>and over the years as i entered the computer science field
>i saw many religious battles over coding standards
>
>what doesn't matter in any of these
> is brace placement or collection type
>
>what matters
> is behavior
>and fit to conceptual pattern matching modes
>
>what matter is how it acts
>
>how it looks is pure aesthetic fetish
>
>-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
>galathaea: prankster, fablist, magician, liar