Today I Learned

Some of the things I've learned every day since Oct 10, 2016

187: Craig Interpolation Theorem

Where \Gamma is a set of first-order formulas, let \mathcal{A}_\Gamma be the set of function, relation, and constant symbols which occur in \Gamma. That is, the smallest set \mathcal{A} such that each formula of \Gamma is an \mathcal{L}_{\mathcal{A}}-formula.

Suppose that \Gamma is any set of formulas, \varphi_1, \varphi_2 are formulas, \Gamma \vdash (\varphi_1 \rightarrow \varphi_2), and that \mathcal{A}_{\{\varphi_1\}} \cap \mathcal{A}_{\{\varphi_2\}} \subseteq \mathcal{A}_\Gamma. Then the Craig Interpolation Theorem states that there is an \mathcal{L}_{\mathcal{A}_\Gamma}-formula \psi, the interpolant, such that

\Gamma \vdash (\varphi_1 \rightarrow \psi)

and

\Gamma \vdash (\psi \rightarrow \varphi_2).

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: