The Henkin style proof of the completeness of predicate logic

The Henkin style proof of the completeness of predicate logic

四月 07, 2020

The Semantics

Definition 1: Structure

A I,J,K,η,ζ\left\langle\mathcal{I},\mathcal{J,}K,\eta,\zeta\right\rangle-structure M\mathcal{M} is a complex of the form M=A,  R={ri|iI},  F={fj|jJ},  {ek|kK}\mathcal{M} = \left\langle A,\ \ R = \left\{ r_{i} \middle| i\mathcal{\in I} \right\},\ \ F = \left\{ f_{j} \middle| j \in \mathcal{J} \right\},\ \ \left\{ e_{k} \middle| k \in K \right\} \right\rangle, with associated functions η:IN+\eta:\mathcal{I} \rightarrow \mathbb{N}^{+} and ζ:IN+\zeta\mathcal{:I \rightarrow}\mathbb{N}^{+}, where

  • AA is a non-empty set, called the domain of M\mathcal{M};
  • for each iIi \in \mathcal{I}, rir_{i} is a η(i)\eta(i)-ary relation on AA;
  • for each jJj\mathcal{\in J}, fjf_{j} is a ζ(j)\zeta(j)-ary function defined on Aζ(j)A^{\zeta(j)} (the ζ(j)\zeta(j)-power Cartesian product of AA) to AA;
  • for each kKk \in K, ekAe_{k} \in A.

Definition 2: Language

A language L\mathcal{L} of the type I,J,K,η,ζ\left\langle \mathcal{I},\mathcal{J},K,\eta,\zeta \right\rangle is defined to be the set sequences consisting of the elements of the following sets: {¬, , ,=,(,),vn ,Pi ,Fj ,ck|nN,  iI,  jJ, kK}\left\{ \neg,\ \rightarrow ,\ \forall, = ,\left( , \right),v_{n}\ ,P_{i}\ ,F_{j}\ ,c_{k} \middle| n\mathbb{\in N},\ \ i\mathcal{\in I},\ \ j \in \mathcal{J}\mathrm{,}\mathrm{\ }k \in K \right\} with associated formation rules as shown below.

Terms: the set T\mathcal{T} of terms is defined as:

  • (T1) vnTv_{n} \in \mathcal{T} for any nNn\mathbb{\in N}.
  • (T2) ckTc_{k}\mathcal{\in T} for any kKk \in K.
  • (T3) If τ1, τ2,,τmT\tau_{1},\ \tau_{2},\ldots,\tau_{m} \in \mathcal{T}, Fj(τ1, τ2,,τm)TF_{j}\left( \tau_{1},\ \tau_{2},\ldots,\tau_{m} \right)\mathcal{\in T}, where ζ(j)=m\zeta\left( j \right) = m.
  • (T4) All elements of T\mathcal{T} are generated as in (T1) - (T3).

Atomic formulae: the set A\mathcal{A} of atomic formulae is defined as:

  • (A1) If τ, ιT\tau,\ \iota \in \mathcal{T}, then τ=ιA\tau = \iota \in \mathcal{A}.
  • (A2) If τ1, τ2,,τmT\tau_{1},\ \tau_{2},\ldots,\tau_{m}\mathcal{\in T}, Pi(τ1, τ2,,τm)AP_{i}\left( \tau_{1},\ \tau_{2},\ldots,\tau_{m} \right)\mathcal{\in A}, where η(i)=m\eta\left( i \right) = m.
  • (A3) All elements of A\mathcal{A} are generated as in (A1) - (A2).

Formulae: the set F\mathcal{F} of formulae is defined as:

  • (F1) AF\mathcal{A} \subset \mathcal{F}.
  • (F2) If ϕF\phi \in \mathcal{F}, then ¬ϕF\neg\phi \in \mathcal{F}.
  • (F3) If ϕ, θF\phi,\ \theta\mathcal{\in F}, then ϕθF\phi \rightarrow \theta\mathcal{\in F}.
  • (F4) If ϕF\phi \in \mathcal{F} and nNn\mathbb{\in N} then vnϕF\forall v_{n}\phi \in \mathcal{F}.
  • (F5) All elements of F\mathcal{F} are generated as in (F1) - (F4).

Definition 3: Assignment

An assignment ς\varsigma of a structure M=A,R,F,ek\mathcal{M =}\left\langle A,R,F,\left\langle e_{k} \right\rangle \right\rangle is a function defined on N\mathbb{N} to AA.

