Logic has shifted in meaning over the many centuries which we've studied the concept derived from ancient greek philosophy. With that it has shifted in function, from the dichotomy of being relegated to a strange past time of men who'm speak of wisdom, or the treasured secrets of statesmen and politicians, using what they discover to govern and scheme... to now a centerpiece to the way we interact with the world, the knowledge of it, and the civilizations that are built on its foundations.
Today, the world runs on Logic; from the theories that mathematicians create, adopted by physicists and engineers to produce great feats that were once thought reserved activities of the mythological deities... and alike by economists, and information scientists, and the managers of the logistical framework that powers the daily lives of ever increasing billions of people. Logic is both a means to utility, and an end to enlightenment.
But what if we viewed Logic intead as a medium of contemplation?
The Cathedral of Axioms
When we enter a formal system, we learn to engage with the ways to communicate and interact with the ideas of our rationality, the mechanisms of the world, and the creativity of our soul. We step into the endless possiblity of a constructable reality where Logic, Language, and Love form the structural pillars, as well as the open rooms of discovery, and the spiritual guides in tangible form. These are not separate disciplines; in the Cathedral, they are one substance viewed from three angles.
Logic: The Architecture of Truth
We often mistake Logic for a constraint—a set of rigid rails that limit where we can go. But in the Cathedral, Logic is the masonry. It is the force that allows structure to exist at all. Without the Law of Non-Contradiction, there is no "here" or "there," only a chaotic soup.
Logic provides the solidity of the spiritual practice. It ensures that when we place a stone (a Lemma), it holds the weight of the spire above it (the Theorem). It is the discipline of coherence.
Language: The Liturgy of Naming
If Logic is the stone, Language is the chant.
Philosophers like Wittgenstein and the formalists understood that logic is a language—a formal grammar for describing reality. In constructive type theory (the foundation of Lean), to have a proof of a proposition is to have a "term" of that "type." Truth is an object we can speak.
When we define a Type, we are performing an Adamical act of naming. We carve a concept out of the void and give it a handle. To code is to speak; to speak clearly is to pray.
Love: The Teleology of Proof
And what is the purpose of this structure? Why speak?
St. Anselm saw Logic not as a dry calculator, but as Logos—the Divine Reason. For Anselm, to reason correctly was to align one’s mind with the mind of God. Logic is the language God speaks.
Therefore, the act of proving is an act of Love. It is the desire to know the Beloved (Truth) so intimately that we re-trace His thoughts. When we close a proof with QED (or ∎), we are not just finishing a task; we are resting in the completed image of Truth.
"I do not seek to understand in order that I may believe, but I believe in order that I may understand." — St. Anselm