Not everything is logical, but before the 1920s, most mathematicians and philosophers believed that it was. When a mathematician began to construct a proof (be it to prove that π is irrational or that arithmetic is modular), the method used to reach the final conclusions was assumed to be done systematically and rationally. But as anyone who has ever tried to solve a too-difficult problem knows, sometimes the best way to reach a solution is just to guess your way there.

But this guessing, coined as “arbitrary assumptions” in 1926 by a professor named Jan Lukasiewicz, presented a big problem for the growing mathematics field of logic. How could a theory be created that would explain arbitrary assumptions within the confines of rational thought? Guessing, history tells us, often leads different minds to the same exact conclusion.

The answer is natural deduction: a proof system with simple rules that mimic the way people actually reason.

Sounds easy, but mathematicians had been trying to figure this out for centuries. And the first two scholars to formally lay out theories of natural deduction, two men named Gerhard Gentzen and Stanisław Jaśkowski, did so in separate papers, through separate approaches, published in the same year: 1934. Gentzen and Jaśkowski did not know each other and did not have overlapping colleagues, yet they arrived at an almost identical solution at the exact same time.

Mathematician Gerhard Gentzen in Prague, 1945 (left) and Stanisław Jaśkowski (right). Credit: Eckart Menzler-Trott/CC BY-SA 2.0 de (left)

Before Gentzen and Jaśkowski’s papers, the most common way for any mathematical problem to be solved was to use something called the Hilbert system. The easiest way to understand this is just that the Hilbert system is too simple and too impractical to track the way human thought actually runs. Many scholars at the time found Hilbert’s (and other axiom) systems too inadequate and artificial. They wanted to write proofs that made sense to them.

Natural deduction is one of the most elementary ideas in basic philosophy. It is a term written on chalkboards in every undergraduate seminar but never really, fully explained. As Gentzen wrote in his 1934 paper coining natural deduction: “First I wished to construct a formalism that comes as close as possible to actual reasoning. Thus arose a ‘calculus of natural deduction.’”

Natural deduction also allowed philosophers and mathematicians to make a complete guess and then see where it went using a formulaic, universal code. This allows entire phrases, formulas, and propositions to be replaced with letter variables and then combined using symbols. Let’s say the letter p stands for “all inventions are the product of the history before them,” and the letter q stands for “telephones are an invention.” The conclusion of those two propositions then is: Telephones are the product of the history before them. The theory of natural deduction is what allows mathematicians and philosophers to build a proof that allows us to infer new sentences logically followed from existing ones.

Natural deduction, then, is the proof of how we think, and in its invention, these two philosophers proved that our brains do work in a logical, traceable pattern. When both absorbed the same information about their industry, they processed it through a series of logical steps to arrive at nearly identical proof processes.

Gentzen was the first to use the actual term “natural deduction” to describe this method developed by both of them, but Jaśkowski’s visual layout became the one used in most elementary logic textbooks in the 1940s and ’50s. In Jaśkowski’s method, proofs were set inside boxes to denote subpoints and laid out in a graphical manner. Later, he would extend this to an easily typed numerical bullet point system. In Gentzen’s method, the proofs are set up in a tree that looks like a very complex fractional problem.

How exactly all of this works out on paper involves a lot of Greek letters and equals signs, and although I had three different mathematicians explain it to me, it’s pretty irrelevant to why this discovery matters. Natural deduction is the mathematical component to how our brains work; it is the scientific effort to make sense of how we come to conclusions and what assumptions we make to get there.

“The story continues with these discoveries going from ‘underground,’ being known only to the logical sophisticates, and being passed from one enlightened initiate to another […to] the early 1950s when the method became a part of some elementary textbooks,” logic professor Francis Jeffry Pelletier wrote in his article “A History of Natural Deduction and Elementary Logic Textbooks.” This populism of natural deduction spread the theorem more quickly than either creator could have imagined. Today, natural deduction using the logical proofs laid out by Gentzen and Jaśkowski’s papers is the primary way most philosophers do their work.

It’s fitting that, like so many other discoveries, the discovery of natural deduction would happen simultaneously. It is at its most basic, a system of relevant formulas and rules to explain how our brains work. Two men, working in separate places with no overlapping interests, came to it at the same time because it was, well, the most logical next step. Like so many inventors before and after them, their moment of revelation was sparked not by a moment of genius but by the exact proposition they laid out: that human brains work in systematic understandable ways based off the information they have gathered before them.