Modal Logic

Any Veeky Forumstizens familiar with modal logic?

In particular Kripke models, and Systems K, KT, S4, and S5.

I think I have figured out most of it, but I still have some questions about the whole ordeal.

I took a class in it. What are your questions?

>Veeky Forumstizens
Please no.

Sorry for the late reply.

Are you familiar with Getzen Proofs or Beth Tableauxs?

Sorry.

I'm familiar with semantic tableaux, but not getzen proofs.

Well, I haven't figured out how to write modal formulae on Veeky Forums, so I'll just improvise.

Question: am I correct in assuming that in KT, the following tableaux is correct:

To analyse #( #P -> #( Q -> P ) ), where # is the box, or 'necessary', I pose it as a false conclusion and deduce whether or not the tableaux closes. If it does, the conclusion is valid, if it doesn't I've found a counter example as well.

So:

F #( #P -> #( Q -> P ) )
F #P -> #( Q -> P )
T #P , F#( Q -> P )
-------------------------
TP, FQ -> P
TP, TQ, FP

Contradiction between TP and FP, so #( #P -> #( Q -> P ) ) is indeed valid.

Question 2: am I correct in assuming that in S4 the same proposition is also valid:

Again we pose the thing as a false conclusion and work our way down:

F #( #P -> #( Q -> P ) )
F #P -> #( Q -> P )
T #P , F#( Q -> P )
-------------------------
T #P, FQ -> P
T #P, TQ, FP
TP, TQ, FP

The difference being in line 4: in KT we immediately have TP as first premise, and in S4 we keep T#P.

This difference is my what my key question is about: Have I understood this difference correctly?

What do you think?

Delete this.

Haven't done this stuff in a while, but I think that looks okay (the way I learned semantic tableaux did not look anything like what you're writing).

However to actually appreciate and understand the difference, I think you gain the best intuition through correspondence with graph theory, as well as looking at various philosophical problems and their formulations within the different logics (with different interpretations of box and diamond--epistemical is particularly fun).

Yeah I know. Philosophy is exactly what this is for, and We're doing 'em all: Temporal, Deontic, Epistemic, you name it.

Can you perhaps elaborate the way you learned tableux?

Honestly, I never bothered memorizing those identities, and just did the truth tables...

Hmm, actually, T is part of S4 right? So why couldn't you have the first proof for both?

I'll try to post a picture of my old homework. Although I'm sure it's just a superficial difference.

...

Yes, the first proof sufficed, as T is indeed part of S4 (well caught). But my question is about the difference between the two, particularly on line 4 of the tableaux.

Oh I see! That is what we call a search-table, where you take a reasoning and expand as much as you can into possible worlds, and mark them as (in)valid or ad infinitum.

What I'm doing is a twist on that. I'm saying (or rather I'm being taught, but you know what I mean) that for a reasoning to be valid, we can simply state the premises as T (if there are any) and the conclusion als F, and then see if this holds.

If the "This reasoning is false" turns out to lead to contradictions, you've done your job already! This saves you a lot of potential expanding and trial and error that your method risks.

TL;DR: You trial and error to find valid and invalid worlds, whereas I can stop as soon as I find a counterexample.

Bit difficult to explain, but really simple pinciple.

In the case of that image, I would start by putting the whole thing into brackets and marking it as F, and take it from there.

Eh, I wouldn't characterize the second proof of being "the essence of S4." If you want to do that it's probably better to consider something that is true in S4 but not in KT.

it's true

OP why the hell did you just post a pic of my dad?

checked

truth values are the most retarded concept ever created by himans

Logos bump

what is a getzen proof desu?

Can nothing be proven?

a waste of time. stick to circuits.