Re: Remarks on an idea on First-Order Logical Duality

2012-07-31 Thread Bruno Marchal
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-Howar

Re: Remarks on an idea on First-Order Logical Duality

2012-07-30 Thread Stephen P. King
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 isomor

Re: Remarks on an idea on First-Order Logical Duality

2012-07-30 Thread Alberto G. Corona
"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 pr

Re: Remarks on an idea on First-Order Logical Duality

2012-07-30 Thread Bruno Marchal
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-Tarsk

Remarks on an idea on First-Order Logical Duality

2012-07-28 Thread Stephen P. King
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 pro