Mọi thuật ngữ mà máy tính, các bài hướng dẫn và bài tập dùng đến, định nghĩa ở một nơi.
Tra một thuật ngữ, xem ký hiệu của nó và mở ví dụ trong máy tính để thấy nó hoạt động. Thuật ngữ ở đây được làm nổi bật ở lần xuất hiện đầu tiên trong mỗi bài hướng dẫn.
Tất cả 62 thuật ngữ
Ngành nghiên cứu kết luận nào thực sự suy ra từ giả thiết nào.
Logic nghiên cứu hình thức của lập luận chứ không phải nội dung. Logic hình thức thay câu bằng ký hiệu, nhờ đó việc một kết luận có suy ra hay không được quyết định chỉ bởi dạng của lập luận và kiểm tra được bằng máy.
Một phát biểu hoặc đúng hoặc sai, không đồng thời cả hai.
Mệnh đề là câu trần thuật có đúng một giá trị chân lý. «Trời đang mưa» là một mệnh đề; câu hỏi hay câu mệnh lệnh thì không, vì ở chúng không có gì để đúng hay sai.
Một trong hai giá trị của mệnh đề: đúng hoặc sai.
Logic cổ điển gán cho mỗi mệnh đề đúng một trong hai giá trị chân lý, viết là ⊤ và ⊥ (hoặc 1 và 0). Mỗi hàng của bảng chân trị là một cách gán giá trị cho các biến cùng kết quả của công thức tại đó.
Mệnh đề bên trong không chứa liên từ logic nào.
Mệnh đề nguyên tử không tách được thành mệnh đề nhỏ hơn: trong nó không có phủ định, hội hay bất kỳ liên từ nào khác. Mọi thứ còn lại là mệnh đề phức, dựng từ các nguyên tử, và giá trị chân lý của nó do chúng quyết định.
Một chữ cái như p hay A thay cho một mệnh đề bất kỳ.
Biến mệnh đề là chỗ trống cho bất kỳ mệnh đề nào. Máy tính nhận các chữ cái đơn làm biến và dành cho mỗi biến một cột của bảng chân trị, với một hàng cho mỗi tổ hợp giá trị có thể.
Trong máy tínhp → qChuỗi ký hiệu mà ngữ pháp của ngôn ngữ thực sự cho phép.
Công thức chỉnh được dựng theo quy tắc: một biến là công thức chỉnh, và mọi công thức tạo từ các công thức nhỏ hơn bằng một liên từ cũng vậy. «p ∧ ∨ q» thì không, nên máy tính báo lỗi thay vì đoán.
Một cách gán giá trị chân lý cho mọi biến trong công thức.
Một phép gán cho biết mỗi biến nhận giá trị nào và do đó ấn định giá trị của cả công thức. Công thức có n biến thì có 2ⁿ phép gán — đúng bằng số hàng của bảng chân trị.
Tập tiền đề đưa ra để ủng hộ một kết luận.
Một lập luận khẳng định rằng kết luận suy ra từ các tiền đề. Nhập nó vào máy tính với dấu suy ra — tiền đề trước, kết luận sau — và mỗi hàng sẽ được kiểm tra xem có trường hợp nào tiền đề đúng mà kết luận sai không.
Trong máy tínhp → q, p ⊨ qMột phát biểu mà lập luận giả định để đi tới kết luận.
Tiền đề là điểm xuất phát của lập luận. Tính hợp lệ chỉ hỏi kết luận có đúng ở mọi nơi mà mọi tiền đề đều đúng hay không; các tiền đề có thực sự đúng hay không là câu hỏi khác, và đó là điều tính đúng đắn thêm vào.
Trong máy tínhp → q, p ⊨ qPhát biểu mà lập luận muốn xác lập.
Kết luận là điều các tiền đề được đưa ra để ủng hộ. Trong máy tính, đó là biểu thức sau dấu suy ra, và một lập luận là hợp lệ khi không phép gán nào làm mọi tiền đề đúng mà kết luận sai.
Trong máy tínhp → q, p ⊨ qKý hiệu dựng nên mệnh đề phức từ những mệnh đề đơn giản hơn.
Liên từ như ¬, ∧, ∨, → hay ↔ ghép các mệnh đề thành một mệnh đề lớn hơn mà giá trị chân lý chỉ phụ thuộc vào giá trị của chúng. Bảng chân trị ghi lại chính sự phụ thuộc ấy, mỗi hàng một tổ hợp đầu vào.
Đảo giá trị chân lý: ¬p đúng đúng khi p sai.
Phủ định là liên từ một ngôi duy nhất của logic mệnh đề. Viết là ¬p, ~p hay !p, nó biến đúng thành sai và sai thành đúng, nên phủ định hai lần trả lại mệnh đề ban đầu.
Trong máy tính¬pChỉ đúng khi cả hai phần đều đúng: p ∧ q.
Phép hội khẳng định cả hai thành phần của nó. Nó đúng ở đúng một hàng của bảng chân trị — hàng mà cả hai thành phần đều đúng — nên là liên từ hai ngôi khắt khe nhất.
Trong máy tínhp ∧ qĐúng khi ít nhất một phần đúng: p ∨ q.
Trong logic, phép tuyển là không loại trừ: p ∨ q đúng khi p đúng, khi q đúng và khi cả hai cùng đúng. Cách hiểu loại trừ của «hoặc», chỉ đúng khi hai phần khác nhau, là một liên từ riêng.
Trong máy tínhp ∨ qĐúng khi đúng một trong hai mệnh đề là đúng.
Tuyển loại trừ, viết ⊕ hay XOR, đúng khi hai thành phần khác nhau và sai khi chúng giống nhau. Nó là phủ định của tương đương và có thể viết thành (p ∨ q) ∧ ¬(p ∧ q).
Trong máy tính(p ∨ q) ∧ ¬(p ∧ q)p → q, chỉ sai khi p đúng và q sai.
Phép kéo theo vật chất không nói gì hơn «không xảy ra chuyện: tiền kiện đúng mà hậu kiện sai», nên nó tự động đúng mỗi khi tiền kiện sai. Vì thế p → q tương đương với ¬p ∨ q.
Trong máy tínhp → qp ↔ q, đúng khi hai phần có cùng giá trị chân lý.
Phép tương đương khẳng định mỗi vế với điều kiện là vế kia: nó đúng khi cả hai phần đều đúng và khi cả hai đều sai. Một tương đương là hằng đúng thì chính là một khẳng định về tương đương logic.
Trong máy tínhp ↔ qPhần «nếu» của mệnh đề kéo theo — chữ p trong p → q.
Tiền kiện là điều kiện mà mệnh đề kéo theo phụ thuộc vào. Khi nó sai thì cả mệnh đề kéo theo đều đúng bất kể hậu kiện, và phần lớn điều gây ngạc nhiên trong bảng của → đến từ đó.
Trong máy tínhp → qPhần «thì» của mệnh đề kéo theo — chữ q trong p → q.
Hậu kiện là điều mà mệnh đề kéo theo tuyên bố sẽ xảy ra nếu tiền kiện đúng. Hậu kiện đúng làm mệnh đề kéo theo đúng, nhưng không làm tiền kiện đúng: suy như thế là một ngụy biện hình thức.
Trong máy tínhp → qMệnh đề kéo theo với hai phần đổi chỗ: q → p.
Mệnh đề đảo của p → q là q → p, và hai cái không tương đương: máy tính tìm ra một hàng mà cái này đúng còn cái kia sai. Coi chúng thay thế được cho nhau chính là khẳng định hậu kiện.
Trong máy tínhq → p¬q → ¬p, luôn cùng giá trị chân lý với p → q.
Mệnh đề phản đảo phủ định cả hai phần của mệnh đề kéo theo rồi đổi chỗ chúng. Khác với mệnh đề đảo, nó thực sự tương đương với mệnh đề gốc, và đó là lý do chứng minh phản đảo hợp lệ trong toán học.
Trong máy tính(p → q) ≡ (¬q → ¬p)Phủ định của phép hội: đúng trừ khi cả hai đầu vào đều đúng.
NAND, viết là ↑, chính là ¬(p ∧ q). Nó đầy đủ về mặt hàm: mọi liên từ khác đều dựng được chỉ từ NAND, nên nó là công cụ chủ lực trong thiết kế mạch số.
Trong máy tính¬(p ∧ q)Phủ định của phép tuyển: chỉ đúng khi cả hai đầu vào đều sai.
NOR, viết là ↓, chính là ¬(p ∨ q). Như NAND, nó tự mình đầy đủ về mặt hàm, nên một mạch có thể dựng hoàn toàn bằng cổng NOR.
Trong máy tính¬(p ∨ q)Liên từ nào được áp dụng trước khi thiếu dấu ngoặc.
Phủ định gắn chặt nhất, rồi đến hội, tuyển, kéo theo và cuối cùng là tương đương. Vì thế ¬p ∧ q ∨ r đọc là ((¬p) ∧ q) ∨ r; dấu ngoặc thay đổi trật tự đó khi cách đọc mong muốn khác đi.
Trong máy tính¬p ∧ q ∨ rMỗi cách gán giá trị một hàng, kèm giá trị của công thức.
Bảng chân trị liệt kê toàn bộ 2ⁿ phép gán cho n biến của công thức và tính giá trị của nó ở từng phép gán. Vì vét cạn nên nó giải quyết mọi câu hỏi ngữ nghĩa của logic mệnh đề: tương đương, hợp lệ, thỏa được và những cái khác.
Trong máy tínhp → qCông thức đúng dưới mọi phép gán.
Công thức hằng đúng đúng ở mọi hàng của bảng chân trị nên chẳng nói gì về thế giới: p ∨ ¬p đúng dù p là gì. Hai công thức tương đương đúng khi mệnh đề tương đương giữa chúng là hằng đúng.
Trong máy tínhp ∨ ¬pCông thức sai dưới mọi phép gán.
Một mâu thuẫn như p ∧ ¬p sai ở mọi hàng của bảng chân trị. Suy ra được mâu thuẫn từ một tập giả định cho thấy chúng không thể cùng đúng — đó là động cơ của chứng minh phản chứng.
Trong máy tínhp ∧ ¬pCông thức đúng dưới một số phép gán và sai dưới số khác.
Công thức khả biến không phải hằng đúng cũng không phải mâu thuẫn: bảng chân trị của nó có ít nhất một hàng đúng và một hàng sai. Hầu hết công thức người ta viết ra đều khả biến, và chính điều đó khiến chúng mang thông tin.
Trong máy tínhp ∧ qCó phép gán nào làm công thức đúng hay không.
Một công thức là thỏa được khi ít nhất một hàng của bảng chân trị là đúng, và hàng đó là một mô hình của nó. Quyết định tính thỏa được là bài toán trung tâm của các bộ giải SAT và qua đó của phần lớn suy luận tự động.
Trong máy tínhp ∧ (p → q)Hai công thức có bảng chân trị giống hệt nhau.
Các công thức tương đương khớp nhau dưới mọi phép gán, nên cái này có thể thay cái kia ở bất cứ đâu mà không đổi nội dung. Đặt dấu bằng giữa hai biểu thức và máy tính sẽ so từng hàng của hai cột.
Trong máy tính(p → q) ≡ (¬p ∨ q)Kết luận đúng trong mọi phép gán mà các tiền đề đều đúng.
Viết là Γ ⊨ φ, hệ quả logic là điều mà một lập luận hợp lệ tuyên bố. Nó được kiểm tra bằng cách tìm phản ví dụ: một phép gán làm mọi tiền đề đúng và kết luận sai. Nếu không có, hệ quả thành lập.
Trong máy tínhp → q, p ⊨ qKhông phép gán nào làm tiền đề đúng và kết luận sai.
Tính hợp lệ là thuộc tính của hình thức lập luận, không phải của sự kiện: một lập luận hợp lệ có thể có tiền đề sai và kết luận sai. Điều nó không thể có là tiền đề đúng đi kèm kết luận sai.
Trong máy tínhp → q, p ⊨ qMột lập luận hợp lệ mà các tiền đề còn đúng trên thực tế.
Tính đúng đắn thêm một khẳng định thực tế vào một khẳng định hình thức: lập luận hợp lệ và các tiền đề của nó đúng. Riêng logic giải quyết nửa đầu; nửa sau thuộc về chủ đề mà lập luận bàn tới.
Phép gán làm các tiền đề đúng và kết luận sai.
Một phản mô hình chứng minh lập luận không hợp lệ — chỉ cần một hàng. Máy tính hiển thị hàng nó tìm được, biến câu «điều này không suy ra» thành một cách gán cụ thể mà bạn kiểm tra được bằng tay.
Trong máy tínhp → q ⊨ q → pCó phép gán làm mọi phát biểu trong tập cùng đúng.
Một tập tiền đề là nhất quán khi tất cả có thể cùng đúng. Tiền đề không nhất quán kéo theo mọi thứ, nên lập luận dựng trên chúng về mặt kỹ thuật là hợp lệ mà chẳng có giá trị gì.
Trong máy tínhp → q, ¬q ⊨ ¬pMột biến hoặc phủ định của nó, như p hay ¬p.
Literal là nguyên tử của các dạng chuẩn: một mệnh đề tuyển là tuyển của các literal, còn hạng tử tối tiểu là hội của chúng. Literal là dương khi biến đứng trần và âm khi biến bị phủ định.
Trong máy tính¬pMột tuyển của các literal, như p ∨ ¬q ∨ r.
Mệnh đề tuyển là một trong các nhóm trong ngoặc tạo nên dạng chuẩn hội. Vì phép hội chỉ đúng khi mọi thành phần đều đúng, công thức ở dạng CNF đúng đúng khi mọi mệnh đề tuyển của nó đều đúng.
Trong máy tínhp ∨ ¬q ∨ rMột HOẶC của các VÀ: tuyển của các hội các literal.
Mọi công thức đều có dạng chuẩn tuyển, và nó đọc thẳng từ bảng chân trị: mỗi hàng đúng cho một hội, nối với nhau bằng ∨. Máy tính còn đưa ra DNF tối giản, nói cùng một điều với ít literal hơn.
Trong máy tính(p ∧ q) ∨ (¬p ∧ r)Một VÀ của các HOẶC: hội của các mệnh đề tuyển.
Dạng chuẩn hội đọc từ các hàng sai của bảng chân trị, mỗi hàng một mệnh đề tuyển. Đây là định dạng đầu vào mà các bộ giải SAT chờ đợi, nên chuyển sang CNF là bước thường lệ của suy luận tự động.
Trong máy tính(p ∨ q) ∧ (¬p ∨ r)Một hội chỉ đích danh đúng một hàng của bảng chân trị.
Hạng tử tối tiểu nhắc đến mỗi biến một lần, có hoặc không có phủ định, nên đúng một phép gán thỏa mãn nó. Gom các hạng tử tối tiểu của những hàng đúng rồi nối bằng ∨ sẽ cho dạng chuẩn tuyển của công thức.
Trong máy tínhp ∧ ¬q ∧ rMột tuyển loại trừ đúng một hàng của bảng chân trị.
Hạng tử tối đại nhắc đến mỗi biến một lần và sai ở duy nhất một phép gán. Lấy hạng tử tối đại của mỗi hàng sai rồi nối bằng ∧ sẽ cho dạng chuẩn hội của công thức.
Trong máy tínhp ∨ ¬q ∨ rPhủ định đổi ∧ thành ∨ và ∨ thành ∧: ¬(p ∧ q) ≡ ¬p ∨ ¬q.
Luật De Morgan đẩy dấu phủ định vào trong một phép hội hay phép tuyển, đồng thời lật liên từ. Đó là cách đưa công thức về dạng chuẩn, và cách rút gọn phủ định trong mã nguồn lẫn trong mạch.
Trong máy tính¬(p ∧ q) ≡ ¬p ∨ ¬qPhủ định hai lần trả lại ban đầu: ¬¬p ≡ p.
Trong logic cổ điển, phủ định kép đúng theo cả hai chiều, nên ¬¬p và p luôn thay thế được cho nhau. Logic trực giác chỉ giữ chiều từ p sang ¬¬p, và đó là chỗ hai hệ thống rẽ lối.
Trong máy tính¬¬p ≡ pĐại số trên hai giá trị, với ∧, ∨ và ¬ làm phép toán.
Đại số Boole là logic mệnh đề viết dưới dạng số học trên 0 và 1, với các luật — giao hoán, phân phối, hấp thụ, De Morgan — cho phép biến đổi và rút gọn biểu thức. Đó là thứ toán học dùng để thiết kế mạch số.
Trong máy tính(p ∧ q) ∨ (p ∧ ¬q) ≡ pCách bày bảng chân trị thành lưới để thấy rõ chỗ rút gọn.
Bìa Karnaugh sắp các hàng sao cho hai ô kề nhau chỉ khác nhau một biến, và các mép nối vòng lại. Nó cũng được viết là bìa K, K-map hay kmap. Những nhóm chữ nhật gồm các số 1 kề nhau có kích thước 1, 2, 4 hay 8 khi đó đọc ra thành các hạng tử của biểu thức tối giản.
Trong máy tính(p ∧ q) ∨ (p ∧ ¬r)Một nhóm trên bìa không thể mở rộng thêm được nữa.
Hạng tử phủ là một hội các literal buộc công thức phải đúng; nó là nguyên tố khi bỏ đi bất kỳ literal nào cũng làm mất tính chất ấy. Trên bìa Karnaugh, các hạng tử nguyên tố là những hình chữ nhật cực đại gồm các số 1.
Hạng tử nguyên tố duy nhất phủ một số 1 nào đó.
Khi một số 1 trên bìa chỉ thuộc về một nhóm cực đại, nhóm đó buộc phải có mặt trong mọi cách phủ tối giản nên được lấy trước. Phần còn lại mới là phần thực sự phải đi tìm.
Phần tử mạch tính một liên từ trên các đầu vào của nó.
Các cổng AND, OR, NOT, NAND, NOR và XOR là bản đối ứng phần cứng của các liên từ. Công thức và mạch là cùng một đối tượng vẽ hai lần, nên máy tính có thể trình bày một biểu thức dưới dạng sơ đồ cổng.
Trong máy tính(p ∧ q) ∨ ¬rBước được phép đi từ những công thức đã có sang công thức mới.
Quy tắc suy diễn là một khuôn mẫu như modus ponens, áp dụng được mỗi khi có sẵn các công thức đúng dạng. Hệ chứng minh dựng từ một nhúm quy tắc như vậy, chọn sao cho chỉ những kết luận thực sự suy ra mới rút ra được.
Từ p → q và p suy ra q.
Modus ponens là quy tắc cơ bản của phép kéo theo: có mệnh đề kéo theo và tiền kiện của nó thì hậu kiện suy ra. Tính hợp lệ hiện rõ trong bảng chân trị — hàng duy nhất mà cả hai tiền đề đều đúng cũng có kết luận đúng.
Trong máy tínhp → q, p ⊨ qTừ p → q và ¬q suy ra ¬p.
Modus tollens đi ngược mệnh đề kéo theo: nếu hậu kiện sai thì tiền kiện không thể đúng. Đó là mệnh đề phản đảo đang hoạt động, và là hình thức của mọi lập luận bác bỏ một giả thuyết bằng cách kiểm tra dự đoán của nó.
Trong máy tínhp → q, ¬q ⊨ ¬pTừ p → q và q → r suy ra p → r.
Tam đoạn luận giả định nối các mệnh đề kéo theo lại với nhau, và chính điều đó làm cho những dẫn xuất dài trở nên khả thi: mỗi mắt xích đưa lập luận thêm một bước mà không khẳng định tiền đề nào.
Trong máy tínhp → q, q → r ⊨ p → rTừ p ∨ q và ¬p suy ra q.
Tam đoạn luận tuyển loại bỏ khả năng đã bị bác: nếu một trong hai khả năng đúng mà khả năng thứ nhất sai thì khả năng thứ hai phải đúng. Đó là quy tắc đứng sau lối suy luận loại trừ.
Trong máy tínhp ∨ q, ¬p ⊨ qChứng minh kết luận bằng cách áp dụng quy tắc từng bước.
Suy diễn tự nhiên rút ra kết luận từ tiền đề bằng các quy tắc nhập và khử cho từng liên từ, cho phép đặt giả định tạm rồi giải phóng sau. Nó chứng minh điều mà bảng chân trị kiểm tra, nhưng không phải duyệt hết mọi hàng.
Giả sử điều ngược lại, suy ra mâu thuẫn, kết luận điều ban đầu.
Để chứng minh φ, ta giả sử ¬φ và suy ra thứ gì đó dạng ψ ∧ ¬ψ. Vì không phép gán nào làm mâu thuẫn đúng, giả định không thể đứng vững và φ được suy ra. Các chứng minh về tính vô tỉ và tính vô hạn thường đi theo lối này.
Trong máy tínhp ∧ ¬pBước không hợp lệ đi từ p → q và q tới p.
Hậu kiện đúng không xác lập tiền kiện: có thể một nguyên nhân khác đã gây ra nó. Máy tính chỉ ra phản mô hình — p sai, q đúng — chính là hàng phân biệt điều này với modus ponens.
Trong máy tínhp → q, q ⊨ pBước không hợp lệ đi từ p → q và ¬p tới ¬q.
Mệnh đề kéo theo không nói gì về chuyện xảy ra khi tiền kiện sai, nên loại bỏ tiền kiện vẫn để ngỏ hậu kiện. Phản mô hình là hàng mà p sai còn q đúng.
Trong máy tínhp → q, ¬p ⊨ ¬qLogic nhìn vào bên trong mệnh đề, tới đối tượng và tính chất.
Logic vị từ thêm vị từ, hạng từ và lượng từ, nhờ đó «mọi số nguyên tố lớn hơn hai đều lẻ» trở thành một công thức thay vì một chữ cái. Nó biểu đạt mạnh hơn hẳn logic mệnh đề, và không bảng chân trị nào quyết định được nó.
Ký hiệu cho biết vị từ đúng với bao nhiêu đối tượng.
Hai lượng từ cổ điển là ∀ (mọi) và ∃ (có ít nhất một), và mỗi cái là phủ định của cái kia với phần thân bị phủ định. Biến mà lượng từ ràng buộc chính là thứ phân biệt logic vị từ với logic mệnh đề.
∀x φ: φ đúng với mọi đối tượng trong miền.
Một khẳng định phổ quát bị bác bỏ bởi chỉ một phản ví dụ và đúng một cách rỗng trên miền rỗng. ∀x φ tương đương với ¬∃x ¬φ — đối ứng của luật De Morgan cho lượng từ.
∃x φ: φ đúng với ít nhất một đối tượng trong miền.
Một khẳng định tồn tại được xác lập bằng cách chỉ ra một nhân chứng. ∃x φ tương đương với ¬∀x ¬φ, nên mỗi lượng từ đều định nghĩa được từ lượng từ kia cùng phủ định.
Logic mở rộng với «tất yếu» (□) và «khả dĩ» (◇).
Logic tình thái đánh giá công thức tại các thế giới khả dĩ thay vì tại một phép gán duy nhất: □φ đúng khi φ đúng ở mọi thế giới truy cập được, ◇φ đúng khi φ đúng ở một thế giới nào đó. Thay đổi nghĩa của «truy cập được» sẽ cho các hệ tình thái khác nhau.
