“Định lý sự đầy đủ” của Godel

NQH | 22/11/2007 |

Trong một cuốn sách em thì nó nói rằng nếu có cái điều kiện gì gì đó thì A |– B sẽ suy ra A |= B. Nhờ anh chỉ giùm cho em thấy sự khác biệt giữa 2 khái niệm A|–B và A|== B này cái…rồi có Gentzen type và Hilbert type gì gì đó …

Tôi không biết nhiều lắm về các loại deductive calculus, nhưng cũng cố thử trả lời bằng những gì tôi biết, qua một năm học logic cổ điển từ khoa Toán. Trong khi đó nhứng gì bạn Thắng và đa số dân KHMT đọc về logic (tôi đoán là) lại hướng đến logic cho AI cổ điển (hoặc databases), có nhiều chi tiết kỹ thuật hơn những gì tôi biết. Logic dành cho bên Toán không quan tâm đến implementation efficiency của deductive systems, còn logic cho AI và database buộc phải quan tâm vì lý do hiển nhiên. Các bác nào làm AI cổ điển (chắc hơi hiếm) và database giứp giùm nhé!Đoạn dưới đây chỉ nói về first-order logic (và trường hợp đặc biệt của nó là propositional logic).

$A \vdash \varphi$ thường được dùng để nói rằng “mệnh đề” $\varphi$ có thể suy ra (deduce) được từ các mệnh đề trong tập mệnh đề $A$ cùng với một tập hợp $\Lambda$ các tiên đề cho trước. (Chính xác hơn, thay vì “mệnh đề” thì phải dùng cụm từ well-formed formula (wff).)

Để thật sự biết là $A \vdash \varphi$ hay không, ta phải có một số luật suy dẫn và một tập tiên đề. Tập tiên đề cùng với tập luật suy dẫn gọi là deductive calculus. Hai loại calculus chính là loại Gentzen và loại Hilbert. Loại Gentzen có ít tiên đề, nhiều luật, và (có vẻ) thích hợp hơn cho tính toán . Loại Hilbert có rất nhiều tiên đề (có thể vô hạn) nhưng lại có rất ít luật. Loại này thích hợp cho chứng minh toán học.

Deductive calculus chỉ là một tập hợp các luật cơ bắp. Ví dụ, luật modus ponens bảo $\{ a, a \to b\} \vdash b$ , nghĩa là nếu đã có $a$ và có $a \to b$ thì ta có thể “suy ra” $b$ . Vì chúng chỉ là luật cơ bắp, ta có thể lập chương trình cho máy tính dựa trên các luật này.

$A \models \varphi$ thì phức tạp hơn nhiều. Nó đòi hỏi là dưới một “cấu trúc” bất kỳ nào thì $\varphi$ cũng suy được từ $A$ trong cấu trúc đó. Định nghĩa cấu trúc thỉ rắc rối, nhưng có thể lấy ví dụ đơn giản: có nhiều phép suy dẫn hay mệnh đề chỉ đúng cho cấu trúc số thực nhưng không đúng cho cấu trúc số tự nhiên, tỉ dụ như mệnh đề “với mọi x, tồn tại y sao cho x+y=0“.

Một deductive calculus gọi là “sound” nếu $A \vdash \varphi$ dẫn đến $A \models \varphi$ . Điều này hiển nhiên là cần thiết vì nếu không luật suy dẫn của ta bị hổng trong một nhánh nào đó của Toán học. Hầu hết các deductive calculus hữu dụng đều sound.

Ngược lại, Godel chứng minh được rằng, nếu ta chọn một deductive calculus đơn giản (kiểu Hilbert) với một số vô hạn các tiên đề và một luật suy dẫn duy nhất là luật modus ponens, thì cái calculus này còn “complete” nữa cơ, nghĩa là $A \models \varphi$ thì dẫn đến $A \vdash \varphi$ . (Cái calculus này cũng sound luôn, dễ chứng minh hơn completeness nhiều.)

Godel completeness theorem cho ta thấy rằng cái calculus nọ cực tốt: thay vì phải chứng minh rằng $A \models \varphi$ dưới một cấu trúc bất kỳ (số nguyên, số thực, phức, nhóm, trường, vành, hình topo, combinatorics và vô hạn các “cấu trúc” có thể có), thì ta “chỉ cần” duy dẫn logic dùng hệ tiên đề nọ và luật modus ponens là có thể chứng minh được $A \models \varphi$

Chủ đề : Lý thuyết tính toán and tagged Deductive Calculus, Godel, Định lý sự đầy đủ. Bookmark the permalink. Trackbacks are closed, but you can post a comment.

4 Comments

