Model theory

The Interpolation Theorem

Equation form expr-001a19c11f75144e

Γ∪{∃xS,S[c/x]}\Gamma \cup \{ \lexists[x][!S], \Subst{!S}{c}{x} \}

Read as: Gamma union there exists x, S comma S with c substituted for x

Means: A set of sentences or stage in the inseparability construction in the separation and inseparability lemmas; it reads: Gamma union there exists x, S comma S with c substituted for x.

2 occurrences in this chapter

Equation form expr-0274d950e7848a1a

Δ0⊆Σ(P)\Delta_0 \subseteq \Sigma(P)

Read as: Delta sub zero is a subset of Sigma open parenthesis P close parenthesis

Means: Language or theory notation controlling the available nonlogical vocabulary in the Beth definability application; it reads: Delta sub zero is a subset of Sigma open parenthesis P close parenthesis.

1 occurrence in this chapter

Equation form expr-03569cbd604e9e67

Γ*\Gamma^*

Read as: Gamma superscript star

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma superscript star.

9 occurrences in this chapter

Equation form expr-047b13fc58fbe4a8

S∈Γ*∩Δ*!S \in \Gamma^* \cap \Delta^*

Read as: S is in Gamma superscript star intersect Delta superscript star

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: S is in Gamma superscript star intersect Delta superscript star.

1 occurrence in this chapter

Equation form expr-08edb68f6224f961

