Hacker News with Generative AI: Logic

Show HN: Formalizing Principia Mathematica using Lean (github.com/ndrwnaguib)
This project aims to formalize the first volume of Prof. Bertrand Russell’s Principia Mathematica using the Lean theorem prover.
Mathematics, Formal Verification, Theorem Proving, Logic
113 points by ndrwnaguib 10 hours ago | 27 comments
Show HN: Logiquiz – Daily Self-Referential Puzzles (logiquiz.com)
Logiquiz, also know as Self-Referential Quiz or Puzzle, is a type of quiz where the questions refer to the quiz itself or other questions within the same quiz. The answers often depend on the content or structure of the quiz, making it a meta-puzzle.
Puzzles, Games, Self-Referential, Logic, Daily
32 points by slig 3 days ago | 17 comments
Surprises in Logic (2016) (math.ucr.edu)
There's a complexity barrier built into the very laws of logic: roughly speaking, while lots of things are more complex than this, we can't prove any specific thing is more complex than this. And this barrier is surprisingly low! Just how low? Read this.
Mathematics, Logic, Complexity
91 points by jxmorris12 4 days ago | 42 comments
Conspiracies Are Often Unnecessary (curi.us)
David Deutsch wrote an article about conspiracy theories and we had conversations about them. It's an interesting topic which is worth analyzing not just dismissing. I now think he was right about some of the logic of his analysis, but wrong about how it applies to the world. Deutsch says:
Conspiracy Theories, Logic, Analysis
5 points by speckx 10 days ago | 0 comments
PyReason: Explainable inference for annotated, real valued, graph based and tem (github.com/lab-v2)
PyReason is a graphical inference tool that uses a set of logical rules and facts (initial conditions) to reason over graph structures.
Graphical Inference, Logic, Python, Graph Structures
27 points by todsacerdoti 17 days ago | 2 comments
Novel Logic-Enhanced LLM for Improved Symbolic Reasoning (ycombinator.com)
I’m experimenting with a novel approach that integrates symbolic logic directly into a transformer’s attention mechanism.
Artificial Intelligence, Logic, Symbolic Reasoning
10 points by N3Xxus_6 21 days ago | 0 comments
Show HN: TypeScript as a proof assistant for intuitionistic propositional logic (github.com)
TypeScript can be used just like a proof assistant (for intuitionistic propositional logic)!
TypeScript, Proof Assistants, Logic, Programming Languages, Computer Science
17 points by xxmarijnw 25 days ago | 3 comments
Argumentation Theory (wikipedia.org)
Argumentation theory is the interdisciplinary study of how conclusions can be supported or undermined by premises through logical reasoning.
Argumentation Theory, Logic, Philosophy, Linguistics
11 points by rnjailamba 34 days ago | 0 comments
Truth Functional Logic for Hackers (lagomor.ph)
Bob and Alice are two hackers working on an embedded system with a severe computational constraint - there is a bug in their low-cost microcontroller making OR operations significantly slower than any other operation on the chipset.
Logic, Programming, Hardware, Security
48 points by ChilledTonic 45 days ago | 14 comments
Translating natural language to first-order logic for logical fallacy detection (arxiv.org)
Translating natural language into formal language such as First-Order Logic (FOL) is a foundational challenge in NLP with wide-ranging applications in automated reasoning, misinformation tracking, and knowledge validation.
Logic, Artificial Intelligence, Automated Reasoning
258 points by ColinWright 52 days ago | 141 comments
Order Doesn’t Matter, But Reasoning Does (arxiv.org)
Artificial Intelligence, Reasoning, Logic
14 points by spaintech 53 days ago | 16 comments
Jan Łukasiewicz (wikipedia.org)
Jan Łukasiewicz (Polish: [ˈjan wukaˈɕɛvit͡ʂ] ⓘ; 21 December 1878 – 13 February 1956) was a Polish logician and philosopher who is best known for Polish notation and Łukasiewicz logic.[1] His work centred on philosophical logic, mathematical logic and history of logic.[2] He thought innovatively about traditional propositional logic, the principle of non-contradiction and the law of excluded middle, offering one of the earliest systems of many-valued logic.
Logic, Philosophy, Poland, Biography, History
4 points by fuzztester 58 days ago | 1 comments
Five Kinds of Nondeterminism (buttondown.com)
No newsletter next week, I'm teaching a TLA+ workshop.
Computer Science, Programming, Theory, Logic, Formal Verification
135 points by BerislavLopac 65 days ago | 32 comments
XOR (greenend.org.uk)
Recently I was called on to explain the ‘XOR’ operator to somebody who vaguely knew of its existence, but didn’t have a good intuition for what it was useful for and how it behaved.
Logic, Programming, Computer Science, Binary Operations
602 points by mariuz 67 days ago | 100 comments
Gödel's Loophole (wikipedia.org)
Gödel's Loophole is a supposed "inner contradiction" in the Constitution of the United States which Austrian-American logician, mathematician, and analytic philosopher Kurt Gödel postulated in 1947.
Constitution, Philosophy, Logic, Mathematics
6 points by croes 74 days ago | 0 comments
Odds and Ends – Introductory Text on Probability and Inductive Logic [pdf] (jonathanweisberg.org)
Probability, Logic, Textbooks, Philosophy, Mathematics
8 points by rnjailamba 82 days ago | 0 comments
Sequent Calculus and Notation – Par Part 1 (ryanbrewer.dev)
This post is the first in a series on Logic. These ideas are very useful in understanding many important papers on programming language theory, especially papers on type theory and the lambda calculus. I will start with an explanation of sequents and Sequent Calculus as a system for doing logic, then I'll dive into linear logic in the next post. I'll finish the trilogy with a post on Par and computational interpretations of classical logic.
Logic, Programming Languages, Type Theory, Lambda Calculus, Linear Logic
38 points by hoping1 93 days ago | 10 comments
Who Can Understand the Proof? A Window on Formalized Mathematics (stephenwolfram.com)
For more than a century people had wondered how simple the axioms of logic (Boolean algebra) could be. On January 29, 2000, I found the answer—and made the surprising discovery that they could be about twice as simple as anyone knew. (I also showed that what I found was the simplest possible.)
Mathematics, Logic, Boolean Algebra, Research, History
190 points by ColinWright 106 days ago | 115 comments
SAT Solver Etudes I (philipzucker.com)
SAT solving is kind of too big a topic for one post. Here is some discussion, programs and links.
SAT Solvers, Programming, Logic, Computer Science
45 points by mathgenius 109 days ago | 30 comments
Lean: Programming Language and Theorem Prover (lean-lang.org)
Programming Language and Theorem Prover
Programming Languages, Theorem Provers, Logic
9 points by SerCe 112 days ago | 0 comments
Transcendental Syntax (github.com/engboris)
The transcendental syntax is a method of constructing logical abstractions from a low-level elementary and "logic-agnostic" language.
Programming, Software, Logic, Computer Science
81 points by 4ad 112 days ago | 34 comments
The Hoare Cube (wordpress.com)
I wrote earlier this year about my attempt to understand the repercussions of toggling and when giving a semantics to Hoare triples.
Programming, Logic, Computer Science, Formal Verification
86 points by matt_d 142 days ago | 23 comments
Beauty of the Gentzen System (wyounas.github.io)
Gentzen system, created by German mathematician Gerhard Gentzen, is a deductive system which can be used to prove propositional formulas. I recently learned about it while I was reading Ben-Ari’s fantastic book on mathematical logic [1] and I like its simplicity.
Mathematics, Logic, Proof Systems
6 points by simplegeek 143 days ago | 0 comments
A boy girl paradox – or maybe not? (shankwiler.com)
The most liked comment answers 1/2, but the user got worn down by others until he recanted and agreed that the answer is 1/3. Many other comments give lengthy explanations as to why the answer is 1/3.
Probability, Math, Puzzles, Logic
12 points by iuvcaw 160 days ago | 0 comments
The Laws of Thought by George Boole (1854) (gutenberg.org)
Logic, History, Mathematics, Books
8 points by sandwichsphinx 164 days ago | 0 comments
Question Sets and All Paths (andrewpwheeler.com)
I was nerd-sniped with a question at work the other day. The set up was like this, imagine a survey where all of the questions have yes-no answers. Some of the answers are terminating, so if you answer No to a particular question, the questions stop. But some if you reach that part of the tree will keep going.
Algorithms, Logic, Programming
5 points by apwheele 175 days ago | 5 comments
Algorithm = Logic and Control [pdf] (ic.ac.uk)
Algorithm, Computer Science, Logic, Control
72 points by acmerfight 177 days ago | 12 comments
Category Theory Illustrated: Logic (2021) (abuseofnotation.github.io)
Logic is the science of the possible. As such, it is at the root of all other sciences, all of which are sciences of the actual, i.e. that which really exists.
Category Theory, Mathematics, Logic
252 points by boris_m 183 days ago | 83 comments
The logical fallacy at the core of patent law, what does non-obviousness test? (academic.oup.com)
Patent laws in different jurisdictions have in their core a logical fallacy that generations of patent professionals have kept practising while seemingly being oblivious to its existence.
Law, Logic, Patents
12 points by croes 190 days ago | 21 comments
LLMs can't perform "genuine logical reasoning," Apple researchers suggest (arstechnica.com)
Irrelevant red herrings lead to "catastrophic" failure of logical inference.
Artificial Intelligence, Logic, Research
115 points by samizdis 193 days ago | 73 comments