RongChoi

Posted 26/11/2007 at 5:10 am | Permalink
RC xin đóng góp một trả lời (tất nhiên cũng có tính chất “có thể sai” như trong giải thích của anh Hưng ) cho câu hỏi của bạng Thang về Logic mệnh đề (propositional logic) và Calculus mệnh đề (propositional calculus).

Nói chung, Calculus là một lý thuyết hình thức hóa của một Logic. Calculus mệnh đề là một lý thuyết hình thúc hóa của Logic mệnh đề. Ký hiệu
```
 \models 
```
mô tả cái đúng ngữ nghĩa trong logic (semantic truth) còn
```
 \vdash 
```
mô tả cái đúng hình thức (syntactic truth) bằng suy diễn trong Calculus.

Trong logic mệnh đề thì đơn vị cơ bản nhất là các mệnh đề (được gán giá trị chân lý đúng hoặc sai). Các mệnh đề phức hợp được xây dựng từ các mệnh đề đơn giản bằng các liên kết logic (ví dụ liên kếy
```
 \vee,  , \rightarrow  
```
; mệnh đề phức
```
A \rightarrow B 
```
. Các qui tắc ngữ nghĩa (mô tả thông qua bảng chân lý) cho ta qui tắc xác định giá trị chân lý đúng/sai của một mệnh đề phức từ các mệnh đề đơn giản.
```
S \models A 
```
được hiểu là công thức
```
A 
```
là hệ quả lô gíc của tập công thức
```
 S 
```
, được xác định thông qua các qui tắc ngữ nghĩa của logic mệnh đề (tức là với mọi phép gán giá trị đúng sai cho các mệnh đề trong
```
 S 
```
, nếu
```
 S 
```
đúng thì
```
 A 
```
đúng)

Chẳng hạn
```
 \models P \vee (\neg P) 
```
vì với mọi phép gán giá trị cho
```
 P 
```
thì
```
P \vee (\neg P) 
```
đều đúng, trong đó giá trị của
```
 (A \vee B) 
```
được mô tả bởi qui tắc ngữ nghĩa thông qua bảng chân lý. Như vậy
```
P \vee (\neg P) 
```
là một công thức đúng trong logic mệnh đề, nó được coi là đúng ngữ nghĩa (semantic truth). Chú ý là ta có thể mô tả
```
S \models A 
```
tương đương
```
\models (S \rightarrow A) 
```
và việc nói
```
A 
```
là hệ quả lô gíc của
```
 S 
```
tương đương với việc nói
```
  (S \rightarrow A) 
```
là công thức mệnh đề đúng.

Như vậy, đối với logic, việc ta quan tâm là việc xác định một công thức là đúng (ngữ nghĩa) hay không. Việc xác định giá trị của một mệnh đề phức bằng cách xét các phép gán gí trị đúng sai thông qua các qui tắc ngữ nghĩa là khá phức tạp (nếu có
```
n 
```
mệnh đề cơ bản thì có thể phải xét
```
 2^n 
```
trường hợp chẳng hạn). Do đó, cần có cách lập luận hiệu quả hơn. Từ đó cần phải hình thức hoá logic mệnh đề.

Calculus mệnh đề là một lý thuyết hình thức hóa của logic mệnh đề. Trong Calculus mệnh đề, có các công thức mệnh đề, liên kết logic (như đối với logic mệnh đề), nhưng thay vì các qui tắc ngữ nghĩa, nó có các sơ đồ tiên đề và một qui tắc suy diễn (Modus ponens như anh Hưng có nói).
```
 S \vdash A 
```
được hiểu là công thức
```
 A 
```
được suy diễn (hay dẫn xuất như bạn Thang nói) từ
```
 S 
```
, thông qua việc áp dụng các tiên đề và qui tắc suy diễn của Calculus mệnh đề.
Chẳng hạn
```
 \vdash P \vee (\neg P) 
```
phải được suy diễn từ các tiên đề và qui tắc suy diễn chứ không phải qua việc xét bảng giá trị như trong logic. Khi đó ta nói
```
 P \vee (\neg P) 
```
là một định lý của Calculus mệnh đề, nó được coi là đúng hình thức (syntactic truth). Chú ý là ta có thể mô tả
```
 S \vdash A 
```
tương đương
```
 \vdash (S \rightarrow A) 
```
và việc nói
```
 A 
```
suy diễn được từ
```
 S 
```
tương đương với việc nói
```
 (S \rightarrow A) 
```
là một định lý của Calculus.

Như vậy, đối với Calculus mệnh đề, việc ta quan tâm là việc xác định một công thức có là định lý (syntactic truth) hay không, việc này được thưc hiện thông thông qua các tiên đề, qui tắc suy diễn.

Đến đây, muốn việc suy luận trong Calculus (lý thuyết hình thức) phản ánh chính xác cái thực tế, cái ta muốn trong logic (lý thuyết có nội dung) thì cần phải chứng minh tính đúng đắn (soundness) và tính đầy đủ (completeness) của nó.
Soundness cho ta an tâm rằng : mọi định lý của Calculus mệnh đề (syntactic truth) đều là công thức mệnh đề đúng (semantic truth).
Completeness cho ta hiểu rằng : mọi công thức mệnh đề đúng của logic mệnh để đều là định lý của Calculus mệnh đề.
Như vậy Soundness và Completeness đảm bảo cho ta Calculus mệnh đề là một lý thuyết hình thức hoá tốt của Logic mệnh đề, nó là cầu nối giữa cái đúng
ngữ nghĩa (semantic trith) và đúng hình thức (syntactic truth).

Gentzen type hay Hilbert type là các phương pháp hình thức hoá khác nhau của logic mệnh đề, chúng sẽ dẫn đến các calculus với các suy diễn
```
 \vdash 
```
khác nhau cho
```
 \models
```
. Nói chung, để chứng minh hai calculus (với cùng một qui tắc suy diễn modus ponens) là tương đương, ta chỉ cần chứng minh các tiên đề của Calculus này là định lý của Calculus kia và ngược lại.

Tóm lại, ký hiệu
```
 \models 
```
mô tả cái đúng ngữ nghĩa trong logic,
```
 \vdash 
```
mô tả cái đúng hình thức (suy diễn được) trong Calculus. Các định lý soundness và completeness là cầu nối giữa đúng ngữ nghĩa và đúng hình thức (hay giữa
```
 \models 
```
và
```
 \vdash ) 
```
Trên đây là ý kiến của mình chỉ dành cho logic mệnh đề. Đối với first-order logic thì phức tạp hơn. Các khái niệm Soundness, Completeness, InCompleteness cũng phức tạp hơn vì sự liên hệ giữa đúng ngữ nghĩa và đúng hình thức được mô tả không thật đơn giản như với logic mệnh đề, cần thông qua các khái niệm structure, model…

Một cấu trúc của một lý thuyết K (calculus mệnh đề chẳng hạn) là một thể hiện của K trong đó mọi tiên đề riêng của K đều đúng.

Một lý thuyết K (calculus mệnh đề chẳng hạn) là sound nếu
Reply
RongChoi

Posted 26/11/2007 at 5:14 am | Permalink

Sorry, 2 câu cuối trong bài trên (ừ “Một cấu trúc của một lý thuyết K …”) mình viết nháp lung tung, thấy dài quá bỏ đi, mà vẫn copy-paste vào đây

Reply
Thang

Posted 26/11/2007 at 10:52 am | Permalink

Cám ơn anh Hưng và anh RC, lúc em post câu hỏi này đợi hai ngày sau không thấy reply, em tưởng chắc “chìm” rồi không ngờ lại thấy các anh trả lời ở đây. (Bất ngờ quá). Câu trả lời của các anh em còn phải nghiền dài dài.
Em đang định tìm hiểu về computation (em hiểu là = computability + complexity) theory nhưng chỉ ở mức “biết” thôi thì liệu có phải đến mức biết luôn cả 3 Godel theorems không các anh nhỉ ?

Reply
Ngô Quang Hưng

Posted 26/11/2007 at 11:14 am | Permalink

Tôi nghĩ sv học KHMT thì phải biết 3 định lý Godel (như đã đề cập sơ bộ trong bài “Chung Qui Chỉ Tại Cantor”). Học về computability/complexity theory thì lại càng phải biết 3 định lý Godel.

Thật tình mà nói, khám phá của Godel tuyệt đối original nhưng cũng tuyệt đối đơn giản (sau khi đã xem chứng minh). Chẳng qua nó là cái liar paradox bằng ngôn ngữ logic hình thức. Vì thế, đọc hiểu định lý Godel không khó khăn đâu, bạn cố gắng vượt qua ngưỡng “notations” phiền hà của logic.

Reply

“Định lý sự đầy đủ” của Godel

4 Comments

Post a Comment Cancel reply

Thông điệp ngắn

Phản hồi mới

Bài mới

Thư khố

Chuyên Mục

Báo chí

Bảo mật

Blog Việt

Chưa phân loại

Giáo dục

Kỹ thuật

Khoa học khác

Kinh tế, luật pháp, xã hội

Lý thuyết & thuật toán

Mạng

Não học

Toán học

Vật Lý