Category Theory Illustrated: Logic (2021)

 (abuseofnotation.github.io)
2 điểm bởi GN⁺ 2024-10-27 | 1 bình luận | Chia sẻ qua WhatsApp
  • Logic starts from atomic propositions accepted as true and builds larger propositions using operators such as and, or, and implies; as in category theory, composition is central.
  • Classical logic interprets propositions as true/false Boolean values, and logical operators as Boolean functions, handling negation, conjunction, disjunction, implication, and equivalence with truth tables.
  • The BHK interpretation of intuitionistic logic views propositions as objects that have proofs, interpreting A ∧ B as a pair of proofs and A → B as a function that turns a proof of A into a proof of B.
  • In some categories, objects correspond to propositions and morphisms to proofs; in orders, this appears as a preorder or partial order where A ≤ B means A → B.
  • Intuitionistic logic corresponds order-theoretically to Heyting algebra, and in general category theory to a bicartesian closed category; conjunction, disjunction, true, false, and implication correspond respectively to meet/join, terminal/initial, and exponential object.

Logic starting from propositions

  • Logic deals with formal rules that are consistent with themselves regardless of observation, and is a system for concluding or proving that something else is true when something is known.
  • A mathematical theory can be seen as logic plus additional definitions.
    • Set theory can be defined by adding the primitive concept of a set membership relation to the standard axioms of logic.
  • To begin logic, you need an initial set of propositions accepted as true or false.
    • These are called premises, atomic propositions, or primary propositions.
  • Two or more propositions become a single composite proposition through logical operators such as and, or, and implies/entails.
    • ∧ means and.
    • ∨ means or.
    • → means follows or implication.
  • Composite propositions can again be composed with other propositions, just like atomic propositions.

Modus ponens and tautologies

  • Modus ponens is an old logical pattern: if A is true and A → B is true, then B is also true.
    • Its form is (A ∧ (A ⇒ B)) → B.
    • It is expressed with examples such as “If Socrates is human, and if humans die, then Socrates dies.”
  • Logic deals not only with single operations but also with combinations of, and relationships among, multiple logical operations.
    • The relationship between and and implies appears in modus ponens.
    • The distributive laws of and and or are also a major topic of interest.
  • A tautology is a proposition that is always true regardless of the truth values of its component propositions.
    • Modus ponens is always true as an entire formula, whether A and B are true or false.
    • A proposition that is always false is called a contradiction.
    • Adding not to a tautology makes it a contradiction, and adding not to a contradiction makes it a tautology.
  • A proposition whose truth or falsity changes depending on values is called a contingent statement, and falls outside the main concerns of logic.
  • The simplest tautology is the law of identity, that each proposition implies itself.

Axiom schemas and logical systems

  • Tautologies become the basis of axiom schemas and rules of inference.
  • An axiom schema is a formula containing placeholders, and concrete propositions can be made by replacing the placeholders with propositions.
    • If you remove colors or concrete propositions from modus ponens, the general structure remains.
    • By inserting atomic or composite propositions into that structure, you can make a specific modus ponens proposition.
  • Rules of inference can be used in almost the same way as axiom schemas, and axiom schemas can also be applied like rules of inference.
  • Every tautology can be used as an axiom schema.
  • A logical system or formal system is a collection of axiom schemas and rules of inference, and it generates all possible propositions by applying them.
    • As an example, a system made up of five axiom schemas and the modus ponens rule of inference is presented.
    • The fact that such a logical system is complete is connected to Gödel's completeness theorem.

Truth-functional interpretation of classical logic

  • Classical logic is based on the dichotomy that a proposition is either true or false.
  • In the classical interpretation, propositions and operators are defined as follows.
    • A proposition is something true or false, like a Boolean value.
    • A logical operator is a function that takes one or more Boolean values and returns a Boolean value.
  • Negation ¬p is a unary operation, changing true to false and false to true.
    • The same content can be expressed with a truth table.
    • Double-negation elimination is proved by applying negation twice and returning to the starting value.
  • and takes two Boolean values and returns true only when both are true.
    • p ∧ q → p
    • p ∧ q → q
  • or returns true if at least one of two Boolean values is true.
    • p → p ∨ q
    • q → p ∨ q
  • implies, or material condition, is written p → q, and is false only when p is true and q is false.
    • In classical logic, p → q is the same as the case where ¬p ∨ q is true.
  • if and only if, or iff, is true when two propositions have the same value.
    • P ↔ Q is equivalent to P → Q ∧ Q → P.
  • The equivalence of p → q and ¬p ∨ q can be proved not only with truth tables but also with axioms and rules of inference.
    • A complete proof of equivalence requires proofs in both directions.

