Re: Remarks on an idea on First-Order Logical Duality
On 30 Jul 2012, at 15:34, 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. http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence 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. Actually I wrote, and did not send a reply on some of your remark on category theory. I agree that category is very interesting. But category are nice and smooth only around the first person notion. In fact in the math part of AUDA, categories and non boolean toposes can be used to model the arithmetical first person (the one we can canonically associate to self-referential machine). They are solipsist by nature, not by doctrine, and this correspond to the simple fact that we build our own private mental space, so the first person is intuitionist. category unfortunately don't handle well the second recursion theorem, and the whole intensional part of non constructive math, which makes them hard to use for the non first person hypostases. Also, category theory is abstract and difficult. It is already hard to find people with some maturity simultaneously in quantum physics, mathematical logic and philosophy-of-mind-computer-science, so adding the category notion tends to make the intersecting set empty. Category are useful for the functional part of comp, and awkward for the intensional part of computer science. The Curry-Howard isomorphism is *very* interesting, and was the main reason I made a little teaching on the combinators (and lambda terms) some year ago on this list, but of course that kind of things tend to be quickly technical, so I have come back with the numbers instead. For those who remember the combinators S and K, the typing of SKK gives the well known proof of A - A from the axioms A-(B-A), and A-(B-C) -. (A-B)-(A-C) which gives the types of K and S respectively. Note that the Curry-Howard isomorphism highlights the fact that proof and computations are different concept, as the proof are related to the programs and not the execution, and this does not fit well with the measure problem on the computations, where we can use instead the correspondence between some proofs of sigma_1 proposition and the computations, but we can still relate all this in some categories indeed. All this is a bit too much technical, and there are many technical open problems. Note also that the Curry-Howard isomorphism was also at the start only linking constructive proof with programs, but people like Jean Louis Krivine (and some others) have extended it on non constructive proofs, and this might be useful in the future of the AUDA program. No doubt on this, even if I am not sure of Jean-Louis Krivine choice of the way to extend it. Bruno PS I am re-connected! 2012/7/30 Bruno Marchal 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 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
Re: Remarks on an idea on First-Order Logical Duality
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. http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence 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. 2012/7/30 Bruno Marchal 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.pdfhttp://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 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 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) identification 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/~marchal/ -- 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.**comeverything-list@googlegroups.com . To unsubscribe from this group, send email to everything-list+unsubscribe@ **googlegroups.com everything-list%2bunsubscr...@googlegroups.com. For more options, visit this group at http://groups.google.com/** group/everything-list?hl=enhttp://groups.google.com/group/everything-list?hl=en . -- 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
Re: Remarks on an idea on First-Order Logical Duality
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. http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence 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 construction 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 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) identification 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
