"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.pdf<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/~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.**com<everything-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=en<http://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 more options, visit this group at 
http://groups.google.com/group/everything-list?hl=en.

Reply via email to