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 <[email protected] <mailto:[email protected]>>
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 [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/everything-list?hl=en.
