Before：稍有强度的一周，主要表现在…超级大的数学物理数理逻辑强度，但感觉经过3、4天的摸爬滚打，基本上还是搞明白了😇还有平安度过的XZJT（感觉还是挺成功的？maybe）继续加油！

ps：昨天小姐姐double happy了🥰🥰

Mathematical Logic 6

Call back: Introduction to Sequent Calculus

10 Basic Rules

1. Antecedent

2. Assumption

3. Case Analysis

4. Contradiction

5. V-introduction in antecedent

6. V-introduction in succedent

7. ∃ -introduction in succedent

8. ∃ -introduction in antecedent

9. Equality

10. Substitution

Every Basic Rules is correct.(can be proved)

Derived Rules 1

1. Excluded middle

2. Modified Contradiction

3. Chain Deduction

Derived Rules 2
Modus Ponens
$\Gamma \vdash \varphi \rightarrow \psi $
$\Gamma \vdash \varphi$
—————————
$\Gamma \vdash \psi$
Derived Rules 3
1.Symmetry of $\equiv$
$\Gamma \vdash t_1 \equiv t_2$
—————————
$\Gamma \vdash t_2 \equiv t_1$

2.Transitivity of $\equiv$
$\Gamma \vdash t_1 \equiv t_2$
$\Gamma \vdash t_2 \equiv t_3$
—————————
$\Gamma \vdash t_1 \equiv t_3$

3.For n-ary relation symbol R $\in$ S
can be proved by using Substitution Lemma
$\Gamma \vdash R t_1 \ldots t_n $
$\Gamma \vdash t_1 \equiv t’_1 $
$\Gamma \vdash t_2 \equiv t’_2 $
$\cdots \cdots$
$\Gamma \vdash t_n \equiv t’_n $
—————————
$\Gamma \vdash R t’_1 \ldots t’_n$

4.For n-ary function symbol R $\in$ S
can also be proved by using Substitution Lemma
$\Gamma \vdash t_1 \equiv t’_1 $
$\Gamma \vdash t_2 \equiv t’_2 $
$\cdots \cdots$
$\Gamma \vdash t_n \equiv t’_n $
—————————
$\Gamma \vdash f t_1 \ldots t_n \equiv f t’_1 \ldots t’_n$

Soundness

• Defintion

• Lemma 1

• Theorem 2(Soundness)
  If $\Phi \vdash \varphi$,then $\Phi \vDash \varphi$

Opposite is Completeness and we will prove it in later lessons.

Consistency

Defintion
$\Phi$ is consistent if there is no $\varphi$ such that both $\Phi$ ⊢ $\varphi$ and $\Phi$ ⊢ $\neg$$\varphi$. Otherwise,$\Phi$ is inconsistent.

Lemma3: $\Phi$ is inconsistent if and only if $\Phi \vdash \varphi$ for any formulas $\varphi$.
This can be proved by using Modified Contradiction.

Lemma 4: $\Phi$ is consistent if and only if there is a $\varphi$ such that $\Phi \not\models \varphi$.
This can be proved by using Modified Contradiction.

Lemma 5: $\Phi$ is consistent if and only if every finite $\Phi_0 \subset \Phi$

Lemma 6: Every satisfiable $\Phi$ is consistent.
(Prove from the negative perspective using soundness and build a model)

Lemma 7:
(1) $\Phi \vdash \varphi$ if and only if $\Phi \cup \neg\varphi$ is inconsistent.

Easy to prove.

(2) $\Phi \vdash \neg\varphi$ if and only if $\Phi \cup \varphi$ is inconsistent.

(3)If cons($\Phi$),then either cons($\Phi \cup \varphi$) or cons($\Phi \cup \neg\varphi$).

So the end of Sequent Calculus.

Start of Question 2: What makes a proof correct?

能证的都是对的（soundness），对的都是能证的（Completeness完备性）。

Theorem 8
If $\Phi \models \varphi$,$\Phi \vdash \varphi$

