@LogicPractice

Logic and applications of logic from @JohnDCook

 Houston, TX
JohnDCook.com/logic
Joined September 2016
  • Tweets2.2K
  • Following8
  • Followers28.3K
127Media
Big logic johndcook.com/blog/applied-l…
10
21
1
74
Linear logic analogies to arithmetic johndcook.com/blog/2022/01/1…

Linear logic additive, multiplicative, and exponential

Why are linear logic operators called additive, multiplicative, and exponential? Why are some called positive and some negative?

johndcook.com
3
32
1,486
“Computer-aided cryptography is an active area of research that develops and applies formal, machine-checkable approaches to the design, analysis, and implementation of cryptography.” eprint.iacr.org/2019/1393
2
16
964
An order preserving map on a complete lattice has a fixed point.
5
3
36
2,046
Continuum hypothesis -- whether there a set with cardinality greater than the integers and less than the reals -- is independent of ZFC.
3
6
50
2,723
Seven normal forms in logic johndcook.com/blog/seven-nor…

Logic normal forms negation, conjunction, Skolem, Blake, etc

This post discusses seven normal forms: Negation normal form Conjunctive normal form Disjunctive normal form Algebraic normal form Prefix normal form Skolem normal form Blake canonical form The photo...

johndcook.com
4
36
1,126
All human beings are different. All apathetic people are indifferent. Therefore, no apathetic people are human beings. -- Solomon Golomb
1
2
2
30
2,182
Kurt Godel Created a hurdle For the truths of a system: You just can't list 'em! -- Steven Cushing
3
2
1
28
1,547
The equivalence A ≡ B in linear logic means the formula (A ⊸ B) & (B ⊸ A) is derivable.
3
37
1,627
Software Foundations cis.upenn.edu/~bcpierce/sf/c… #coq
5
37
2,065
'You can sway a thousand men by appealing to their prejudices quicker than you can convince one man by logic.' -- Robert A. Heinlein
6
23
1,127
How much can Boolean expressions be simplified? johndcook.com/blog/2020/11/1…

How much does Boolean expression minimization shorten?

If you have a Boolean function with n variables, how long can a minimized version of the expression be? How much does minimization save?

johndcook.com
6
24
1,095
Logic & Applications retweeted
little grey mouse 🐭@mouse_mathOct 13
11
16
5
191
6,781
'Logic, like whiskey, loses its beneficial effect when taken in too large quantities.' -- Edward Plunkett
19
47
1,718
Where did combinators come from? writings.stephenwolfram.com/…
1
13
1,445
TLA: Temporal Logic of Actions research.microsoft.com/en-us…
5
29
1,622
Logic & Applications retweeted
John D. Cook
@JohnDCookOct 8
New post: Privacy Policies and Modal Logic johndcook.com/blog/2026/10/0…
2
4
15
1,811
Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs arxiv.org/abs/2610.08144

Navier-Stokes lost in translation: Why Lean verification of AI...

Autoformalisation is increasingly used to verify mathematical texts, including those generated by AI, as in OpenAI's announced proof of blow-up of solutions to the Navier-Stokes equations. In this...

arxiv.org
8
23
2
122
9,352
The diamond symbol <> in modal logic can be interpreted as possibility, e.g. <>P means 'it is possible that P holds.'
1
1
1
24
1,797
Logic & Applications retweeted
Topology Fact@TopologyFactOct 6
A topological model for provability logic johndcook.com/blog/2026/10/0…

A topological model for provability logic

Provability logic, a.k.a. Gödel-Löb logic, is a modal logic in which the box operator means a proposition is provable. It has a different topological model.

johndcook.com
3
16
2,430
Coq proof of Feit-Thompson theorem msr-inria.fr/news/feit-thoms…

Feit thomson proved in coq - Microsoft Research Inria Joint Centre

Home > News > Feit thomson proved in coq […]

msr-inria.fr
1
6
1,022
Load more