Category Theory Illustrated: Logic (2021)

 (abuseofnotation.github.io)
2 पॉइंट द्वारा GN⁺ 2024-10-27 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • Logic starts from atomic propositions accepted as true and builds larger propositions with operators such as and, or, and implies; as in category theory, composition is central
  • Classical logic interprets propositions as true/false Boolean values, logical operators as Boolean functions, and handles negation, conjunction, disjunction, implication, and equivalence through truth tables
  • The BHK interpretation of intuitionistic logic treats 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 order theory, this appears as a preorder or partial order where A ≤ B means A → B
  • Intuitionistic logic corresponds order-theoretically to a 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 objects

Logic Starting from Propositions

  • Logic deals with formal rules that are consistent with themselves regardless of observation; it 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 set membership relation to the standard logical axioms
  • To start 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 one 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 “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 law between and and or is also a major subject of interest
  • A tautology is a proposition that is always true regardless of the true/false 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 yields a contradiction, and adding not to a contradiction yields a tautology
  • A proposition whose truth or falsity varies depending on values is called a contingent statement, and lies outside logic’s main concern
  • The simplest tautology is the law of identity, that each proposition implies itself

Axiom Schemas and Logical Systems

  • Tautologies become the basis for axiom schemas and rules of inference
  • An axiom schema is a formula containing placeholders; concrete propositions can be created 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 create 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; by applying them, it generates all possible propositions
    • 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-Function Interpretation of Classical Logic

  • Classical logic is based on the dichotomy that every proposition is either true or false
  • In the classical interpretation, propositions and operators are defined as follows
    • A proposition is something that is 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, turning true into false and false into true
    • The same content can be expressed with a truth table
    • Double-negation elimination is proved by showing that applying negation twice returns 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 sees proofs not as discoveries of universal truths, but as constructions
  • From this viewpoint, the dichotomy that every proposition is necessarily true or false cannot be used
    • Some propositions may be unproved not because they are false, but because they are 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 are placed at the center rather than propositions
    • A proposition is something that has a proof
    • Logical operators are constructions that create proofs from other proofs
  • A proof of A ∧ B is a pair, or product, consisting of a proof of A and a proof of B
  • A → B means that there exists a function that transforms 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 operation, but it has arrows
    • When there is a function from A to B and a function from B to A, the two propositions are treated like equivalents
    • From a set-theoretic viewpoint, this is the 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
    • ⊥ plays the role of 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

Seeing Logic as a Category

  • The BHK interpretation provides a high-level perspective for interpreting logic through category theory
  • Some categories can be seen like 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, if we first look at an order, a logical system and a set of atomic propositions form a category
    • If there is only one way from A to B, or if 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 lies below B, A → B holds

Order-Theoretic Correspondence of Logical Operations

  • Logic’s and and or appear as product and sum in the BHK interpretation, and correspond to meet and join in order theory
  • To become a logical system, it must be possible to combine any two propositions 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 represent 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, 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-theory 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 representing 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 sufficient
    • Other objects such as A ⇒ B ∧ C or A ⇒ B ∧ C ∧ D can also 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
  • Categorically, 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 matches intuitionistic logic
    • In classical logic, due to the law of excluded middle, A ⇒ B simplifies to ¬A ∨ B
  • Like meet, join, and implication objects, A ⇒ B is also defined up to unique isomorphism

Heyting Algebra and Bicartesian Closed Category

  • Intuitionistic logic consists of True, False, and, or, and implies
  • Expressed as an order, this 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 seen as a Heyting algebra
    • and and or are meet and join
    • True and False are greatest and least objects
    • implies is an exponential object
  • Translating the same definition to general categories gives 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 seen as a bicartesian closed category
    • and and or are product and coproduct
    • True and False are terminal and initial objects
    • implies is an exponential object
  • A lattice following classical logic must be bounded and distributive, and also complemented
    • 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

Simple Proofs from Categorical Logic

  • A ∨ ⊤ ≅ ⊤ follows directly from the definition of join
    • Join is the least upper bound greater than or equal to the two objects
    • Since the only object greater than or equal to ⊤ is ⊤ itself, the join of any A and ⊤ is ⊤
    • Logically, it is the tautology “any A or True is True”
  • If A → B exists, then A ∨ B = B
    • If one of the two objects is above the other, the join is the higher object
    • This can be seen as a generalization of A ∨ ⊤ = ⊤
    • Because A → ⊤ always holds for every object A
  • The law of identity is also proved with the implication object
    • A ⇒ A is the greatest X satisfying A ∧ X → A
    • This condition holds for every X, so it becomes the greatest object ⊤
    • Therefore A → A is always true
  • If A semantically entails B in every model, written 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

Creating 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
  • Compositions of composite propositions must also be included again, so the full list becomes infinite
  • Whether one proposition implies another is checked by following paths of arrows going out from the starting proposition
  • Performing logic is the process of finding a path from what is already known to what you want to prove, or of constructing a proof by manipulating proofs you already have
  • In intuitionistic logic, it is generally difficult to prove that some fact is unreachable from the axioms, that is, that it cannot be proved