Theorem 9
cons($\Phi$) implies that $\Phi$ is satisfiable.

Term Model（version 1）

Define the term model $\mathcal{I}^\Phi(t)$ so that for every t $\in T^S$.
$\mathcal{I}^\Phi(t) = t$
把语法对象作为语义的universe
That is, the interpretation of an S-term $t$ is the syntax object $t \in T^S$ itself.

Universe：A = $T^S$
n-ary function symbol：
$f^A(t_1, \ldots, t_n) := f t_1 \ldots t_n.$

n-ary relation symbol：
$R^A = {(t_1, \ldots, t_n) | \Phi \vdash R t_1 \ldots t_n}.$

$c^A := c$ and $\beta(v_i) := v_i$ for every variable $v_i$

But：we will meet a problem.
Let S = {f} where f is a function symbol and $\Phi:={fv_0 \equiv fv_1}$

• $\mathcal{I}^\Phi(fv_0) = fv_0 \neq fv_1 = \mathcal{I}^\Phi(fv_1)$(2 strings are not the same)

• $\mathcal{I}^\Phi \models \Phi$ implies that $\mathcal{I}^\Phi(fv_0) = \mathcal{I}^\Phi(fv_1)$

Contradict!😢😰😢😰
To Overcome The Issue!
在项的集合上定义一个等价关系，define an equivalence relation ~ on $T^S$

Let $t_1$, $t_2$ $\in T^S$.Then $t_1$ ~ $t_2$ if $\Phi \vdash t_1 \equiv t_2$.
(Easy to prove equivalence relation)

Introduce the Equivalence Class of t.
For every $t \in T^S$ we define:
$\overline{t} := {t’ \in T^S \mid t’ \sim t}$

Through Derived Rules 3,we can prove that:

• For every $n$-ary function symbol $f \in S$ and terms $t_1 \sim t_1’, \ldots, t_n \sim t_n’$, we have
  $f t_1 \cdots t_n \sim f t_1’ \cdots t_n’.$

• For every $n$-ary relation symbol $R \in S$ and terms $t_1 \sim t_1’, \ldots, t_n \sim t_n’$, we have
  $\Phi \vdash R t_1 \cdots t_n \iff \Phi \vdash R t_1’ \cdots t_n’.$

So we will introduce…

Term Model（version 2）!!!

The term structure for $\Phi$, denoted by $\mathfrak{T}^{\Phi}$, is defined as follows.

(i) The universe is ${T}^{\Phi} := {\overline{t} \mid t \in T^S}$.

(ii) For every $n$-ary relation symbol $R \in S$, and $\overline{t}_1, \ldots, \overline{t}_n \in T^{\Phi}$

$(\overline{t}_1, \ldots, \overline{t}_n)$ $\in {R}^\mathfrak{T}{\Phi} \text{if} \Phi \vdash R t_1 \ldots t_n.$

(iii) For every $n$-ary function symbol $f \in S$, and $\overline{t}_1, \ldots, \overline{t}_n \in T^{\Phi}$

${f}^\mathfrak{T}{\Phi}$ $(\overline{t}_1, \ldots, \overline{t}_n)$ := $\overline{f t_1 \ldots t_n}.$

(iv) For every constant $c \in S$
${c}^\mathfrak{T}{\Phi}$ := $\overline{c}.$

And we still need an assignment:
$\mathfrak{\beta}^{\Phi}(v_i):= \overline{v_i}$

So we have the Heenkin’s term model:
$\mathfrak{I}^{{\Phi}$:=($\mathfrak{T}}{\Phi},\mathfrak{\beta}^{\Phi}$)

Lemma 11:
(1)For any $t$ $\in T^S$:
$\mathfrak{I}^{\Phi}(t) = \overline{t}$

(2)For every atomic $\varphi$
$\mathfrak{I}^{\Phi} \models \varphi \iff \Phi \vdash \varphi$