On 7/30/2012 9:34 AM, Alberto G. Corona wrote:
"Computations are not proof. There are similarities, and there are a lot of interesting relationships between the two concepts, but we cannot use proof theory for computation theory"

What goes to Another intriging duality : The Curry-Howard isomorphism between computer programs and mathematical proofs. It seems that both have the same structure after all.


And, as the Stephen mentioned paper makes use of Category theory and Topos Theory (That is a variation of CT) to discover the duality , The curry howard isomorphism can be reshaped in terms of category theory.

What all these dualities say is that math structures can be expressed as particular cases of a few, more encompassing categories. And 2) since the human mind arrange his knowledge in categories, according with the Phillips paper I mention a few posts ago, this bring light about the nature of reality . No only the phisical world is mathematical, but this mathematical world has a few patterns after all. That economy may say something about the reality, that for me is related with the process of discovery both conscious and mechanical discovery: the natural evolution has discovered the mathematical essence of reality and organized the brain in categories. And scientist create hypotheses by applying their categorical intuitions to new fields of knowledge, for example to discover new mathematical structures or new relations between existing structures. At the same time, if the mathematical reality is not so simple, it would have been not discoverable in the first place, and it would not exist.

Dear Alberto,

You are pointing out exactly the relation that I was trying to explain. Thank you for pointing this out.

2012/7/30 Bruno Marchal <marc...@ulb.ac.be <mailto:marc...@ulb.ac.be>>

    Le 29-juil.-12, à 07:34, Stephen P. King a écrit :

         Dear Bruno,

         From http://www.andrew.cmu.edu/user/awodey/preprints/fold.pdf
         First-Order Logical Duality
         we read:
         "In the propositional case, one passes from a propositional
        theory  to a Boolean algebra by
         constructing the Lindenbaum-Tarski algebra of the theory, a
         which identifies provably equivalent formulas (and orders them
        by provable
         implication). Thus any two complete theories, for instance,
        are ‘algebraically
         equivalent’ in the sense of having isomorphic
        Lindenbaum-Tarski algebras.
         The situation is precisely analogous to a presentation of an
         by generators and relations: a logical theory corresponds to
        such a presentation,
         and two theories are equivalent if they present ‘the same’ –
        i.e. isomorphic –

             The construction of the Lindenbaum-Tarski algebra is
        implemented by

         1) identification of provably equivalent formulas
         2) ordering them by provable implication

             1) might be equivalent to your sheaf of infinities of

    Computations are not proof. There are similarities, and there are
    a lot of interesting relationships between the two concepts, but
    we cannot use proof theory for computation theory.

        (but requires a bisimilarity measure) and 2) seems contrary to
        the Universal Dovetailer ordering idea as it implies  tight
        sequential strings (but tightness might be recovered by Godel
        Numbering but not uniquely for infinitely long strings). But
        there is a question regarding the constructability of the
        Lindenbaum-Tarski algebra itself!

    This is needed for special application of the Lindenbaum-Tarski

             Does it require Boolean Satisfiability for an arbitrary
        propositional theory to allow  the construction?

    Not in general. Boolean satisfiability concerns only classical
    logic, but none of the hypostases, except the "arithmetical
    truth",  do correspond (internally) to a classical logic.


        It surely seems to! But is there a unique sieve or  filter for
        the ordering of implication? How do we define invariance of
        meaning under transformations of language? Two propositional
        theories in different languages would have differing
        implication diagrams , so how is bisimulation between them
        defined?????  There has to be a transformation that generates
        a diffeomorphism between them.




"Nature, to be commanded, must be obeyed."
~ Francis Bacon

You received this message because you are subscribed to the Google Groups 
"Everything List" group.
To post to this group, send email to everything-list@googlegroups.com.
To unsubscribe from this group, send email to 
For more options, visit this group at 

Reply via email to