Logic bậc nhất

Logic bậc nhất - còn được gọi là logic vị từ (predicate logic), quantificational logic, và phép tính vị từ bậc nhất (first-order predicate calculus) là một tập hợp các hệ thống hình thức được sử dụng trong toán học, triết học, ngôn ngữ học và khoa học máy tính. Logic bậc nhất sử dụng các biến lượng từ hóa trên các đối tượng phi logic và cho phép sử dụng các câu có chứa các biến, do đó, thay vì các mệnh đề như Socrates là một người đàn ông, có thể có các biểu thức dạng "tồn tại x sao cho x là Socrates và x là một người đàn ông", và "tồn tại" là một lượng từ trong khi x là một biến. Điều này phân biệt nó với logic mệnh đề, không sử dụng các lượng từ hay các quan hệ; theo nghĩa này, logic mệnh đề là nền tảng của logic bậc nhất.

Một lý thuyết về một chủ đề thường là một logic bậc nhất cùng với một miền diễn ngôn được chỉ định trong đó các biến lượng hóa được khởi tạo, các hàm từ miền vào chính nó, một số hữu hạn các vị từ xác định trên miền đó và một tập hợp các tiên đề được tin là đúng cho những đối tượng trong miền diễn ngôn. (Đôi khi "lý thuyết" cũng được hiểu theo nghĩa hình thức hơn, là một tập hợp các câu trong logic bậc nhất.)

Cụm từ "bậc nhất" phân biệt logic bậc nhất với logic bậc cao hơn trong đó có các vị từ có các đối số là các vị từ khác hoặc các hàm. Trong các lý thuyết bậc nhất, các vị từ thường được liên kết với các tập hợp. Trong các lý thuyết bậc cao được diễn giải, các vị từ có thể được hiểu là tập hợp của các tập hợp.

Giới thiệu

Trong khi logic mệnh đề quan tâm đến các mệnh đề dưới dạng phát biểu đơn giản, logic bậc nhất bao hàm cả các vị từ (các phát biểu.chứa biến, predicate) và các phép lượng hóa.

Một vị từ lấy một thực thể hoặc các thực thể trong miền diễn ngôn làm đầu vào trong khi đầu ra là Đúng hoặc Sai. Hãy xem xét hai câu "Socrates là một triết gia" và "Plato là một triết gia". Trong logic mệnh đề, các câu này được xem là không liên quan và có thể được biểu thị, ví dụ, bởi các biến như p và q. Vị ngữ "là một triết gia" xuất hiện trong cả hai câu, có cấu trúc chung là " a là một triết gia". Biến a được khởi tạo là "Socrates" trong câu đầu tiên và được khởi tạo là "Plato" trong câu thứ hai. Trong khi logic bậc nhất cho phép sử dụng các vị từ, chẳng hạn như "(a) là một triết gia" trong ví dụ này, logic mệnh đề không cho phép điều đó.

Mối quan hệ giữa các vị từ có thể được phát biểu bằng cách sử dụng các phép nối logic. Ví dụ, xem xét công thức bậc nhất "nếu a là một triết gia, thì a là một học giả". Công thức này là một tuyên bố có điều kiện với "a là một triết gia" như giả thuyết của nó và " a là một học giả" như kết luận của nó. Sự thật của công thức này phụ thuộc vào đối tượng nào được biểu thị bởi a, và dựa trên các diễn giải của các vị ngữ "là một triết gia" và "là một học giả". Trong công thức này, "nếu... thì..." là một phép nối logic giữa hai vị từ "là một triết gia" và "là một học giả".

Các lượng từ có thể được áp dụng lên các biến trong một công thức. Ví dụ, biến a trong công thức trước có thể được áp dụng một lượng từ phổ dụng để tạo thành câu bậc nhất "Với mọi a, nếu a là nhà triết học, thì a là học giả". Lượng từ phổ dụng "với mọi" trong câu này thể hiện ý tưởng rằng tuyên bố "nếu a là một triết gia, thì a là một học giả" đúng cho tất cả các lựa chọn của a.

Phủ định của câu "Với mọi a, nếu a là một nhà triết học, thì a là một học giả" tương đương logic với câu "Tồn tại a, a là một nhà triết học và không phải là một học giả". Lượng từ hiện sinh "tồn tại" thể hiện ý tưởng rằng tuyên bố "a là một nhà triết học và không phải là một học giả" nghiệm đúng với một số (ít nhất một) lựa chọn của a.