Intuitionistic logic and the BHK interpretation

  • Intuitionistic logic views proof as construction rather than the discovery of universal truth.
  • From this viewpoint, we cannot use the dichotomy that every proposition must be either true or false.
    • Some propositions may be unproved not because they are false, but because they lie outside the scope of the given logical system.
    • The twin prime conjecture is often presented as such an example.
  • In the Brouwer–Heyting–Kolmogorov (BHK) interpretation, proofs, rather than propositions, are central.
    • A proposition is something that has a proof.
    • Logical operators are constructions that make proofs from other proofs.
  • A proof of A ∧ B is a pair consisting of a proof of A and a proof of B, that is, a product.
  • A → B means that there exists a function converting a proof of A into a proof of B.
    • The set of proofs of A → B is expressed as the set of functions from A to B, that is, a hom-set.
    • If this set is empty, there is no way to turn a proof of A into a proof of B.
  • The BHK interpretation has no separate iff operator, but it does have arrows.
    • When there is a function from A to B and from B to A, the two propositions are treated as equivalent.
    • From the set viewpoint, this is a situation where the proof sets of the two propositions are isomorphic.
  • Negation does not simply mean that there is no proof; rather, one must show that assuming A is true leads to a contradiction.
    • ⊥ serves as the proof of a formula with no proof, namely False or the bottom value.
    • In BHK, ¬A is read as A → ⊥.
    • In set theory, ⊥ is represented by the empty set.

Viewing logic as a category

  • The BHK interpretation provides a high-level perspective for interpreting logic through category theory.
  • Some categories can be seen as logical systems.
    • Objects are propositions.
    • Morphisms are proofs.
  • Not every category becomes a logical system; conditions are needed so that there are objects corresponding to valid logical propositions and no objects corresponding to invalid propositions.
  • A category satisfying such conditions is called a bicartesian closed category.
  • As a simple case, looking first at an order, a logical system and its set of atomic propositions form a category.
    • If there is only one way from A to B, or differences are ignored, it becomes a preorder.
    • If propositions that follow from each other are regarded as equivalent, it becomes a partial order.
    • A ≤ B means A → B.
  • In a Hasse diagram, when A is below B, A → B holds.

Order-theoretic correspondences of logical operations

  • In the BHK interpretation, logical and and or appear as product and sum; in order theory, they correspond to meet and join.
  • To be a logical system, any two propositions must be combinable with and or or, so the order must have meet and join for all elements.
    • Such an order is called a lattice.
  • An important law between and and or is distributivity.
    • If A ∧ (B ∨ C) ≅ (A ∧ B) ∨ (A ∧ C) holds for all A, B, and C, it is a distributive lattice.
  • To express intuitionistic logic, the lattice must also have elements corresponding to True and False.
    • False is written ⊥, and is connected to the principle of explosion, that if there is a proof of False, then any proposition can be proved.
    • True is written ⊤; it follows from every proposition, but nothing meaningful follows from it by itself.
  • In an order, True and False are respectively the greatest object and the least object.
    • In category-theoretic terms, they correspond to the terminal object and the initial object.
    • A lattice with least and greatest elements is a bounded lattice.

Implication objects and exponential objects

  • A lattice expressing a logical system needs, for every pair A, B, an implication object representing the proposition that A implies B.
  • This object is defined by the modus ponens structure.
    • A ∧ (A ⇒ B) → B must hold.
  • This condition alone is not enough.
    • Other objects such as A ⇒ B ∧ C or A ⇒ B ∧ C ∧ D could fit in the same place.
    • The actual A ⇒ B is the greatest object among the Xs satisfying A ∧ X → B.
  • In order theory, A ⇒ B is called an exponential element or relative pseudo-complement.
    • It is the greatest X satisfying A ∧ X ≤ B.
  • Logically, the most trivial proposition X satisfying A ∧ X → B is the implication proposition A ⇒ B.
  • Category-theoretically, it is defined as an exponential object or internal homomorphism object.
    • There must be a morphism A × X → B.
    • From any other candidate object with the same property, there must exist a unique morphism to the actual exponential object.
  • This definition of the implication object fits intuitionistic logic.
    • In classical logic, because of the law of excluded middle, A ⇒ B simplifies to ¬A ∨ B.
  • Like meet, join, and implication objects, A ⇒ B is defined up to a unique isomorphism.

