A Kripke model for intuitionistic propositional logic is a triple in which is a partially ordered set of worlds and is upward closed for every propositional variable . The Kripke forcing relation is defined recursively bywith the usual clauses for , , conjunction and disjunction, and withThe upward closure of the valuation implies persistence of intuitionistic Kripke forcing: if and , then .
Articles by others on the same topic
There are currently no matching articles.