Đến nội dung


Chú ý

Nếu các bạn đăng kí thành viên mà không nhận được email kích hoạt thì hãy kiểm tra thùng thư rác (spam). Nếu không biết cách truy cập vào thùng thư rác thì các bạn chịu khó Google hoặc đăng câu hỏi vào mục Hướng dẫn - Trợ giúp để thành viên khác có thể hỗ trợ.


Hình ảnh

Logic bậc nhất: Tính đúng đắn vs. tính chặt chẽ

logic

  • Please log in to reply
Chủ đề này có 4 trả lời

#1 nmlinh16

nmlinh16

    Binh nhất

  • Thành viên mới
  • 25 Bài viết
  • Giới tính:Nam
  • Đến từ:Hạ Long
  • Sở thích:Algebraic invariant theory, Algebraic topology, Analytic number theory

Đã gửi 14-01-2020 - 22:48

Khác với định lý về tính không đầy đủ (incompleteness theorem) của Gödel, định lý về tính đầy đủ (completeness theorem) ít được biết đến (và bị xuyên tạc) với đại chúng hơn. Lý do là vì phát biểu của định lý này trông "có vẻ" không có gì đặc biệt. Định lý được hiểu nôm na như sau: (trong logic bậc nhất) cái gì chứng minh được thì luôn đúng, cái gì luôn đúng thì chứng minh được. Nghe thật lạ. Thế nào gọi là đúng? Chẳng phải đó "chứng minh" có nghĩa là như vậy sao? Không hẳn. Khái niệm "đúng" và "chứng minh" trong phát biểu trên được hiểu theo 2 khía cạnh khác nhau của logic: "đúng" là một khái niệm ngữ nghĩa (semantic), nghĩa là ta nói đến các mô hình cụ thể; "chứng minh" là một khái niệm hình thức (syntactic). Ở những bài viết này, chúng ta sẽ giới thiệu về logic bậc nhất và định lý về tính đầy đủ.

 

Định lý về tính đầy đủ là một kết quả quan trọng của logic bậc nhất. Nó liên kết lý thuyết mô hình (model theory), tức là các đối tượng ngữ nghĩa cụ thể với lý thuyết chứng minh (proof theory), tức là các thao tác trên logic hình thức. Định lý thống nhất hai khái niệm sau đây.

 

$\Phi \vDash \chi$: "Một khi $\Phi$ đúng thì $\chi$ cũng đúng" (tính đúng đắn/verity).

$\Phi \vdash \chi$: "Tồn tại một quá trình suy luân cho phép chứng minh $\chi$ từ $\Phi$" (tính chặt chẽ/rigor).

 

Hai kết quả của logic bậc nhất là định lý về tính đúng đắn (soundness theorem): Nếu $\Phi \vdash \chi$ thì $\Phi \vDash \chi$. Định lý về tính đầy đủ khẳng định điều ngược lại: Nếu $\Phi \vDash \chi$ thì $\Phi \vdash \chi$.

 

 

1. Logic bậc nhất

 

Trong logic bậc nhất, ta luôn mặc định rằng có sẵn những đối tượng sau đây.

 

1. các toán tử logic: phủ định (negation, $\neg$, "không"), hội (conjunction, $\land$, "và"), tuyển (disjunction, $\lor$, "hoặc"), kéo theo (implication, $\rightarrow$, "suy ra");

2. một tập hợp vô hạn (thường là đếm được) $\mathcal{V}$ các biến.

3. lượng từ phổ biến (universal quantifier, $\forall$, "với mọi") và lượng từ tồn tại (existential quantifier, $\exists$, "tồn tại").

4. dấu phẩy và các dấu ngoặc $($, $)$.

 

Logic bậc nhất có các quy tắc sau đây

- Các lượng từ chỉ sử dụng cho từng phần tử, KHÔNG sử dụng cho một tập hợp các phần tử, hay cho hàm số, quan hệ,...

- Các công thức logic phải hữu hạn (finitary logic), ta có thể viết $\forall x_1 \ldots \forall x_n$ để viết tắt cho $n$ lần dùng lượng từ liên tiếp, nhưng nói chung số ký hiệu trong $\ldots$ bắt buộc phải hữu hạn (và cố định). Nói riêng, không có cách nào để nói "tồn tại vô hạn... sao cho...".

 

 

Định nghĩa. Một ngôn ngữ bậc nhất (language) $\mathcal{L}$ gồm

1. các ký hiệu hằng (constant);

2. các ký hiệu quan hệ (relation); mỗi ký hiệu có một số biến (arity) là một số nguyên dương nhất định; một quan hệ $R$ với số biến bằng $n$ được gọi là một quan hệ $n$ ngôi. Thông thường, chúng ta mặc định rằng mọi ngôn ngữ đều có sẵn quan hệ hai ngôn $=$ (đẳng thức);

3. các ký hiệu hàm (function), mỗi ký hiệu có một số biến là một số nguyên dương nhất định; một quan hệ $f$ với số biến bằng $n$ được gọi là một hàm $n$ biến.

 

 

Ví dụ.

1. Ngôn ngữ nhóm $\mathcal{L}_{\text{grp}} = \{1, \,^{-1}, \cdot\}$, trong đó $1$ là một ký hiệu hằng (chỉ phần tử đơn vị), $\,^{-1}$ là một ký hiệu hàm một biến (chỉ ánh xạ nghịch đảo), $\cdot$ là một ký hiệu hàm hai biến (chỉ phép toán của nhóm).
2. Ngôn ngữ vành $\mathcal{L}_{\text{rng}} = \{0,1, +, - , \cdot\}$  (ở đây $-$ là một ký hiệu hàm một biến, tượng trưng cho "phần tử đối", thay vì phép trừ).
3. Ngôn ngữ thứ tự $\mathcal{L}_{\text{ord}} = \{<\}$.
4. Ngôn ngữ tập hợp $\mathcal{L}_{ZF} = \{\in\}$.
5. Ngôn ngữ Peano bậc nhất $\mathcal{L}_{PA} = \{0,s,+,\cdot\}$ (ở đây $s$ là một ký hiệu hàm một biến, dùng để chỉ "số liền sau" (successor)).
 
 
Giả sử $\mathcal{L}$ là một ngôn ngữ.
 

Định nghĩa. Một $\mathcal{L}$-cấu trúc (structure) gồm

1. một tập hợp nền $\mathbb{S}$;
2. với mỗi ký hiệu hằng $c \in \mathcal{L}$, một phần tử $c^{\mathbb{S}} \in \mathbb{S}$;
3. với mỗi ký hiệu quan hệ $n$ ngôi $R \in \mathcal{L}$, một tập con $R^{\mathbb{S}} \subseteq \mathbb{S}^n$;
4. với mỗi ký hiệu hàm $n$ biến $f \in \mathcal{L}$, một ánh xạ $f^{\mathbb{S}}: \mathbb{S}^n \to \mathbb{S}$.
 
 
Ví dụ. Mỗi nhóm là một $\mathcal{L}_{\text{grp}}$-cấu trúc (với cách thông dịch $1$, $\,^{-1}$ và $\cdot$ theo nghĩa thông thường). Tuy nhiên không phải mọi $\mathcal{L}_{\text{grp}}$-cấu trúc đều là một nhóm; chúng cần phải thỏa mãn các tiên đề của nhóm nữa.

 

 

Định nghĩa. Tập hợp $\mathcal{L}\text{-Term}$ các $\mathcal{L}$-biểu thức (term) là tập hợp nhỏ nhất sao cho

1. mỗi ký hiệu hằng $c \in \mathcal{L}$ là một biểu thức;

2. mỗi biến $x \in \mathcal{V}$ là một biểu thức;

3. nếu $f \in \mathcal{L}$ là một ký hiệu hàm $n$ biến và $t_1,\ldots,t_n$ là các biểu thức thì $f(t_1,\ldots,t_n)$ là một biểu thức.

 

 

Ví dụ. Trong một ngôn ngữ không có ký hiệu hàm (relational language), các biểu thức là các ký hiệu hằng và các biến.

 

 

Định nghĩa. Một phép chọn tham số (choice of parameters) là một ánh xạ $p:\mathcal{V} \to \mathbb{S}$.

 

Giả sử $t$ là một biểu thức và $p$ là một phép chọn tham số.

 

Định nghĩa. Thông dịch (interpretation) của $t$ bởi $p$ là phần tử $p(t) \in \mathbb{S}$ được xác định một cách quy nạp như sau.

1. nếu $c$ là một ký hiệu hằng, $p(c) = c^{\mathbb{S}}$;

2. nếu $x$ là một biến, $p(x)$ chính là ảnh của $x$ bởi ánh xạ $p$;

3. nếu $t$ có dạng $f(t_1,\ldots,t_n)$, $p(t) = f^\mathbb{S}(p(t_1),\ldots,p(t_n))$.

 

Định nghĩa. Tập hợp $V(t) \subseteq \mathcal{V}$ các biến của $t$ được xác định một cách quy nạp như sau.