Definition 4: Semantic Value

For τT\tau \in \mathcal{T}, a structure M\mathcal{M} and an assignment ς\varsigma of M\mathcal{M}, we define the semantic value of τ\bm{\tau} at at ς\bm{\varsigma} in M\bm{\mathcal{M}}, notated by τM[ς]\tau^{\mathcal{M}}\left\lbrack \varsigma \right\rbrack, as:

    1. Case 1: τ=vn\tau = v_{n}, for some nNn \in \mathbb{N}, τM[ς]=ζ(n)\tau^{\mathcal{M}}\left\lbrack \varsigma \right\rbrack = \zeta\left( n \right).
    1. Case 2: τ=ck\tau = c_{k}, for some kKk \in K, τM[ς]=ek\tau^{\mathcal{M}}\left\lbrack \varsigma \right\rbrack = e_{k}.
    1. Case 3: τ=Fj(τ1,,τζ(j))\tau = F_{j}\left( \tau_{1},\ldots,\tau_{\zeta(j)} \right), for some jJj \in \mathcal{J} and τ1,,τζ(j)T\tau_{1},\ldots,\tau_{\zeta\left( j \right)} \in \mathcal{T}, τM[ς]=fj(τ1M[ς],,τζ(j)M[ς])\tau^{\mathcal{M}}\left\lbrack \varsigma \right\rbrack = f_{j}\left( {\tau_{1}}^{\mathcal{M}}\left\lbrack \varsigma \right\rbrack,\ldots,{\tau_{\zeta(j)}}^{\mathcal{M}}\left\lbrack \varsigma \right\rbrack \right).

Definition 5: Tarski's Definition of Satisfaction

For a sentence ϕ\phi in L\mathcal{L}, a structure M\mathcal{M}, and an assignment ς\varsigma of M\mathcal{M}, the satisfaction of ϕ\mathbf{\phi} at ς\mathbf{\varsigma} in M\mathcal{M}, notated by Mςϕ\mathcal{M} \vDash_{\varsigma}\phi, is defined by:

    1. ϕA\phi \in \mathcal{A}:
      1. ϕ\phi is the form of τ=ι\tau = \iota: τM[ς]\tau^{\mathcal{M}}\left\lbrack \varsigma \right\rbrack equals to τM[ι]\tau^{\mathcal{M}}\left\lbrack \iota \right\rbrack.
      1. ϕ\phi is the form of Pi(τ1, τ2,,τζ(i))P_{i}\left( \tau_{1},\ \tau_{2},\ldots,\tau_{\zeta(i)} \right): riτ1, τ2,,τζ(i)Rr_{i}\left\langle \tau_{1},\ \tau_{2},\ldots,\tau_{\zeta(i)} \right\rangle \in R.
    1. ϕ\phi is the form of ¬θ\neg\theta: it is not the case that Mςθ\mathcal{M} \vDash_{\varsigma}\theta.
    1. ϕ\phi is the form of θψ\theta \rightarrow \psi: Mς¬θ\mathcal{M} \vDash_{\varsigma}\neg\theta or Mςψ\mathcal{M} \vDash_{\varsigma}\psi.
    1. ϕ\phi is the form of vθ\forall v\theta: for all aAa \in A, Mς(i/a)θ\mathcal{M} \vDash_{\varsigma(i/a)}\theta, where ς(i/a)\varsigma(i/a) is the assignment defined by

ς(i/a)(n)={ς(j)if jnaif j=n\varsigma(i/a)(n) = \begin{cases}\varsigma (j) &\text{if } j \neq n \\ a &\text{if } j = n \end{cases}

The Preparation

Definition 6: Henkin Theory

TT is a Henkin theory in a language L\mathcal{L} iff} for any xϕ\exists x\phi, there is a constant cc in L\mathcal{L} such that (xϕϕ(x/c))T(\exists x\phi \rightarrow \phi(x/c)) \in T. Such cc is called a Henkin witness in L\mathcal{L} of xϕ\exists x\phi (notated by cxϕc_{\exists x\phi}).

Definition 7: Alphabet Extension

If L\mathcal{L} is a language. A language L+\mathcal{L}^{+} is called an alphabet extension (or constant extension) of L\mathcal{L}, iff L+\mathcal{L}^{+} is obtained by numerable steps of adding a new constant to L\mathcal{L}.

Property 1

