Inference Rules and Proof Theory

Negating a proposition

General rules:

• $\lnot \forall x \phi \equiv \exists x \not \phi$
• $\lnot \exists x \phi \equiv \forall x \lnot \phi$
• $\lnot \forall x(\phi \to \psi) \equiv \exists x(\phi \land \lnot \psi)$
• $\lnot \exists x(\phi \land \psi) \equiv \forall x(\phi \to \lnot \psi)$
• $\lnot (\phi \land \psi) \equiv \lnot \phi \lor \lnot \psi$
• $\lnot (\phi \lor \psi)\equiv \lnot \phi \land \psi$
• $\lnot (\phi\to \psi)\equiv \phi \land \lnot \psi$

Example
Proof of:

$$\lnot \exists x \in \mathbb{N}. \exists y \in \mathbb{N}. \gcd(x, y) = 1 \text{ and } x^2 = 2y^2.$$

Suppose there exists $x \in \mathbb{N}$ and $y \in \mathbb{N}$ s.t. $x^2 = 2y^2$.
Thus, $x$ must be an even number and we can assume $x = 2x_0$.
Now, we have $y^2 = 2x_0^2$.
Thus, $y$ must be an even number too and we can assume $y = 2y_0$.
Therefore, $\gcd(x, y) \neq 1$.
Qed.

Proof step: In order to prove $\lnot \exists x \in \mathbb{N}. \exists y \in \mathbb{N}. \gcd(x, y) = 1 \text{ and } x^2 = 2y^2$, it suffices to prove that if $x \in \mathbb{N}$, $y \in \mathbb{N}$ and $x^2 = 2y^2$ then $\gcd(x, y) \neq 1$.

Logic: The negation of $\exists x (\psi_1 \land \exists y (\psi_2 \land \psi_3 \land \chi))$ is $\forall x (\psi_1 \rightarrow \forall y (\psi_2 \rightarrow (\psi_3 \rightarrow \lnot \chi)))$.

证明逻辑：

$$\begin{aligned} &\Phi\vdash\lnot \exists x(\psi_1\land\exists y(\psi_{2}\land(\psi_{3}\land\chi)))\\ \impliedby& \Phi\vdash\forall x(\psi_1\to \forall y (\psi_{2}\rightarrow(\psi_{3}\rightarrow \lnot \chi)))\\ \impliedby& \Phi\vdash \psi_1\to \forall y (\psi_{2}\rightarrow(\psi_{3}\rightarrow \lnot \chi)) \quad (x \text{ does not freely occur in } \Phi) \\ \impliedby&\Phi,\psi_{1}\vdash\forall y (\psi_{2}\rightarrow(\psi_{3}\rightarrow \lnot \chi))\\ \impliedby&\Phi,\psi_{1}\vdash \psi_{2}\rightarrow(\psi_{3}\rightarrow \lnot \chi) \quad (y \text{ does not freely occur in } \Phi, \psi_1) \\ \impliedby&\Phi,\psi_{1}, \psi_2, \psi_3 \vdash \lnot \chi \end{aligned}$$

Important properties of logic equivalence and consequence relation

Theorem 4

• $\forall x\ (\phi \wedge \psi) \equiv \forall x\phi \wedge \forall x\psi$
• $\forall x\phi \vee \forall x\psi \models \forall x\ (\phi \vee \psi)$
• $\exists x\ (\phi \vee \psi) \equiv \exists x\ \phi \vee \exists x\ \psi$
• $\exists x\ (\phi \wedge \psi) \models \exists x\ \phi \wedge \exists x\ \psi$
• If $x$ does not freely occur in $\phi$, $\exists x(\phi \wedge \psi) \equiv \phi \wedge \exists x\psi$
• If $x$ does not freely occur in $\phi$, $\forall x(\phi \rightarrow \psi) \equiv \phi \rightarrow \forall x\psi$
  Proof: For any $\mathcal{J}$
  $\llbracket \forall x (\phi\to \psi) \rrbracket_{\mathcal{J}} = T$
  $\iff$ for any $a$ in $\mathcal{J}$'s domain, s.t. $\llbracket \phi\to \psi \rrbracket_{\mathcal{J}} = T$
  $\iff$ for any $a$ in $\mathcal{J}$'s domain, s.t. $\llbracket \phi \boldsymbol{\rrbracket}_\mathcal{J[x\mapsto a]}=F$ or $\llbracket \psi \rrbracket_{\mathcal{J}[x\mapsto a]} = T$
  $\iff$ for any $a$ in $\mathcal{J}$'s domain, s.t. $\llbracket \phi \boldsymbol{\rrbracket}_\mathcal{J}=F$ or $\llbracket \psi \rrbracket_{\mathcal{J}[x\mapsto a]} = T$
  $\iff$ $\llbracket \phi \boldsymbol{\rrbracket}_\mathcal{J}=F$ or for any $a$ in $\mathcal{J}$'s domain, s.t. $\llbracket \psi \rrbracket_{\mathcal{J}[x\mapsto a]} = T$
  $\iff$ $\llbracket \phi\to \forall x\psi \rrbracket_{\mathcal{J}} = T$
  Qed

