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

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.