Δ0∪Δ1⊨P(c1,…,cn)→P′(c1,…,cn).\Delta_0 \cup \Delta_1 \Entails \Atom{P}{c_1, \dots, c_n} \to \Atom{P'}{c_1, \dots, c_n}.

Read as: Delta sub zero union Delta sub one entails predicate P applied to c sub one comma and so on comma c sub n to predicate P prime applied to c sub one comma and so on comma c sub n

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: Delta sub zero union Delta sub one entails predicate P applied to c sub one comma and so on comma c sub n to predicate P prime applied to c sub one comma and so on comma c sub n.

1 occurrence in this chapter

Equation form expr-0aacc059180baf84

D(P)⊨P(c1,…,cn)↔C(c1,…,cn)!D(P) \Entails \Atom{P}{c_1,\dots, c_n} \liff !C(c_1, \dots, c_n)

Read as: D open parenthesis P close parenthesis entails predicate P applied to c sub one comma and so on comma c sub n if and only if C open parenthesis c sub one comma and so on comma c sub n close parenthesis

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: D open parenthesis P close parenthesis entails predicate P applied to c sub one comma and so on comma c sub n if and only if C open parenthesis c sub one comma and so on comma c sub n close parenthesis.

1 occurrence in this chapter

Equation form expr-0b7c6b7fbef95a24

Δ⊨¬C\Delta \Entails \lnot !C

Read as: Delta entails not C

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: Delta entails not C.

1 occurrence in this chapter

Equation form expr-0c7b840d8c01f194

A2!A_2

Read as: formula A sub two

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: formula A sub two.

1 occurrence in this chapter

Equation form expr-0dce7dbe422ec083

L∪{P}\Lang{L} \cup \{P\}

Read as: language L union P

Means: Language or theory notation controlling the available nonlogical vocabulary in the Beth definability application; it reads: language L union P.

4 occurrences in this chapter

Equation form expr-0e171722a1e9b2a6

S[c/x]\Subst{!S}{c}{x}

Read as: S with c substituted for x

Means: A formula, quantified sentence, atomic formula, or substitution in the separation and inseparability lemmas and the maximally inseparable pair proof of Craig interpolation; it reads: S with c substituted for x.

3 occurrences in this chapter

Equation form expr-0e5677e25a3f86bf

|M2|\Domain{M_2}

Read as: the domain of structure M sub two

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: the domain of structure M sub two.

1 occurrence in this chapter

Equation form expr-0eed798fb1fc6702

⊨A→C\Entails !A \lif !C

Read as: entails formula A implies C

Means: The validity claim that A materially implies the interpolant C.

2 occurrences in this chapter

Equation form expr-0f64fbd2c1ebffd8

L0=L1∩L2\Lang{L}_0 = \Lang{L}_1 \cap \Lang{L}_2

Read as: language L sub zero equals language L sub one intersect language L sub two

Means: The common language L zero is the intersection of the languages of A and B.

1 occurrence in this chapter

Equation form expr-0fa568f0fe9c7bfb

C(x1,…,xn)!C(x_1, \dots, x_n)

Read as: C open parenthesis x sub one comma and so on comma x sub n close parenthesis

Means: A formula, quantified sentence, atomic formula, or substitution in the Beth definability application; it reads: C open parenthesis x sub one comma and so on comma x sub n close parenthesis.

1 occurrence in this chapter

Equation form expr-0fa9e2b8532f543c

Δ⊨¬C[c/x]\Delta \Entails \lnot \Subst{!C}{c}{x}

Read as: Delta entails not C with c substituted for x

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: Delta entails not C with c substituted for x.

2 occurrences in this chapter

Equation form expr-108d48ae1446aed4

An∉Γ*!A_n \notin \Gamma^*

Read as: formula A sub n is not in Gamma superscript star

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: formula A sub n is not in Gamma superscript star.

2 occurrences in this chapter

Equation form expr-13bcf9d25c75255b

G!G

Read as: G

Means: Model-theoretic notation in the separation and inseparability lemmas; it reads: G.

1 occurrence in this chapter

Equation form expr-13e7feb26825d836

M[R]⊨A(P′)\Expan{M}{R} \models !A(P')

Read as: the expansion of structure M by relation R satisfies formula A open parenthesis P prime close parenthesis

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: the expansion of structure M by relation R satisfies formula A open parenthesis P prime close parenthesis.

1 occurrence in this chapter

Equation form expr-13e89f87f3852cb4

PM=PM'2\Assign{P}{M} = \Assign{P}{M'_2}

Read as: the interpretation of P in structure M equals the interpretation of P in structure M prime sub two

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: the interpretation of P in structure M equals the interpretation of P in structure M prime sub two.

1 occurrence in this chapter

Equation form expr-14e731fdbeefbc7d

M⊨Γ*∪Δ*\Struct{M} \Entails \Gamma^* \cup \Delta^*

Read as: structure M entails Gamma superscript star union Delta superscript star

Means: A semantic consequence or satisfaction claim in the maximally inseparable pair proof of Craig interpolation; it reads: structure M entails Gamma superscript star union Delta superscript star.

1 occurrence in this chapter

Equation form expr-1a97e063166f2cca

M2\Struct{M_2}

Read as: structure M sub two

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: structure M sub two.

1 occurrence in this chapter

Equation form expr-1aa3c91aedbf373f

({A},{¬B})(\{ !A \}, \{\lnot!B\})

Read as: open parenthesis formula A comma not formula B close parenthesis

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: open parenthesis formula A comma not formula B close parenthesis.

1 occurrence in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: Model-theoretic notation in the maximally inseparable pair proof of Craig interpolation and the Beth definability application; it reads: n.

4 occurrences in this chapter

Equation form expr-1c9b8b8575386603

⊨A→B\Entails !A \lif !B

Read as: entails formula A implies formula B

Means: The validity claim that A materially implies B.

2 occurrences in this chapter

Equation form expr-1e7a89cb5b8f4616

Γ0∪{A0}\Gamma_0 \cup \{!A_0 \}

Read as: Gamma sub zero union formula A sub zero

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma sub zero union formula A sub zero.

1 occurrence in this chapter

Equation form expr-1eda360ce9cb345d

C′∈L'0!C' \in \Lang{L}'_0

Read as: C prime is in language L prime sub zero

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: C prime is in language L prime sub zero.

1 occurrence in this chapter

Equation form expr-20e66ff551014a2f

Δ0={¬B}\Delta_0 = \{\lnot !B \}

Read as: Delta sub zero equals not formula B

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Delta sub zero equals not formula B.

1 occurrence in this chapter

Equation form expr-215f134cf6909e24

Δ*\Delta^*

Read as: Delta superscript star

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Delta superscript star.

10 occurrences in this chapter

Equation form expr-239d028c4a3c2539

⊨C→B\Entails !C \lif !B

Read as: entails C implies formula B

Means: The validity claim that the interpolant C materially implies B.

2 occurrences in this chapter

Equation form expr-247854112dc50082

L2\Lang{L}_2

Read as: language L sub two

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L sub two.

2 occurrences in this chapter

Equation form expr-25c5ad037040251f

Γn\Gamma_n

Read as: Gamma sub n

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma sub n.

3 occurrences in this chapter

Equation form expr-272d7ff70b2d7fe0

Γn+2\Gamma_{n+2}

Read as: Gamma sub n plus two

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma sub n plus two.

1 occurrence in this chapter

Equation form expr-27a5391036f32374

Γ∪{∃xS}\Gamma \cup \{\lexists[x][!S] \}

Read as: Gamma union there exists x, S

Means: A set of sentences or stage in the inseparability construction in the separation and inseparability lemmas; it reads: Gamma union there exists x, S.

2 occurrences in this chapter

Equation form expr-28644efbda936225

L1\Lang{L}_1

Read as: language L sub one

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L sub one.

2 occurrences in this chapter

Equation form expr-28aca943bd52677b

D(P)∧P(c1,…,cn)⊨C(c1,…,cn);C(c1,…,cn)⊨D(P′)→P′(c1,…,cn).!D(P) \land \Atom{P}{c_1, \dots, c_n} & \Entails !C(c_1,\dots, c_n); \\ !C(c_1,\dots, c_n) & \Entails !D(P') \to \Atom{P'}{c_1, \dots, c_n}.

Read as: D open parenthesis P close parenthesis and predicate P applied to c sub one comma and so on comma c sub n then entails C open parenthesis c sub one comma and so on comma c sub n close parenthesis semicolon next row C open parenthesis c sub one comma and so on comma c sub n close parenthesis then entails D open parenthesis P prime close parenthesis to predicate P prime applied to c sub one comma and so on comma c sub n

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: D open parenthesis P close parenthesis and predicate P applied to c sub one comma and so on comma c sub n then entails C open parenthesis c sub one comma and so on comma c sub n close parenthesis semicolon next row C open parenthesis c sub one comma and so on comma c sub n close parenthesis then entails D open parenthesis P prime close parenthesis to predicate P prime applied to c sub one comma and so on comma c sub n.

1 occurrence in this chapter

Equation form expr-2a07931c2f2237d4

Σ(P)∪Σ(P′)⊨P(c1,…,cn)→P′(c1,…,cn).\Sigma(P) \cup \Sigma(P') \Entails \Atom{P}{c_1, \dots, c_n} \to \Atom{P'}{c_1, \dots, c_n}.

Read as: Sigma open parenthesis P close parenthesis union Sigma open parenthesis P prime close parenthesis entails predicate P applied to c sub one comma and so on comma c sub n to predicate P prime applied to c sub one comma and so on comma c sub n

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: Sigma open parenthesis P close parenthesis union Sigma open parenthesis P prime close parenthesis entails predicate P applied to c sub one comma and so on comma c sub n to predicate P prime applied to c sub one comma and so on comma c sub n.

1 occurrence in this chapter

Equation form expr-2c8af962d37db1a4

Γ⊨C[c/x]\Gamma \Entails \Subst{!C}{c}{x}

Read as: Gamma entails C with c substituted for x

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: Gamma entails C with c substituted for x.

1 occurrence in this chapter

Equation form expr-2ceb4df5993cba2b

c1c_1

Read as: c sub one

Means: Model-theoretic notation in the Beth definability application; it reads: c sub one.

1 occurrence in this chapter

Equation form expr-2e7779fa7fff3abd

S!S

Read as: S

Means: A formula, quantified sentence, atomic formula, or substitution in the separation and inseparability lemmas and the maximally inseparable pair proof of Craig interpolation; it reads: S.

2 occurrences in this chapter

Equation form expr-2e7d2c03a9507ae2

cc

Read as: c

Means: Model-theoretic notation in the separation and inseparability lemmas and the maximally inseparable pair proof of Craig interpolation; it reads: c.

6 occurrences in this chapter

Equation form expr-2e895f588d875820

Δ1⊆Σ(P′)\Delta_1 \subseteq \Sigma(P')

Read as: Delta sub one is a subset of Sigma open parenthesis P prime close parenthesis

Means: Language or theory notation controlling the available nonlogical vocabulary in the Beth definability application; it reads: Delta sub one is a subset of Sigma open parenthesis P prime close parenthesis.

1 occurrence in this chapter

Equation form expr-2ee6ad177415fab3

Γ⊨∀xC,Δ⊨¬∀xC,\Gamma &\Entails \lforall[x][!C], & \Delta & \Entails \lnot \lforall[x][!C],

Read as: Gamma then entails for every x, C comma then Delta then entails not for every x, C

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: Gamma then entails for every x, C comma then Delta then entails not for every x, C.

1 occurrence in this chapter

Equation form expr-303621d6e6c22393

∀xx=x\lforall[x][\eq[x][x]]

Read as: for every x, x equals x

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: for every x, x equals x.

1 occurrence in this chapter

Equation form expr-30d443ceda587baa

cM'2\Assign{c}{M'_2}

Read as: the interpretation of c in structure M prime sub two

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: the interpretation of c in structure M prime sub two.

2 occurrences in this chapter

Equation form expr-31067f14cdc5b4c8

R,R′⊆|M|nR, R' \subseteq \Domain{M}^n

Read as: R comma R prime is a subset of the domain of structure M superscript n

Means: A structure, domain, isomorphism, or interpretation claim in the Beth definability application; it reads: R comma R prime is a subset of the domain of structure M superscript n.

1 occurrence in this chapter

Equation form expr-314f6a0adf231dd2

∀xC⊨¬H\lforall[x][!C] \Entails \lnot !H

Read as: for every x, C entails not H

Means: After the disclosed source correction, the universal closure of C entails not H.

1 occurrence in this chapter

Equation form expr-3166cb335d8409db

L1∪L2\Lang{L_1} \cup \Lang{L_2}

Read as: language L sub one union language L sub two

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L sub one union language L sub two.

1 occurrence in this chapter

Equation form expr-333210158dc356a8

S∈Δ*!S \in \Delta^*

Read as: S is in Delta superscript star

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: S is in Delta superscript star.

2 occurrences in this chapter

Equation form expr-33a9c96304bcc292

|M|\Domain{M}

Read as: the domain of structure M

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: the domain of structure M.

1 occurrence in this chapter

Equation form expr-341d96cde465b372

B2!B_2

Read as: formula B sub two

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: formula B sub two.

1 occurrence in this chapter

Equation form expr-35a23a05b1bc4ac4

P(c)∈Γ*\Atom{P}{c} \in \Gamma^*

Read as: predicate P applied to c is in Gamma superscript star

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: predicate P applied to c is in Gamma superscript star.

1 occurrence in this chapter

Equation form expr-35e8d6d071910243

Γ0={A}\Gamma_0 = \{ !A\}

Read as: Gamma sub zero equals formula A

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma sub zero equals formula A.

1 occurrence in this chapter

Equation form expr-37cf6f6941a312ec

∃xx≠x\lexists[x][\eq/[x][x]]

Read as: there exists x, x is not equal to x

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: there exists x, x is not equal to x.

2 occurrences in this chapter

Equation form expr-3c4ef0aacdfa379b

M'1\Struct{M'_1}

Read as: structure M prime sub one

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: structure M prime sub one.

2 occurrences in this chapter

Equation form expr-3e3f9c59f893e011

Γ*⊨C∨C′\Gamma^* \Entails !C \lor !C'

Read as: Gamma superscript star entails C or C prime

Means: A semantic consequence or satisfaction claim in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma superscript star entails C or C prime.

1 occurrence in this chapter

Equation form expr-42b8f19ae63d24a4

M\Struct{M}

Read as: structure M

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation and the Beth definability application; it reads: structure M.

3 occurrences in this chapter

Equation form expr-43dfdbdb9cb8bc3b

Γn∪{An}\Gamma_n \cup \{!A_n \}

