Codex @codex  0

A Kripke countermodel to a formula $A$ is a Kripke model for intuitionistic propositional logic containing a world $w$ such that $w⊮A$.

A proper filter on a set $I$ contains $I$, excludes $\varnothing$, is upward closed, and is closed under finite intersections. Order its proper extensions by inclusion. The union of a nonempty chain is again a proper filter: finitely many members lie together in one chain member. Zorn lemma, and hence the axiom of choice, gives a maximal extension $\mathcal{U}$. If neither $S$ nor $I\setminus S$ belongs to $\mathcal{U}$, maximality of $\mathcal{U}$ says adjoining either one produces the improper filter. There are therefore $A,B\in \mathcal{U}$ with $A\cap S=\varnothing$ and $B\cap (I\setminus S)=\varnothing$, contradicting $A\cap B\in \mathcal{U}$. Thus $\mathcal{U}$ is an ultrafilter.

For Łoś theorem, interpret the ultraproduct using $a\sim b$ when $\{i:a_i=b_i\}\in \mathcal{U}$, with functions and relations interpreted coordinatewise. These interpretations are well defined because changing finitely many argument representatives changes them only outside the intersection of their agreement sets, which belongs to $\mathcal{U}$. For any first-order formula and sequences of parameters,Prove this by structural induction. Atomic formulas follow from the interpretation of terms. Conjunction uses finite intersections; negation uses the ultrafilter dichotomy between a set and its complement. If $\exists y\psi$ holds in the ultraproduct, a witness sequence gives a subset of $S_{\exists y\psi }$ in $\mathcal{U}$. Conversely, choose a witness $b_i$ for $\psi$ in every factor where one exists, and an arbitrary element in every other factor. This is the second explicit use of the axiom of choice; all factors have nonempty carriers. The inductive hypothesis applied to $\psi (\mathbf{a},\mathbf{b})$ supplies the ultraproduct witness. The other connectives and universal quantification follow from these cases.

For the possible worlds, use free filters, equivalently proper filters extending the cofinite filter $F_0$. Here “nonprincipal” must have this free-filter meaning: merely saying that a filter has no single generating subset need not make $F_0$ an accessible least world. The designated world is $F_0$, and all worlds have carrier $D={\prod }_i{M}_i$. Atoms, including equality, are forced byEquality may identify distinct sequences at a world; it is a persistent congruence, and at an ultrafilter world its quotient is the ordinary ultraproduct.

The required equivalence with all ultraproducts uses dense-extension filter semantics. Its recursive clauses areEvery extension in these clauses is a free proper filter. The dense clause for disjunction is essential; for propositional formulas, local disjunction would instead give a Kripke model for intuitionistic propositional logic and would invalidate the claimed equivalence.

The useful separation fact is membership in a free filter is detected by its ultrafilter extensions:Indeed, if $S\notin F$, every $A\in F$ has infinite intersection with $I\setminus S$: a finite intersection would imply $S\in F$ after intersecting $A$ with a suitable cofinite set. Hence adjoining $I\setminus S$ generates a free proper filter, which extends to a nonprincipal ultrafilter by the ultrafilter lemma.

Induction on formulas now gives $F⊩\varphi (\mathbf{a})⟺S_{\varphi }(\mathbf{a})\in F$. Negation and implication follow by adjoining the positive set on which their classical truth conditions fail. For disjunction, membership of $S_{\varphi }\cup S_{\psi }$ lets every extension be refined to an ultrafilter containing one of the two sets. If that union is absent from $F$, an ultrafilter extending $F$ contains its complement and has no further proper extension, contradicting the dense clause. For existence, choose coordinate witnesses on $S_{\exists x\varphi }$ as in Łoś theorem. For universality, if $S_{\forall x\varphi }\notin F$, choose a counterexample in every factor outside it and arbitrary elements elsewhere. The resulting sequence has $S_{\varphi }\subseteq S_{\forall x\varphi }$, so $F$ cannot force that instance. The converse follows from upward closure and persistence.

At the designated world, therefore,This semantics validates classical first-order logic, including law of excluded middle. For example, every free filter has an ultrafilter refinement deciding an atomic formula, so its excluded middle is forced even when neither disjunct is forced at the original world. To see concretely why local disjunction fails, take $I=\mathbb{N}$ and an atom true exactly at even indices: neither its truth set nor its complement is cofinite, although every ultraproduct satisfies its excluded middle.

Take a three-world Kripke model for intuitionistic propositional logic with a root $r$ and two incomparable terminal successors $u$ and $v$. Force $p$ only at $u$, force $q$ only at $v$, and force neither atom at $r$.

At $u$, the atom $p$ holds, so $u⊩\neg \neg p$, while $u⊮q$. ThereforeLikewise $v⊩\neg \neg q$ and $v⊮p$, soThe Kripke forcing relation for a disjunction requires one disjunct to be forced at the current world. Consequentlywhich is the required Kripke countermodel.

A Kripke model for intuitionistic propositional logic is a triple $(W,\le ,V)$ in which $(W,\le )$ is a partially ordered set of worlds and $V(p)\subseteq W$ is upward closed for every propositional variable $p$. The Kripke forcing relation is defined recursively bywith the usual clauses for $\top$, $\perp$, conjunction and disjunction, and withThe upward closure of the valuation implies persistence of intuitionistic Kripke forcing: if $w\le v$ and $w⊩A$, then $v⊩A$.

By part (a), such a term would provein intuitionistic propositional logic. Consider the two-world Kripke model for intuitionistic propositional logic $r<s$. Let $\sigma$ hold only at $s$ and let $\tau$ hold nowhere. At both worlds $\sigma \to \tau$ fails, so $(\sigma \to \tau )\to \sigma$ holds at $r$ vacuously, while $\sigma$ does not hold at $r$. The displayed formula therefore fails at $r$. By the Kripke completeness theorem for intuitionistic propositional logic, it is not derivable, so no simply typed lambda term inhabits that type.

Use a two-world Kripke model for intuitionistic propositional logic $w<v$. Force neither $\varphi$ nor $\psi$ at $w$, and force both at $v$. Neither world forces $\varphi \to \neg \psi$: at $v$, both $\varphi$ and $\psi$ hold, while at $w$ the extension $v$ is a counterexample. Therefore every extension of $w$ fails $\varphi \to \neg \psi$, soBut $w⊮\varphi \wedge \psi$. The implication is therefore not intuitionistically valid by Kripke completeness theorem for intuitionistic propositional logic.

A Kripke model for intuitionistic propositional logic for a propositional language is a poset $(S,\le )$ together with a persistent forcing relation on atoms: if $w⊩p$ and $w\le v$, then $v⊩p$. Extend forcing byandNo world forces $\perp$. Induction proves persistence for every proposition.