1. nếu $c$ là một ký hiệu hằng, $V(c) = \varnothing$;

2. nếu $x$ là một biến, $V(x) = \{x\}$;

3. nếu $t$ có dạng $f(t_1,\ldots,t_n)$, $V(t) = V(t_1) \cup \cdots \cup V(t_n)$.

 

 

Ví dụ. Trong ngôn ngữ vành, $x + y \cdot z$ là một biểu thức với các biến $x, y, z$.

 

 

Bằng cách quy nạp theo độ phức tạp của biểu thức, ta có thể chứng minh dễ dàng

 

Bổ đề. Nếu $p, p'$ là hai phép chọn tham số sao cho $p|_{V(t)} = p'|_{V(t)}$ thì $p(t) = p'(t)$.

 

 

Trong bài sau, chúng ta sẽ nói về ký hiệu $\vDash$ (sự thỏa mãn).


Bài viết đã được chỉnh sửa nội dung bởi nmlinh16: 15-01-2020 - 14:39

$$x - \sum_{\substack{0 < \operatorname{Re} \rho < 1 \\ \zeta(\rho) = 0}} \frac{x^\rho}{\rho} - \log 2\pi - \frac{1}{2}\log(1-x^{-2}) = \frac{\psi(x+0) + \psi(x - 0)}{2}, \qquad \psi(x) = \sum_{\substack{p^n \le x \\  n \ge 1}} \log p.$$

 

"Wir müssen wissen, wir werden wissen." - David Hilbert


#2 nmlinh16

nmlinh16

    Binh nhất

  • Thành viên mới
  • 25 Bài viết
  • Giới tính:Nam
  • Đến từ:Hạ Long
  • Sở thích:Algebraic invariant theory, Algebraic topology, Analytic number theory

Đã gửi 15-01-2020 - 02:39

2. Sự thỏa mãn

Ta cố định một ngôn ngữ $\mathcal{L}$.

 

Định nghĩa. Tập hợp $\mathcal{L}\text{-Form}$ các $\mathcal{L}$-công thức (formula) là tập hợp nhỏ nhất sao cho

1. nếu $R \in \mathcal{L}$ (có thể là dấu $=$) là một ký hiệu hàm $n$ ngôi và $t_1,\ldots,t_n$ là các biểu thức thì $R(t_1,\ldots,t_n)$ là một công thức. Mỗi công thức như vậy được gọi là một công thức cơ sở hay công thức nguyên tử;
2. nếu $\varphi$ và $\psi$ là các công thức thì $\neg \varphi$, $\varphi \land \psi$, $\varphi \lor \psi$ và $\varphi \rightarrow \psi$ là các công thức;
3. nếu $\varphi$ là một công thức và $x$ là một biến thì $\forall x\, \varphi$ và $\exists x\, \varphi$ là các công thức.
 
Định nghĩa. Giả sử $\varphi$ là một $\mathcal{L}$-công thức. Tập hợp $V(\varphi)$ (tương ứng, $FV(\varphi)$) các biến (tương ứng, biến tự do) được xác định một cách quy nạp như sau.
1. nếu $\varphi$ có dạng $R(t_1,\ldots,t_n)$, $V(\varphi) = FV(\varphi) = V(t_1) \cup \cdots \cup V(t_n)$;
2. nếu $\varphi$ và $\psi$ là các công thức và $\boxdot$ là một trong các toán tử $\land$, $\lor$ hoặc $\rightarrow$ thì $V(\neg \varphi) = V(\varphi)$, $FV(\neg \varphi) = FV(\varphi)$, $V(\varphi \boxdot \psi) = V(\varphi) \cup V(\psi)$ và $FV(\varphi \boxdot \psi) = FV(\varphi) \cup FV(\psi)$;
3. nếu $\varphi$ là một công thức và $x$ là một biến thì $V(\forall x \,\varphi) = V(\exists x\, \varphi) = V(\varphi)$ và $FV(\forall x \,\varphi) = FV(\exists x\, \varphi) = FV(\varphi) \setminus \{x\}$.
 
Một biến không tự do của $\varphi$ được gọi là một biến phụ thuộc. Mỗi công thức không có biến tự do được gọi là một phát biểu (sentence). Ta ký hiệu tập hợp các $\mathcal{L}$-phát biểu bởi $\mathcal{L}\text{-Sent}$.
 
Ví dụ. Trong công thức $(\exists x\,x^2 = y) \rightarrow (x = y)$, lần xuất hiện thứ nhất của $x$ là phụ thuộc, nhưng lần xuất hiện thứ hai là tự do.
 
 
Ta giả sử $\mathbb{S}$ là một $\mathcal{L}$-cấu trúc và $p: \mathcal{V} \to \mathbb{S}$ là một phép chọn tham số. Cặp $(\mathbb{S},p)$ được gọi là một cấu trúc với tham số.
 
