On 7/30/2012 9:34 AM, Alberto G. Corona wrote:

"Computations are not proof. There are similarities, and there are alot of interesting relationships between the two concepts, but wecannot use proof theory for computation theory"## Advertising

What goes to Another intriging duality : The Curry-Howard isomorphismbetween computer programs and mathematical proofs. It seems that bothhave the same structure after all.http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondenceAnd, as the Stephen mentioned paper makes use of Category theory andTopos 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 expressedas particular cases of a few, more encompassing categories. And 2)since the human mind arrange his knowledge in categories, accordingwith the Phillips paper I mention a few posts ago, this bring lightabout the nature of reality . No only the phisical world ismathematical, but this mathematical world has a few patterns afterall. That economy may say something about the reality, that for me isrelated with the process of discovery both conscious and mechanicaldiscovery: the natural evolution has discovered the mathematicalessence of reality and organized the brain in categories. Andscientist create hypotheses by applying their categorical intuitionsto new fields of knowledge, for example to discover new mathematicalstructures or new relations between existing structures. At the sametime, if the mathematical reality is not so simple, it would have beennot 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 construction which identiﬁes 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 algebra 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 – algebras." The construction of the Lindenbaum-Tarski algebra is implemented by 1) identiﬁcation of provably equivalent formulas and 2) ordering them by provable implication 1) might be equivalent to your sheaf of infinities of computations 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 algebra. 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. Bruno 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. http://iridia.ulb.ac.be/~marchal/ <http://iridia.ulb.ac.be/%7Emarchal/>

-- Onward! Stephen "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 everything-list+unsubscr...@googlegroups.com. For more options, visit this group at http://groups.google.com/group/everything-list?hl=en.