संबंधित पढ़ाई

1 टिप्पणियां

 
GN⁺ 2024-10-27
Hacker News की टिप्पणियां

  • यह पेज वाकई बेहतरीन है, और संबंधित सामग्री पढ़ते समय कई बार सामने आया है
    फिर भी मैं Milewski से सीखने के पक्ष में वोट दूंगा। इसे सीखना एक यात्रा है, और लगता है ct-illustrated के लेखक अभी उस यात्रा के बीच में हैं
    Milewski वह व्यक्ति हैं जो इस रास्ते पर पहले ही कई बार जा चुके हैं, इसलिए उनकी किताब और ब्लॉग अच्छे शुरुआती बिंदु हैं
    https://github.com/hmemcpy/milewski-ctfp-pdf Book
    https://bartoszmilewski.com/2014/10/28/category-theory-for-p... Blog

    • मैंने Milewski के शुरुआती करीब दर्जन भर अध्याय पढ़े, और पहले कुछ अध्याय सचमुच अच्छे थे, लेकिन सटीक परिभाषाएं और notation न देने वाली शैली धीरे-धीरे परेशान करने लगी
      लगता है वे मानते हैं कि हल्की-फुल्की और असटीक गद्य शैली में लिखने से कुछ भी समझना आसान हो जाता है, लेकिन इसी वजह से यह reference book के तौर पर लगभग बेकार हो जाती है
      बिल्कुल ऐसा नहीं है¹
      ¹) https://news.ycombinator.com/item?id=41756286
    • bartoszmilewski क्या कह रहे हैं, यह मुझे समझ नहीं आता, इसलिए वह किताब मेरे लिए बेकार लगती है
      लेकिन काम पर मैं अपने पूरे domain model में category theory इस्तेमाल कर रहा हूं

  • पहले किसी और URL पर इस पर चर्चा हो चुकी है
    https://news.ycombinator.com/item?id=28660131 (2 comments)
    https://news.ycombinator.com/item?id=28660157 (112 comments)

  • किताब के शुरुआती हिस्से में, गणित की तुलना science या engineering से करते हुए यह शानदार वाक्य मिला
    “इसी कारण गणितज्ञ एक अजीब, और कहें तो अनोखी स्थिति में आ जाते हैं, जहां उन्हें दूसरे academic क्षेत्रों के लिए value के संदर्भ में अपने काम का लगातार बचाव करना पड़ता है। फिर से जोर देकर कहें, किसी भी दूसरे academic क्षेत्र के लिए ऐसी बात बेतुकी मानी जाएगी।”
    जिसने भी ऐसा क्षेत्र पढ़ा है जो सीधे पैसे कमाने वाले परिणामों तक नहीं पहुंचता, वह इस अवधारणा से जुड़ पाएगा, और यह सुनना अच्छा है कि numbers में प्रतिभा रखने वाले लोगों को भी Milton Friedman के razor से जूझना पड़ता है

    • तो फिर यह अच्छी बात है कि “cultural studies” के कई projects को असल में अमेरिकी रक्षा विभाग और विदेश विभाग से सीधे funding मिलती है
      आज “postcolonialism” का पूरा अध्ययन अमेरिकी soft power के backend से ज्यादा कुछ नहीं है, और युद्ध होने पर शायद hard power का backend भी बन जाएगा

  • अगर अंदर वाले circles हमेशा vertical center में रखे जाएं, तो circle के अंदर circle वाला diagram बड़े scale पर अच्छा टिकता नहीं है

  • क्या category theory का इस्तेमाल करके CS/SWE की कोई ऐसी समस्या उपयोगी ढंग से हल करने की success story है जिसे category theory के बिना हल नहीं किया जा सकता था? Monad इसमें count नहीं होता, क्योंकि स्थिति की जरूरत हो तो आप उसे naturally invent कर लेते हैं
    मैंने grad school में इसे 1 साल पढ़ा, लेकिन अंत में छोड़ दिया

    • ऐसी कोई समस्या नहीं है जिसे category theory के बिना model न किया जा सके
      category theory के सबसे बुनियादी प्रमेयों में से एक, Yoneda lemma, सीधे कहता है कि categories की भाषा में व्यक्त हर समस्या को sets और functions की भाषा में translate किया जा सकता है। यही बात sets से define होने वाली हर mathematical object पर भी लागू होती है, इसलिए किसी नाम को कभी भी उसकी definition से बदला जा सकता है
      categorical language किसी theory के implicit framework में जितना योगदान देती है, वह “category” की definition से ज्यादा नहीं हो सकता, और वह definition बहुत छोटी है। यह पूछने जैसा है कि “associativity, closure, identity element और inverse के साथ set पर operation” ज्यादा approachable है, तो फिर group क्यों इस्तेमाल करें
      abstract algebra, sets पर sufficiently common simple operation types को इंगित करने वाली definitions की library पर आधारित है। tools या techniques ऐसी चीजें नहीं हैं जो definition के अंदर मिलती हों
      rings, vector spaces और modules को अपने-आप तुरंत स्वीकार कर लिया जाता है, लेकिन categories के मामले में believers और non-believers बंट जाते हैं। मुझे आश्चर्य है कि ऐसा क्यों होता है
    • मुझे जो सबसे नजदीकी उदाहरण पता है वह UMAP का काम है
      जब मैंने Leland McInnes का interview लिया था, उन्होंने विस्तार से बताया कि final result के वास्तविक code में जरूरी न होने पर भी category theory ने कई dots connect करने में बड़ी भूमिका निभाई
      पहले की state-of-the-art technique t-SNE की तुलना में relative improvement देखकर, software में category theory पर बात करने के तरीके को लेकर मेरी आलोचना पर फिर से सोचने को मजबूर करने वाला यह एकमात्र उदाहरण है
      https://arxiv.org/abs/1802.03426
    • यह पूछने जैसा है, “क्या कोई success story है कि car का इस्तेमाल करके ऐसी जगह गए जहां पैदल नहीं जा सकते थे?”
      category theory एक भाषा और tool है, इसलिए category theory की भाषा में जो कहा जा सकता है, वह दूसरी भाषाओं में भी कहा जा सकता है
      car की तरह, अगर आप चलाना सीख लें—और इसका learning curve बहुत steep है—तो आप ज्यादा तेजी से जा सकते हैं। सिद्धांत रूप में ऐसा कुछ नहीं है जहां पैदल नहीं जा सकते, बशर्ते category theory concepts का स्पष्ट उल्लेख न करें
    • जो बात आप पहले से समझते हैं उसे अधिक general framework में फिर से formalize करने पर, यह बेहतर दिखता है कि उसका असल मतलब क्या है और messy details से essence को अलग किया जा सकता है
      मेरी बहुत सीमित समझ के अनुसार, universal properties से objects को characterize करना category theory का एक महत्वपूर्ण हिस्सा है
      category theory की एक और practical उपयोगिता यह है कि यह computer scientists, mathematicians और physicists को बात करने के लिए common language देती है। अगर सभी लोग समान patterns को अलग-अलग नामों और थोड़ी-थोड़ी incompatible definitions से बुलाएं, तो collaboration आसान नहीं होता
    • Topos Institute ऐसा नया software बना रहा है जो category theory Kool-Aid अभी तक न पीने वालों को बहुत ज्यादा transparent दिखे, ऐसी उम्मीद है
      मौजूदा pre-alpha मुख्यतः systems dynamics modeling के लिए है, लेकिन जिन कामों की range को लक्ष्य बनाया गया है, उनके लिए category-theoretic foundation जरूरी लगता है। किसी के भी विचार खुशी से सुनना चाहूंगा
      https://topos.site/blog/2024-10-02-introducing-catcolab/

  • मुझे लगता है category theory उपयोगी है, लेकिन शायद अभी computing में नहीं
    अगर सच में इसकी जरूरत न हो तो यह मुश्किल लगनी ही है। क्या universal properties, adjoint functors और Yoneda lemma को सचमुच समझने की जरूरत है? अगर जरूरत नहीं है, तो वे क्या हैं यह सीखने में संघर्ष होगा
    दिलचस्प बात यह है कि functional programming का अनुभव category theory समझने में मदद करता है, लेकिन उल्टा उतना नहीं। उदाहरण के लिए parametric polymorphism natural transformations के लिए intuition देता है, और natural transformations category theory के हर application में core हैं
    category theory के convincing applications बहुत mathematical हैं। वे algebraic topology, representation theory, algebraic geometry और non-classical logic में मिलते हैं

  • एक गलती है
    “modus ponens दो अन्य propositions, यहां A और B से दर्शाए गए propositions से बना proposition है, और कहता है कि यदि proposition A true है और proposition A --> B भी true है, यानी A, B को imply करता है, तो B भी true है। उदाहरण के लिए, अगर हम जानते हैं कि ‘Socrates मानव है’ और ‘मानव नश्वर हैं’, तो हम यह भी जानते हैं कि ‘Socrates नश्वर है’।”
    यह उदाहरण propositional logic के rule modus ponens का मामला नहीं है, बल्कि categorical syllogism है जिसके लिए predicate logic चाहिए

  • यहां कहा गया है कि “logic possible की science है”, लेकिन क्या logic definite चीजों की science नहीं होनी चाहिए?
    मुझे लगता है मुख्य बात यह है कि क्या valid है और क्या नहीं, इसे निश्चित रूप से कहने में सक्षम बनाना

  • diagrammatic notation रोचक है
    क्या लेखक diagrams के truth-preserving transformations के लिए inference rules भी प्रस्तुत करते हैं?