Định nghĩa. Giả sử $\varphi$ và $\psi$ là các công thức. Ta định nghĩa sự thỏa mãn của một công thức trong $\mathbb{S}$ với tham số $p$ một cách quy nạp như sau.
1. nếu $\varphi$ có dạng $R(t_1,\ldots,t_n)$ thì $\mathbb{S} \vDash \varphi(p)$ khi và chỉ khi $(p(t_1),\ldots,p(t_n)) \in R^{\mathbb{S}}$;
2. $\mathbb{S} \vDash (\neg \varphi)(p)$ khi và chỉ khi $\mathbb{S} \not\vDash \varphi(p)$;
3. $\mathbb{S} \vDash (\varphi \land \psi)(p)$ khi và chỉ khi $\mathbb{S} \vDash \varphi(p)$ và $\mathbb{S} \vDash \psi(p)$;
4. $\mathbb{S} \vDash (\varphi \lor \psi)(p)$ khi và chỉ khi $\mathbb{S} \vDash \varphi(p)$ hoặc $\mathbb{S} \vDash \psi(p)$;
5. $\mathbb{S} \vDash (\varphi \rightarrow \psi)(p)$ khi và chỉ khi $\mathbb{S} \vDash \neg\varphi(p)$ hoặc $\mathbb{S} \vDash \psi(p)$;
6. $\mathbb{S} \vDash (\forall x\, \varphi) (p)$ khi và chỉ khi với mỗi phép chọn tham số $p'$ sao cho $p'|_{x^c} = p|_{x^c}$, ta có $\mathbb{S} \vDash \varphi(p')$;
7. $\mathbb{S} \vDash (\exists x\, \varphi) (p)$ khi và chỉ khi tồn tại một phép chọn tham số $p'$ sao cho $p'|_{x^c} = p|_{x^c}$ và $\mathbb{S} \vDash \varphi(p')$.
 
Sự thỏa mãn của một công thức không phụ thuộc chỉ phụ thuộc vào các biến tự do của nó. Cụ thể hơn, nếu $\varphi$ là một công thức, bằng cách quy nạp theo độ phức tạp của $\varphi$, ta có
 
Bổ đề.  Nếu $p$ và $p'$ là hai phép chọn tham số sao cho $p|_{FV(\varphi)} = p'|_{FV(\varphi)}$ thì $\mathbb{S} \vDash \varphi(p)$ khi và chỉ khi $\mathbb{S} \vDash \varphi(p')$.
 
Chẳng hạn, nếu $\varphi$ là một phát biểu thì sự thỏa mãn của nó không phụ thuộc vào phép chọn tham số. Khi đó, ta có thể viết $\mathbb{S} \vDash \varphi$ thay cho $\mathbb{S} \vDash \varphi(p)$.
 
 
Giả sử $\Phi$ là một tập hợp các công thức. Ta viết $\mathbb{S} \vDash \Phi(p)$ nếu với mỗi công thức $\varphi \in \Phi$, ta có $\mathbb{S} \vDash \varphi(p)$.
 
 
Định nghĩa. Giả sử $\chi$ là một công thức. Ta nói $\chi$ là một hệ quả logic (semantic consequence) của $\Phi$ (hay $\Phi$ thỏa mãn $\chi$) nếu với mọi cấu trúc $\mathbb{S}$ và mọi phép chọn tham số $p: \mathcal{V} \to \mathbb{S}$ sao cho $\mathbb{S} \vDash \Phi(p)$, ta có $\mathbb{S} \vDash \chi(p)$. Khi đó, ta viết $\Phi \vDash \chi$.
 
 
 
Sau đây, chúng ta nói về khái niệm hệ tiên đề và lý thuyết.
 
Định nghĩa. Một hệ tiên đề (axiomatization) là một tập hợp $\Phi$ các phát biểu. Mỗi phát biểu $\varphi \in \Phi$ được gọi là một tiên đề (axiom).
 
Định nghĩa. Một lý thuyết (theory) là một hệ tiên đề $\mathcal{T}$ sao cho $\varphi \in \mathcal{T}$ khi và chỉ khi $\mathcal{T} \vDash \varphi$.
 
Nếu $\Phi$ là một hệ tiên đề, tập hợp $$\text{Th}(\Phi):=\{\chi \in \mathcal{L}\text{-Sent}: \Phi \vDash \chi\}$$ các hệ quả logic của $\Phi$ được gọi là lý thuyết sinh bởi $\Phi$. Ta thường đồng nhất mỗi hệ tiên đề với lý thuyết sinh bởi nó.
 
Định nghĩa. Một hệ tiên đề $\Phi$ được gọi là đầy đủ (complete) nếu với mỗi phát biểu $\chi$, ta có $\Phi \vDash \chi$ hoặc $\Phi \vDash \neg \chi$.
 
Ví dụ. 
1. Nếu $\mathbb{S}$ là một cấu trúc thì $\text{Th}(\mathbb{S}):=\{\chi \in \mathcal{L}\text{-Sent}: \mathbb{S} \vDash \chi\}$ được gọi là lý thuyết của $\mathbb{S}$. Đây là một lý thuyết đầy đủ.
 
2. Trong ngôn ngữ rỗng $\{\}$, các tập hợp vô hạn được tiên đề hóa bởi hệ tiên đề gồm các tiên đề $$\exists x_1 \ldots \exists x_n \bigwedge_{i \neq j}\neg(x_i = x_j).$$
 
Chú ý rằng đó là một TẬP HỢP các tiên đề (hay lược đồ tiên đề/schema of axiom). Đây là một lý thuyết đầy đủ.
 
3. Trong ngôn ngữ thứ tự $\mathcal{L}_{\text{ord}} = \{<\}$, hệ tiên đề DLO (dense linear order without endpoints) gồm các tiên đề sau:
 

$<$ là một thứ tự toàn phần (thứ tự tuyến tính), chính xác hơn là các tiên đề

  • $\forall x \, \neg(x < x)$.
  • $\forall x \forall y\, \neg(x < y \land y < x)$.
  • $\forall x \forall y \forall z \, (x < y \land y < z) \rightarrow x < z$.
  • $\forall x \forall y\, \neg(x = y) \rightarrow (x < y \lor y < x)$.
  • (tính trù mật) $\forall x \forall y\, (x < y) \rightarrow \exists z\, (x < z \land z < y)$.
  • (không có đầu mút) $\forall x \exists y \exists z\, y < x \land z < x$.
Đây là một lý thuyết đầy đủ.
 
4. Trong ngôn ngữ nhóm, các nhóm được tiên đề hóa bởi hệ tiên đề gồm
  • $\forall x \forall y \forall z\,(x\cdot y) \cdot z = x \cdot (y \cdot z)$.
  • $\forall x \, (x\cdot 1 = x) \land (1 \cdot x = x)$.
  • $\forall x \, (x\cdot x^{-1} = 1) \land (x^{-1} \cdot x = 1)$.

 

5. Tương tự, ta dễ dàng viết được hệ tiên đề của vành và hệ tiên đề của trường trong ngôn ngữ vành.

 

6. Với mỗi số nguyên tố $p$, gọi $\varphi_p$ là tiên đề $\underbrace{1 + \cdots + 1}_{p \text{ lần}} = 0$. Ta cũng có các hệ tiên đề $\text{ACF}_p = \text{ACF} \cup \{\varphi_p\}$ (trường đóng đại số với đặc số $p$) và $\text{ACF}_0 = \text{ACF} \cup \{\neg \varphi_p: p \text{ nguyên tố}\}$ (trường đóng đại số với đặc số $0$). ACF không phải là một lý thuyết đầy đủ, nhưng các lý thuyết ACF$_0$ và ACF$_p$ đều đầy đủ.

 
7. Hình học Euclid được tiên đề hóa bởi hệ tiên đề Tarski. Đây là một hệ tiên đề đầy đủ, ta có thể dùng nó để chứng minh bất kỳ định lý hình học nào.
 
8. Số học Peano là một hệ tiên đề không đầy đủ (Định lý Gödel về tính không đầy đủ). Vì thế, $\text{Th(PA}_1) \subsetneq \text{Th}(\mathbb{N})$.
 
9. Các hệ tiên đề ZF và ZFC của lý thuyết tập hợp đều không đầy đủ. Giả thuyết continuum không thể chứng minh (Gödel) hay bác bỏ (Cohen) trong các hệ này.
 
Giả sử $\Phi$ là một hệ tiên đề và $\mathbb{S}$ là một cấu trúc.
 
Định nghĩa. Ta nói $\mathbb{S}$ là một mô hình (model) của $\Phi$ nếu $\mathbb{S} \vDash \Phi$. Khi đó ta cũng nói rằng $\Phi$ là thỏa mãn được (satisfiable).
 
 
Ví dụ. 
1. Dễ thấy rằng lý thuyết duy nhất không thỏa mãn được là lý thuyết chứa tất cả các phát biểu.
2. Trong ngôn ngữ nhóm, một cấu trúc là một nhóm khi và chỉ khi nó là một mô hình của hệ tiên đề nhóm, v.v.
 
 
Mệnh đề. $\Phi \vDash \chi$ khi và chỉ khi $\Phi \cup \{\neg \chi\}$ không thỏa mãn được.
Chứng minh. Nếu $\Phi \vDash \chi$ thì mọi mô hình của $\Phi$ đều thỏa mãn $\chi$, vì thế không thỏa mãn $\neg \chi$, vì thế $\Phi \cup \{\neg \chi\}$ không có bất kỳ một mô hình nào. Ngược lại, nếu $\Phi \cup \{\neg \chi\}$ không thỏa mãn được thì mọi mô hình (nếu có) của $\Phi$ đều không thỏa mãn $\neg \chi$, vì thế thỏa mãn $\chi$. $\square$
 
 
 
Trong bài sau, chúng ta sẽ nói về ký hiệu $\vdash$ (suy luận hình thức).

Bài viết đã được chỉnh sửa nội dung bởi nmlinh16: 15-01-2020 - 13:54

$$x - \sum_{\substack{0 < \operatorname{Re} \rho < 1 \\ \zeta(\rho) = 0}} \frac{x^\rho}{\rho} - \log 2\pi - \frac{1}{2}\log(1-x^{-2}) = \frac{\psi(x+0) + \psi(x - 0)}{2}, \qquad \psi(x) = \sum_{\substack{p^n \le x \\  n \ge 1}} \log p.$$

 

"Wir müssen wissen, wir werden wissen." - David Hilbert


#3 nmlinh16

nmlinh16

    Binh nhất

  • Thành viên mới
  • 25 Bài viết
  • Giới tính:Nam
  • Đến từ:Hạ Long
  • Sở thích:Algebraic invariant theory, Algebraic topology, Analytic number theory

Đã gửi 15-01-2020 - 18:06

3. Suy luận

Ta cố định một ngôn ngữ $\mathcal{L}$.

 

Một dãy ký tự $\Phi \vdash \chi$ trong đó $\Phi$ là một tập hợp các công thức và $\chi$ là một công thức được gọi là một trình tự tự nhiên (natrual sequent). 

 

Một suy luận tự nhiên (natural deduction) là một cây hữu hạn được trang trí bởi các trình tự tự nhiên thỏa mãn các quy luật nhất định.

 

Ta nói $\Phi$ chứng minh $\chi$ nếu tồn tại một tập con HỮU HẠN $\Phi_0 \subseteq \Phi$ và một suy luận tự nhiên trong đó gốc của cây là trình tự $\Phi_0 \vdash \chi$, và các lá của cây là dãy ký tự trống.

 

Định nghĩa. Một hệ tiên đề $\mathcal{T}$ được gọi là một lý thuyết suy diễn nếu $\phi \in \mathcal{T}$ khi và chỉ khi $\mathcal{T} \vdash \phi$.

 

 

Định nghĩa. Cho $\Phi$ là một hệ tiên đề.

1. Với mỗi phát biểu $\chi$ sao cho $\Phi \vdash \chi$, ta gọi $\chi$ là một định lý (theorem/syntactic consequence) của hệ tiên đề $\Phi$.

2. Tập hợp các định lý của $\Phi$ được gọi là lý thuyết suy diễn (deductive theory) sinh bởi $\Phi$.

3. Ta nói $\Phi$ là nhất quán (consistent / coherent) nếu không có phát biểu $\chi$ nào sao cho $\Phi \vdash \chi$ và $\Phi \vdash \neg \chi$.

4. Ta nói $\Phi$ là đầy đủ (complete) nếu với mọi phát biểu $\chi$, ta có $\Phi \vdash \chi$ hoặc $\Phi \vdash \neg \chi$.

 

 

 

So sánh giữa hai khái niệm $\vDash$ và $\vdash$:

  • Semantics (ngữ nghĩa) vs. Syntax (hình thức) 
  • Hệ quả logic vs. Định lý
  • Lý thuyết vs. Lý thuyết suy diễn
  • Tính thỏa mãn được vs. Tính nhất quán
  • Tính đầy đủ vs. Tính đầy đủ
 
Mục tiêu của chúng ta là chỉ ra rằng mỗi cặp khái niệm tương ứng ở trên là tương đương nhau.
 
 
 
Các quy luật suy luận của logic mệnh đề (propositional logic)
 

 

1. $(\text{Ax})$ Các tiên đề (hay giả thiết) được chứng minh một cách trực tiếp:
$$\frac{}{\{\varphi\} \vdash \varphi} \,_{\text{Ax}}.$$
2. $(\text{Aff})$ Làm yếu/weakening:
$$\frac{\Phi \vdash \chi}{\Phi \cup \{\varphi\} \vdash \chi} \,_{\text{Aff}}$$
(trình tự ở dưới là đỉnh cha của các trình tự ở trên, ta đọc: "Nếu $\Phi$ chứng minh $\chi$ thì $\Phi \cup \{\varphi\}$ chứng minh $\chi$").

 

 

Các toán tử logic $\neg, \land, \lor, \rightarrow$ có thể được thêm vào (introduce) hoặc khử đi (eliminate).

 

 

Phép phủ định cho phép chứng minh bằng phản chứng:
3. $\dfrac{\Phi \cup \{\chi\} \vdash \psi \qquad \Phi \cup \{\chi\} \vdash \neg\psi}{\Phi \vdash \neg \chi} \,_{\neg_i}$
4. $\dfrac{\Phi \vdash \neg \neg \chi}{\Phi \vdash \chi} \,_{\neg_e}$
 
Phép hội:
5. $\dfrac{\Phi \vdash \chi \qquad \Phi \vdash \psi}{\Phi \vdash \chi \land \psi} \,_{\land_i}$
6. $\dfrac{\Phi \vdash \chi \land \psi}{\Phi \vdash \chi} \,_{\land_e}$ và $\dfrac{\Phi \vdash \chi \land \psi}{\Phi \vdash \psi} \,_{\land_e}$
 
Phép tuyển:
7. $\dfrac{\Phi \vdash \chi}{\Phi \vdash \chi \lor \psi} \,_{\lor_i}$ và $\dfrac{\Phi \vdash \psi}{\Phi \vdash \chi \lor \psi} \,_{\lor_i}$
8. $\dfrac{\Phi \vdash \chi \lor \psi \qquad \Phi \cup \{\chi\} \vdash \varphi \qquad \Phi \cup \{\psi\} \vdash \varphi}{\Phi \vdash \varphi} \,_{\lor_e}$ ("xét từng trường hợp")
 
Phép kéo theo:
7. $\dfrac{\Phi \cup \{\chi\} \vdash \psi}{\Phi \vdash \chi \rightarrow \psi} \,_{\rightarrow_i}$
8. $\dfrac{\Phi \vdash \chi \qquad \Phi \vdash \chi \rightarrow \psi}{\Phi \vdash \psi} \,_{\rightarrow_e}$

 

Ví dụ. Ta đưa ra một chứng minh hình thức cho luật bài trung (excluded middle)

$$\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{}{\{\varphi\} \vdash \varphi}\,_{\text{Ax}}}{\{\neg(\varphi \lor \neg \varphi), \varphi\} \vdash \varphi}\,_{\text{Aff}}}{\{\neg(\varphi \lor \neg \varphi), \varphi\} \vdash \varphi \lor \neg \varphi}\,_{\lor_i} \qquad \dfrac{\dfrac{}{\{\neg(\varphi \lor \neg \varphi)\} \vdash \neg(\varphi \lor \neg \varphi)} \,_{\text{Ax}}}{\{\neg(\varphi \lor \neg \varphi), \varphi\} \vdash \neg(\varphi \lor \neg \varphi)}\,_{\text{Aff}}}{\dfrac{\{\neg(\varphi \lor \neg \varphi)\} \vdash \neg \varphi}{\{\neg(\varphi \lor \neg \varphi)\} \vdash \varphi \lor \neg \varphi} \,_{\lor_i}}\,_{\neg_i} \qquad \dfrac{}{\{\neg(\varphi \lor \neg \varphi)\} \vdash \neg(\varphi \lor \neg \varphi)} \,_{\text{Ax}}}{\dfrac{\vdash \neg \neg (\varphi \lor \neg \varphi)}{\vdash \varphi \lor \neg \varphi} \,_{\neg_e}} \,_{\neg_i}$$

 

