I'm working on a question in the field of intuitionistic logic:
In an intuitionistic model, assume p ∨ ¬p is verified at the root state. Give a brief argument showing that every state in the model verifies ¬¬p → p. (You will need to exploit the semantic clauses for ∨, ¬, and →.)
The semantic clauses are these:
- s ⊧ A ∨ B = + iff s ⊧ A = + or s ⊧ B = +
- s ⊧ ¬A = + iff t ⊧ A = – for all t such that Rst
- s ⊧ A → B = + iff, for all t such that Rst, either t ⊧ A = – or t ⊧ B = +
but I don't have a clue how to turn that into an argument. If anyone can help I'd be really grateful. Thank you!