I have a question about the negation case and the implication case. So, you assume that something (B in the negation case, and A, not-B in the implication case) is the case in some further world. Then you show that it leads to a contradiction, so not-B and A->B hold in any further world. It is classical reasoning, right? Is it in this particular case intuitionistically valid? If not, then could you also explain this proof in intuitionistic meta-theory?
Yes it’s classical reasoning. That’s usual for kripke models which are basically classical. So full intuitionists won’t accept this reasoning, but they won’t accept the semantics either. For the negation case, you can reason intuitionistically, assuming p is there higher up & getting a contradiction, inferring ~p.
@@CatTheKomrade One way you can look at it alternatively is by considering the modality (i.e. the box he talked about), and show that p -> box p implies the corresponding statement for the rest.
What do you think of this proof? Any questions about how it works? Leave me a comment below!
Would love to hear&watch more about different logics as well: bunched, separation, calculus of structures, deep inference!..
A bit niche!
I have a question about the negation case and the implication case. So, you assume that something (B in the negation case, and A, not-B in the implication case) is the case in some further world. Then you show that it leads to a contradiction, so not-B and A->B hold in any further world. It is classical reasoning, right? Is it in this particular case intuitionistically valid? If not, then could you also explain this proof in intuitionistic meta-theory?
Yes it’s classical reasoning. That’s usual for kripke models which are basically classical. So full intuitionists won’t accept this reasoning, but they won’t accept the semantics either. For the negation case, you can reason intuitionistically, assuming p is there higher up & getting a contradiction, inferring ~p.
@@AtticPhilosophy Thanks, Mark!
@@CatTheKomrade One way you can look at it alternatively is by considering the modality (i.e. the box he talked about), and show that p -> box p implies the corresponding statement for the rest.