Theorem 5

• $\forall x\forall y\phi \equiv \forall y\forall x\phi$
• If $x$ does not freely occur in $\phi_{2}$ and $y$ does not freely occur in $\phi_{1}$, then $\forall x(\phi_{1} \rightarrow \forall y(\phi_{2} \rightarrow \psi)) \equiv \forall y(\phi_{2} \rightarrow \forall x(\phi_{1} \rightarrow \psi))$
  Proof:

  $$\begin{aligned} &\forall x(\phi_{1} \rightarrow \forall y(\phi_{2} \rightarrow \psi)) \\ \equiv & \forall x \forall y (\phi_1 \to (\phi_2 \to \psi)) \\ \equiv & \forall x\forall y(\phi_1 \land \phi_2\to \psi) \\ \equiv &\forall x\forall y(\phi_2\to (\phi_1\to \psi))\\ \equiv &\forall y\forall x(\phi_2\to (\phi_1\to \psi))\\ \equiv &\forall y(\phi_2\to \forall x(\phi_1\to \psi))\\ \end{aligned}$$

• $\exists x\exists y\phi \equiv \exists y\exists x\phi$
• If $x$ does not freely occur in $\phi_{2}$ and $y$ does not freely occur in $\phi_{1}$, then $\exists x(\phi_{1} \land \exists y(\phi_{2} \land \psi)) \equiv \exists y(\phi_{2} \land \exists x(\phi_{1} \land \psi))$
• $\exists x\forall y\phi \models \forall y\exists x\phi$

Inference Rules and Proof Theory

Proof theory is an independent theory to the semantic theory.

Definition 6 (The natural deduction system). $\Phi \vdash \psi$ ($\Phi$ derives $\psi$) if and only if it can be established by the following proof rules in finite steps:

• $\forall x \phi \vdash \phi[x \mapsto t]$; $\quad \phi[x \mapsto t] \vdash \exists x \phi$;

• If $\Phi \vdash \psi$ and $x$ does not freely occur in $\Phi$, then $\Phi \vdash \forall x \psi$.

• If $\Phi, \psi \vdash \chi$ and $x$ does not freely occur in $\Phi$ or $\chi$, then $\Phi, \exists x \psi \vdash \chi$.

• $\phi, \psi \vdash \phi \land \psi$; $\quad \phi \land \psi \vdash \phi$; $\quad \phi \land \psi \vdash \psi$

• $\phi \vdash \phi \lor \psi$; $\quad \psi \vdash \phi \lor \psi$

• If $\Phi, \phi_1 \vdash \psi$ and $\Phi, \phi_2 \vdash \psi$, then $\Phi, \phi_1 \lor \phi_2 \vdash \psi$

• $\Phi \vdash \psi \lor \neg \psi$

• $\Phi, \psi, \neg \psi \vdash \chi$

• If $\phi \in \Phi$, then $\Phi \vdash \phi$

• If $\Phi \subseteq \Psi$ and $\Phi \vdash \phi$, then $\Psi \vdash \phi$

• If $\Phi \vdash \psi$ and $\Phi \vdash \psi \rightarrow \chi$, then $\Phi \vdash \chi$.

• If $\Phi, \psi \vdash \chi$, then $\Phi \vdash \psi \rightarrow \chi$.