Bruno, I know just a little about the curry-howard isomorphism... I looked into it somewhat, because I was thinking about the possibility of representing programs as proof methods (so that a single run of the program would correspond to a proof about the relationship between the input and the output). But, it seems that the curry-howard relationship between programs and proofs is much different than what I was thinking of. In the end, I don't really see any *use* to the curry-howard isomorphism! Sure, the correspondence is interesting, but what can we do with it? Perhaps you can answer this.
--Abram On Mon, May 18, 2009 at 12:54 PM, Bruno Marchal <marc...@ulb.ac.be> wrote: > > Hi Abram, > > > On 24 Apr 2009, at 18:55, Abram Demski wrote: > >> >> I'm starting a mailing list for logic, and I figured some people from >> here might be interested. >> >> http://groups.google.com/group/one-logic > > Interesting! Thanks for the link. But logic is full of mathematical > mermaids and I am personally more problem driven. I may post some day > an argument for logical pluralism (even a classical logical argument > for logical pluralism!), though. Ah! but you can easily guess the > nature of the argument ... > > >> >> >> I've looked around for a high-quality group that discusses these >> things, but I haven't really found one. The logic-oriented mailing >> lists I've seen are either closed to the public (being only for >> professional logicians, or only for a specific university), or >> abandoned, filled with spam, et cetera. > > > > But it is a very large domain, and a highly technical subject. It is > not taught in all the universities. It is not a well known subject. > Unlike quantum mechanics and theoretical computer science, the > difficulty is in grasping what the subject is about. > It take time to understand the difference between formal implication > and deduction. I have problem to explain the difference between > computation and description of computation ... > > > > >> So, I figured, why not try to >> start my own? > > > Why not? Actually I have many questions in logic, but all are > technical and long to explain. Some have been solved by Eric, who then > raised new interesting question. > > Have you heard about the Curry Howard isomorphism? I have send posts > on this list on the combinators, and one of the reason for that is > that combinators can be used for explaining that CH correspondence > which relates in an amazing way logic and computer science. > > Do you know Jean-Louis Krivine? A french logician who try to extend > the CH (Curry Howard) isomorphism on classical logic and set theory. I > am not entirely convinced by the details but I suspect something quite > fundamental and important for the future of computer science and logic. > You can take a look, some of its paper are in english. > http://www.pps.jussieu.fr/~krivine/ > Jean-Louis Krivine wrote also my favorite book in set theory. > The CH correspondence of the (classical) Pierce law as a comp look! > > Don't hesitate to send us link to anything relating computer science > and logic (like the Curry-Howard isomorphism), because, although I > doubt it can be used easily in our framework, in a direct way, it > could have some impact in the future. Category theory is a very nice > subject too, but is a bit technically demanding at the start. Yet, it > makes possible to link knot theory, quantum computation, number > theory, gravity, ... > Not yet consciousness, though. Intensional free mathematics still > resist ... > > >> >> >> In fact, I originally joined this list hoping for a logic-oriented >> mailing list. I haven't been entirely disappointed there, > > You are kind! > > >> but at the >> same time that isn't what this list is really intended for. > > Logic is a very interesting field. Too bad it is not so well known by > the large public. The everything list is more "theory of everything" > oriented. Logic has a big role to play, (assuming comp) but physics, > cognitive science and even "theology" can hardly be avoided in a truly > unifying quest ... And we try to be as less technic as possible, which > is for me very hard, ... oscillating between UDA and AUDA. > > Best, > > Bruno > > > > http://iridia.ulb.ac.be/~marchal/ > > > > > > > -- Abram Demski http://dragonlogic-ai.blogspot.com/ --~--~---------~--~----~------------~-------~--~----~ You received this message because you are subscribed to the Google Groups "Everything List" group. To post to this group, send email to firstname.lastname@example.org 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 -~----------~----~----~----~------~----~------~--~---