Modal Logic [Logic]

Prev: Why Has None of Computer Science been Formalized?
Next: On Ultrafinitism

From: Owen on 8 Oct 2006 08:47

Owen wrote:
> Frederick Williams wrote:
>
> >
> > Sure, S5 is not n valued for finite n, but the op says _similar_ to the
> > Lewis system S5. Didn't Lukasiewicz have a four-valued modal logic?
> > Iirc it's in his North-Holland collected papers and Prior discusses it
> > somewhere.
> >
> > >
> > > Confutus wrote:
> > > > I'm interested, but I have a radically unorthodox approach to the
> > > > subject. A number of years ago I worked out how a modal logic formally
> > > > similar to the Lewis system S5 could be based on Lukasiewicz 3-valued
> > > > logic, and I haven't yet been able to find anyone much interested in
> > > > it.
>
>
> Truth tables for Modal logic

> Not (~)
> ~t = f, ~f = t, ~F = T, ~T = F.
>
> And (&)
> t & t = t, t & f = F, t & F = F, t & T = t,
> f & t = F, f & f = f, f & F = F, f & T = f,
> F & t = F, F & f = F, F & F = F, F & T = F,
> T & t = t, T & f = f, T & F = F, T & T = T.
>
> Or (v)
> t v t = t, t v f = T, t v F = t, t v T = T,
> f v t = T, f v f = f, f v F = f, f v T = T,
> F v t = t, F v f = f, F v F = F, F v T = T,
> T v t = T, T v f = T, T v F = T, T v T = T.
>
> Implies (->)
> t -> t = T, t -> f = f, t -> F = f, t -> T = T,
> f -> t = t, f -> f = T, f -> F = t, f -> T = T,
> F -> t = T, F -> f, = T, F -> F = T, F -> T = T,
> T -> t = t, T -> f = f, T -> F = F, T -> T = T.
>
> Equivalence (<->)
> t <-> t = T, t <-> f = F, t <-> F = f, t <-> T = t,
> f <-> t = F, f <-> f = T, f <-> F = t, f <-> T = f,
> F <-> t = f, F <-> t = f, F <-> F = T, F <-> T = F,
> T <-> t = t, T <-> f = f, T <-> F = F, T <-> T = T.
>
> Necessity ([])
> []t = F, []f = F, []F = F, []T = T.
>
> Possibility (<>)
> <>t = T, <>f = T, <>F = F, <>T = T.

> Owen

From: Owen on 8 Oct 2006 09:06

From: Chris Menzel on 8 Oct 2006 14:51

On 8 Oct 2006 06:06:32 -0700, Owen <owenholden(a)rogers.com> said:
> Chris Menzel wrote:
>> On 6 Oct 2006 04:24:08 -0700, Owen <owenholden(a)rogers.com> said:
>> > ...the axioms and theorems of modal propositional logic (eg.S5) are
>> > truth functional tautologies.
>>
>> Do you have a proof of this? (Would seem to be an easy induction on
>> length of proof.)
>
> No, I don't know how to formally prove it.

Seems like all you'd need to do is assume as an induction hypothesis
that, for an arbitrary n, every theorem of S5 with a proof of length m<n
is a tautology in your sense, and then show, on the basis of this
assumption, that if p1,...,pn is a proof of length n of pn, then pn is a
tautology. There are three cases to consider: either pn is an axiom of
S5 (in which case, you have claimed, it is one of your tautologies), or
pn follows by MP from wffs pi, pj occurring earlier in the proof (that
presumably follows from your truth table for ->, given the induction
hypothesis that pi and pj are tautologies), or pn follows by
necessitation from a wff pk occurring earlier in the proof (which IIRC
seems to follow immediately from your truth table for []p given the
induction hypothesis).

>> > This logic greatly expands classical logic.
>>
>> In what way does it greatly expand classical logic (by which I take it
>> you mean classical propositional modal logic)? Are some of its
>> tautologies not theorems of S5? (If so, is that a good thing?) If not,
>> and if your claim above is true, your system is semantically equivalent
>> to S5 and simply provides an alternative decision procedure -- on the
>> face of it, one that is exponential and hence computationally harder
>> than the usual S5 decision procedures.
>
> I am happy with the notion of an alternative decision procedure, and
> the theorems are easily handled with a small program in BASIC, (12
> lines for functions of three propositional variables).

Well, yes, it is very easy to program truth tables, but the complexity
of the simplest algorithms for doing so -- likely the one you encode in
your 15 line program -- is exponential, mimicking the exponential growth
in the size of truth tables one sees as one considers wffs containing
more and more propositional variables. This means that the validity of
even relatively simple wffs cannot be determined by means of those
algorithms in a practical amount of time. It is well-known, however,
that the validity problem for S5 is "NP-complete", which, while not
exactly great news from a computational standpoint, does mean that there
are algorithms that can determine validity in S5 much more quickly --
and return answers in a practical amount of time on a far greater range
of wffs -- than can any truth-table algorithm. (Those algorithms, btw,
typically play off of the usual possible world semantics for
propositional modal languages.) So your modal truth table semantics,
while interesting, and perhaps heuristically useful, does not seem to
offer any theoretical advantages over the usual approaches to modal
logic.

From: Confutus on 8 Oct 2006 15:23

Chris Menzel wrote:
> On 6 Oct 2006 04:24:08 -0700, Owen <owenholden(a)rogers.com> said:
> > ...the axioms and theorems of modal propositional logic (eg.S5) are
> > truth functional tautologies.
>
> Do you have a proof of this? (Would seem to be an easy induction on
> length of proof.)
>
> > This logic greatly expands classical logic.
>
> In what way does it greatly expand classical logic (by which I take it
> you mean classical propositional modal logic)? Are some of its
> tautologies not theorems of S5? (If so, is that a good thing?) If not,
> and if your claim above is true, your system is semantically equivalent
> to S5 and simply provides an alternative decision procedure -- on the
> face of it, one that is exponential and hence computationally harder
> than the usual S5 decision procedures.

I might have said the same thing about the 3VL I have proposed. I
can't answer for Owen's system, but since those are good questions,
I'll go ahead and answer for the one I have proposed.

1) I could produce a proof, by means of truth tables, that
equivalents to all the axioms of S5 (and many other modal systems) are
tautologies of S5; and therefore all the theorems of S5 are also
theorems of the 3VL. However, this might be misleading, because it
would be only a formal similarity. The interpretation and behavior of
the various connectives are not consistent with those usually adopted
for modal logic.
2) The 3VL is an extension and expansion of classical 2VL, in that
the theorems of 3VL reduce to those of 2VL in the special case where
the third (middle) truth value is eliminated or escluded. However, some
of them, including many that are considered fundamental and important,
are not true in general. They have to be modified or restricted in some
fashion.
3) Yes, some tautologies of the 3VL are not theorems of S5, so the
two are not semantically equivalent. Hence the differences in
interpretation and behavior.
4) Whether this is a good thing seems to be a subjective question.
There are advantages and disavantages to the 3VL. A comparison of the
different features might be enligthening and instructive.

First | Prev |
Pages: 1 2 3 4 5 6
Prev: Why Has None of Computer Science been Formalized?
Next: On Ultrafinitism