At 10:11 -0700 14/08/2002, Wei Dai wrote: >Let me generalize my question then. Is it true that for any modal logic >that has a semantics, any sentence in that logic has a corresponding >sentence in non-modal quantificational logic with the same meaning?

## Advertising

It depends of the semantics. It depends of the order of quantification. It depends what you want to do. At 10:11 -0700 14/08/2002, Wei Dai wrote: >Before the invention of possible world semantics, people had to reason >about modalities on a purely syntactical basis. Are there still modal >logics for which no semantics is known? There are the modal logics of your servitor :-) Z, Z1, Z*, Z1* and X, X1, X*, X1* Those are well-defined modal logics. It is easy to prove them even decidable. I have partial soundness theorem for Z and Z1. No completeness! None of those logics have not even been axiomatized. (Open problems!). Remember the high constraint due to the fact that I "interview" sounds universal machines. The "mother box" corresponds to the Goedelian "beweisbar" predicate. If we interpret the propositional letters p, q, r ... by arithmetical sentences, and "[]p" is interpreted by beweisbar(godel-number-of(p)) then a natural question, which curiously did not appear in Godel 1933, is: which modal logic, if any, does the beweisbar box obey? Thanks to the work of Lob, Magari, Boolos, Solovay and others we know such a logic exists and it is G. Here is a presentation of G: AXIOMS: [](p -> q) -> ([]p -> []q) []([]p -> p) -> []p []p -> [][]p (this one can been shown redundant) RULES: p p->q p --------, --- q []p A class of Kripke frames (there exists others!) is set of finite, irreflexive, transitive frames. Actually G gives the part of that logic which remains provable by the machine itself. Solovay showed much more: the following *non normal* (indeed: NON necessetation rules) logic gives the whole propositional logic, including what is true but such that the machine cannot prove: AXIOMS: <All theorems of G> []p -> p RULES: p p->q -------- q In particular G* minus G gives the set of all 0-order modal propositions corresponding to true unprovable (by the sound machines), but bettable self-referential sentences. G* has no Kripke semantics, but it can be shown G* has some "natural" semantics in term of sequences of Kripke models. All the logics defined in my work are defined syntactically *from* G and G*, so that it is non trivial at all to find semantics. Roughly speaking the "knower" is defined by ([]p & p), the observer/bet-ter by []p & <>p, the "observer/better-embedded-in-UD*-with-comp-true" is []p & <>p with p interpretation restricted on "\Sigma_1" sentences (if they are true there are provable). The sensible observer = []p & <>p & p , with p \Sigma_1) At 10:11 -0700 14/08/2002, Wei Dai wrote: >We know that in general syntactical formulas and rules are not powerful >enough to always let us reason without meaning, because the set of >mathematical truths that are derivable syntactically from a fixed set of >axioms is just a subset of all mathematical truths. Yes but self-transforming "theories" or "machine/brains" can learn to makes bets and change themselves. That never gives the "whole" truth, a priori, but can help a machine to progress or just survive. At 10:11 -0700 14/08/2002, Wei Dai wrote: >The rest can only be >obtained by considering the semantic consequences of the axioms. I think >the point of syntax is just to give us a way to obtain at least some of >the truths through syntactical manipulation - a way to grab the >low-hanging fruit. Yes. And it is a point of the brain/body too. Bruno