Mệnh đề. Ta có các khẳng định sau.

1. $\varphi \vdash \chi$ khi và chỉ khi $\vdash \varphi \rightarrow \chi$.
2. $\vdash \varphi \leftrightarrow \neg \neg \varphi$.
3. $\vdash (\varphi \rightarrow \chi) \leftrightarrow (\neg \varphi \lor \chi)$ (ở đây $\psi_1\leftrightarrow \psi_2$ là viết tắt của $(\psi_1 \rightarrow \psi_2) \land (\psi_2 \rightarrow \psi_1)$).
4. (phản đề) $\vdash (\varphi \rightarrow \chi) \leftrightarrow (\neg \chi \rightarrow \neg \varphi)$.
5. (luật De Morgan) $\vdash \neg(\varphi \land \chi) \leftrightarrow (\neg \varphi \lor \neg \chi)$.
6. (luật De Morgan) $\vdash \neg(\varphi \lor \chi) \leftrightarrow (\neg \varphi \land \neg \chi)$.
 
Nhận xét rằng, một hệ tiên đề không nhất quán có thể chứng minh tất cả các phát biểu (nói cách khác, không thể phân biệt đúng sai). Thật vậy, nếu $\Phi \vdash \chi$ và $\Phi \vdash \neg \chi$ thì với mọi phát biểu $\varphi$, ta có $\Phi \cup \{\neg \varphi \} \vdash \chi$ và $\Phi \cup \{\neg \varphi \} \vdash \neg \chi$ (do $(\text{Aff})$), vì thế $\Phi \vdash \neg \neg \varphi$ (do $(\neg_i)$) và $\Phi \vdash \varphi$ (do $(\neg_e)$).
 
 
 
 

Thay thế

 

Cho $\varphi$ là một công thức và $t$ là một biểu thức. Ta ký hiệu bởi $\varphi[x:=t]$ công thức thu được khi thay đồng thời tất cả các lần xuất hiện TỰ DO của $x$ trong $\varphi$ bởi $t$. Ta nói $t$ thay được vào $x$ trong $\varphi$ nếu không có biến của $V(t)$ trở thành một biến phụ thuộc khi thay vào $\varphi$.

 

Ví dụ.  Xét công thức $\varphi$: $(\forall x\, R(x,y)) \rightarrow S(x,y,z)$.
1. $x$ không thay được vào $y$ trong $\varphi$.
2. Một biểu thức $t$ thay được vào $y$ trong $\varphi$ khi và chỉ khi $x \notin V(t)$.
3. Mọi biểu thức $t$ đều thay được vào $x$ trong $\varphi$, và khi đó $\varphi[x:=t]$ là $(\forall x\, R(x,y)) \rightarrow S(t,y,z)$.
4. Mọi biểu thức $t$ đều thay được vào $z$ trong $\varphi$.
 
 
 
Các quy luật suy luận của logic bậc nhất
Đẳng thức:
1. $\dfrac{}{t = t}\,_{=_i}$ (mọi lá của một suy luận tự nhiên đều có dạng ($=_i$) hoặc ($\text{Ax}$)).
2. $\dfrac{\Phi \vdash \chi[x:=t] \qquad \Phi \vdash t = t'}{\Phi \vdash \chi[x:=t']}\,_{=_e}$ nếu $t$ và $t'$ đều thay được vào $x$ trong $\chi$.
 
Lượng từ phổ biến:
1. $\dfrac{\Phi \vdash \chi}{\Phi \vdash \forall x\,\chi}\,_{\forall_i}$ nếu $x$ không xuất hiện tự do trong $\Phi$.
2. $\dfrac{\Phi \vdash \forall x\,\chi}{\Phi \vdash \chi[x:=t]}\,_{\forall_e}$ nếu $t$ thay được vào $x$ trong $\chi$.
 
Lượng từ tồn tại:
1. $\dfrac{\Phi \vdash \chi[x:=t]}{\Phi \vdash \exists x\,\chi}\,_{\exists_i}$ nếu $t$ thay được vào $x$ trong $\chi$.
2. $\dfrac{\Phi \vdash \exists x\,\psi \qquad \Phi \cup \{\psi\} \vdash \chi}{\Phi \vdash \chi}\,_{\exists_e}$ nếu $x$ không xuất hiện tự do trong $\Phi \cup \{\chi\}$.

 

Ví dụ. Ta đưa ra một chứng minh hình thức cho khẳng định $\vdash (\neg \exists x\,\varphi) \leftrightarrow (\forall x\, \neg \varphi)$. Một mặt,