Heyting algebra and bicartesian closed categories

  • Intuitionistic logic consists of True, False, and, or, and implies.
  • Expressed as an order, it becomes a Heyting algebra.
    • It has join and meet.
    • It has greatest and least objects.
    • It has implication objects.
  • An intuitionistic logical system can be viewed as a Heyting algebra.
    • and and or are meet and join.
    • True and False are greatest and least objects.
    • implies is the exponential object.
  • If the same definition is adapted to general categories, it becomes a bicartesian closed category.
    • It has products and coproducts.
    • It has initial and terminal objects.
    • It has exponential objects.
  • An intuitionistic logical system can also be viewed as a bicartesian closed category.
    • and and or are product and coproduct.
    • True and False are terminal and initial objects.
    • implies is the exponential object.
  • A lattice that follows classical logic must be complemented in addition to being bounded and distributive.
    • For each proposition A, there is a unique ¬A satisfying A ∨ ¬A = 1 and A ∧ ¬A = 0.
    • Such a lattice is called a Boolean algebra.

A simple proof in categorical logic

  • A ∨ ⊤ ≅ ⊤ follows directly from the definition of join.
    • Join is the least upper bound greater than or equal to two objects.
    • Since the only object greater than or equal to ⊤ is ⊤ itself, the join of any A and ⊤ is ⊤.
    • Logically, this is the tautology “any A or True is True.”
  • If A → B exists, then A ∨ B = B.
    • If one of two objects is above the other, the join is the higher object.
    • This can be seen as a generalization of A ∨ ⊤ = ⊤.
    • This is because A → ⊤ always holds for every object A.
  • The law of identity can also be proved with an implication object.
    • A ⇒ A is the greatest X satisfying A ∧ X → A.
    • Since this condition holds for every X, it becomes the greatest object ⊤.
    • Therefore, A → A is always true.
  • If A semantically entails B in every model, A ⊨ B, then A ⇒ B also corresponds to ⊤.
    • Since A itself already implies B, A ∧ X → B holds for every X.
    • This is also called the deduction theorem.

Building logic with Free Heyting algebra

  • To perform logic, first choose the atomic propositions to use according to the problem domain.
  • If the chosen kind of logic is intuitionistic logic, you must draw composite propositions such as A ∧ B and A ∨ B as a graph for every A and B.
  • Since compositions of composite propositions must also be included again, the full list becomes infinite.
  • Whether one proposition implies another is checked by following paths of arrows out from the starting proposition.
  • Performing logic is the process of finding a path from what is already known to what one wants to prove, or of constructing a proof by manipulating proofs already in hand.
  • In intuitionistic logic, it is generally difficult to prove that some fact is unreachable from the axioms, that is, that it cannot be proved.

Bài viết liên quan

