The Beautiful Simplicity of the Gentzen System
Gentzen system, created by German mathematician Gerhard Gentzen, is a deductive system which can be used to prove propositional formulas. I recently learned about it while I was reading Ben-Ari’s fantastic book on mathematical logic [1] and I like its simplicity.
Should we care about the Gentzen system? Let’s say you’re a programmer, why should you care about logic or mathematical reasoning?
I recently started learning more about mathematical logic, and I’ve realized that, just as writing can clarify your thoughts, formal mathematical reasoning can bring coherence to your thinking. If parts of your reasoning lack logical soundness, you won’t be able to construct a coherent argument as a whole—mathematical reasoning helps prevent this.
I’ve been programming for a while now, mostly self-taught, and I’ve observed that while learning mathematical formalism isn’t necessary for most programming jobs, it definitely helps you think more carefully about the correctness of your code. It helps you reason through problems with greater precision.
.png)
