I’m just about to be on the road again, to talk about proof theory, modal logic, a hint of medieval logic, and even a tiny smidgen of metaphysics.
On this little European jaunt, the first stop is Prague, then Vienna, and at the end, Amsterdam. I’m looking forward to meeting old friends and making new ones. If you’re in that part of the world, and you’re into that sort of thing, I’d love to see you.
Ejercicios de deducción natural en lógica de primer orden. https://web.archive.org/web/https://www.cs.us.es/~jalonso/cursos/li-10/temas/ej-ded-natural-LPO.pdf #Logic #Math
“better numerical and logical #reasoning skills were associated with better real-world #decision outcomes (N ≈ 1000), and this relationship remained when controlling for general cognitive abilities, although the effects we found were small.”
Bi-intuitionistic logics through the abstract algebraic logic lens. ~ Jonte Deakin, Ian Shillito. https://arxiv.org/abs/2503.17159 #ITP #Coq #Rocq #Logic
Readings shared March 26, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/26-readings_shared_03-26-25 #AI #FunctionalProgramming #Haskell #ITP #IsabelleHOL #Logic #Math #Maxima
LogicLearner: A tool for the guided practice of propositional logic proofs. ~ Amogh Inamdar et als. https://arxiv.org/abs/2503.19280 #Logic
Feelings are poor reasons, but they may not be meaningless.
People had higher feelings of rightness (FOR) about their valid guesses.
Valid final answers also correlated with lower FOR about biased answers and higher high FORs about valid answers.
I wrote on particulars, universals, and alternating between the two https://www.bryankam.com/p/from-will-to-representation-and-back?r=447n8&utm_campaign=post&utm_medium=web&showWelcomeOnShare=false #Aristotle #Schopenhauer #philosophy #logic @philosophy
A fundamental result in universal algebra is the Subdirect Representation Theorem, which tells us how to decompose an algebra \(A\) into its "basic parts". Formally, we say that \(A\) is a subdirect product of \(A_1\), \(A_2\), ..., \(A_n\) when \(A\) is a subalgebra of the product
\[
A_1\times A_2\times\cdots\times A_n
\]
and for each index \(1\le i\le n\) we have for the projection \(\pi_i\) that \(\pi_i(A)=A_i\). In other words, a subdirect product "uses each component completely", but may be smaller than the full product.
A trivial circumstance is that \(\pi_i:A\to A_i\) is an isomorphism for some \(i\). The remaining components would then be superfluous. If an algebra \(A\) has the property than any way of representing it as a subdirect product is trivial in this sense, we say that \(A\) is "subdirectly irreducible".
Subdirectly irreducible algebras generalize simple algebras. Subdirectly irreducible groups include all simple groups, as well as the cyclic \(p\)-groups \(\Z_{p^n}\) and the Prüfer groups \(\Z_{p^\infty}\).
In the case of lattices, there is no known classification of the finite subdirectly irreducible (or simple) lattices. This page (https://math.chapman.edu/~jipsen/posets/si_lattices92.html) by Peter Jipsen has diagrams showing the 92 different nontrivial subdirectly irreducible lattices of order at most 8. See any patterns?
We know that every finite subdirectly irreducible lattice can be extended to a simple lattice by adding at most two new elements (Lemma 2.3 from Grätzer's "The Congruences of a Finite Lattice", https://arxiv.org/pdf/2104.06539), so there must be oodles of finite simple lattices out there.
My North American tour is just about over, and it’s gone better than I could have hoped, with excellent discussions with colleagues at Chapman, UC Berkeley, UC Davis and Calgary, and really helpful questions and feedback at each of my talks.
My last talk of this trip will be this afternoon, at the CUNY Graduate Center, for the Logic and Metaphysics Workshop.
#formalMethods #gamedev #programming #commonLisp #acl2 #itch https://lispy-gopher-show.itch.io/lispmoo2/devlog/907091/formal-game-logic
Since yesterday I advocated strong use of defgeneric, defmethod and McCLIM's define-command, here I present
just giving lisp's defun to acl2's first order #logic.
I present a batch processing style for using acl2 both in #shell and in #lisp with a worked example.
Thoughts and opinions, gamedevs and logical types?
Spring Sale on Steam has just arrived! Buy Quadrata and Lovux with 40% OFF between Mar 13th and Mar 20th! 
https://store.steampowered.com/developer/mindlabor
Why-why-why did I update #Logic when I didn't have to? Will I never learn?
- It "forgot" all downloaded library packs, refused to acknowledge their presence. Had to download everything again.
- All settings were gone. Startup is different and weird. Adding tracks is different and weird.
- So many new bugs! My current favourite is that sometimes the volume of some track randomly drops to zero during playback. Hit stop and play, boom, it's back at regular volume. Makes mixing fun again.
Many thanks to everyone who attended and made this an amazing day of #logic, #computabilitytheory and #categorytheory!
Recordings and slides will be available on the website sometime next week (hopefully)!
My solution to the liars paradox is geometry. Especially topology.
A liars paradox is just a linguistic Möbius strip. It has only one side and only looks like having more.
If you follow one path, you will realize it.
The >>whole<< object is a lie.
