Hi John, (01)
Quoting "John F. Sowa" <sowa@xxxxxxxxxxx>: (02)
> Till and Chris,
>
> By using Dunn's semantics, modal logic can be formalized in
> a first-order metalanguage about a first-order object language.
> After you do that, you can then collapse the two levels and
> define a single-level Tarski-style model for the combined
> system. That collapsed form is less readable than the original,
> but it demonstrates that you can map the modalities into a
> first-order framework. See
>
> http://www.jfsowa.com/pubs/laws.htm
> Laws, Facts, and Contexts
>
> With Dunn's semantics instead of Kripke's semantics, each
> world w is replaced by a pair (M,L), where M is the set of
> propositions true in w (called facts) and L is the subset
> of facts (called laws) that are necessary in w.
>
> Both versions are formally equivalent, but Dunn's approach
> supports very useful generalizations that are difficult or
> unwieldy with Kripke semantics:
>
> 1. The object language (metalevel 0) is purely first-order
> and a theorem prover can ignore the distinction between
> laws and facts at the object level.
>
> 2. Each modal operator is treated as a metalevel comment
> about provability from the laws (necessity) or consistency
> with the laws (possibility). (03)
This has always seemed fishy to me.
The modal logic in which provability is a modal operator
is called G, which includes an axiom that is the analogue of
Loeb's theorem for provability predicates (as Till and Chris
have already mentioned). Furthermore, this modal logic is
not first-order definable (since the additional axiom requires
that the accessibility is well-founded).
So I can't see how any approach in which the modal operator
is "treated as a metalevel comment about provability"
can be equivalent to first-order logic.
Alternatively, I can't see how any such approach could be
related to any other modal system that doesn't include G. (04)
- michael (05)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (06)
|