Any /sci/tizens 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?
>>8202189
>/sci/tizens
Please no.
>>8202216
I'm familiar with semantic tableaux, but not getzen proofs.
>>8202242
Well, I haven't figured out how to write modal formulae on 4chan, 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?
>>8202267
Delete this.
>>8202251
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).
>>8202274
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?
>>8202278
Honestly, I never bothered memorizing those identities, and just did the truth tables...
>>8202278
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.
>>8202278
>>8202290
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.
>>8202292
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.
>>8202299
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.
>>8202267
it's true
>>8202189
OP why the hell did you just post a pic of my dad?
>>8202533
checked
>>8202307
truth values are the most retarded concept ever created by himans
Logos bump
>>8204555
what is a getzen proof desu?
>>8204584
Can nothing be proven?
>>8204584
a waste of time. stick to circuits.
