Showing every state in an intuitionistic model verifies ¬¬p → p

47 Views Asked by At

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:

  1. s ⊧ A ∨ B = + iff s ⊧ A = + or s ⊧ B = +
  2. s ⊧ ¬A = + iff t ⊧ A = – for all t such that Rst
  3. 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!