In the explanations of intuitionistic logic I've been reading (1, 2, 3), especially in the explanation of the semantics, I don't understand how a proposition being false influences the situation.
These explanations say something like "$W \Vdash p$ iff $p$ is true in $W$". That sounds clear enough, and then they continue and define the other operators. What I don't get is, when $W \not\Vdash p$? In source 3 they later show some diagrams where actually in every world each proposition has a truth value, either 0 or 1, so in that case I guess when $W(p) = 0$ then $W \not\Vdash p$. I feel like, for this to be the case, the explanation should have contained a short line saying, $\Vdash$ is the minimal relation following these definitions, otherwise it would be allowed to have $W \Vdash p$ even though $W(p) = 0$.
However 1 makes me doubt my interpretation for 3, as it contains the following:
you can think of intuitionistic logic as a logic where at a given point of time, a statement can have three truth values: T (top), which means provably true; ⏊ (bottom) which means provably false, and unproved
Following this line of reasoning, whenever $p$ is unproved, you can have neither $\Vdash$ nor $\not\Vdash$. But I feel this would make the definition of negation in 3 useless...? As a computer scientist with only a passing knowledge of formal logic, this is were my brain sputters to a halt.
My questions:
Is the explanation in 3 correct in that in a given world, a $p$ is either assigned $0$ or $1$?(This is the case, as stated on slide 27.)- Is it a safe way to model intuitionistic logic, or does it exclude true statements/proofs that the description in 1 would allow?
- What is the canonical source I can read for a a semantics for inuitionistic propositional logic that is broadly accepted as standard (or, at least has some degree of consensus around it)?
(As a side note: 1 seems to skip defining negation for formulas, is that just an oversight or could 3 have skipped defining it, as it is implied by the other definitions?)
Thanks for any explanatations or tips for other reading material!
You say
This isn’t correct. Consider the Law of the Excluded Middle $A \lor \neg A$. Intuitionistic Logic doesn’t have to have this formula satisfied at an arbitrary world, but that doesn’t mean it has to be false in every world in a given model. That of course would be inconsistent, since Intuitionism proves the double-negated version.
In particular, there is a difference between
$w \not \Vdash p$
and
$w \Vdash \neg p$
as the latter means $v \not \Vdash p$ whenever $w \le v$, while the former simply means the value of $p$ is $0$ at $w$.