Các vị từ "là một triết gia" và "là một học giả" đều có một biến duy nhất. Nói chung, các vị từ có thể có nhiều biến. Trong câu bậc nhất "Socrates là thầy của Plato", vị từ "là thầy của" có hai biến (và giá trị của hai biến đó trong câu bậc nhất trên lần lượt là "Socrates" và "Plato". (Lưu ý rằng về mặt ngữ pháp ngôn ngữ tiếng Việt, Socrates là chủ ngữ và Plato là bổ ngữ).

Một diễn giải (hoặc một mô hình) của một công thức bậc nhất xác định ý nghĩa của từng vị từ và các thực thể có thể khởi tạo các vị từ (tức là các thực thể mà các biến có thể biểu thị). Các thực thể này tạo thành miền diễn ngôn hoặc vũ trụ, thường được yêu cầu là một tập hợp khác rỗng. Ví dụ, trong một diễn giải với miền diễn ngôn bao gồm tất cả mọi người (trên thế giới, còn sống hay đã chết hay chưa sinh ra) và vị từ "là một nhà triết học" được hiểu là "là tác giả của cuốn Cộng hòa ", câu "Tồn tại a sao cho a là một nhà triết học" có giá trị sự thật ĐÚNG, bởi Plato là tác giả của cuốn Cộng hòa.

Cú pháp

Có hai phần chính của logic bậc nhất. Cú pháp xác định chuỗi ký tự hữu hạn nào là biểu thức hợp pháp trong logic bậc nhất, trong khi ngữ nghĩa xác định ý nghĩa đằng sau các biểu thức này.

Bảng chữ cái

Các ký hiệu logic

• Các lượng từ ∀ và ∃
• Các phép nối logic
• Dấu ngoặc đơn, ngoặc nhọn và các ký hiệu chấm câu khác.
• Một tập hợp vô hạn các biến, thường được biểu thị bằng các chữ cái viết thường ở cuối bảng chữ cái x, y, z,.... Các chỉ số thường được sử dụng để phân biệt các biến: x₀, x₁, x₂,... .
• Một ký hiệu đẳng thức =

Ngữ nghĩa

Một diễn giải của một ngôn ngữ bậc nhất gán một giải nghĩa cho mỗi ký hiệu khác ký hiệu logic trong ngôn ngữ đó. Nó cũng xác định một miền diễn ngôn chỉ định phạm vi của các lượng từ. Kết quả là mỗi từ (term) được gán một đối tượng mà nó đại diện, mỗi vị từ được gán một thuộc tính của các đối tượng và mỗi câu được gán một giá trị sự thật. Theo cách này, một diễn giải cung cấp ý nghĩa ngữ nghĩa cho các từ, vị từ và câu của logic bậc nhất. Nghiên cứu về các diễn giải của ngôn ngữ hình thức được gọi là ngữ nghĩa hình thức.

Xem thêm

• Logic toán
• Logic bậc hai

Tham khảo

• A Concise Introduction to Mathematical Logic, 2010, ISBN 978-1-4419-1220-6
• Andrews, Peter B. (2002); An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed., Berlin: Kluwer Academic Publishers. Available from Springer.
• Avigad, Jeremy; Donnelly, Kevin; Gray, David; and Raff, Paul (2007); "A formally verified proof of the prime number theorem", ACM Transactions on Computational Logic, vol. 9 no. 1 doi:10.1145/1297658.1297660
• Barwise, Jon (1977). “An Introduction to First-Order Logic”. Trong Barwise, Jon (biên tập). Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics. Amsterdam, NL: North-Holland (xuất bản 1982). ISBN 978-0-444-86388-1.
• Barwise, Jon; and Etchemendy, John (2000); Language Proof and Logic, Stanford, CA: CSLI Publications (Distributed by the University of Chicago Press)
• Bocheński, Józef Maria (2007); A Précis of Mathematical Logic, Dordrecht, NL: D. Reidel, translated from the French and German editions by Otto Bird
• Ferreirós, José (2001); The Road to Modern Logic — An Interpretation, Bulletin of Symbolic Logic, Volume 7, Issue 4, 2001, pp. 441–484, doi:10.2307/2687794, JSTOR 2687794
• Logic, Language, and Meaning, Volume 2: Intensional Logic and Logical Grammar
• Hilbert, David; and Ackermann, Wilhelm (1950); Principles of Mathematical Logic, Chelsea (English translation of Grundzüge der theoretischen Logik, 1928 German first edition)
• Hodges, Wilfrid (2001); "Classical Logic I: First Order Logic", in Goble, Lou (ed.); The Blackwell Guide to Philosophical Logic, Blackwell
• Ebbinghaus, Heinz-Dieter; Flum, Jörg; and Thomas, Wolfgang (1994); Mathematical Logic, Undergraduate Texts in Mathematics, Berlin, DE/New York, NY: Springer-Verlag, Second Edition, ISBN 978-0-387-94258-2
• Tarski, Alfred and Givant, Steven (1987); A Formalization of Set Theory without Variables. Vol.41 of American Mathematical Society colloquium publications, Providence RI: American Mathematical Society, ISBN 978-0821810415

Liên kết ngoài

Tiếng Anh

• Hazewinkel, Michiel biên tập (2001), “Predicate calculus”, Bách khoa toàn thư Toán học, Springer, ISBN 978-1-55608-010-4
• Stanford Encyclopedia of Philosophy: Shapiro, Stewart; "Classical Logic". Covers syntax, model theory, and metatheory for first-order logic in the natural deduction style.
• Magnus, P. D.; forall x: an introduction to formal logic. Covers formal semantics and proof theory for first-order logic.
• Metamath: an ongoing online project to reconstruct mathematics as a huge first-order theory, using first-order logic and the axiomatic set theory ZFC. Principia Mathematica modernized.
• Podnieks, Karl; Introduction to mathematical logic
• Cambridge Mathematical Tripos notes (typeset by John Fremlin). These notes cover part of a past Cambridge Mathematical Tripos course taught to undergraduate students (usually) within their third year. The course is entitled "Logic, Computation and Set Theory" and covers Ordinals and cardinals, Posets and Zorn's Lemma, Propositional logic, Predicate logic, Set theory and Consistency issues related to ZFC and other set theories.
• Tree Proof Generator can validate or invalidate formulas of first-order logic through the semantic tableaux method.

Tiếng Việt

• Tài liệu trực tuyến tại zun.vn