Semantics for Intuitionistic Logic | Attic Philosophy

This is part 2 of Meaning in Intuitionistic Logic. Part 1 is here: • Meaning in Intuitionis...
Intuitionistic logic rejects one of the central building blocks of classical logic: that we can always say 'true or false', A-or-not-A. In this video, we continue looking at what it means, through the Kripke (relational model) semantics.
00:00 - Intro
01:43 - Models
04:11 - Verifying a Sentence
04:21 - Semantic clauses
05:21 - Validity and Entailment
05:41 - Translation into Modal Logic
More videos on intuitionistic logic coming next! If there’s a topic you’d like to see covered, leave me a comment below.
Links:
My academic philosophy page: markjago.net
My book What Truth Is: bit.ly/JagoTruth
Most of my publications are available freely here: philpapers.org/s/Mark%20Jago
Get in touch on Social media!
Instagram: / atticphilosophy
Twitter: / philosophyattic
#logic #philosophy #semantics

[@vitusschafftlein1282]

Thanks for the video! I haven't quite understood why the accessability relation does not need to be antisymmetric. How do you make sure you can only go forth and not go backward without this condition? As far as I see it, K4 allows that there is an arrow from S1 to S2 and the other way arround. It seems to me that the interpretation of these models being like an investigation starts crumbling without antisymmetry because it somehow involves the aspect of time, and time is asymmetric - so even irreflexive, which would contradict a K4 model. But maybe I have not understood something important.

[@AtticPhilosophy]

Great question! We can distinguish the official logical definition of a model, which allows for 2-way arrows, from the intuitive gloss as 'stages of an investigation', which hints that it should go in just one direction. But luckily, there's a little trick that helps align these: any time we have a (modal or intuitionistic) model that isn't a tree, we can 'unwind' it into a tree. Using this trick, a two-way arrow x y becomes a sequence:
x1 --> y1 --> x2 --> y2 -->
And, it turns out that modal or intuitionistic logic can't tell the difference between these, 'from the inside'. So we can always take an intuitionistic model with 2-way arrows and turn it into a tree, which then looks like the intuitive 'stages of an investigation'.

[@vitusschafftlein1282]

​@@AtticPhilosophy Thanks for your answer! I think I'm starting to get it. I have some questions of clarification:
1) Is the main idea, then, that for any model M containing a symmetric instance xy, there is a model M' not containing one but in which all truth-values of for any formula at any world of M are the same?
2) Are x1 and x2, for example, distinct states or the same? It seems to me that they must be distinct. From that would follow that the set of worlds of M must then be a proper subset of the worlds of M', and that M and M' are not isomorphic. If this was the case, it would be interesting to see why the two models cannot be distinguised within modal semantics.
3) Why don't you get problems with the heredetary constraint with this procedure? If xy, then x and y have the same formulas true (and false, because here we are in classical logic). But it seems to me that the sequence above does not guarantee that. Or does that not matter because there will always be some model in which x and y have the same formulas true and false, and you would just pick that particular one for the tree model?
4) Why does the sequence not need to be infinite? A real symmetric instance has some kind of circular property to it: You get from one to the other, from the other to the one again, and won't ever stop.

[@redbook7347]

A formula is valid in a model iff. the formula is valid at each state in the model. Is that correct? If so, does it follow that the only models which will validate a formula are the ones which are built on this investigative idea, i.e. the ones where if p is true at state s_0 then it is true are all future (accessible) states s_k?

[@AtticPhilosophy]

Would usually say ‘true in a model’, reserving validity for truth in all models. But yes, Kripke models for intuitionistic logic are restricted so that atomic sentences true at a state are true at all accessible states.