If Γ\Gamma is a consistent set in L\mathcal{L}, then, for any formula xϕ\exists x\phi and cc is a Henkin witness in L+(L)\mathcal{L}^{+}\mathcal{( \supset L)} (but not in L\mathcal{L}) of xϕ\exists x\phi, Γ{xϕϕ(x/c)}\Gamma \cup \left\{ \exists x\phi \rightarrow \phi(x/c) \right\} is consistent.

Proof.

Suppose Γ{xϕϕ(x/c)}\Gamma \cup \left\{ \exists x\phi \rightarrow \phi(x/c) \right\} is inconsistent.

(⇒) Γ¬(xϕϕ(x/c))\Gamma \vdash \neg(\exists x\phi \rightarrow \phi(x/c)).

(⇒) Γxϕ\Gamma \vdash \exists x\phi and Γ¬ϕ(x/c)\Gamma \vdash \neg\phi(x/c).

(⇒) Γx¬ϕ\Gamma \vdash \forall x\neg\phi since cc does not occur in any formula of Γ\Gamma (by rule of Generalization and Γ¬ϕ(x/c)\Gamma \vdash \neg\phi(x/c)).

(⇒) Γ¬xϕ\Gamma \vdash \neg\exists x\phi.

(⇒) Then Γ\Gamma is inconsistent. A contradiction.

Definition 8: Deductive Closure

Given Γ\Gamma is a set of sentences in L\mathcal{L}. Γ\overline{\Gamma} is called a deductive closure of Γ\Gamma in L\mathcal{L}, iff Γ={ϕ|Γϕ}\overline{\Gamma} = \left\{ \phi \middle| \Gamma \vdash \phi \right\}, which ϕ\phi is in L\mathcal{L}.

Property 2

A set of sentences Γ\Gamma is a consistent, iff Γ\overline{\Gamma} is a consistent.

Proof.

Trivial.

The Proof

Lemma 1: Full Extension

For any consistent set of sentences Γ\Gamma in L\mathcal{L}, there is a set of sentences Σ\Sigma in L+\mathcal{L}^{+} such that (1) ΓΣ\Gamma \subset \Sigma and (2) Σ\Sigma is a consistent Henkin theory in L+\mathcal{L}^{+}.

Proof.

Given Γ\Gamma is a consistent set in L\mathcal{L}.

We define the sequences Γn\left\langle \Gamma_{n} \right\rangle recursively:

  1. Γ0=Γ\Gamma_{0} = \Gamma and L0=L\mathcal{L}_{0}\mathcal{= L};
  2. Γk=Γk1{xk1ϕk1ϕk1(xk1/cxk1ϕk1)}\Gamma_{k} = \Gamma_{k - 1} \cup \left\{ \exists x_{k - 1}\phi_{k - 1} \rightarrow \phi_{k - 1}(x_{k - 1}/c_{\exists x_{k - 1}\phi_{k - 1}}) \right\} and Lk=Lk1+{cxk1ϕk1}\mathcal{L}_{k} = \mathcal{L}_{k - 1} + \left\{ c_{\exists x_{k - 1}\phi_{k - 1}} \right\}, where ck1c_{k - 1} is a new Henkin constant of xk1ϕk1\exists x_{k - 1}\phi_{k - 1}.

Then we define Γ=k=0Γk\Gamma^{*} = \bigcup_{k = 0}^{\infty}\Gamma_{k} andL+=k=0Lk\mathcal{L}^{+} = \bigcup_{k = 0}^{\infty}\mathcal{L}_{k}.

By Property 1, Γn\Gamma_{n} is consistent for any nn (easily proved by induction), and Γn\left\langle \Gamma_{n} \right\rangle is a chain. Therefore, Γ\Gamma^{*} should be consistent unless entail a contradiction. So do Γ\overline{\Gamma^{*}} by Property 2.

For any xϕ\exists x\phi such that Γxϕ\overline{\Gamma^{*}} \vdash \exists x\phi, there is some nn such that xϕ\exists x\phi is equal to xnϕn\exists x_{n}\phi_{n} and Γ xnϕnϕn(xn/cxnϕn)\Gamma^{*}\ \vdash \exists x_{n}\phi_{n} \rightarrow \phi_{n}(x_{n}/c_{\exists x_{n}\phi_{n}})