$$\dfrac{\dfrac{\dfrac{\dfrac{}{\{\varphi\} \vdash \varphi}\,_{\text{Ax}}}{\{\neg \exists x\,\varphi, \varphi\} \vdash \varphi}\,_{\text{Aff}}}{\{\neg\exists x\,\varphi, \varphi\} \vdash \exists x\,\varphi}\,_{\exists_i} \qquad \dfrac{\dfrac{}{\{\neg\exists x\,\varphi\} \vdash \neg\exists x\,\varphi} \,_{\text{Ax}}}{\{\neg\exists x\,\varphi, \varphi\} \vdash \neg\exists x\,\varphi}\,_{\text{Aff}}}{\dfrac{\{\neg\exists x\,\varphi\} \vdash \neg \varphi}{\{\neg\exists x\,\varphi\} \vdash \forall x\, \neg \varphi} \,_{\forall_i}} \,_{\neg_i}$$
Mặt khác
$$\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{}{\{\forall x \, \neg\varphi\} \vdash \forall x\, \neg \varphi}\,_{\text{Ax}}}{\{\forall x\,\neg\varphi, \exists x\,\varphi, \varphi\} \vdash \forall x\,\neg\varphi}\,_{\text{Aff}}}{\{\forall x\,\neg\varphi, \exists x\,\varphi, \varphi\} \vdash \neg\varphi}\,_{\forall_e} \qquad \dfrac{\dfrac{}{\{\varphi\} \vdash \varphi} \,_{\text{Ax}}}{\{\forall x\,\neg\varphi, \exists x\,\varphi, \varphi\} \vdash \varphi}\,_{\text{Aff}}}{\dfrac{\{\forall x\, \neg\varphi, \varphi\} \vdash \neg \exists x\, \varphi}{\{\forall x\, \neg\varphi, \exists x\, \varphi, \varphi\} \vdash \neg \exists x\, \varphi} \,_{\text{Aff}}} \,_{\neg_i} \qquad \dfrac{\dfrac{}{\{\exists x \, \varphi\} \vdash \exists x\, \varphi}\,_{\text{Ax}}}{\{\forall x\,\neg\varphi, \exists x\,\varphi\} \vdash \exists x\,\varphi}\,_{\text{Aff}}}{\{\forall x\,\neg \varphi,\exists x \,\varphi\} \vdash \neg \exists x\,\varphi}\,_{\exists_e}$$
Sau đó, sử dụng $\text{(Ax)}$, $\text{(Aff)}$ và $(\neg_i)$, ta thu được $\{\forall x\,\neg \varphi\} \vdash \neg \exists x\,\varphi$. Cuối cùng, sử dụng $(\rightarrow_i)$ và $(\land_i)$.
 
 
Chú ý. Nếu $\{\varphi\} \vdash \chi$ thì $\{\exists x\, \varphi\} \vdash \exists x\, \chi$ và $\{\forall x\, \varphi\} \vdash \forall x\, \chi$. Tuy nhiên, ta KHÔNG có $\vdash (\varphi \rightarrow \chi) \rightarrow (\exists x\,\varphi \rightarrow \exists x\,\chi)$ cũng như $\vdash (\varphi \rightarrow \chi) \rightarrow (\forall x\,\varphi \rightarrow \forall x\,\chi)$.
 
 
Nhận xét. Ta cũng có $\vdash (\varphi \lor \chi) \leftrightarrow \neg (\neg \varphi \land \neg \chi)$ và $\vdash (\varphi \rightarrow \chi) \leftrightarrow \neg (\varphi \land \neg \chi)$. Như vậy, tất cả các công thức đều tương đương với một công thức chỉ chứa gồm các toán tử logic $\neg$ và $\land$ và lượng từ $\exists$. Các chứng minh cũng có thể được thực hiện sao cho chỉ có các ký tự này xuất hiện, chúng ta sẽ không đi quá sâu vào các chi tiết (có thể chứng minh, chẳng hạn bằng quy nạp theo độ phức tạp của các công thức). Sự tương đương trên cũng đúng về mặt ngữ nghĩa $(\vDash)$, nên kể từ nay, khi quy nạp theo độ phức tạp của công thức, ta chỉ cần xét các trường hợp: Công thức nguyên tử, công thức có dạng $\neg \varphi$, $\varphi \land \chi$ và $\exists x \,\varphi$. Đặc biệt, khi nói về các phát biểu, ta chỉ cần xét các phát biểu có dạng $R(t_1,\ldots,t_n)$ (các biểu thức $t_1,\ldots,t_n$ không chứa biến); $\neg \varphi$, $\varphi \land \chi$ với $\varphi$ và $\chi$ là các phát biểu; $\exists x\, \varphi$ với $\varphi$ là một công thức sao cho $FV(\varphi) \subseteq x$.
 
 
Trong bài sau, chúng ta sẽ nói kỹ hơn về việc thay thế và định lý về tính đúng đắn: Nếu $\Phi \vdash \chi$ thì $\Phi \vDash \chi$.

Bài viết đã được chỉnh sửa nội dung bởi nmlinh16: 15-01-2020 - 18:19

$$x - \sum_{\substack{0 < \operatorname{Re} \rho < 1 \\ \zeta(\rho) = 0}} \frac{x^\rho}{\rho} - \log 2\pi - \frac{1}{2}\log(1-x^{-2}) = \frac{\psi(x+0) + \psi(x - 0)}{2}, \qquad \psi(x) = \sum_{\substack{p^n \le x \\  n \ge 1}} \log p.$$

 

"Wir müssen wissen, wir werden wissen." - David Hilbert


#4 nmlinh16

nmlinh16

    Binh nhất

  • Thành viên mới
  • 25 Bài viết
  • Giới tính:Nam
  • Đến từ:Hạ Long
  • Sở thích:Algebraic invariant theory, Algebraic topology, Analytic number theory

Đã gửi 18-01-2020 - 17:35

4. Soundness theorem

 

Ta cố định một ngôn ngữ $\mathcal{L}$.

 

Logic bậc nhất có tính "hợp lý" (sound): Nếu $\Phi \vdash \chi$ thì $\Phi \vDash \chi$.

 

Bổ đề. (đổi tên biến) Cho $\varphi$ là một công thức, $x$ là một biến và $t$ là một biểu thức. Tồn tại một công thức $\varphi'$ thu được từ $\varphi$ bằng cách đổi tên các biến phụ thuộc sao cho

  • $\vdash \varphi \leftrightarrow \varphi'$ (nói riêng,  $\vdash \exists x\, \varphi \leftrightarrow \exists x\,\varphi'$).
  • $t$ thay được vào $x$ trong $\varphi'$.