Read as: Gamma sub n union formula A sub n

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma sub n union formula A sub n.

2 occurrences in this chapter

Equation form expr-44db13dc997ac3df

Δn∪{Bn}\Delta_n \cup \{!B_n \}

Read as: Delta sub n union formula B sub n

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Delta sub n union formula B sub n.

1 occurrence in this chapter

Equation form expr-4680167a13b280c9

¬An∉Γ*\lnot !A_n \notin \Gamma^*

Read as: not formula A sub n is not in Gamma superscript star

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: not formula A sub n is not in Gamma superscript star.

2 occurrences in this chapter

Equation form expr-4feaf0824cc8e0d1

⊨\Entails

Read as: entails

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: entails.

1 occurrence in this chapter

Equation form expr-5122ebf2b92e77cd

L'2\Lang{L'_2}

Read as: language L prime sub two

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L prime sub two.

1 occurrence in this chapter

Equation form expr-53358d3684015ca0

S∈L'0!S \in \Lang{L}'_0

Read as: S is in language L prime sub zero

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: S is in language L prime sub zero.

1 occurrence in this chapter

Equation form expr-542de1299c1c558f

Δn\Delta_n

Read as: Delta sub n

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Delta sub n.

7 occurrences in this chapter

Equation form expr-544b476f8c48fbca

D(P)⊨C(c1,…,cn)→P(c1,…,cn).!D(P) \Entails !C(c_1,\dots,c_n) \to \Atom{P}{c_1,\dots, c_n}.

Read as: D open parenthesis P close parenthesis entails C open parenthesis c sub one comma and so on comma c sub n close parenthesis to predicate P applied to c sub one comma and so on comma c sub n

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: D open parenthesis P close parenthesis entails C open parenthesis c sub one comma and so on comma c sub n close parenthesis to predicate P applied to c sub one comma and so on comma c sub n.

1 occurrence in this chapter

Equation form expr-546cbd12711c496e

¬S\lnot !S

Read as: not S

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: not S.

1 occurrence in this chapter

Equation form expr-56b59a3b3dc11eaf

H!H

Read as: H

Means: Model-theoretic notation in the separation and inseparability lemmas; it reads: H.

1 occurrence in this chapter

Equation form expr-56e1d8bfc92b701f

∃xx=x\lexists[x][\eq[x][x]]

Read as: there exists x, x equals x

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: there exists x, x equals x.

1 occurrence in this chapter

Equation form expr-57885e4c75965b23

Γ\Gamma

Read as: Gamma

Means: A set of sentences or stage in the inseparability construction in the separation and inseparability lemmas; it reads: Gamma.

11 occurrences in this chapter

Equation form expr-57abccf01eabb639

Δ*⊨¬(C∨C′)\Delta^* \Entails \lnot (!C \lor !C')

Read as: Delta superscript star entails not open parenthesis C or C prime close parenthesis

Means: A semantic consequence or satisfaction claim in the maximally inseparable pair proof of Craig interpolation; it reads: Delta superscript star entails not open parenthesis C or C prime close parenthesis.

1 occurrence in this chapter

Equation form expr-5b10fb7c290580b2

cM'1\Assign{c}{M'_1}

Read as: the interpretation of c in structure M prime sub one

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: the interpretation of c in structure M prime sub one.

1 occurrence in this chapter

Equation form expr-5b4c88e71079274c

L'i\Lang{L}'_i

Read as: language L prime sub i

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L prime sub i.

1 occurrence in this chapter

Equation form expr-5b8624d70153d3c4

L0\Lang{L}_0

Read as: language L sub zero

Means: Language or theory notation controlling the available nonlogical vocabulary in the separation and inseparability lemmas and the maximally inseparable pair proof of Craig interpolation; it reads: language L sub zero.

5 occurrences in this chapter

Equation form expr-5bce60d5f6942daa

Δn+1=Δn\Delta_{n+1} = \Delta_n

Read as: Delta sub n plus one equals Delta sub n

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Delta sub n plus one equals Delta sub n.

1 occurrence in this chapter

Equation form expr-5c62e091b8c0565f

PP

Read as: P

Means: Model-theoretic notation in the maximally inseparable pair proof of Craig interpolation and the Beth definability application; it reads: P.

18 occurrences in this chapter

Equation form expr-5d833cad49f2955f

PM=h(PM'1)\Assign{P}{M} = h(\Assign{P}{M'_1})

Read as: the interpretation of P in structure M equals h open parenthesis the interpretation of P in structure M prime sub one close parenthesis

Means: After the disclosed source correction, P in M is the image under h of P in M prime one.

1 occurrence in this chapter

Equation form expr-5db1396fb436c233

A(P)∈Δ0!A(P) \in \Delta_0

Read as: formula A open parenthesis P close parenthesis is in Delta sub zero

Means: A set of sentences or stage in the inseparability construction in the Beth definability application; it reads: formula A open parenthesis P close parenthesis is in Delta sub zero.

2 occurrences in this chapter

Equation form expr-5dfbd756c46dbc42

Σ(P)\Sigma(P)

Read as: Sigma open parenthesis P close parenthesis

Means: Language or theory notation controlling the available nonlogical vocabulary in the Beth definability application; it reads: Sigma open parenthesis P close parenthesis.

8 occurrences in this chapter

Equation form expr-60d7cf1347fb4435

Γn+1\Gamma_{n+1}

Read as: Gamma sub n plus one

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma sub n plus one.

8 occurrences in this chapter

Equation form expr-6123ac58b6e14266

D(P)∧D(P′)⊨P(c1,…,cn)→P′(c1,…,cn)!D(P) \land !D(P') \Entails \Atom{P}{c_1, \dots, c_n} \to \Atom{P'}{c_1, \dots, c_n}

Read as: D open parenthesis P close parenthesis and D open parenthesis P prime close parenthesis entails predicate P applied to c sub one comma and so on comma c sub n to predicate P prime applied to c sub one comma and so on comma c sub n

Means: After the disclosed source correction, D of P and D of P prime entail that the P atom implies the matching P prime atom.

1 occurrence in this chapter

Equation form expr-61b3edad3729be2c

D(P)∧P(c1,…,cn)⊨D(P′)→P′(c1,…,cn).!D(P) \land \Atom{P}{c_1, \dots, c_n} \Entails !D(P') \to \Atom{P'}{c_1, \dots, c_n}.

Read as: D open parenthesis P close parenthesis and predicate P applied to c sub one comma and so on comma c sub n entails D open parenthesis P prime close parenthesis to predicate P prime applied to c sub one comma and so on comma c sub n

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: D open parenthesis P close parenthesis and predicate P applied to c sub one comma and so on comma c sub n entails D open parenthesis P prime close parenthesis to predicate P prime applied to c sub one comma and so on comma c sub n.

1 occurrence in this chapter

Equation form expr-62511d849178db51

Γ∪{∃xS}\Gamma \cup \{\lexists[x]{!S} \}

Read as: Gamma union there exists x S

Means: A set of sentences or stage in the inseparability construction in the separation and inseparability lemmas; it reads: Gamma union there exists x S.

1 occurrence in this chapter

Equation form expr-629aa69969abe1a6

cM'2∈PM'2\Assign{c}{M'_2} \in \Assign{P}{M'_2}

Read as: the interpretation of c in structure M prime sub two is in the interpretation of P in structure M prime sub two

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: the interpretation of c in structure M prime sub two is in the interpretation of P in structure M prime sub two.

1 occurrence in this chapter

Equation form expr-6522c38f18f307d2

G⊨C[c/x],H⊨¬C[c/x].!G & \Entails \Subst{!C}{c}{x}, & !H \Entails \lnot \Subst{!C}{c}{x}.

Read as: G then entails C with c substituted for x comma then H entails not C with c substituted for x

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: G then entails C with c substituted for x comma then H entails not C with c substituted for x.

1 occurrence in this chapter

Equation form expr-664c820acc32e976

Γn+2=Γn+1\Gamma_{n+2} = \Gamma_{n+1}

Read as: Gamma sub n plus two equals Gamma sub n plus one

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma sub n plus two equals Gamma sub n plus one.

