I want to study the semantics of intuitionistic propositional logic.
Fix a topological space $X$, let $\Gamma\models^X A$ denote that $A$ is valid under $\Gamma$ in the algebra of all open sets of $X$.
I want to prove that $\Gamma\vdash A$ is equivalent to $\Gamma\models^X A$ for all finite $X$.
Soundness is easy. To prove completeness, I divide the problem into 2 steps.
First, prove $\Gamma\vdash A$ is equivalent to $\Gamma\models^\mathcal{H} A$ for all finite Heyting algebra $\mathcal{H}$. I think it is equivalent to prove that an element $x$ of a finitely presented Heyting algebra $\mathcal{H}$ is $1$ if it is $1$ in all finite quotient algebras of $\mathcal{H}$(But I don't know how to prove this).
Second, prove that every finite Heyting algebra is the algebra of all open sets of $X$ for some finite topological space $X$. (I can't prove this either).
Please help me solve the two subproblems.
Best Answer
I think you underestimate the difficulty of these completeness proofs. Making them work requires making many non-trivial logical observations, and a fairly sophisticated understanding of order theory as well. Fortunately, Gehrke and Van Gool's recent textbook, Topological Duality for Distributive Lattices: Theory and Applications covers all the order-theoretic prerequisites that one might need. I will sketch the arguments below, but keep in mind that they require some complicated steps, and even these sketches might be missing details that prevent you from reconstructing the full argument.
Part 1
This part is hard. Doing it for an infinite $\Gamma$ is also annoying and verbose, so for the purposes of this proof sketch I assume that your $\Gamma$ is finite.
From soundness, you already know that if you can prove $\Gamma \vdash A$ in intuitionistic logic, then $v\left(\bigwedge \Gamma \rightarrow A\right) = \top$ holds under any valuation $v$ taking values in any Heyting algebra $H$.
Similarly, you can show that whenever $\Gamma \vdash A$ is not provable in intuitionistic logic, you can find an (infinite) Heyting algebra $L$ and an $L$-valuation $v$ so that $v\left(\bigwedge \Gamma \rightarrow A\right) \neq \top$, simply by considering the Lindenbaum–Tarski algebra $L$.
How could we use this $L$ to construct a finite Heyting algebra $H$ and $H$-valuation $v'$ so that $v'\left(\bigwedge \Gamma \rightarrow A\right) \neq \top$?
Well, what if we considered the Heyting algebra generated by the set of all values that we actually use to determine the value of $v\left(\bigwedge \Gamma \rightarrow A\right)$? Unfortunately, that won't work, since generating a Heyting algebra this way will generally result in something infinite. We'll need a few tricks to get around this issues.
The Tricks
Trick 1: even though finitely generated Heyting algebras are usually infinite, finitely generated distributive lattices are in fact always finite. You can prove this by starting with the well-known fact that Boolean algebras over a finite set of generators are finite. Combined with Lemma 4.11 in the textbook above, you get that the free distributive lattice over a finite set of generators is also finite, from which it follows that finitely generated distributive lattices are always finite, as claimed.
Trick 2: every finite distributive lattice $H$ is a Heyting algebra. You can just set
$$a \rightarrow b = \bigvee \{c \in H \:|\: a \wedge c \leq b\}$$
and note that since $H$ is finite, the join on the right is also finite, and distributive lattices are closed under finite joins.
Part 1 cont.
So let's consider the bounded distributive lattice generated by the set of all values that we actually use to determine the value of $v\left(\bigwedge \Gamma \rightarrow A\right)$, i.e. the bounded distributive lattice $H$ generated by the set
$$ \left\{ v(B) \:\mid\: B \in \mathrm{Subformulas}\left(\bigwedge \Gamma \rightarrow A\right) \right\} $$
under all the lattice operations of $L$.
One has to prove that if $a \in H$ and $b \in H$ and $a \rightarrow b \in H$ all hold, then in fact $a \rightarrow b = \bigvee \{c \in H \:|\: a \wedge c \leq b\}$.
This immediately implies that the $L$-valuation $v$ gives rise to a $H$-valutaion $v'$ on which $v'\left(\bigwedge \Gamma \rightarrow A\right) \neq top$. But $H$ is a finitely generated, so by Trick 1 it is finite, and by Trick 2 it is a Heyting algebra.
We have shown that when $\Gamma \vdash A$ is not provable in intuitionistic logic, it fails in some finite Heyting algebra $H$. Conversely, if $v\left(\bigwedge \Gamma \rightarrow A\right) = \top$ in all valuations in finite Heyting algebras, then $\Gamma \vdash A$ is provable.
Part 2
This is known as Birkhoff's representation theorem. You can look up a standard proof, or write your own proof with the same conclusion, e.g. by proving that every finite distributive lattice order-embeds into a finite Boolean algebra $B$ (see also Proposition 1.26 of the textbook above), and using the fact that every finite Boolean algebra is a powerset algebra over some set $S$.