(⇒) xnϕnϕn(xn/cxnϕn)Γ\exists x_{n}\phi_{n} \rightarrow \phi_{n}(x_{n}/c_{\exists x_{n}\phi_{n}}) \in \overline{\Gamma^{*}} by definition.

(⇒) Γ\overline{\Gamma^{*}} is a Henkin theory in L+\mathcal{L}^{+}.

Definition 9: Syntactic Complete

A set of sentences in L\mathcal{L}, Γ\Gamma, is complete iff, for any ϕ\phi in L\mathcal{L}, either Γϕ\Gamma \vdash \phi or Γ¬ϕ\Gamma \vdash \neg\phi. If Σ\Sigma is a subset of Γ\Gamma, we say Γ\Gamma is a complete extension of Σ\Sigma.

Lemma 2: Complete Extension

For any consistent set of sentences Γ\Gamma in L\mathcal{L}, there is a set of sentences Σ\Sigma in L\mathcal{L} such that Σ\Sigma is a consistent complete extension of Γ\Gamma in L\mathcal{L}.

Proof.

Given Γ\Gamma is a consistent set in L\mathcal{L}. We define the sequences Γn\left\langle \Gamma_{n} \right\rangle recursively:

  1. Γ0=Γ\Gamma_{0} = \Gamma
  2. Γk=Γk1{ϕk1}\Gamma_{k} = \Gamma_{k - 1} \cup \left\{ \phi_{k - 1} \right\} if Γk1{ϕk1}\Gamma_{k - 1} \cup \left\{ \phi_{k - 1} \right\} is consistent, Γk=Γk1\Gamma_{k} = \Gamma_{k - 1} otherwise, where ϕn\left\langle \phi_{n} \right\rangle is the sequence of all sentences in L\mathcal{L}.

Then we define Γ=k=0Γk\Gamma^{*} = \bigcup_{k = 0}^{\infty}\Gamma_{k}.

Easily check Γ\Gamma^{*} is consistent and complete.

The Extension Lemma

For any consistent set of sentences Γ\Gamma in L\mathcal{L}, we can extend Γ\Gamma to a consistent complete Henkin theory in L+\mathcal{L}^{+}.

Proof.

So far, we have these two lemmas:

  • For any consistent set of sentences Γ\Gamma in L\mathcal{L}, we can extend Γ\Gamma to a consistent Henkin theory Γ\Gamma^{*} in L+\mathcal{L}^{+}. We can call Γ\Gamma^{*} a full-extension Γ\Gamma.
  • For any consistent set of sentences Γ\Gamma in L\mathcal{L}, we can extend Γ\Gamma to a consistent complete set Γ\Gamma^{*} in L\mathcal{L}. We can call Γ\Gamma^{*} a complete-extension of Γ\Gamma.

Given Γ\Gamma is a consistent set in L\mathcal{L}.

We define the sequences Γn\left\langle \Gamma_{n} \right\rangle, Σn\left\langle \Sigma_{n} \right\rangle and Ln\left\langle \mathcal{L}_{n} \right\rangle recursively:

  1. Γ0=Γ\Gamma_{0} = \Gamma,  L0=L\ \mathcal{L}_{0}\mathcal{= L};
  2. Define Σn\Sigma_{n} as a full-extension of Γn1\Gamma_{n - 1} in Ln\mathcal{L}_{n} (defined as the language defined as the proof of Lemma 1), Γn\Gamma_{n} as a compete-extension of Σn\Sigma_{n}.

Then we define Γ=k=0Γk\Gamma^{*} = \bigcup_{k = 0}^{\infty}\Gamma_{k}, Σ=k=1Σk\Sigma^{*} = \bigcup_{k = 1}^{\infty}\Sigma_{k} and L+=k=1Lk\mathcal{L}^{+} = \bigcup_{k = 1}^{\infty}\mathcal{L}_{k}.

We can easily check Γ=Σ\Gamma^{*} = \Sigma^{*}.

So Γ\Gamma^{*} is a consistent complete Henkin theory in L+\mathcal{L}^{+} which contains Γ\Gamma.

The Model Existence Lemma

If a set of sentences Γ\Gamma is a complete consistent Henkin theory in L\mathcal{L}, then Γ\Gamma has a model.

Proof.

Let {Pn}\left\{ P_{n} \right\} be the set of predicate symbols in L\mathcal{L} and {cn}\left\{ c_{n} \right\} be the set of all constants in L\mathcal{L}, nNn\mathbb{\in N}.