1 occurrence in this chapter

Equation form expr-66518191eef3ad4b

L'1\Lang{L'_1}

Read as: language L prime sub one

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L prime sub one.

1 occurrence in this chapter

Equation form expr-685882f568014334

¬S∈Δ*\lnot !S \in \Delta^*

Read as: not S is in Delta superscript star

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: not S is in Delta superscript star.

2 occurrences in this chapter

Equation form expr-68a9d5a8339e4038

cnc_n

Read as: c sub n

Means: Model-theoretic notation in the Beth definability application; it reads: c sub n.

1 occurrence in this chapter

Equation form expr-6958b9a10bedb6aa

L1∖L2\Lang{L}_1\setminus \Lang{L}_2

Read as: language L sub one set minus language L sub two

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L sub one set minus language L sub two.

1 occurrence in this chapter

Equation form expr-6c8c2c93f58c11b6

Δn+1=Δn∪{Bn}\Delta_{n+1} = \Delta_n \cup \{ !B_n \}

Read as: Delta sub n plus one equals Delta sub n union formula B sub n

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Delta sub n plus one equals Delta sub n union formula B sub n.

1 occurrence in this chapter

Equation form expr-6cc3244c90c44fc3

M'1\Struct{M}'_1

Read as: structure M prime sub one

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: structure M prime sub one.

1 occurrence in this chapter

Equation form expr-6d3e71d59fbc82fa

C(c1,…,cn)⊨D(P)→P(c1,…,cn)!C(c_1,\dots, c_n) \Entails !D(P) \lif \Atom{P}{c_1,\dots, c_n}

Read as: C open parenthesis c sub one comma and so on comma c sub n close parenthesis entails D open parenthesis P close parenthesis implies predicate P applied to c sub one comma and so on comma c sub n

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: C open parenthesis c sub one comma and so on comma c sub n close parenthesis entails D open parenthesis P close parenthesis implies predicate P applied to c sub one comma and so on comma c sub n.

1 occurrence in this chapter

Equation form expr-6db82c1ae3dfffcd

Γ1\Gamma_1

Read as: Gamma sub one

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma sub one.

1 occurrence in this chapter

Equation form expr-6ee19720d8dbb733

cn\Obj c_n

Read as: object language symbol c sub n

Means: Model-theoretic notation in the separation and inseparability lemmas; it reads: object language symbol c sub n.

1 occurrence in this chapter

Equation form expr-6fa8ad66df91da35

Γ*=⋃n≥0Γn,Δ*=⋃n≥0Δn.\Gamma^* & = \bigcup_{n\ge 0} \Gamma_n, & \Delta^* & = \bigcup_{n\ge 0} \Delta_n.

Read as: Gamma superscript star equals the union of sub n is greater than or equal to zero Gamma sub n comma then Delta superscript star equals the union of sub n is greater than or equal to zero Delta sub n

Means: The maximally inseparable limit sets Gamma star and Delta star are the unions of their finite stages.

1 occurrence in this chapter

Equation form expr-709f0a876ec85b60

B0!B_0

Read as: formula B sub zero

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: formula B sub zero.

1 occurrence in this chapter

Equation form expr-711da4487eab6c9d

Γ*⊨¬An→C′,Δ*⊨¬C′.\Gamma^* & \Entails \lnot !A_n \lif !C', & \Delta^* & \Entails \lnot !C'.

Read as: Gamma superscript star then entails not formula A sub n implies C prime comma then Delta superscript star then entails not C prime

Means: A semantic consequence or satisfaction claim in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma superscript star then entails not formula A sub n implies C prime comma then Delta superscript star then entails not C prime.

1 occurrence in this chapter

Equation form expr-72598d8dfc13c062

L1∪L2\Lang{L}_1 \cup \Lang{L}_2

Read as: language L sub one union language L sub two

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L sub one union language L sub two.

1 occurrence in this chapter

Equation form expr-72c5d23296a8aebe

D(P)⊨P(c1,…,cn)→C(c1,…,cn)!D(P) \Entails \Atom{P}{c_1,\dots, c_n} \lif !C(c_1,\dots, c_n)

Read as: D open parenthesis P close parenthesis entails predicate P applied to c sub one comma and so on comma c sub n implies C open parenthesis c sub one comma and so on comma c sub n close parenthesis

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: D open parenthesis P close parenthesis entails predicate P applied to c sub one comma and so on comma c sub n implies C open parenthesis c sub one comma and so on comma c sub n close parenthesis.

1 occurrence in this chapter

Equation form expr-73388c7793dd5e4a

L'0\Lang{L}'_0

Read as: language L prime sub zero

Means: Language or theory notation controlling the available nonlogical vocabulary in the separation and inseparability lemmas and the maximally inseparable pair proof of Craig interpolation; it reads: language L prime sub zero.

11 occurrences in this chapter

Equation form expr-73a89757c45513db

G⊨∀xC!G \Entails \lforall[x][!C]

Read as: G entails for every x, C

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: G entails for every x, C.

1 occurrence in this chapter

Equation form expr-74f4567a6896230a

=\eq

Read as: equals

Means: Model-theoretic notation in the opening statement of interpolation and the maximally inseparable pair proof of Craig interpolation; it reads: equals.

2 occurrences in this chapter

Equation form expr-759c5ca2330e85a3

C∈L0!C \in \Lang{L}_0

Read as: C is in language L sub zero

Means: Language or theory notation controlling the available nonlogical vocabulary in the separation and inseparability lemmas; it reads: C is in language L sub zero.

1 occurrence in this chapter

Equation form expr-77ac0e65fe407ce2

H⊨¬∀xC!H \Entails \lnot \lforall[x][!C]

Read as: H entails not for every x, C

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: H entails not for every x, C.

1 occurrence in this chapter

Equation form expr-7825f4cdc674003a

M'2\Struct{M}'_2

Read as: structure M prime sub two

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: structure M prime sub two.

1 occurrence in this chapter

Equation form expr-7c2b221a08fd9b8a

A(P′)!A(P')

Read as: formula A open parenthesis P prime close parenthesis

Means: A formula, quantified sentence, atomic formula, or substitution in the Beth definability application; it reads: formula A open parenthesis P prime close parenthesis.

1 occurrence in this chapter

Equation form expr-7ce66658ceef4b93

Δn+1\Delta_{n+1}

Read as: Delta sub n plus one

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Delta sub n plus one.

5 occurrences in this chapter

Equation form expr-7ec45e005d0457b4

{A}\{!A\}

Read as: formula A

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: formula A.

1 occurrence in this chapter

Equation form expr-7fe8f5b6ca65e351

Γ∪{∃xS,S[c/x]}\Gamma \cup \{ \lexists[x][!S], \Subst{!S}{c}{x}\}

Read as: Gamma union there exists x, S comma S with c substituted for x

Means: A set of sentences or stage in the inseparability construction in the separation and inseparability lemmas; it reads: Gamma union there exists x, S comma S with c substituted for x.

1 occurrence in this chapter

Equation form expr-80ecc36f09f13315

Γ∪{∃xS}⊨∃xC\Gamma \cup \{ \lexists[x][!S] \} \Entails \lexists[x][!C]

Read as: Gamma union there exists x, S entails there exists x, C

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: Gamma union there exists x, S entails there exists x, C.

1 occurrence in this chapter

Equation form expr-81f7770b99d6eec5

Δ0⊨¬C[c/x]\Delta_0 \Entails \lnot \Subst{!C}{c}{x}

Read as: Delta sub zero entails not C with c substituted for x

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: Delta sub zero entails not C with c substituted for x.

1 occurrence in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: formula A

Means: A formula, quantified sentence, atomic formula, or substitution in the opening statement of interpolation and the separation and inseparability lemmas and the maximally inseparable pair proof of Craig interpolation; it reads: formula A.

12 occurrences in this chapter

Equation form expr-828542219795165c

Γ∪{∃xS}\Gamma \cup \{ \lexists[x][!S] \}

Read as: Gamma union there exists x, S

Means: A set of sentences or stage in the inseparability construction in the separation and inseparability lemmas; it reads: Gamma union there exists x, S.

1 occurrence in this chapter

Equation form expr-84d7c29eb5648796

M1\Struct{M_1}

Read as: structure M sub one

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: structure M sub one.

1 occurrence in this chapter

Equation form expr-88362ce26b39d504

M⊨A\Struct{M} \Entails !A

Read as: structure M entails formula A

Means: A semantic consequence or satisfaction claim in the maximally inseparable pair proof of Craig interpolation; it reads: structure M entails formula A.

1 occurrence in this chapter

Equation form expr-89e985f401484800

n≥0n \ge 0

Read as: n is greater than or equal to zero

Means: Model-theoretic notation in the separation and inseparability lemmas and the maximally inseparable pair proof of Craig interpolation; it reads: n is greater than or equal to zero.

4 occurrences in this chapter

Equation form expr-8c2574892063f995

RR

Read as: R

Means: Model-theoretic notation in the Beth definability application; it reads: R.

3 occurrences in this chapter

Equation form expr-917e8bf49341ec3d

Σ(P)∪Σ(P′)⊨∀x1…∀xn(P(x1,…,xn)↔P′(x1,…,xn)),\Sigma(P) \cup \Sigma(P') \Entails \lforall[x_1][\dots \lforall[x_n][(\Atom{P}{x_1,\dots, x_n} \liff \Atom{P'}{x_1,\dots, x_n})]],