Chứng minh. Chứng minh. Quy nạp theo độ phức tạp của $\varphi$. Nếu $\varphi$ là một công thức nguyên tử (không có biến phụ thuộc) thì ta chọn $\varphi'$ chính là $\varphi$. Đối với các công thức dạng $\neg \varphi$ và $\varphi \land \chi$, ta lấy $\varphi'$ và $\chi'$ lần tương ứng với $\varphi$ và $\chi$, khi đó $\neg \varphi'$ và $\varphi' \land \chi'$ là các công thức cần tìm. Cuối cùng, xét công thức có dạng $\exists y\, \varphi$.

  • Nếu $y$ là $x$, ta giữ nguyên công thức $\exists x\, \varphi$ (nhắc lại rằng khi thay một biểu thức vào $x$, ta chỉ thay vào những lần xuất hiện tự do của $x$).
  • Nếu $y$ không phải là $x$ và $y \notin V(t)$, ta xét $\varphi'$ tương ứng với $\varphi$ và chọn $\exists y \,\varphi'$.
  • Nếu $y$ không phải là $x$ và $y \in V(t)$, gọi $z$ là một biến không xuất hiện trong $V(t) \cup V(\varphi') \cup \{x\}$. Khi đó công thức $\exists z \,\varphi'[y:=z]$ thỏa mãn những gì ta muốn.

$\square$

 

 

Ví dụ. Ta xét $\varphi$ là công thức $(\forall x\, R(x,y)) \rightarrow S(x,y,z)$ và $t$ là biểu thức $f(x,u)$. Rõ ràng $t$ không thay được vào $y$ trong $\varphi$. Ta có thể lấy $\varphi'$ là công thức $(\forall v\, R(v,y)) \rightarrow S(x,y,z)$.

 

 

Bổ đề. (tổng quát hóa) Nếu $\Phi \vdash \chi$ và $c$ là một ký hiệu hằng không xuất hiện trong $\Phi$ thì tồn tại một biến $x \notin V(\chi)$ sao cho $\Phi \vdash \forall x\, \chi[c:=x]$ (ta đã lạm dụng ký hiệu khi "thay" một biến vào một hằng số).
 
Chứng minh. Ta xét một tập con hữu hạn $\Phi_0 \subseteq \Phi$ và một cây suy luận $D$ với gốc là trình tự $\Phi_0 \vdash \chi$. Chọn một biến $x$ không xuất hiện trong toàn bộ $D$. Gọi $D[c:=x]: \Phi_0 \vdash \chi[c:=x]$ là cây thu được khi thay tất cả những lần xuất hiên của $c$ bởi $x$. Ta chứng minh rằng đây cũng là một suy luận bằng quy nạp theo gốc của $D$.
  • Nếu $D$ chỉ gồm một tiên đề $(\text{Ax})$, hoặc $(=_i)$, hoặc kết thúc ở $(=_e)$, kết luận là hiển nhiên.
  • Nếu $D$ dừng lại ở $(\text{Aff})$, hoặc ($\neg_i$), hoặc ($\neg_e$), hoặc ($\land_i$), hoặc ($\land_e$), kết luận đều hiển nhiên.
  • Nếu $D$ dừng lại ở $\dfrac{\Psi \vdash \psi}{\Psi \vdash \forall y\, \psi} \,_{\forall_i}$ với $y$ không xuất hiện tự do trong $\Psi$. Vì $x \notin V(\psi)$ và $x \neq y$ nên công thức $(\forall y\, \psi)[c:=x]$ chính là $\forall y\, \psi[c:=x]$ và $y$ không xuất hiện tự do trong $\Psi[c:=x]$, do đó $\dfrac{\Psi[c:=x] \vdash \psi[c:=x]}{\Psi[c:=x] \vdash \forall y\, \psi[c:=x]}$ thỏa mãn luật suy luận $(\forall_i)$.
  • Nếu $D$ dừng lại ở $\dfrac{\Psi \vdash \forall y\, \psi}{\Psi \vdash \psi[y:=t]} \,_{\forall_e}$ với $t$ thay được vào $y$ trong $\psi$. Tương tự như trên, công thức $(\forall y\, \psi)[c:=x]$ chính là $\forall y\, \psi[c:=x]$. Dễ thấy $t$ thay được vào $y$ trong $\psi[c:=x]$ và $\psi[c:=x][y:=t]$ chính là $\psi[y:=t][c:=x]$, nên $\dfrac{\Psi[c:=x] \vdash \forall y\, \psi[x:=c]}{\Psi \vdash \psi[y:=t][c:=x]}$  thỏa mãn luật suy luận $(\forall_e)$.

Tóm lại, $\Phi_0 \vdash \chi[c:=x]$, và vì $x$ không xuất hiện trong $\Phi_0$ nên $\Phi_0 \vdash \forall x\, \chi[c:=x]$ do $(\forall_i)$. $\square$

 

 

 

Một số kết quả về thay thế
 

Bổ đề 1. Cho $(\mathbb{S},p)$ là một cấu trúc với tham số, $t$, $\tau$ là các biểu thức và $x$ là một biến. Gọi $\check{t}$ là biểu thức $t[x:=\tau]$ là $\check{p}$ là phép chọn tham số sao cho $\check{p}|_{x^c} = p|_{x^c}$ và $\check{p}(x) = p(\tau)$. Khi đó $p(\check{t}) = \check{p}(t)$.

 

Chứng minh. Quy nạp theo độ phức tạp của $t$. Nếu $t$ là một ký hiệu hằng hoặc một biến khác $x$, kết luận là hiển nhiên. Nếu $t$ là $x$ thì $\check{t}$ là $\tau$, nên $p(\check{t}) = p(\tau) = \check{p}(x) = \check{p}(t)$. Cuối cùng, nếu $t$ có dạng $f(t_1,\ldots,t_n)$ thì $\check{t}$ là $f(\check{t}_1,\ldots,\check{t}_n)$, do đó theo giả thiết quy nạp $$p(\check{t}) = f^{\mathbb{S}}(p(\check{t}_1),\ldots,p(\check{t}_n)) = f^{\mathbb{S}}(\check{p}(t_1),\ldots,\check{p}(t_n)) = \check{p}(t).$$ $\square$

 

 

Bổ đề 2. Cho $\mathbb{S}$ là một cấu trúc, $\tau$ là một biểu thức, $x$, $y$ là hai biến phân biệt với $y \notin V(\tau)$ và $a \in \mathbb{S}$. Với mọi phép chọn tham số $p$, gọi

  • $\check{p}$ là phép chọn tham số sao cho $\check{p}|_{x^c} = p|_{x^c}$ và $\check{p}(x) = p(\tau)$;
  • $p'$ là phép chọn tham số sao cho $p'|_{y^c} = p|_{y^c}$ và $p'(y) = a$.
Khi đó, $\check{p'} = (\check{p})'$.
 
Chứng minh. Với mọi biến $z$ khác $x$ và $y$, ta có $$\check{p'}(z) = p'(z) = p(z) = \check{p}(z) = (\check{p})'(z).$$
Ta cũng có $$\check{p'}(y) = p'(y) = a = (\check{p})'(y)$$ và, do $y \notin V(\tau)$  $$\check{p'}(x) = p'(\tau) = p(\tau) = \check{p}(x) = (\check{p})'(x).$$
 
Bổ đề. (thay thế) Cho $(\mathbb{S},p)$ là một cấu trúc có tham số, $\varphi$ là một công thức, $x$ là một biến và $\tau$ là một biểu thức thay được vào $x$ trong $\varphi$. Gọi $\check{\varphi}$ là công thức $\varphi[x:=\tau]$ là $\check{p}$ là phép chọn tham số sao cho $\check{p}|_{x^c} = p|_{x^c}$ và $\check{p}(x) = p(\tau)$. Khi đó $\mathbb{S} \vDash \check{\varphi}(p)$ khi và chỉ khi $\mathbb{S} \vDash \varphi(\check{p})$.
 
Chứng minh. Quy nạp theo độ phức tạp của $\varphi$.
  • Nếu $\varphi$ có dạng $R(t_1,\ldots,t_n)$ thì $\check{\varphi}$ là $R(\check{t}_1,\ldots,\check{t}_n)$. Do đó $\mathbb{S} \vDash \varphi(\check{p})$ khi và chỉ khi $(\check{p}(t_1),\ldots,\check{p}(t_n)) \in R^{\mathbb{S}}$, và $\mathbb{S} \vDash \check{\varphi}(p)$ khi và chỉ khi $(p(\check{t_1}),\ldots,p(\check{t_n})) \in R^{\mathbb{S}}$. Tuy nhiên $\check{p}(t_i) = p(\check{t_i})$ theo Bổ đề 1.
  • Trường hợp của các toán tử $\neg$ và $\land$ là tầm thường.
  • Giả sử $\varphi$ có dạng $\forall y\, \chi$. Nếu $x$ không xuất hiện tự do trong $\varphi$ thì $\check{\varphi}$ vẫn là $\varphi$ và kết luận là hiển nhiên vì sự thỏa mãn không phụ thuộc vào giá trị của phép chọn tham số tại $x$. Nếu $x$ xuất hiện tự do trong $\varphi$ thì $y$ không phải là $x$ và $x$ xuất hiện do trong $\chi$. Nói riêng, $\tau$ thay được vào $x$ trong $\chi$ và (do $y \notin V(\tau)$) $\check{\varphi}$ là $\forall y\,\check{\chi}$. Nếu $\mathbb{S} \vDash \check{\varphi}(p)$ thì tồn tại $a \in \mathbb{S}$ và phép chọn tham số $p'$ với $p'|_{y^c} = p|_{y^c}$ và $p'(y) = a$ sao cho $\mathbb{S} \vDash \check{\chi}(p')$, và vì thế $\mathbb{S} \vDash \chi(\check{p'})$ (quy nạp) và $\mathbb{S} \vDash \chi((\check{p})')$ (Bổ đề 2). Điều này chứng tỏ rằng $\mathbb{S} \vDash \varphi(\check{p})$. Nếu $\mathbb{S} \vDash \varphi(\check{p})$, chứng minh hoàn toàn tương tự.

$\square$

 

 

Định lý về tính đúng đắn. Nếu $\Phi \vdash \chi$ thì $\Phi \vDash \chi$.

 

Chứng minh. Ta xét một tập con hữu hạn $\Phi_0 \subseteq \Phi$ và một cây suy luận $D$ với gốc là trình tự $\Phi_0 \vdash \chi$. Ta chứng minh bằng quy nạp theo gốc của $D$. Thật ra mọi trường hợp đều tầm thường, trừ trường hợp $D$ kết thúc ở $\dfrac{\Psi \vdash \forall x\, \varphi}{\Psi \vdash \varphi[x:=t]}\,_{\forall_e}$ với $t$ thay được vào $x$ trong $\varphi$. Bằng quy nạp, ta có $\Psi \vDash \forall x\, \varphi$. Giả sử $(\mathbb{S},p)$ là một mô hình (với tham số) của $\Phi$. Gọi $\check{p}$ là phép chọn tham số sao cho $\check{p}|_{x^c} = p|_{x^c}$ và $\check{p}(x) = p(t)$. Vì $\mathbb{S} \vDash (\forall x \,\varphi)(p)$ nên $\mathbb{S} \vDash \varphi(\check{p})$. Theo Bổ đề về thay thế, ta có $\mathbb{S} \vDash \varphi[x:=t](p)$. Vậy $\Psi \vDash \varphi[x:=t]$. $\square$

 

 

Hệ quả. Mọi hệ tiên đề thỏa mãn được đều nhất quán.

 

 

Trong bài cuối cùng, chúng ta sẽ nói về Định lý về tính đầy đủ: nếu $\Phi \vDash \chi$ thì $\Phi \vdash \chi$.


Bài viết đã được chỉnh sửa nội dung bởi nmlinh16: 18-01-2020 - 17:43

$$x - \sum_{\substack{0 < \operatorname{Re} \rho < 1 \\ \zeta(\rho) = 0}} \frac{x^\rho}{\rho} - \log 2\pi - \frac{1}{2}\log(1-x^{-2}) = \frac{\psi(x+0) + \psi(x - 0)}{2}, \qquad \psi(x) = \sum_{\substack{p^n \le x \\  n \ge 1}} \log p.$$

 

"Wir müssen wissen, wir werden wissen." - David Hilbert


#5 nmlinh16

nmlinh16

    Binh nhất

  • Thành viên mới
  • 25 Bài viết
  • Giới tính:Nam
  • Đến từ:Hạ Long
  • Sở thích:Algebraic invariant theory, Algebraic topology, Analytic number theory

Đã gửi Hôm qua, 02:04

5. Completeness theorem

 

Trong phần này, "lý thuyết" được hiểu là lý thuyết suy diễn. Ta luôn giả sử $\mathcal{L}$ là một ngôn ngữ.

 

 

Định lý về tính đầy đủ. Nếu $\Phi \vDash \chi$ thì $\Phi \vdash \chi$. 

 

 

Trong các tài liệu hiện đại về logic, người ta thường trình bày chứng minh xây dựng của Henkin thay vì chứng minh gốc của Gödel. 

 

 

Bước 1 (Bổ đề ngữ nghĩa)

 

Ta chỉ cần chứng minh rằng mọi lý thuyết nhất quán đều thỏa mãn được.

 

Chứng minh. Giả sử $\Phi$ và $\chi$ chỉ gồm các phát biểu. Nếu $\Phi \vDash \chi$ thì $\Phi \cup \{\neg \chi\}$ không thỏa mãn được. Theo giả thiết, nó không nhất quán, do đó $\Phi \vdash \neg \neg \chi$, và vì thế $\Phi \vdash \chi$.   

Giả sử $\Phi$ và $\chi$ gồm các công thức tùy ý. Ta chia tập các biến $\mathcal{V} = \{x_i:i \in \mathbb{N}\}$ thành hai phần: phần với chỉ số chẵn và phần với chỉ số lẻ. Ta xét mỗi lần xuất hiện của các biến trong tất cả công thức của $\Phi$ như sau: Nếu $x_i$ xuất hiện phụ thuộc, đổi tên nó và các lượng từ ứng với nó thành $x_{2i}$. Nếu $x_i$ xuất hiện tự do, đổi tên nó thành $x_{2i+1}$. Ta thu được một hệ tiên đề $\Phi'$ tương đương với $\Phi$ về hình thức cũng như ngữ nghĩa, và các biến tự do đều có chỉ số lẻ. Ta làm điều tương tự cho $\chi$ để thu được $\chi'$. Xét ngôn ngữ $\mathcal{L}'$ thu được từ $\mathcal{L}$ bằng các thêm vào các ký hiệu hằng $x_{2i+1}$, $i \in \mathbb{N}$. Trong ngôn ngữ mới, $\Phi'$ và $\chi'$ là các phát biểu. $\square$

 

 

Mục tiêu của chúng ta bây giờ là tìm một mô hình cho một lý thuyết nhất quán cho trước.
 
Giả sử $\mathcal{T}$ là một $\mathcal{L}$-lý thuyết.
 
 

Bước 2 (Ngôn ngữ)

 

Chúng ta Henkin hóa ngôn ngữ $\mathcal{L}$. Khó khăn nằm ở những công thức có lượng từ dạng $\exists x\, \varphi$: ta không kiểm soát được các nhân chứng của công thức $\varphi$ trong các mô hình khác nhau. Ý tưởng của chúng ta là thêm vào ngôn ngữ $\mathcal{L}$ ký hiệu hằng $c_{(x,\varphi)}$; trong cấu trúc được xây dựng, ký hiệu này sẽ được thông dịch thành một nhân chứng của $\varphi$ (nhân chứng Henkin - Henkin's witness).
 
Với mỗi phát biểu dạng $\exists x \, \varphi$ với $FV(\varphi) \subseteq \{x\}$, ta thêm một ký hiệu hằng mới $c_{(x,\varphi)}$ (hằng số Henkin) vào $\mathcal{L}$. Ngôn ngữ $$\mathcal{L}':=\mathcal{L} \sqcup \{c_{(x,\varphi)}: x \in \mathcal{V}, \varphi \in \mathcal{L}\text{-Form}, FV(\varphi) \subseteq \{x\}\}$$ được gọi là ngôn ngữ Henkin hóa của $\mathcal{L}$.
 
Ta đặt $\mathcal{L}_0:=\mathcal{L}$, $\mathcal{L}_{n+1} = \mathcal{L}'_n$ với mỗi $n \in \mathbb{N}$ và $\hat{\mathcal{L}} = \bigcup_{n \in \mathbb{N}} \mathcal{L}_n$. Nhận xét rằng với mỗi $\hat{\mathcal{L}}$-phát biểu dạng $\exists x \, \varphi$ với $FV(\varphi) \subseteq \{x\}$, ta có một ký hiệu hằng $c_{(x,\varphi)} \in \hat{\mathcal{L}}$. Ta nói rằng $\hat{\mathcal{L}}$ là một ngôn ngữ Henkin-đầy đủ.
 
 

Bổ đề. Giả sử $\tilde{\mathcal{L}}$ là một ngôn ngữ thu được bằng cách thêm các ký hiệu hằng vào $\mathcal{L}$. Nếu $\mathcal{T}$ là $\mathcal{L}$-nhất quán thì nó cũng $\tilde{\mathcal{L}}$-nhất quán.

 

Chứng minh. Ta dùng ký hiệu $\vdash_{\mathcal{L}}$ để chỉ các suy luận với các ký hiệu đều nằm trong $\mathcal{L}$. Giả sử $\varphi$ là một $\tilde{\mathcal{L}}$-công thức sao cho $\mathcal{T} \vdash \varphi$. Tồn tại một suy luận $D:\Phi \vdash \varphi$ với $\Phi \subseteq \mathcal{T}$ là một lý thuyết hữu hạn. Giả sử một ký hiệu hằng $c \in \tilde{\mathcal{L}} \setminus \mathcal{L}$ xuất hiện trong suy luận $D$. Theo bổ đề về tổng quát hóa, vì $c$ không xuất hiện trong $\Phi$ nên tồn tại biến $x$ không xuất hiện trong cả $\varphi$ và $\Phi$ sao cho ta có một suy luận $D[c:=x] : \Phi \vdash \varphi[c:=x]$. Sau một số hữu hạn lần thay thế các ký hiệu hằng trong $\tilde{\mathcal{L}} \setminus \mathcal{L}$ bởi các biến, ta thu được một suy luận $D':\Phi \vdash \varphi'$, trong đó mọi ký hiệu đều nằm trong $\mathcal{L}$ (nghĩa là $\varphi'$ là một $\mathcal{L}$-công thức và $\Phi \vdash_{\mathcal{L}} \varphi'$). Vì thế, $\mathcal{T} \not\vdash \neg \varphi$, vì nếu ngược lại thì $\Phi \vdash_{\mathcal{L}} \neg \varphi'$, nên $\mathcal{T} \vdash_{\mathcal{L}} \neg \varphi'$, mâu thuẫn với tính $\mathcal{L}$-nhất quán của $\mathcal{T}$. Điều này cho thấy $\mathcal{T}$ cũng $\tilde{\mathcal{L}}$-nhất quán. $\square$

 

 

 

Bước 3 (Lý thuyết)

 

Chúng ta bổ sung thêm các tiên đề Henkin. Với mỗi $\mathcal{L}$-phát biểu dạng $\exists x\,\varphi$ với $FV(\varphi) \subseteq \{x\}$, gọi $\eta_{(x,\varphi)}$ là phát biểu $$\exists x\,\varphi \rightarrow \varphi[x:=c_{(x,\varphi)}],$$ nói cách khác, tiên đề này nói rằng ký hiệu hằng $c_{(x,\varphi)}$ là một nhân chứng cho công thức $\varphi$. Ta gọi $\mathcal{L}'$-lý thuyết $$\mathcal{T}':=\mathcal{L} \sqcup \{\eta_{(x,\varphi)}: x \in \mathcal{V}, \varphi \in \mathcal{L}\text{-Form}, FV(\varphi) \subseteq \{x\}\}$$ là lý thuyết Henkin hóa của $\mathcal{T}$.
 
Ta đặt $\mathcal{T}_0:=\mathcal{T}$ và $\mathcal{T}_{n+1} = \mathcal{T}'_n$  với mỗi $n \in \mathbb{N}$. Trong $\hat{\mathcal{L}}$-lý thuyết $$\hat{\mathcal{T}}:= \bigcup_{n \in \mathbb{N}} \mathcal{T}_n = \mathcal{T} \cup \{\eta_{(x,\varphi)}: x \in \mathcal{V},\varphi \in \hat{\mathcal{L}}\text{-Form},FV(\varphi) \subseteq \{x\}\},$$
mỗi định lý dạng $\exists x\,\varphi$ đều có một ký hiệu hằng làm nhân chứng. Ta nói $\hat{\mathcal{T}}$ là một lý thuyết Henkin.
 
 
Bổ đề. Nếu $\mathcal{T}$ nhất quán thì $\hat{\mathcal{T}}$ cũng nhất quán.
 
Chứng minh. Do tính hữu hạn của các công thức và các suy luận, ta chỉ cần chứng minh rằng $\mathcal{T}_n$ nhất quán với mỗi $n \in \mathbb{N}$. Bằng quy nạp, ta chỉ cần chứng minh rằng $\mathcal{T}'$ là nhất quán. Thật vậy, nếu ngược lại thì tồn tại một $\mathcal{L}$-phát biểu dạng $\exists x\,\varphi$ sao cho $FV(\varphi) \subseteq \{x\}$ và $\mathcal{T} \vdash \neg \eta_{(x,\varphi)}$, vì thế $\mathcal{T} \vdash \neg \varphi[x:=c_{(x,\varphi)}]$. Vì $c_{(x,\varphi)}$ không nằm trong $\mathcal{T}$ nên theo bổ đề về tổng quát hóa, tồn tại biến $y \notin V(\varphi)$ sao cho $\mathcal{T} \vdash \forall y\, \neg \varphi[x:=y]$, nên $\mathcal{T} \vdash \forall x\,\neg\varphi$, do đó $\mathcal{T} \vdash \neg \exists x\, \varphi$. Điều này cho thấy $\mathcal{T} \vdash \eta_{(x,\varphi)}$, nghĩa là $\mathcal{T}$ không nhất quán. $\square$
 
 
 

Bước 4 (Tính đầy đủ)

 

Giả sử $\{\Phi_i\}_{i \in I}$ một tập hợp các $\hat{\mathcal{L}}$-lý thuyết nhất quán chứa $\hat{\mathcal{T}}$ sao cho với mọi $i, j \in I$, ta có $\Phi_i \subseteq \Phi_j$ hoặc $\Phi_i \subseteq \Phi_j$, thế thì $$\Phi = \bigcup_{i \in I} \Phi_i$$ là một lý thuyết nhất quán chứa tất cả các lý thuyết $\Phi_i$, $i \in I$. Theo bổ đề Zorn, tồn tại một lý thuyết nhất quán $\mathcal{T}^\ast$ cực đại theo quan hệ bao hàm và chứa $\hat{\mathcal{T}}$. Đây là một lý thuyết đầy đủ, vì nếu $\varphi$ là một phát biểu sao cho $\mathcal{T}^\ast \not \vdash  \varphi$ thì $\mathcal{T}^\ast \cup \{\neg \varphi\}$ là một lý thuyết nhất quán chứa $\mathcal{T}^\ast$. Do tính cực đại của $\mathcal{T}^\ast$ nên ta có $\mathcal{T}^\ast \vdash \neg \varphi$.

 

 

 

Bước 5 (Cấu trúc)

 

Gọi $\mathbb{T}$ là tập hợp tất cả các $\hat{\mathcal{L}}$-biểu thức không chứa biến. Xét quan hệ tương đương $\sim$ trên $\mathbb{T}$ cho bởi: $t_1 \sim t_2$ khi và chỉ khi $\mathcal{T} \vdash t_1 = t_2$.
 
Xét cấu trúc $\mathbb{S}:=\mathbb{T}/\sim$, trong đó
  • với mỗi ký hiệu hằng $c$, $c^{\mathbb{S}} = [c]$;
  • với mỗi ký hiệu quan hệ $n$ ngôi $R$, $$R^{\mathbb{S}} = \{([t_1],\ldots,[t_n]) \in \mathbb{S}^n: \mathcal{T}^\ast \vdash R(t_1,\ldots,t_n)\};$$
  • với mỗi ký hiệu hàm $n$ biến $f$, $$f^{\mathbb{S}}: \mathbb{S}^n \to \mathbb{S}, \qquad ([t_1],\ldots,[t_n]) \mapsto [f(t_1),\ldots,f(t_n)].$$

Dễ thấy các định nghĩa trên đều không phụ thuộc và cách chọn đại diện của mỗi lớp tương đương của các biểu thức. Xét một phép chọn tham số $p: \mathcal{V} \to \mathbb{S}$ bất kỳ. Với mỗi biểu thức không chứa biến $t$, bằng quy nạp, ta chứng minh được rằng $p(t) = [t]$.

 

Bổ đề. Với mỗi $\hat{\mathcal{L}}$-phát biểu $\varphi$, ta có $\mathbb{S} \vDash \varphi$ khi và chỉ khi $\mathcal{T}^\ast \vdash \varphi$.

 

Chứng minh. Ta chứng minh bằng quy nạp theo độ phức tạp của $\varphi$.

  • Nếu $\varphi$ có dạng nguyên tử $R(t_1,\ldots,t_n)$ thì $t_1,\ldots,t_n$ không chứa biến. Do đó, $\mathbb{S} \vDash \varphi$ khi và chỉ khi $([t_1],\ldots,[t_n]) \in R^{\mathbb{S}}$, tức là khi và chỉ khi $T^\ast \vdash \varphi$ (theo cách xây dựng).
  • Nếu $\varphi$ có dạng $\neg \chi$, ta sử dụng tính đầy đủ của $\mathcal{T}^\ast$.
  • Trường hợp của toán tử $\land$ tầm thường.
  • Nếu $\varphi$ có dạng $\exists x\, \chi$ với $V(\chi) \subseteq \{x\}$, gọi $\eta$ là tiên đề Henkin $\eta_{(x,\chi)}$ và $c$ là hằng số Henkin $c_{(x,\varphi)}$. Nếu $\mathcal{T}^\ast \vdash \varphi$ thì $\mathcal{T}^\ast \vdash \chi[x:=c]$ (vì $\mathcal{T}^\ast \vdash \eta$), nên $\mathbb{S} \vDash \chi(\check{p})$ theo bổ đề về thay thế, với $\check{p}$ là phép chọn tham số sao cho $\check{p}|_{x^c} = p|_{x^c}$ và $\check{p}(x) = [c]$. Điều này chứng tỏ $\mathbb{S} \vDash \varphi$. Ngược lại, giả sử $\mathbb{S} \vDash \varphi$. Gọi $p'$ là một phép chọn tham số sao cho $p'|_{x^c} = p|_{x^c}$ và $\mathbb{S} \vDash \chi(p')$. Gọi $t$ là biểu thức không chứa biến sao cho $p'(x) = [t]$. Nói tiêng, $t$ thay được vào $x$ trong $\chi$, nên $\mathbb{S} \vDash \chi[x:=t]$ theo bổ đề về thay thế, suy ra $\mathcal{T}^\ast \vdash \chi[x:=t]$, và vì thế $\mathcal{T}^\ast \vdash \varphi$.

$\square$

 

Nói riêng, ta có $\mathbb{S} \vDash \mathcal{T}$. Điều này chứng minh định lý Gödel theo bổ đề ngữ nghĩa.

 

Hệ quả. (Định lý biểu diễn compact) Một hệ tiên đề $\Phi$ là thỏa mãn được khi và chỉ khi mọi tập con hữu hạn của $\Phi$ đều thỏa mãn được.

 

Lí do là vì hai khái niệm "thỏa mãn được" và "nhất quán" là tương đương, đồng thời $\Phi$ là nhất quán khi và chỉ khi mọi tập con hữu hạn của nó đều nhất quán.


Bài viết đã được chỉnh sửa nội dung bởi nmlinh16: Hôm qua, 02:05

$$x - \sum_{\substack{0 < \operatorname{Re} \rho < 1 \\ \zeta(\rho) = 0}} \frac{x^\rho}{\rho} - \log 2\pi - \frac{1}{2}\log(1-x^{-2}) = \frac{\psi(x+0) + \psi(x - 0)}{2}, \qquad \psi(x) = \sum_{\substack{p^n \le x \\  n \ge 1}} \log p.$$

 

"Wir müssen wissen, wir werden wissen." - David Hilbert






0 người đang xem chủ đề

0 thành viên, 0 khách, 0 thành viên ẩn danh