Bên gỡ rối tơ lòng, bạn Thắng hỏi:
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).
thường được dùng để nói rằng “mệnh đề”
có thể suy ra (deduce) được từ các mệnh đề trong tập mệnh đề
cùng với một tập hợp
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à
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 [các bác làm AI, automatic theorem proving confirm nhé]. 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
, nghĩa là nếu đã có
và có
thì ta có thể “suy ra”
. 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.
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ì
cũng suy được từ
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
dẫn đến
. Đ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à
thì dẫn đến
. (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
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 
Chuyên mục: Lý thuyết tính toán | Bình luận (4) »