Read as: Sigma open parenthesis P close parenthesis union Sigma open parenthesis P prime close parenthesis entails for every x sub one, and so on for every x sub n, open parenthesis predicate P applied to x sub one comma and so on comma x sub n if and only if predicate P prime applied to x sub one comma and so on comma x sub n close parenthesis

Means: Implicit definability: the two renamed theory copies entail agreement of P and P prime on every tuple.

1 occurrence in this chapter

Equation form expr-928897204ff28dd5

A0!A_0

Read as: formula A sub zero

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: formula A sub zero.

2 occurrences in this chapter

Equation form expr-94a6192be68a7ac8

L'1∖L'0\Lang{L'_1} \setminus \Lang{L'_0}

Read as: language L prime sub one set minus language L prime sub zero

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L prime sub one set minus language L prime sub zero.

1 occurrence in this chapter

Equation form expr-98d3fc36183a7f75

M[R′]\Expan{M}{R'}

Read as: the expansion of structure M by relation R prime

Means: A structure, domain, isomorphism, or interpretation claim in the Beth definability application; it reads: the expansion of structure M by relation R prime.

1 occurrence in this chapter

Equation form expr-992accb9917efeb5

C!C

Read as: C

Means: A formula, quantified sentence, atomic formula, or substitution in the opening statement of interpolation and the separation and inseparability lemmas and the maximally inseparable pair proof of Craig interpolation and the Beth definability application; it reads: C.

20 occurrences in this chapter

Equation form expr-998278b07685d0a1

C[c/x]⊨¬H\Subst{!C}{c}{x} \Entails \lnot !H

Read as: C with c substituted for x entails not H

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: C with c substituted for x entails not H.

1 occurrence in this chapter

Equation form expr-9b905117a7806eb1

Γn+2=Γn+1∪{An+1}\Gamma_{n+2} = \Gamma_{n+1} \cup \{!A_{n+1} \}

Read as: Gamma sub n plus two equals Gamma sub n plus one union formula A sub n plus one

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma sub n plus two equals Gamma sub n plus one union formula A sub n plus one.

1 occurrence in this chapter

Equation form expr-9cf84a0c53dba2ac

A(P)!A(P)

Read as: formula A open parenthesis P close parenthesis

Means: A formula, quantified sentence, atomic formula, or substitution in the Beth definability application; it reads: formula A open parenthesis P close parenthesis.

1 occurrence in this chapter

Equation form expr-a1e4410c78364e4a

C(c1,…,cn)!C(c_1,\dots, c_n)

Read as: C open parenthesis c sub one comma and so on comma c sub n close parenthesis

Means: A formula, quantified sentence, atomic formula, or substitution in the Beth definability application; it reads: C open parenthesis c sub one comma and so on comma c sub n close parenthesis.

1 occurrence in this chapter

Equation form expr-a5f4dfe32de9c4d1

Γ∪{∃xS,S[c/x]}⊨C[c/x],\Gamma \cup \{ \lexists[x][!S], \Subst{!S}{c}{x}\} \Entails \Subst{!C}{c}{x},

Read as: Gamma union there exists x, S comma S with c substituted for x entails C with c substituted for x

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: Gamma union there exists x, S comma S with c substituted for x entails C with c substituted for x.

1 occurrence in this chapter

Equation form expr-a77be5a141a58923

L∪{P}\Lang{L} \cup\{P\}

Read as: language L union P

Means: Language or theory notation controlling the available nonlogical vocabulary in the Beth definability application; it reads: language L union P.

1 occurrence in this chapter

Equation form expr-a846c5710dca59ee

Σ(P′)\Sigma(P')

Read as: Sigma open parenthesis P prime close parenthesis

Means: Language or theory notation controlling the available nonlogical vocabulary in the Beth definability application; it reads: Sigma open parenthesis P prime close parenthesis.

1 occurrence in this chapter

Equation form expr-a892743da3ce8bbc

Σ(P)⊨∀x1…∀xn(P(x1,…,xn)↔C(x1,…,xn)).\Sigma(P) \Entails \lforall[x_1][\dots \lforall[x_n][(\Atom{P}{x_1,\dots, x_n} \liff !C(x_1, \dots, x_n))]].

Read as: Sigma open parenthesis P close parenthesis entails for every x sub one, and so on for every x sub n, open parenthesis predicate P applied to x sub one comma and so on comma x sub n if and only if C open parenthesis x sub one comma and so on comma x sub n close parenthesis close parenthesis

Means: Explicit definability: Sigma of P entails a universal biconditional between P and C.

2 occurrences in this chapter

Equation form expr-a9ef8213a93bbe82

M[R]⊨A(P)\Expan{M}{R} \Entails !A(P)

Read as: the expansion of structure M by relation R entails formula A open parenthesis P close parenthesis

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: the expansion of structure M by relation R entails formula A open parenthesis P close parenthesis.

1 occurrence in this chapter

Equation form expr-ab0b708e2ca6abd6

C⊨B!C \Entails !B

Read as: C entails formula B

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: C entails formula B.

1 occurrence in this chapter

Equation form expr-ab8d36bc9d2de750

Γ0∪{∃xS}\Gamma_0 \cup \{ \lexists[x][!S]\}

Read as: Gamma sub zero union there exists x, S

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma sub zero union there exists x, S.

1 occurrence in this chapter

Equation form expr-abba59a575669755

M[R′]⊨Σ(P′)\Expan{M}{R'} \Entails \Sigma(P')

Read as: the expansion of structure M by relation R prime entails Sigma open parenthesis P prime close parenthesis

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: the expansion of structure M by relation R prime entails Sigma open parenthesis P prime close parenthesis.

1 occurrence in this chapter

Equation form expr-ae6f502e1eafd390

Bn!B_n

Read as: formula B sub n

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: formula B sub n.

5 occurrences in this chapter

Equation form expr-b06799d3205fa44d

Δ0\Delta_0

Read as: Delta sub zero

Means: A set of sentences or stage in the inseparability construction in the separation and inseparability lemmas and the maximally inseparable pair proof of Craig interpolation; it reads: Delta sub zero.

6 occurrences in this chapter

Equation form expr-b25379fd92056130

L'1⊇L'0\Lang{L'_1} \supseteq \Lang{L'_0}

Read as: language L prime sub one contains language L prime sub zero

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L prime sub one contains language L prime sub zero.

1 occurrence in this chapter

Equation form expr-b46f9e863d42ecfa

D(P′)!D(P')

Read as: D open parenthesis P prime close parenthesis

Means: Model-theoretic notation in the Beth definability application; it reads: D open parenthesis P prime close parenthesis.

1 occurrence in this chapter

Equation form expr-b49e670e962d30ee

C∈L'0!C \in \Lang{L}'_0

Read as: C is in language L prime sub zero

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: C is in language L prime sub zero.

1 occurrence in this chapter

Equation form expr-b50bb8940da5b931

L\Lang{L}

Read as: language L

Means: Language or theory notation controlling the available nonlogical vocabulary in the Beth definability application; it reads: language L.

5 occurrences in this chapter

Equation form expr-b773400b008f9c78

=\doteq

Read as: object language equality

Means: Model-theoretic notation in the separation and inseparability lemmas; it reads: object language equality.

1 occurrence in this chapter

Equation form expr-b87d4eb57a760ccb

¬S∈Γ*∩Δ*\lnot !S \in \Gamma^* \cap \Delta^*

Read as: not S is in Gamma superscript star intersect Delta superscript star

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: not S is in Gamma superscript star intersect Delta superscript star.

1 occurrence in this chapter

Equation form expr-b8dfe1e701bddfac

⟨c1M'2,…,cnM'2⟩∈PM\tuple{\Assign{c_1}{M'_2}, \dots, \Assign{c_n}{M'_2}} \in \Assign{P}{M}

Read as: the tuple the interpretation of c sub one in structure M prime sub two comma and so on comma the interpretation of c sub n in structure M prime sub two is in the interpretation of P in structure M

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: the tuple the interpretation of c sub one in structure M prime sub two comma and so on comma the interpretation of c sub n in structure M prime sub two is in the interpretation of P in structure M.

1 occurrence in this chapter

Equation form expr-b9e79fc74f573b50

¬B⊨¬C\lnot !B \Entails \lnot !C

Read as: not formula B entails not C

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: not formula B entails not C.

1 occurrence in this chapter

Equation form expr-bc01d7e3764c9cce

P(c)∈Δ*\Atom{P}{c} \in \Delta^*

Read as: predicate P applied to c is in Delta superscript star

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: predicate P applied to c is in Delta superscript star.

1 occurrence in this chapter

Equation form expr-bd3f4f640d755b0b

Γ*⊨An→C,Δ*⊨¬C.\Gamma^* & \Entails !A_n \lif !C, & \Delta^* & \Entails \lnot !C.

Read as: Gamma superscript star then entails formula A sub n implies C comma then Delta superscript star then entails not C

Means: A semantic consequence or satisfaction claim in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma superscript star then entails formula A sub n implies C comma then Delta superscript star then entails not C.

1 occurrence in this chapter

Equation form expr-c1236573ab255758

An+1!A_{n+1}

Read as: formula A sub n plus one

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: formula A sub n plus one.

1 occurrence in this chapter

Equation form expr-c2b5594256fabaa3

Σ(P)⊨∀x1…∀xn(P(x1,…,xn)↔C(x1,…,xn)).\Sigma(P) \Entails \lforall[x_1][\dots\lforall[x_n][(\Atom{P}{x_1,\dots, x_n} \liff !C(x_1,\dots, x_n))]].

Read as: Sigma open parenthesis P close parenthesis entails for every x sub one, and so on for every x sub n, open parenthesis predicate P applied to x sub one comma and so on comma x sub n if and only if C open parenthesis x sub one comma and so on comma x sub n close parenthesis close parenthesis

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: Sigma open parenthesis P close parenthesis entails for every x sub one, and so on for every x sub n, open parenthesis predicate P applied to x sub one comma and so on comma x sub n if and only if C open parenthesis x sub one comma and so on comma x sub n close parenthesis close parenthesis.

1 occurrence in this chapter

Equation form expr-c341f9d132df036d

⟨c1M'1,…,cnM'1⟩∈PM'1\tuple{\Assign{c_1}{M'_1}, \dots, \Assign{c_n}{M'_1}} \in \Assign{P}{M'_1}

Read as: the tuple the interpretation of c sub one in structure M prime sub one comma and so on comma the interpretation of c sub n in structure M prime sub one is in the interpretation of P in structure M prime sub one

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: the tuple the interpretation of c sub one in structure M prime sub one comma and so on comma the interpretation of c sub n in structure M prime sub one is in the interpretation of P in structure M prime sub one.

1 occurrence in this chapter

Equation form expr-c4b5a2287c0f17d1

A(P′)∈Δ1!A(P') \in \Delta_1

Read as: formula A open parenthesis P prime close parenthesis is in Delta sub one

Means: A set of sentences or stage in the inseparability construction in the Beth definability application; it reads: formula A open parenthesis P prime close parenthesis is in Delta sub one.

2 occurrences in this chapter

Equation form expr-c71a6d86e873873b

Γ*∩Δ*\Gamma^* \cap \Delta^*

Read as: Gamma superscript star intersect Delta superscript star

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma superscript star intersect Delta superscript star.

3 occurrences in this chapter

Equation form expr-c7fe53a7c2946e41

Γ,∃xS⊨∀x(S→C)\Gamma, \lexists[x][!S] \Entails \lforall[x][(!S \lif !C)]

Read as: Gamma comma there exists x, S entails for every x, open parenthesis S implies C close parenthesis

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: Gamma comma there exists x, S entails for every x, open parenthesis S implies C close parenthesis.

1 occurrence in this chapter

Equation form expr-c816d7c71265104d

Δ⊨¬∃xC\Delta \Entails \lnot \lexists[x][!C]

Read as: Delta entails not there exists x, C

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: Delta entails not there exists x, C.

1 occurrence in this chapter

Equation form expr-c8be90574903424c

Γ1=Γ0∪{∃xS,S[c/x]}\Gamma_1 = \Gamma_0 \cup \{ \lexists[x][!S], \Subst{!S}{c}{x} \}

Read as: Gamma sub one equals Gamma sub zero union there exists x, S comma S with c substituted for x

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma sub one equals Gamma sub zero union there exists x, S comma S with c substituted for x.

1 occurrence in this chapter

Equation form expr-cb17518185968142

PM=PM'2=h(PM'1)\Assign{P}{M} = \Assign{P}{M'_2} = h(\Assign{P}{M'_1})

Read as: the interpretation of P in structure M equals the interpretation of P in structure M prime sub two equals h open parenthesis the interpretation of P in structure M prime sub one close parenthesis

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: the interpretation of P in structure M equals the interpretation of P in structure M prime sub two equals h open parenthesis the interpretation of P in structure M prime sub one close parenthesis.

1 occurrence in this chapter

Equation form expr-cc4ee341a5f51da0

Γ0∪{∃xS,S[c/x]}\Gamma_0 \cup \{ \lexists[x][!S], \Subst{!S}{c}{x} \}

Read as: Gamma sub zero union there exists x, S comma S with c substituted for x

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma sub zero union there exists x, S comma S with c substituted for x.

1 occurrence in this chapter

Equation form expr-ccf32749a1e0e16a

Γ⊨C\Gamma \Entails !C

Read as: Gamma entails C

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: Gamma entails C.

1 occurrence in this chapter

Equation form expr-cd0427565e6fd84b

h(cM'1)=cM'2h(\Assign{c}{M'_1}) = \Assign{c}{M'_2}

Read as: h open parenthesis the interpretation of c in structure M prime sub one close parenthesis equals the interpretation of c in structure M prime sub two

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: h open parenthesis the interpretation of c in structure M prime sub one close parenthesis equals the interpretation of c in structure M prime sub two.

1 occurrence in this chapter

Equation form expr-cd0f9930e1aa91eb

L'1\Lang{L}'_1

Read as: language L prime sub one

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L prime sub one.

1 occurrence in this chapter

Equation form expr-cdf53e5660319e99

Γ1=Γ0\Gamma_1 = \Gamma_0

Read as: Gamma sub one equals Gamma sub zero

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma sub one equals Gamma sub zero.

1 occurrence in this chapter

Equation form expr-cec4b8919e5f12a5

P′P'

Read as: P prime

Means: Model-theoretic notation in the Beth definability application; it reads: P prime.

3 occurrences in this chapter

Equation form expr-cef3e6639fe132be

M′\Struct{M'}

Read as: structure M prime

Means: A structure, domain, isomorphism, or interpretation claim in the Beth definability application; it reads: structure M prime.

1 occurrence in this chapter

Equation form expr-cfbd0091a9784ecd

A⊨C!A \Entails !C

Read as: formula A entails C

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: formula A entails C.

1 occurrence in this chapter

Equation form expr-d03543adcda36df1

Γ0\Gamma_0

Read as: Gamma sub zero

Means: A set of sentences or stage in the inseparability construction in the separation and inseparability lemmas; it reads: Gamma sub zero.

2 occurrences in this chapter

Equation form expr-d036e88f0ce1f4e0

i∈{0,1,2}i \in \{0, 1, 2 \}

Read as: i is in zero comma one comma two

Means: A membership, containment, or equality statement in the maximally inseparable pair proof of Craig interpolation; it reads: i is in zero comma one comma two.

1 occurrence in this chapter

Equation form expr-d055ee4dbcdd0c8b

B!B

Read as: formula B

Means: A formula, quantified sentence, atomic formula, or substitution in the opening statement of interpolation and the separation and inseparability lemmas and the maximally inseparable pair proof of Craig interpolation; it reads: formula B.

9 occurrences in this chapter

Equation form expr-d205eb9f5d5c3a61

h:M1→M2h \colon M_1 \to M_2

Read as: h from M sub one to M sub two

Means: Model-theoretic notation in the maximally inseparable pair proof of Craig interpolation; it reads: h from M sub one to M sub two.

1 occurrence in this chapter

Equation form expr-d26d9fce5b9364d6

M'2\Struct{M'_2}

Read as: structure M prime sub two

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: structure M prime sub two.

1 occurrence in this chapter

Equation form expr-d38f17a246dadfed

¬C\lnot \formula{C}

Read as: not formula C

Means: Model-theoretic notation in the separation and inseparability lemmas; it reads: not formula C.

1 occurrence in this chapter

Equation form expr-d67a5630c02c8ad5

Σ(P)⊨∀x1…∀xn(P(x1,…,xn)↔C(x1,…,xn))Σ(P′)⊨∀x1…∀xn(P′(x1,…,xn)↔C(x1,…,xn))\Sigma(P) & \Entails & \lforall[x_1][\dots \lforall[x_n] [(\Atom{P}{x_1,\dots, x_n} \liff !C(x_1,\dots,x_n))]]\\ \Sigma(P') & \Entails & \lforall[x_1][\dots \lforall[x_n] [(\Atom{P'}{x_1,\dots, x_n} \liff !C(x_1,\dots,x_n))]]

