The notion of model of intuitionistic propositional logic (IPL) I'm

most familiar with (being a category theory/PL nerd) is a Heyting

algebra (HA): a poset with finite meets, finite joins and a Heyting

implication. If you add propositional variables, the model includes a

choice of how to interpret them as elements of the HA and if you

include axioms, their interpretation must be true in the HA.

Then you can interpret every proposition of IPL as an element of the

HA where you interpret conjunctions as meets, disjunctions as joins

and implication as the Heyting implication. If G |- A is provable then

/\ [G] |- [A] is true.

If you look up what a model of IPL is though, you'll likely find

Kripke models, and they look at first a bit different: It's a pair of

a poset W, and a "forcing relation" ||- between elements of W and

propositions of IPL satisfying a bunch of properties:

1. for variables x, if w ||- x and v <= w then v ||- x

2. w ||- p /\ q iff w ||- p and w ||- q

3. w ||- true is true

4. w ||- p \/ q iff w ||- p or w ||- q

5. w ||- false is false

6. w ||- p => q iff for any v <= w if v ||- p then v ||- q

Despite the cosmetic difference, Kripke models are instances of the HA

model construction. Given a poset W, the HA in question is

Prop^(W^op), the poset of antitone functions from W to Prop

(classically, Prop is just the boolean order 0 <= 1). This has the

pointwise ordering: f <= g if for every w. f w implies g w.

This is a Heyting Algebra:

top w iff true

(f /\ g) w iff f w and g w

bot w iff false

(f \/ g) w iff f w or g w

(f => g) w iff for any v <= w. if f w then g w

Then an interpretation of the propositional variables in this HA would

be an assignment for each variable X and w a proposition [x] w that is

antitone in w: if [x] w and v <= w then [x] v. Then the model HA

interpretation defines exactly our Kripke forcing semantics. It

defines for each proposition of IPL p a function from W to Prop that

is antitone, i.e., [p] : W^op -> Prop. Then the definition of Kripke

model is just an infix notation for this semantics:

w ||- p := [p] w

And if you unravel the definitions of the HA semantics and the HA

structure of the poset, you reproduce exactly the definition of a

Kripke model.

Bonus: this is all a "de-categorification" of a similar situation for

lambda calculus. The Kripke models are presheaf categories and the HA

are bi-cartesian closed categories.