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 firstorder metalanguage about a firstorder object language.
> After you do that, you can then collapse the two levels and
> define a singlelevel Tarskistyle 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
> firstorder 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 firstorder
> 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 firstorder definable (since the additional axiom requires
that the accessibility is wellfounded).
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 firstorder 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/ontologforum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontologforum@xxxxxxxxxxxxxxxx (06)
