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/
--
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.