Read as: Sigma open parenthesis P close parenthesis entails for every x sub one, and so on for every x sub n, open parenthesis predicate P applied to x sub one comma and so on comma x sub n if and only if C open parenthesis x sub one comma and so on comma x sub n close parenthesis close parenthesis next row Sigma open parenthesis P prime close parenthesis entails for every x sub one, and so on for every x sub n, open parenthesis predicate P prime applied to x sub one comma and so on comma x sub n if and only if C open parenthesis x sub one comma and so on comma x sub n close parenthesis close parenthesis

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: Sigma open parenthesis P close parenthesis entails for every x sub one, and so on for every x sub n, open parenthesis predicate P applied to x sub one comma and so on comma x sub n if and only if C open parenthesis x sub one comma and so on comma x sub n close parenthesis close parenthesis next row Sigma open parenthesis P prime close parenthesis entails for every x sub one, and so on for every x sub n, open parenthesis predicate P prime applied to x sub one comma and so on comma x sub n if and only if C open parenthesis x sub one comma and so on comma x sub n close parenthesis close parenthesis.

1 occurrence in this chapter

Equation form expr-dc84ba74989c81df

Γ∪{∃xS,¬C}\Gamma \cup \{\lexists[x][!S], \lnot!C \}

Read as: Gamma union there exists x, S comma not C