1 bình luận

 
GN⁺ 2024-10-27
Ý kiến trên Hacker News

  • Trang này thật sự rất tuyệt, và tôi đã gặp lại nó nhiều lần khi học các nội dung liên quan
    Dù vậy, tôi vẫn muốn bỏ một phiếu cho hướng học với Milewski. Học thứ này là cả một hành trình, và tác giả của ct-illustrated có vẻ vẫn đang ở giữa hành trình đó
    Milewski là người đã đi con đường ấy nhiều lần rồi, nên sách và blog của ông ấy là điểm khởi đầu tốt
    https://github.com/hmemcpy/milewski-ctfp-pdf Book
    https://bartoszmilewski.com/2014/10/28/category-theory-for-p... Blog

    • Tôi đã đọc hơn chục chương đầu của Milewski; vài chương đầu thật sự rất hay, nhưng văn phong không đưa ra định nghĩa và ký pháp chính xác ngày càng khiến tôi khó chịu
      Có vẻ ông ấy cho rằng cứ viết bằng văn xuôi nhẹ nhàng, thiếu chính xác thì cái gì cũng dễ hiểu hơn, nhưng vì thế nó gần như vô dụng với tư cách tài liệu tham khảo
      Hoàn toàn không phải vậy¹
      ¹) https://news.ycombinator.com/item?id=41756286
    • Tôi không hiểu bartoszmilewski đang nói gì, nên cuốn sách đó với tôi có vẻ vô dụng
      Nhưng ở chỗ làm, tôi đang dùng lý thuyết phạm trù cho toàn bộ mô hình miền của mình

  • Trước đây đã từng được thảo luận dưới một URL khác
    https://news.ycombinator.com/item?id=28660131 (2 bình luận)
    https://news.ycombinator.com/item?id=28660157 (112 bình luận)

  • Ở phần đầu cuốn sách, tôi bắt gặp câu này rất hay khi so sánh toán học với khoa học hay kỹ thuật
    “Vì điều này mà các nhà toán học rơi vào một vị thế kỳ lạ, có thể nói là rất đặc thù, nơi họ luôn phải biện hộ cho công việc mình làm dưới góc độ giá trị đối với các lĩnh vực học thuật khác. Xin nhấn mạnh lại, nếu chuyện này xảy ra với bất kỳ lĩnh vực học thuật nào khác thì sẽ bị xem là vô lý.”
    Bất kỳ ai từng học một lĩnh vực không dẫn trực tiếp tới kết quả kiếm ra tiền đều có thể đồng cảm với ý này, và thật vui khi nghe rằng cả những người có năng khiếu về số má cũng phải vật lộn với dao cạo của Milton Friedman

    • Vậy thì thật may khi nhiều dự án trong “nghiên cứu văn hóa” thực ra được tài trợ trực tiếp bởi Bộ Quốc phòng Mỹ và Bộ Ngoại giao Mỹ
      Toàn bộ nghiên cứu “hậu thực dân” ngày nay chẳng qua chỉ là backend của quyền lực mềm Mỹ, và khi chiến tranh nổ ra có lẽ còn sẽ là backend của cả quyền lực cứng

  • Sơ đồ vòng tròn trong vòng tròn sẽ không chịu tải tốt khi mở rộng quy mô nếu các vòng tròn bên trong luôn được đặt ở giữa theo chiều dọc

  • Có câu chuyện thành công nào về việc dùng lý thuyết phạm trù để giải quyết hữu ích một bài toán CS/SWE mà nếu không có lý thuyết phạm trù thì không giải được không? Monad không tính, vì nếu tình huống cần thì người ta tự nhiên cũng sẽ phát minh ra nó thôi
    Tôi đã học nó một năm ở cao học nhưng cuối cùng vẫn bỏ cuộc

    • Không có bài toán nào không thể mô hình hóa nếu thiếu lý thuyết phạm trù
      Một trong những định lý nền tảng nhất của bổ đề Yoneda trực tiếp nói rằng mọi bài toán được diễn đạt bằng ngôn ngữ của các phạm trù đều có thể được dịch sang ngôn ngữ của tập hợp và hàm số. Điều tương tự cũng đúng với mọi đối tượng toán học được định nghĩa bằng tập hợp, nên bạn luôn có thể thay tên bằng định nghĩa
      Phần mà ngôn ngữ phạm trù đóng góp vào khung ngầm của một lý thuyết không thể lớn hơn định nghĩa của “phạm trù”, mà định nghĩa đó thì rất nhỏ. Cũng giống như hỏi tại sao lại dùng nhóm trong khi “một phép toán trên tập hợp có tính kết hợp, tính đóng, đơn vị và nghịch đảo” có vẻ dễ tiếp cận hơn
      Đại số trừu tượng dựa trên một thư viện các định nghĩa chỉ những kiểu phép toán trên tập hợp vừa đủ đơn giản nhưng lại xuất hiện rất thường xuyên. Công cụ hay kỹ thuật không phải là thứ có thể tìm thấy bên trong định nghĩa
      Vành, không gian vectơ, mô-đun thường được chấp nhận ngay, nhưng với phạm trù thì lại chia thành người tin và người không tin. Tôi tò mò vì sao chuyện đó lại xảy ra
    • Ví dụ gần nhất mà tôi biết là công trình về UMAP
      Khi tôi phỏng vấn Leland McInnes, ông ấy giải thích khá chi tiết rằng lý thuyết phạm trù đã đóng vai trò lớn trong việc nối các điểm lại với nhau, dù trong mã nguồn thực tế của kết quả cuối cùng nó không nhất thiết là bắt buộc
      Nhìn vào mức cải thiện tương đối so với t-SNE, vốn là kỹ thuật tiên tiến nhất trước đó, đây là ví dụ duy nhất khiến tôi phải nghĩ lại về những chỉ trích của mình đối với cách người ta nói về lý thuyết phạm trù trong phần mềm
      https://arxiv.org/abs/1802.03426
    • Nó giống như hỏi: “Có câu chuyện thành công nào về việc dùng ô tô để đi đến nơi mà đi bộ không đến được không?”
      Lý thuyết phạm trù là một ngôn ngữ đồng thời là một công cụ, nên điều gì nói được bằng ngôn ngữ phạm trù thì cũng có thể nói bằng ngôn ngữ khác
      Giống như ô tô, nếu bạn học được cách lái — mà đường cong học tập ở đây cực kỳ dốc — thì bạn có thể đi nhanh hơn. Về nguyên tắc thì không có gì là không thể đến được chỉ vì bạn không nhắc tường minh đến các khái niệm của lý thuyết phạm trù
    • Khi bạn phát biểu lại điều mình đã hiểu trong một khung tổng quát hơn, bạn sẽ thấy rõ hơn nó thực sự có nghĩa gì và tách được bản chất ra khỏi những chi tiết lộn xộn
      Theo hiểu biết rất hạn chế của tôi, một phần quan trọng của lý thuyết phạm trù là đặc trưng hóa các đối tượng bằng tính chất phổ quát
      Một tính thực dụng khác của lý thuyết phạm trù là nó cung cấp ngôn ngữ chung để các nhà khoa học máy tính, nhà toán học và nhà vật lý cùng trao đổi. Nếu mọi người đều gọi cùng một mẫu hình bằng những cái tên khác nhau và các định nghĩa hơi không tương thích với nhau thì cộng tác sẽ không dễ
    • Ở Topos Institute, chúng tôi đang xây phần mềm mới mà hy vọng sẽ minh bạch hơn nhiều với những người vẫn chưa uống Kool-Aid của lý thuyết phạm trù
      Bản pre-alpha hiện chủ yếu dành cho mô hình hóa động lực học hệ thống, nhưng chúng tôi xem nền tảng phạm trù là thiết yếu cho phạm vi công việc mà mình nhắm tới. Tôi rất sẵn lòng nghe ý kiến của bất kỳ ai
      https://topos.site/blog/2024-10-02-introducing-catcolab/

  • Tôi nghĩ lý thuyết phạm trù hữu ích, nhưng có lẽ vẫn chưa phải trong điện toán
    Nếu không có việc thực tế buộc phải dùng, nó tất nhiên sẽ rất khó. Có thực sự cần phải hiểu thấu đáo tính chất phổ quát, hàm tử adjoint, và bổ đề Yoneda không? Nếu không cần, thì việc học xem chúng là gì sẽ rất vất vả
    Điều thú vị là kinh nghiệm lập trình hàm giúp ích cho việc hiểu lý thuyết phạm trù, nhưng chiều ngược lại thì không hẳn vậy. Ví dụ, đa hình tham số đem lại trực giác về biến đổi tự nhiên, và biến đổi tự nhiên là cốt lõi của mọi ứng dụng của lý thuyết phạm trù
    Những ứng dụng thật sự thuyết phục của lý thuyết phạm trù mang tính toán học rất cao. Có thể tìm thấy chúng trong tôpô đại số, lý thuyết biểu diễn, hình học đại số và logic phi cổ điển

  • Có lỗi
    “Modus ponens là một mệnh đề gồm hai mệnh đề khác, ở đây ký hiệu là A và B; nếu mệnh đề A đúng và mệnh đề A --> B cũng đúng, tức A hàm ý B, thì ta nói B cũng đúng. Ví dụ, nếu biết ‘Socrates là con người’ và ‘con người thì phải chết’, ta cũng biết ‘Socrates phải chết’.”
    Ví dụ này không phải là một trường hợp của modus ponens, vốn là quy tắc của logic mệnh đề, mà là tam đoạn luận hạng từ cần đến logic vị từ

  • Ở đây nói rằng “logic là khoa học về cái khả hữu”, nhưng chẳng phải logic nên là khoa học về cái tất định sao?
    Tôi cho rằng cốt lõi là cho phép ta nói một cách dứt khoát điều gì là hợp lệ và điều gì không

  • Ký pháp sơ đồ khá thú vị
    Tác giả có đưa ra các quy tắc suy luận cho các phép biến đổi bảo toàn chân lý của sơ đồ không?