We can define a relation on terms \sim as: ιτ\iota\sim\tau iff Γι=τ\Gamma \vdash \iota = \tau. \sim has these properties:

  • Reflexivity: For any constant ι\iota, Γι=ι\Gamma \vdash \iota = \iota.
  • Symmetry: For any constant ι\iota and τ\tau, if Γι=τ\Gamma \vdash \iota = \tau, then Γτ=ι\Gamma \vdash \tau = \iota.
  • Transitivity: For any constant ι\iota, τ\tau and π\pi, if Γι=τ\Gamma \vdash \iota = \tau and Γτ=π\Gamma \vdash \tau = \pi, then Γι=π\Gamma \vdash \iota = \pi.

That is, \sim is an equivalence relation. And we can define an equivalence class by [ι]{ι}/\left\lbrack \iota \right\rbrack \in \left\{ \iota \right\}/\sim.

Let M=A, R={ri|iI},F={fj|iJ},E={ek}\mathcal{M =}\left\langle A,\ R = \left\{ r_{i} \middle| i\mathcal{\in I} \right\},F = \left\{ f_{j} \middle| i \in \mathcal{J} \right\},E = \left\{ e_{k} \right\} \right\rangle with η:IN+\eta\mathcal{:I \rightarrow}\mathbb{N}^{+} and ζ:JN+\zeta:\mathcal{J \rightarrow}\mathbb{N}^{+}:

  1. We define A={[cn]}A = \left\{ \left\lbrack c_{n} \right\rbrack \right\}.
  2. Suppose PiP_{i} is an kik_{i}-ary relation of L\mathcal{L}, we define rir_{i} and η\eta as: ri([τ1],[τ2],,[τki])r_{i}\left( \left\lbrack \tau_{1} \right\rbrack,\left\lbrack \tau_{2} \right\rbrack,\ldots,\left\lbrack \tau_{k_{i}} \right\rbrack \right) iff Pi(τ1,τ2,,τki) Γ P_{i}\left( \tau_{1},\tau_{2},\ldots,\tau_{k_{i}} \right) \in \text{\ Γ}\ and η(i)=ki\eta\left( i \right) = k_{i}.
  3. Suppose FjF_{j} is an kjk_{j}-ary function of L\mathcal{L}, we define fjf_{j} and ζ\zeta as: fj([τ1],[τ2],,[τkj])=Fj(τ1,τ2,,τkj)f_{j}\left( \left\lbrack \tau_{1} \right\rbrack,\left\lbrack \tau_{2} \right\rbrack,\ldots,\left\lbrack \tau_{k_{j}} \right\rbrack \right) = F_{j}\left( \tau_{1},\tau_{2},\ldots,\tau_{k_{j}} \right) and ζ(j)=kj\zeta\left( j \right) = k_{j}.
  4. We define ek=[ck]e_{k} = \left\lbrack c_{k} \right\rbrack.

We need to show that, for any ϕ\phi in L\mathcal{L}, Mϕ\mathcal{M \vDash}\phi, iff Γϕ\Gamma \vdash \phi. Note: we can also define the assignment function ς:NA\varsigma\mathbb{:N \rightarrow}A.

Basis case: ϕ\phi is atomic.

Case 1: ϕ\phi is the form of τ=ι\tau = \iota.

Mϕ\mathcal{M \vDash}\phi.

(⇔) For any ς\varsigma, Mςϕ\mathcal{M} \vDash_{\varsigma}\phi i.e. Mςτ=ι\mathcal{M} \vDash_{\varsigma}\tau = \iota.

(⇔) For any ς\varsigma, τM[ς]=ιM[ς]\tau^{\mathcal{M}}\lbrack\varsigma\rbrack = \iota^{\mathcal{M}}\lbrack\varsigma\rbrack.

(⇔) For any ς\varsigma, τM[ς]ιM[ς]\tau^{\mathcal{M}}\lbrack\varsigma\rbrack\sim\iota^{\mathcal{M}}\lbrack\varsigma\rbrack.

(⇔) Γτ=ι\Gamma \vdash \tau = \iota.

(⇔) Γϕ\Gamma \vdash \phi.

Case 2: ϕ\phi is the form of P(τ1,τ2,,τn)P(\tau_{1},\tau_{2},\ldots,\tau_{n}).

Mϕ\mathcal{M \vDash}\phi.