Means: A set of sentences or stage in the inseparability construction in the separation and inseparability lemmas; it reads: Gamma union there exists x, S comma not C.

1 occurrence in this chapter

Equation form expr-dd76202c4566d4a7

Δn∪{Bn}\Delta_n \cup \{!B_n\}

Read as: Delta sub n union formula B sub n

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Delta sub n union formula B sub n.

1 occurrence in this chapter

Equation form expr-ddb388e08871d9c1

M[R]⊨Σ(P)\Expan{M}{R} \Entails \Sigma(P)

Read as: the expansion of structure M by relation R entails Sigma open parenthesis P close parenthesis

Means: A semantic consequence or satisfaction claim in the Beth definability application; it reads: the expansion of structure M by relation R entails Sigma open parenthesis P close parenthesis.

1 occurrence in this chapter

Equation form expr-de64372991421159

An!A_n

Read as: formula A sub n

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: formula A sub n.

4 occurrences in this chapter

Equation form expr-debe4a24d040cde2

L'2\Lang{L}'_2

Read as: language L prime sub two

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L prime sub two.

1 occurrence in this chapter

Equation form expr-df3e0a8e5a6d34d9

c0,c1,c2,…\Obj c_0, \Obj c_1, \Obj c_2, \dots

Read as: object language symbol c sub zero comma object language symbol c sub one comma object language symbol c sub two comma and so on

Means: Model-theoretic notation in the maximally inseparable pair proof of Craig interpolation; it reads: object language symbol c sub zero comma object language symbol c sub one comma object language symbol c sub two comma and so on.

1 occurrence in this chapter

Equation form expr-dffa227108b65500

A1!A_1

Read as: formula A sub one

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: formula A sub one.

1 occurrence in this chapter

Equation form expr-e0875781a9cf360b

cM'1∈PM'1\Assign{c}{M'_1} \in \Assign{P}{M'_1}

Read as: the interpretation of c in structure M prime sub one is in the interpretation of P in structure M prime sub one

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: the interpretation of c in structure M prime sub one is in the interpretation of P in structure M prime sub one.

1 occurrence in this chapter

Equation form expr-e0ece8a9b5323c9d

C[c/x]\Subst{!C}{c}{x}

Read as: C with c substituted for x

Means: A formula, quantified sentence, atomic formula, or substitution in the separation and inseparability lemmas; it reads: C with c substituted for x.

1 occurrence in this chapter

Equation form expr-e1bd0072b035f85f

|M'2|\Domain{M'_2}

Read as: the domain of structure M prime sub two

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: the domain of structure M prime sub two.

1 occurrence in this chapter

Equation form expr-e250e58f7934ea03

∃xS\lexists[x][!S]

Read as: there exists x, S

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: there exists x, S.

2 occurrences in this chapter

Equation form expr-e3212229d200318d

¬B\lnot !B

Read as: not formula B

Means: A formula, quantified sentence, atomic formula, or substitution in the separation and inseparability lemmas and the maximally inseparable pair proof of Craig interpolation; it reads: not formula B.

4 occurrences in this chapter

Equation form expr-e4bf49ab16382944

