Deep0Thinking

Notes

Study notes, tutorials, and references. Use tags to filter by subject, or view a series in reading order.

Open filters No filters active
Order
Published
Tags 0 selected

Select one or more tags. Results must match every selected tag.

All notes

66 entries, newest published first
  1. Boole and the Algebraic TraditionHow an algebra of classes became a calculus of relations and quantifiers, through Boole, De Morgan, Peirce, and Schröder. Series: History of Logic, Part 1 #history-of-logic#mathematical-logic#algebraic-logic#history-of-mathematics#boolean-algebra#relations#quantifiers#interactive-labs
  2. Frege, Quantifiers, and Logical FormWhy variables, scope, and explicit inference changed the representation of mathematical proof, and how Frege's project differed from modern first-order logic. Series: History of Logic, Part 2 #history-of-logic#mathematical-logic#formal-language#foundations-of-mathematics#quantifiers#first-order-logic#logicism#higher-order-logic#interactive-labs
  3. Rigor, Infinity, and the Axiomatic MethodHow analysis, infinite sets, arithmetic, and alternative geometries changed the questions mathematicians asked about foundations. Series: History of Logic, Part 3 #history-of-logic#mathematical-logic#foundations-of-mathematics#set-theory#axiomatization#infinity#real-analysis#non-euclidean-geometry#interactive-labs
  4. Paradoxes and Competing FoundationsRussell's contradiction, Frege's Basic Law V, ramified types, predicativity, and axiomatic set theory as distinct responses to foundational problems. Series: History of Logic, Part 4 #history-of-logic#mathematical-logic#foundations-of-mathematics#set-theory#type-theory#logicism#paradoxes#russells-paradox#predicativity#axiomatization#interactive-labs
  5. Hilbert's Program and the Study of ProofFormalization, finitary reasoning, and the attempt to justify infinitary mathematics through a mathematical analysis of finite derivations. Series: History of Logic, Part 5 #history-of-logic#mathematical-logic#proof-theory#consistency#foundations-of-mathematics#hilberts-program#finitism#epsilon-calculus#formalization
  6. Intuitionism and Mathematical ConstructionBrouwer, Heyting, constructive evidence, realizability, and the different mathematical programs behind the word constructive. Series: History of Logic, Part 6 #history-of-logic#mathematical-logic#constructivism#proof-theory#intuitionistic-logic#realizability#classical-logic
  7. Syntax, Truth, and CompletenessThe distinction between derivability and semantic consequence, from formal syntax and Tarski's semantics to Gödel's theorem, Henkin's construction, and nonstandard models. Series: History of Logic, Part 7 #history-of-logic#mathematical-logic#semantics#model-theory#completeness#first-order-logic#truth#compactness#lowenheim-skolem
  8. Gödel, Rosser, and IncompletenessHow arithmetic represents proofs, how diagonalization produces an undecidable sentence, and what the two incompleteness theorems establish. Series: History of Logic, Part 8 #history-of-logic#mathematical-logic#incompleteness#proof-theory#foundations-of-mathematics#godels-theorems#arithmetic#diagonalization#consistency
  9. The Emergence of ComputabilityChurch, Turing, Kleene, Post, and the mathematical analysis of algorithms, undecidability, relative computation, and Diophantine equations. Series: History of Logic, Part 9 #history-of-logic#mathematical-logic#computability#algorithms#turing-machines#undecidability#halting-problem#lambda-calculus#interactive-labs
  10. Gentzen and the Structure of ProofNatural deduction, sequent calculus, cut elimination, ordinal analysis, and the continuing investigation of the strength and computational content of proofs. Series: History of Logic, Part 10 #history-of-logic#mathematical-logic#proof-theory#natural-deduction#consistency#reverse-mathematics#sequent-calculus#cut-elimination#ordinal-analysis#interactive-labs
  11. Model Theory Becomes MathematicsDefinability, quantifier elimination, ultraproducts, nonstandard analysis, and classification as tools for understanding mathematical structures. Series: History of Logic, Part 11 #history-of-logic#mathematical-logic#model-theory#semantics#definability#quantifier-elimination#ultraproducts#nonstandard-analysis#stability-theory
  12. Set Theory and IndependenceChoice, the continuum hypothesis, Gödel's constructible universe, Cohen's forcing, and the continuing question of which axioms to adopt. Series: History of Logic, Part 12 #history-of-logic#mathematical-logic#set-theory#independence#foundations-of-mathematics#forcing#continuum-hypothesis#axiom-of-choice#constructibility
  13. Modal Logic: Necessity, Time, Knowledge, and ProvabilityHow the study of implication developed into a family of logics whose operators express different kinds of necessity. Series: History of Logic, Part 13 #history-of-logic#mathematical-logic#modal-logic#semantics#kripke-semantics#temporal-logic#epistemic-logic#provability-logic#interactive-labs
  14. Alternative Logics: Truth, Relevance, Inconsistency, and ResourcesFour distinct reasons to reconsider classical inference, illustrated through truth values, relevant implication, inconsistent information, and structural rules. Series: History of Logic, Part 14 #history-of-logic#mathematical-logic#nonclassical-logic#proof-theory#linear-logic#many-valued-logic#relevance-logic#paraconsistent-logic#structural-rules
  15. Lambda Calculus and the Curry–Howard CorrespondenceHow substitution became a theory of computation, and how typed terms came to represent proofs with computational behavior. Series: History of Logic, Part 15 #history-of-logic#mathematical-logic#lambda-calculus#type-theory#curry-howard#proof-theory#computation#normalization#interactive-labs
  16. Dependent Type Theory: Proofs, Data, and UniversesHow types came to express specifications that depend on values, and why equality, induction, and universe rules became foundational decisions. Series: History of Logic, Part 16 #history-of-logic#mathematical-logic#dependent-types#foundations-of-mathematics#proof-assistants#type-theory#identity-types#universes#inductive-types
  17. Categorical Logic: Structure, Quantification, and Internal LanguagesHow categories provided structural interpretations of proof, function types, quantifiers, and mathematical foundations. Series: History of Logic, Part 17 #history-of-logic#mathematical-logic#categorical-logic#semantics#foundations-of-mathematics#category-theory#adjunctions#topos-theory#type-theory
  18. Functional Programming and Programming-Language SemanticsFrom Lisp and lambda-based language design to mathematical accounts of recursion, polymorphic type inference, and abstraction. Series: History of Logic, Part 18 #history-of-logic#mathematical-logic#functional-programming#programming-languages#semantics#lambda-calculus#denotational-semantics#type-inference#domain-theory
  19. Automated Theorem Proving: Clauses, Unification, Equality, and SearchHow proof procedures turn a mathematical problem into a search, and why representation, inference rules, and search strategy each matter. Series: History of Logic, Part 19 #history-of-logic#mathematical-logic#automated-reasoning#resolution#theorem-proving#unification#equality#proof-search#first-order-logic
  20. Complexity, SAT, and SMTWhy decidable reasoning can be difficult, how conflict-driven solvers exploit structure, and how Boolean search cooperates with mathematical theories. Series: History of Logic, Part 20 #history-of-logic#mathematical-logic#complexity#sat#smt#automated-reasoning#np-completeness#dpll#cdcl#decision-procedures#interactive-labs
  21. Logic Programming: Clauses as ProgramsHow proof search can compute answers, and why a program's logical consequences must be distinguished from the behavior of its execution strategy. Series: History of Logic, Part 21 #history-of-logic#mathematical-logic#logic-programming#prolog#automated-reasoning#horn-clauses#sld-resolution#datalog#unification
  22. Proof Assistants: Foundations and TrustThe distinct histories of Automath, LCF, Mizar, inductive provers, dependent-type systems, Metamath, and Lean—and what each architecture asks us to trust. Series: History of Logic, Part 22 #history-of-logic#mathematical-logic#proof-assistants#formalization#foundations-of-mathematics#type-theory#trusted-kernel#lean#lcf#coq
  23. Program Verification: Invariants, Semantics, and Local ReasoningHow assertions became a logic of programs, and how proofs of loops, heap operations, compilers, and kernels depend on precise specifications. Series: History of Logic, Part 23 #history-of-logic#mathematical-logic#program-verification#hoare-logic#separation-logic#formal-methods#loop-invariants#weakest-preconditions#compiler-correctness
  24. Temporal Verification, Model Checking, and AbstractionHow logics of time became tools for checking ongoing systems, and how symbolic representations and abstraction address the growth of possible behaviors. Series: History of Logic, Part 24 #history-of-logic#mathematical-logic#model-checking#temporal-logic#abstract-interpretation#formal-methods#safety-and-liveness#symbolic-verification#abstraction#interactive-labs
  25. Formalized Mathematics: Proofs and Reusable LibrariesHow mechanically checked mathematics grew from individual texts and landmark proofs into shared infrastructure for further mathematical work. Series: History of Logic, Part 25 #history-of-logic#mathematical-logic#formalized-mathematics#mathematical-libraries#proof-assistants#formalization#proof-reflection#mathlib#lean
  26. Homotopy Type Theory and UnivalenceHow identity types acquired a geometric interpretation, why equivalence can induce identification, and how cubical theories address computation. Series: History of Logic, Part 26 #history-of-logic#mathematical-logic#homotopy-type-theory#univalence#foundations-of-mathematics#type-theory#dependent-types#identity-types#cubical-type-theory
  27. Learned Theorem Proving: Search, Formalization, and DiscoveryHow statistical guidance works with formal checking, from premise selection to AlphaProof and research formalization, with careful distinctions about evidence and novelty. Series: History of Logic, Part 27 #history-of-logic#mathematical-logic#ai#theorem-proving#formalization#automated-reasoning#machine-learning#proof-search#autoformalization
  28. Greek and Late-Antique LogicAristotelian demonstration, syllogistic inference, Stoic arguments, and the commentators and translators who shaped their later study. Series: History of Logic: Earlier Traditions, Part 1 #history-of-logic#ancient-logic#aristotle#stoicism#history-of-philosophy#syllogistic-logic#propositional-logic#demonstration
  29. Arabic, Islamic, and Jewish Logical TraditionsTranslation, demonstration, Avicennan innovations, later teaching traditions, and the movement of logical ideas across Arabic, Hebrew, and Latin. Series: History of Logic: Earlier Traditions, Part 2 #history-of-logic#arabic-logic#avicenna#medieval-logic#islamic-philosophy#jewish-philosophy#syllogistic-logic#translation
  30. Medieval Latin Logic: Reference, Consequence, and ParadoxHow medieval logicians analyzed the use of terms, the force of logical particles, valid consequences, and self-referential statements. Series: History of Logic: Earlier Traditions, Part 3 #history-of-logic#medieval-logic#semantics#paradoxes#supposition-theory#logical-consequence#self-reference#history-of-philosophy
  31. Indian Logic: Inference, Evidence, and AnalysisNyāya, Buddhist theories of inference, and Navya-Nyāya's technical language, examined through the justification and failure of inferential signs. Series: History of Logic: Earlier Traditions, Part 4 #history-of-logic#indian-logic#nyaya#buddhist-logic#epistemology#inference#navya-nyaya#history-of-philosophy
  32. Chinese Traditions of Argument: Names, Kinds, and DistinctionsMohist standards of reasoning, the School of Names, the white-horse discussion, and Xunzi's account of naming and orderly discourse. Series: History of Logic: Earlier Traditions, Part 5 #history-of-logic#chinese-philosophy#mohism#argumentation#philosophy-of-language#analogy#school-of-names#history-of-philosophy
  33. Before Boole: Reform, Leibniz, and BolzanoEarly-modern projects for improving inquiry and calculation, followed by Bolzano's account of propositions, variation, consequence, and explanation. Series: History of Logic: Earlier Traditions, Part 6 #history-of-logic#early-modern-logic#leibniz#bolzano#induction#logical-consequence#symbolic-logic#history-of-philosophy
  34. Apex Legends: Game SenseNotes on the mistakes I keep making in Apex and how I try to stop repeating them. This is only part of game sense, and only the part I have managed to name so far. #apex-legends#fps#battle-royale#multiplayer#gaming#guide
  35. History of Logic: Series GuidePart 0 introduces the series, its reading order, and routes through foundations, computation, formalization, and earlier logical traditions. Series: History of Logic, Part 0 #history-of-logic#mathematical-logic#foundations-of-mathematics#formalization#history-of-philosophy#interactive-learning
  36. Why Mathematical Logic Textbooks Look CircularStandard textbooks use sets to define first order logic, then define set theory inside first order logic. Where that apparent circularity resolves, and what the metatheory consists of. #mathematical-logic#logic#foundations#metamathematics#formalism#lean#textbook#mathematics
  37. Apex Legends: Settings and GearThe settings, keybinds, sensitivity, and gear I actually play on. #apex-legends#fps#battle-royale#multiplayer#settings#sensitivity#gear#gaming
  38. I Switched from WordPress to AstroNotes from the move off WordPress to a static Astro site, what I gained, and what I gave up. #ai#astro#blog#design#migration#site#static-site#web-development#website#milestone
  39. How Separation Resolves Russell's ParadoxUnrestricted comprehension is inconsistent. Separation replaces it, and the relative Russell set is a subset of its base set but never an element of it. #mathematical-logic#set-theory#logic#foundations#paradox#proof#mathematics
  40. Why Can't You Solve an Equation by Differentiating Both Sides?Squaring both sides keeps every original solution, but differentiating does not. The difference comes from the type of the function you apply. #algebra#chinese#differential-equation#mathematical-logic#mathematics#proof
  41. Can Lorentz Transformations Be Derived from General Relativity?How local inertial frames connect Lorentz transformations in special relativity to curved spacetime. #differential-geometry#general-relativity#manifold#mathematics#metric-space#physics#special-relativity
  42. Why Does Friction Break Time-Reversal Symmetry?How microscopic reversibility, probability, and coarse-graining produce macroscopic irreversibility. #classical-mechanics#loschmidts-paradox#mathematics#paradox#physics#probability#statistical-mechanics#thermodynamics#time-reversal-symmetry
  43. Why Is the Lorentz Transformation Linear?A derivation of Lorentz linearity from the structure of inertial frames and spacetime transformations. #differential-geometry#linear-algebra#manifold#mathematics#physics#special-relativity
  44. Could the Speed of Light Be Variable?What the constancy of light speed means, how it is tested, and where variable-speed ideas would have to differ. #experimental-physics#mathematics#physics#special-relativity#speed-of-light
  45. Why Are So Many Equations of Motion Second Order?How first-derivative actions lead to second-order motion, and what Ostrogradsky’s theorem does—and does not—exclude. #classical-mechanics#differential-equation#lagrangian-mechanics#mathematics#ostrogradsky-instability#physics
  46. Why Are Phasors Used in Circuit Analysis?How phasors turn sinusoidal circuit equations into algebra, and what their components represent physically. #algebra#circuit-analysis#circuits#differential-equation#electromagnetism#linear-algebra#linear-time-invariant#mathematics#phasor#physics#proof
  47. Intro to Generalized CoordinatesAn introduction to generalized coordinates and why they simplify constrained mechanical systems. #classical-mechanics#introduction#lagrangian-mechanics#mathematics#physics
  48. A Mathematical Exploration of the Virial TheoremA derivation and interpretation of the virial theorem through the mathematics of classical mechanics. #classical-mechanics#introduction#latex#mathematics#physics
  49. Recommendations for Rigorous Classical Mechanics TextbooksA reading list for approaching classical mechanics with greater mathematical rigor. #classical-mechanics#experience#formalism#guide#mathematics#physics#recommendation#textbook
  50. Why Aren't Generalized Coordinates Treated as Functions of Time?How partial derivatives of a Lagrangian differ from differentiation along a time-dependent trajectory. #classical-mechanics#introduction#lagrangian-mechanics#latex#mathematics#physics
  51. A Mathematical Exploration of Norton's Dome and Determinism in Classical MechanicsA mathematical look at Norton's dome, non-unique motion, and determinism in classical mechanics. #chinese#classical-mechanics#differential-equation#introduction#latex#mathematics#paradox#physics
  52. Why Use Squared Error Rather Than Absolute Error?A probabilistic and optimization-based explanation of why squared error is so common in loss functions. #algebra#computer-science#deep-learning#latex#likelihood#machine-learning#mathematics#optimization#probability#probability-theory#regression-analysis#statistics
  53. Intro to Git, GitHub, and VS CodeA bilingual guide to repositories, forks, clones, branches, commits, and pull requests, with a complete local workflow. #chinese#computer-science#git#github#guide#introduction#programming#vscode
  54. Diandian: Two Years After the RescueThe story of the kitten my family rescued in February 2022, with a 2024 video update. #chinese#diandian#experience#family#love#pet#video#memory
  55. Constructing Logic Gates from Truth TablesUsing mathematical logic and Python to reason through a logic-gate construction challenge in Turing Complete. #coding#computer-science#gaming#introduction#latex#logic#logic-gate#mathematical-logic#mathematics#programming#python
  56. Using a Raspberry Pi to Build a U.S. VPN Server for My Family in ChinaA practical record of building a family VPN with Raspberry Pi, SSH, DNS, and Cloudflare. #cloudflare#coding#computer-science#ddns#dns#github#great-firewall#linux#network#programming#raspberry-pi#server#software#ssh#video#vpn
  57. I Switched from GitHub Pages to WordPressNotes from the 2023 move from a Jekyll site on GitHub Pages to WordPress. #backend#blog#developer#frontend#github#site#web-development#website#milestone
  58. Competitive Mathematics: FactorizationA structured guide to polynomial factorization, identities, methods, and proofs for mathematical competitions. #competition#competitive#guide#latex#mathematical-competition#mathematics#notes
  59. A Guide to Preparing for the William Lowell Putnam Mathematical CompetitionPreparation ideas, references, and expectations for the William Lowell Putnam Mathematical Competition. #competition#competitive#guide#introduction#latex#mathematical-competition#mathematics
  60. Why Must a Linear Subspace Contain the Additive Identity?Why nonemptiness and scalar closure force a subspace to contain the ambient zero vector. #latex#linear-algebra#mathematics#modern-algebra
  61. A Simple Physical Approach to Understanding the Taylor SeriesAn intuitive route from motion with changing acceleration to the structure of a Taylor series. #guide#mathematics#physics#taylor-series
  62. Intro to the Colemak keyboard layoutA concise introduction to Colemak, its layout choices, and the process of learning it. #computer-science#introduction#keyboard-layout#typing
  63. My U.S. Visa Interview in Guangzhou, July 2022A first-person account of preparing for and completing a U.S. visa interview in Guangzhou. #chinese#experience
  64. Summation by Parts (Abel Transformation)An introduction to summation by parts and its role as the discrete analogue of integration by parts. #algebra#chinese#introduction#latex#mathematics
  65. Some Advice for New Python LearnersPractical advice about editors, IDEs, and learning habits for people beginning Python. #chinese#experience#guide#ide#programming#python#text-editor
  66. A Simple Analogy to Understand Terminal, Shell, TTY, and ConsoleA practical mental model for distinguishing terminals, shells, TTYs, and consoles. #chinese#computer-science#introduction#linux#operating-system