🧮 De Morgan of Tarsus

Paul is doing something in the epistles that reads as rhetoric and behaves as engineering.

Strip the ornament and the arguments don't collapse into vibes. They resolve into inference rules. Named ones. The same ones, over and over, applied deliberately, with the failure modes patched.

I mean this literally. It compiles.

The first cut

Do ye not know that the saints shall judge the world? and if the world shall be judged by you...

judge(Saints, X)
member(You, Saints)
───────────────────
judge(You, X)

That's where this started. And it's half an argument.

Verse 3 has an explicit marker — πόσῳ μᾶλλον, how much more. Paul's conclusion isn't that you can judge the world. It's that you can settle a property dispute between two church members. The force is all in a second step, and that step needs an ordering relation, not an implication:

harder(world, smallest_matters)
judge(X, H) ∧ harder(H, E) → judge(X, E)

Normalizing makes you write down the premise Paul never states. That's the first thing it buys you, and it generalizes: every formalization of a Pauline argument surfaces a suppressed one. Two thousand years of commentary lives in exactly those gaps.

Three operators

Once the ornament is off, the same three things keep surfacing. They aren't figures of speech. They're opcodes.

οὐκ οἴδατε — do ye not know. Around ten times in 1 Corinthians alone. Not a premise: an audit. Paul never argues for these. He asserts you already hold them and aren't querying. The letter's whole posture is you have the facts, you're not running the inference.

μὴ γένοιτο — God forbid. Fourteen times in Paul, ten of them in Romans. It's the discharge marker on a refutation, and most often it's the ¬Q of a modus tollens:

P → Q
μὴ γένοιτο ≡ ¬Q
───────────────
¬P

πολλῷ μᾶλλον — much more. The ordering relation. Rom 5:9, 5:10, 5:15, 5:17, 11:12, 11:24.

Three operators, consistently applied, across a corpus written over twenty years to different cities about different fights.

That isn't a style. It's an instruction set.

The part that made me stop

Romans 8:38–39.

For I am persuaded, that neither death, nor life, nor angels, nor principalities, nor powers, nor things present, nor things to come, nor height, nor depth, nor any other creature, shall be able to separate us from the love of God.

Demorganize it: Paul wrote a negated disjunction, the normal form is a conjunction of negations. Standard.

Then look at what the list actually is.

Paired extremes along axes. Naming both poles of a dimension implies everything between them — interval closure, not a flat enumeration. Already engineered.

That still isn't the good part.

The catch-all

Every enumeration leaks. Not as a stylistic weakness — as a hard limit. A finite list can always be defeated by naming something not on it, and length doesn't help. Nine items or nine thousand, the gap stays exactly as wide.

I pulled the closure clause out of the program and asked about something Paul hadn't listed:

?- neg(separates(quantum_decoherence,us,love_of_god))
     NOT DERIVABLE

Read that carefully. It does not say decoherence can separate you. It says I have no information. Open world. And for a letter written to people who expect to be executed, nothing can separate you, and about that other thing I couldn't say is not consolation. Silence fails as badly as a no.

Put the clause back:

?- neg(separates(quantum_decoherence,us,love_of_god))
  domain closure                    [Rom 8:39  ktisis hetera]

οὔτε τις κτίσις ἑτέρα — nor any other created thing.

That phrase does not extend the list. It changes the type of the claim. Before it: a finite conjunction. After it: a universally quantified statement bounded by a sort. Paul can't close the domain by enumerating it — nobody can — so he closes it with a partition of reality he has already established. Everything that exists is either Creator or created. Bind the variable to creature and the list stops mattering. It was never doing the logical work.

You have written this. It's the move from a blocklist to a type check.

if (x === "death" || x === "life" || x === "angels") { … }  // leaks forever
if (x instanceof Creature) { … }                            // closed

Security people say it as you cannot enumerate badness. Paul hit the same wall in the first century, wrote the enumeration anyway because it lands, and sealed it in the final clause so the thing would hold.

The rhetoric and the logic are doing two different jobs in the same sentence.

Where the metaphysics lives

My first encoding of that clause was one line:

creature(X) :- nonvar(X).

Anything you can name is created. Run it and the prover cheerfully derives that God cannot separate you from the love of God — by classifying God as a creature. A conclusion you might not even blink at, resting on a proof that's garbage, with a real verse number attached to it.

Fix the sort and it falls away:

?- neg(separates(god,us,love_of_god))     NOT DERIVABLE

Correct. Romans 8:39 doesn't range over God. Not in scope — that's a different claim, and it would need a different verse.

The entire Creator/creature distinction is load-bearing on one line of Prolog. This is what formalization is actually good for. It doesn't tell you a conclusion is false. It tells you the justification is.

The control case

Here's how you know Rom 8:39 is deliberate rather than decorative: there's a place where Paul does it wrong, and we have it.

1 Corinthians 1:14–16:

I thank God that I baptized none of you, but Crispus and Gaius... And I baptized also the household of Stephanas: besides, I know not whether I baptized any other.

An enumeration. A live patch mid-sentence. Then an explicit refusal to close.

Look at the context — the Corinthians are splitting into factions over who baptized whom. He is under active fire on this exact topic, unrehearsed, and he fumbles the list in real time.

In the program it sits next to Romans 8 with no closure axiom:

?- neg(baptized(paul,fortunatus))
     NOT DERIVABLE

     negation-as-failure would say: YES, Paul did not baptize him.
     1 Cor 1:16 declines to run it. He says he cannot recall.

Prolog's \+ returns no here without hesitating, and is wrong. Paul is more careful than the default semantics of the language. He knows the list is incomplete and he won't let you close it.

Same man, same move, twelve years apart. One hardened, one not.

It doesn't all compile

1 Corinthians 7 will not go into Horn form, and pretending otherwise would be cheating.

Paul tags his own clauses with provenance, inline:

• 7:6 — by permission, and not of commandment
• 7:12 — to the rest speak I, not the Lord
• 7:25 — I have no commandment of the Lord: yet I give my judgment

Defaults with exceptions, ranked by source authority. Non-monotonic. You'd need defeasible logic with a priority order over rules, and the prover has nowhere to put them. They sit in the file, recorded and unused.

Which is the honest version of the claim. Not the epistles are a program. Some of it is a program. The parts that are, are tight.

The genius isn't design

The obvious objection to all of this is that Romans 8:38–39 reads too smooth to be engineered. Patches look like patches. This looks like architecture.

But smooth is what patched work looks like after enough iterations.

Paul had been arguing this material aloud for roughly two decades before Tertius took down Romans. Every one of those arguments was an opening for a heckler to stand up and say but what about—. And we know it happened, because he complains about it by name:

And not rather, (as we be slanderously reported, and as some affirm that we say,) Let us do evil, that good may come? — Rom 3:8

That is Paul objecting to people running inference on his premises and reaching conclusions he never licensed. Not misquoting him. Deriving from him. He is filing a proof-theoretic bug report against his own audience.

So the closed quantifier in Romans 8 isn't a first draft. It's the hardened version — every hole anyone found already sealed, the seam sanded off by repetition. The same reflex shows up in 1 Cor 3:21–22, bracketed (all things are yours, list, all things are yours), and again in Phil 4:8 (if there be any virtue, and if there be any praise). Three letters, three different closure mechanisms, one habit.

You don't see the diff. You see the fixed version.

That's how battle-tested code always looks. It's sculpture: the shape was in the marble, and twenty years of hecklers took away everything that wasn't it.

The program is pauline.pl — 188 lines. swipl pauline.pl. It declines to prove vain(faith), which is the entire point of 1 Corinthians 15.