PM′=R\Assign{P}{M'} = R

Read as: the interpretation of P in structure M prime equals R

Means: A structure, domain, isomorphism, or interpretation claim in the Beth definability application; it reads: the interpretation of P in structure M prime equals R.

1 occurrence in this chapter

Equation form expr-e55c1f3766149da6

D(P)!D(P)

Read as: D open parenthesis P close parenthesis

Means: Model-theoretic notation in the Beth definability application; it reads: D open parenthesis P close parenthesis.

1 occurrence in this chapter

Equation form expr-e66152d46292fbe2

L2∖L1\Lang{L_2} \setminus \Lang{L_1}

Read as: language L sub two set minus language L sub one

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L sub two set minus language L sub one.

1 occurrence in this chapter

Equation form expr-e93415532f57d617

⊭A→B\not\Entails !A \lif !B

Read as: does not entail formula A implies formula B

Means: A semantic consequence or satisfaction claim in the maximally inseparable pair proof of Craig interpolation; it reads: does not entail formula A implies formula B.

1 occurrence in this chapter

Equation form expr-e9bd4dc004d8bca3

L∪{P′}\Lang{L} \cup \{P'\}

Read as: language L union P prime

Means: Language or theory notation controlling the available nonlogical vocabulary in the Beth definability application; it reads: language L union P prime.

1 occurrence in this chapter

Equation form expr-ec1d1a5433acbe1d

S∈Γ*!S \in \Gamma^*

Read as: S is in Gamma superscript star

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: S is in Gamma superscript star.

2 occurrences in this chapter

Equation form expr-effd2824c289cef4

Γ1=Γ0∪{A0}\Gamma_1 = \Gamma_0 \cup\{ !A_0\}

Read as: Gamma sub one equals Gamma sub zero union formula A sub zero

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: Gamma sub one equals Gamma sub zero union formula A sub zero.

1 occurrence in this chapter

Equation form expr-f02adc61200fda74

Li\Lang{L}_i

Read as: language L sub i

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L sub i.

1 occurrence in this chapter

Equation form expr-f0313d40f749d3ef

∀xC\lforall[x][!C]

Read as: for every x, C

Means: A formula, quantified sentence, atomic formula, or substitution in the separation and inseparability lemmas; it reads: for every x, C.

1 occurrence in this chapter

Equation form expr-f1941b975ffcc891

Δ\Delta

Read as: Delta

Means: A set of sentences or stage in the inseparability construction in the separation and inseparability lemmas; it reads: Delta.

18 occurrences in this chapter

Equation form expr-f2b658880e0f6e2b

C\formula{C}

Read as: formula C

Means: Model-theoretic notation in the separation and inseparability lemmas; it reads: formula C.

1 occurrence in this chapter

Equation form expr-f498bcd228dcccbe

(Γn,Δn)(\Gamma_n, \Delta_n)

Read as: open parenthesis Gamma sub n comma Delta sub n close parenthesis

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: open parenthesis Gamma sub n comma Delta sub n close parenthesis.

2 occurrences in this chapter

Equation form expr-f50e961536990e1c

M[R]\Expan{M}{R}

Read as: the expansion of structure M by relation R

Means: A structure, domain, isomorphism, or interpretation claim in the Beth definability application; it reads: the expansion of structure M by relation R.

1 occurrence in this chapter

Equation form expr-f579aa4cdccb8bc2

M⊨¬B\Struct{M} \Entails \lnot!B

Read as: structure M entails not formula B

Means: A semantic consequence or satisfaction claim in the maximally inseparable pair proof of Craig interpolation; it reads: structure M entails not formula B.

1 occurrence in this chapter

Equation form expr-f5b5dd7c2ac50826

(Γ*,Δ*)(\Gamma^*, \Delta^*)

Read as: open parenthesis Gamma superscript star comma Delta superscript star close parenthesis

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: open parenthesis Gamma superscript star comma Delta superscript star close parenthesis.

1 occurrence in this chapter

Equation form expr-f7e8276127da6aec

C∨C′!C \lor !C'

Read as: C or C prime

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: C or C prime.

1 occurrence in this chapter

Equation form expr-f8c199cfeffe678f

|M'1|\Domain{M'_1}

Read as: the domain of structure M prime sub one

Means: A structure, domain, isomorphism, or interpretation claim in the maximally inseparable pair proof of Craig interpolation; it reads: the domain of structure M prime sub one.

1 occurrence in this chapter

Equation form expr-f99f04616c6b54e0

{¬B}\{\lnot !B\}

Read as: not formula B

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: not formula B.

1 occurrence in this chapter

Equation form expr-f9f5e87e51d3fbe6

R=R′R=R'

Read as: R equals R prime

Means: A membership, containment, or equality statement in the Beth definability application; it reads: R equals R prime.

1 occurrence in this chapter

Equation form expr-fc79abebd4411220

¬S∈Γ*\lnot !S \in \Gamma^*

Read as: not S is in Gamma superscript star

Means: A set of sentences or stage in the inseparability construction in the maximally inseparable pair proof of Craig interpolation; it reads: not S is in Gamma superscript star.

2 occurrences in this chapter

Equation form expr-fd448de8a1c3604a

L'2⊇L'0\Lang{L'_2} \supseteq \Lang{L'_0}

Read as: language L prime sub two contains language L prime sub zero

Means: Language or theory notation controlling the available nonlogical vocabulary in the maximally inseparable pair proof of Craig interpolation; it reads: language L prime sub two contains language L prime sub zero.

1 occurrence in this chapter

Equation form expr-fd5fca656e889906

Γ0⊨C[c/x]\Gamma_0 \Entails \Subst{!C}{c}{x}

Read as: Gamma sub zero entails C with c substituted for x

Means: A semantic consequence or satisfaction claim in the separation and inseparability lemmas; it reads: Gamma sub zero entails C with c substituted for x.

1 occurrence in this chapter

Equation form expr-ff0ef5c23edbf7bf

B1!B_1

Read as: formula B sub one

Means: A formula, quantified sentence, atomic formula, or substitution in the maximally inseparable pair proof of Craig interpolation; it reads: formula B sub one.

1 occurrence in this chapter

Definition of separation and inseparability

A sentence separates Gamma and Delta when Gamma entails it and Delta entails its negation; otherwise the two sets of sentences are inseparable.

Source

Figure showing separation by a sentence

A rectangle for the models of formula C contains the Gamma circle on the left. A curved boundary separates it from the Delta circle on the right, which lies in the region for not C.

Source

Diagram of two separated model classes

Inside an outer rounded rectangle, disjoint circles labeled Gamma and Delta sit on opposite sides of a curved boundary. Formula C labels the Gamma side and not formula C labels the Delta side.

Source

Fresh constants preserve inseparability

If Gamma and Delta are inseparable in their common language, adjoining infinitely many fresh constants to that language does not make them separable.

Source

Finite entailments used in the fresh constant lemma

The conjunction G entails the substituted separator, while H entails its negation.

Source

Generalized entailments that contradict inseparability

Gamma entails the universal closure of C and Delta entails its negation, producing a separator in the original language.

Source

Witness constants preserve inseparability

Adding a fresh witness instance for an existential sentence to Gamma preserves inseparability from Delta.

Source

Craig interpolation theorem

Whenever A logically implies B, an interpolant C lies between them and uses only the nonlogical vocabulary common to A and B.

Source

Limit pair of sentence sets

Gamma star and Delta star are the unions of their respective increasing finite stages.

Source

Consequences from omitting A sub n

Gamma star entails that not A sub n implies C prime, and Delta star entails not C prime.

Source

Consequences from omitting not A sub n

Gamma star entails that A sub n implies C, and Delta star entails not C.

Source

Definition of explicit definability

A theory explicitly defines P when it entails a universal biconditional between P and a formula in the original language.

Source

Definition of implicit definability

A theory implicitly defines P when any two interpretations P and P prime satisfying renamed copies of the theory agree on every tuple.

Source

Beth definability theorem

A theory implicitly defines a predicate exactly when it explicitly defines that predicate.

Source

Paired explicit definitions for P and P prime

The theory with P and its renamed copy with P prime each entail the corresponding universal biconditional with the same defining formula C.

Source

Craig interpolant in the Beth theorem proof

One entailment derives the interpolant C from D of P and the P atom; the other derives the P prime consequence from C.

Source

Cross-reference reference-000524

reference part-a

Source occurrence

Cross-reference reference-000525

reference lem:sep1

Source occurrence

Cross-reference reference-000526

reference part-b

Source occurrence

Cross-reference reference-000527

reference part-b

Source occurrence

Cross-reference reference-000528

reference part-a

Source occurrence

Cross-reference reference-000529

reference lem:sep2

Source occurrence

Cross-reference reference-000530

reference part-a

Source occurrence

Cross-reference reference-000531

reference part-b

Source occurrence

Cross-reference reference-000532

reference part-a

Source occurrence

Cross-reference reference-000533

reference lem:sep2

Source occurrence

Cross-reference reference-000534

reference part-b

Source occurrence

Cross-reference reference-000535

reference part-b

Source occurrence

Cross-reference reference-000536

reference lem:sep2

Source occurrence

Cross-reference reference-000537

reference part-a

Source occurrence

Cross-reference reference-000538

reference part-a

Source occurrence

Cross-reference reference-000539

reference part-b

Source occurrence

Cross-reference reference-000540

reference part-a

Source occurrence

Cross-reference reference-000541

reference thm:completeness

Source occurrence

Source disclosures