(⇔) For any ς\varsigma, Mςϕ\mathcal{M} \vDash_{\varsigma}\phi i.e. MςP(τ1,τ2,,τn)\mathcal{M} \vDash_{\varsigma}P(\tau_{1},\tau_{2},\ldots,\tau_{n}).

(⇔) For any ς\varsigma, there is some ii, such that ri(τ1M[ς],τ2M[ς],,τnM[ς])r_{i}\left( {\tau_{1}}^{\mathcal{M}}\lbrack\varsigma\rbrack,{\tau_{2}}^{\mathcal{M}}\lbrack\varsigma\rbrack,\ldots,{\tau_{n}}^{\mathcal{M}}\lbrack\varsigma\rbrack \right).

(⇔) ΓP(τ1,τ2,,τn)\Gamma \vdash P(\tau_{1},\tau_{2},\ldots,\tau_{n}).

(⇔) Γϕ\Gamma \vdash \phi.

Inductive step: for some ϕ\phi, we assume that all proper subformulae of ϕ\phi hold the result as the inductive hypothesis.

Case 1: ϕ\phi is the form of ¬ψ\neg\psi. Clearly hold by definition and completeness of Γ\Gamma.

Case 2: ϕ\phi is the form ψθ\psi \rightarrow \theta.

Mϕ\mathcal{M \vDash}\phi i.e. Mψθ\mathcal{M \vDash}\psi \rightarrow \theta.

(⇔) M¬ψ\mathcal{M \vDash \neg}\psi or Mθ\mathcal{M \vDash}\theta.

(⇔) Γ¬ψ\Gamma \vdash \neg\psi or Γθ\Gamma \vdash \theta (by the inductive hypothesis).

(⇔) Γψθ\Gamma \vdash \psi \rightarrow \theta.

(⇔) Γϕ\Gamma \vdash \phi.

Case 3: ϕ\phi is the form xψ\forall x\psi, and, WLOG, we suppose the variables of ψ\psi is (τ1,τ2,,τn1, x)(\tau_{1},\tau_{2},\ldots,\tau_{n - 1},\ x).

Mϕ\mathcal{M \vDash}\phi.

(⇔) For any ς\varsigma, Mςϕ\mathcal{M} \vDash_{\varsigma}\phi i.e. Mςxψ\mathcal{M} \vDash_{\varsigma}\forall x\psi.

(⇔) For any ς\varsigma and [c]A\lbrack c\rbrack \in A, Mς(i/[c])ψ\mathcal{M} \vDash_{\varsigma(i/\lbrack c\rbrack)}\psi.

(⇔) For any [c]A\lbrack c\rbrack \in A, Γψ(τ1,τ2,,τn1,c)\Gamma \vdash \psi(\tau_{1},\tau_{2},\ldots,\tau_{n - 1},c) (by the inductive hypothesis).

(⇔) Γxψ\Gamma \vdash \forall x\psi.

(⇔) Γϕ\Gamma \vdash \phi.

So, for any ϕ\phi in L\mathcal{L}, Mϕ\mathcal{M \vDash}\phi, iff Γϕ\Gamma \vdash \phi.}

Completeness Theorem

If Γϕ\Gamma \vDash \phi, then Γϕ\Gamma \vdash \phi where ϕ\phi is a sentence in LCPL\mathcal{L}_{\text{CPL}} and Γ\Gamma is a set of sentences in LCPL\mathcal{L}_{\text{CPL}}.

Proof.

Suppose Γϕ\Gamma \vDash \phi but Γϕ\Gamma \nvdash \phi.

(⇒) Γ{¬ϕ}\Gamma \cup \left\{ \neg\phi \right\} is constant.

(⇒) There is a consistent complete Henkin theory Γ\Gamma^{*} in LCPL+{\mathcal{L}_{\text{CPL}}}^{+} contains Γ{¬ϕ}\Gamma \cup \left\{ \neg\phi \right\} (by ).

(⇒) There is a model M\mathcal{M} such that MΓ{¬ϕ}\mathcal{M \vDash}\Gamma \cup \left\{ \neg\phi \right\} in LCPL+{\mathcal{L}_{\text{CPL}}}^{+} (by ). But it is impossible: if Γϕ\Gamma \vDash \phi in L\mathcal{L}, then Γϕ\Gamma \vDash \phi in L+\mathcal{L}^{+}.

So, Γϕ\Gamma \vdash \phi.


如果你喜歡這篇文章,請不吝用實際行動支持我: