Bookmarks tagged with: logic

An Infinitely Long Sentence Made of Just One Word

2026-07-06T21:36:33Z

In which we go deep down the grammatical rabbit hole, and unlock the infinite buffalo sentence.

This guy really likes recursion.

Nixon diamond

2026-06-21T17:55:49Z

In nonmonotonic reasoning, the Nixon diamond is a scenario in which default assumptions lead to mutually inconsistent conclusions.

This is a fun example in logic I recalled recently.

Richard Nixon is both a Quaker and a Republican

Rethinking set theory

2026-06-18T14:29:56Z

Mathematicians manipulate sets with confidence almost every day, rarely making mistakes. Few of us, however, could accurately quote what are often referred to as “the” axioms of set theory. This suggests that we all carry around with us, perhaps subconsciously, a reliable body of operating principles for manipulating sets. What if we were to take some of those principles and adopt them as our axioms instead? The message of this article is that this can be done, in a simple, practical way (due to Lawvere). The resulting axioms are ten thoroughly mundane statements about sets.

This is an expository article for a general mathematical readership.

A nice read, although it definitely gets a bit difficult towards the end.

via: https://topos.institute/blog/2025-07-13-liberating-synthetic-quasi-coherence-from-forcing/

Quantifying over functions

2026-06-05T02:18:38Z

via: https://buttondown.com/hillelwayne/archive/logic-for-programmers-extra-credits/

Partial Orders

2026-06-05T02:04:11Z

Partial orderings are a useful concept that would have taken too many pages in the book, so I’m putting it here.

via: https://buttondown.com/hillelwayne/archive/logic-for-programmers-extra-credits/

On circuits and numbers

2026-05-28T20:50:34Z

We establish new, yet intimate relationships between the 2-adic integers /sub 2/Z from arithmetics and digital circuits, both finite and infinite, from electronics.

VERY interesting paper! Sadly didn’t answer all my questions about 2-adic circuits, but it did answer quite a lot.

see: https://www.di.ens.fr/~jv/HomePage/pdf/cirnum.pdf

see: https://scispace.com/pdf/on-circuits-and-numbers-3du2olohli.pdf

via: https://en.wikipedia.org/wiki/Two%27s_complement#Two’s_complement_and_2-adic_numbers

Specification and Formal Verification of Hardware-Software Contracts for High-Assurance Computer Architectures

2026-05-27T01:32:04Z

This talk will focus on one such verification approach that takes as input a design under verification (DUV), modest architect-friendly DUV metadata, and a HW-SW contract. The approach automatically generates many simple formal properties that provably compose to imply the contract, and then evaluates them against the DUV to assess contract compliance. The enabling insight is that many important HW-SW contracts decompose into instantiations of a small, finite set of property templates, fillable automatically from the supplied metadata or from the results of evaluating other generated properties. This verification approach eliminates manual property writing, targets full HW-SW contracts rather than coverage metrics, and yields properties simple enough that commercial formal model checkers can produce unbounded proofs for most, even on complex designs.

Assumptions weaken properties

2026-05-22T12:16:24Z

One consequence of this is that checking whether assumptions hold is a different problem from verifying that your code works given the assumptions. Like to make sure “all unsafe blocks are safe” can’t use the Rust compiler, you need a second tool like Miri. I wonder if checking assumptions is, in practice, generally more difficult than checking everything else.

Two-Column Proof

2026-05-16T20:16:10Z

A formal type of proof most frequently encountered in elementary geometry courses in which known or derived statements are written in the left column, and the reason that each statement is known or valid is written next to it in the right column. The proof then proceeds from the known facts to the theorem to be demonstrated. […] However, this form of proof is virtually never used by practicing mathematicians because its confining and verbose format render it of very limited utility to any but the most simple of theorems.

Hmm, maybe this is why people don’t like Lean LOL.

Something Disturbing Happens When You Solve Einstein's Equations This Way

2026-04-03T12:11:18Z

Kurt Gödel discovered a solution to General Relativity that allows time travel without any exotic physics, revealing that the theory doesn’t actually guarantee a consistent chain of cause and effect . His “Gödel universe” shows that under certain conditions, the structure of spacetime itself can loop back on itself—blurring the line between past and future and exposing a deep limitation in our understanding of reality.

The GÖAT!

Lets Go! by Francis McCabe (Paperback) - Lulu

2026-02-27T09:19:40Z

Buy Lets Go! by Francis McCabe (Paperback) online at Lulu. Visit the Lulu Marketplace for product details, ratings, and reviews.

Proving What's Possible

2026-02-11T19:45:40Z

When “what CAN happen” is as important as “what SHOULD happen”

Some things are MORE EQUAL than others??

2026-01-18T13:51:28Z

Monads leave traces

2025-12-14T16:38:51Z

Can’t fully understand because there are no words, but the author looks to be making a very neat connection between coalgebras and the executions (here “traces”) of transition systems. Became aware of her work through Adjoint School 2026.

via: https://www.cs.uni-salzburg.at/~anas/talks.html

The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

2025-12-09T18:14:09Z

This is the kind of mathematics I was put on this earth to do. The equation explorer is also just a genuinely useful tool for looking up equations; did so earlier this year as part of preparations for a lecture I gave.

Set-sets

2025-11-29T16:02:53Z

I think this is the first highly technical Topos Institute blog post where I walked away and felt like I understood everything I was meant to understand. Heck yeah.

Uncountably Categorical Theories

2025-11-27T15:28:54Z

I’ve been thinking about very similar ideas for the better part of a year now; excited to see there’s good work regarding this.

(Provably) Unprovable and Undisprovable... How??

2025-11-18T22:36:45Z

No matter how hard we try to axiomatise mathematics, there will always be strong, independent propositions that don’t need no proofs… but how do we show that a proposition can’t be proven nor disproven?

Counting past infinity

2025-11-15T20:42:24Z

Nice set of videos on the theory of ordinals and their application to Goldstein sequences.

Mathematics doesn't actually make any sense

2025-11-12T14:28:10Z

Ever feel like the mathematics you’re learning doesn’t make any sense to you? Good. In a way, it would’ve been worse if you thought it did make sense.