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?
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
Received on Fri Aug 16 2002 - 08:14:22 PDT