Roadmap

Where the library is

Every result this library claims is tagged @[headline] in the Lean source, and the table below is generated from those tags by lake exe statusgen. It is not a summary someone maintains beside the arguments: rename a theorem, restate it, or delete it, and the next run moves the table. lake exe statusgen --check fails CI when the committed copy has drifted.

Each heading links to that argument's own page, where the same results are set out with their docstrings, the premises they rest on, and the rival readings they are checked against — also generated, by lake exe argdoc.

6 arguments, carrying 223 headline results, listed below in source order. one of them is marked ⚗: a result this library constructs rather than reports, with no source found advancing it in that form.

Born in Bethlehem — Micah 5:2

Born of a virgin — Isaiah 7:14, Genesis 3:15, Micah 5:2–3

Sola fide

The canonical witness — faith alone, from the texts all parties accept

Sola scriptura

Spirit baptism — at conversion, after it, or in the sacraments

Twelve findings emerged that were not designed for.

Redundancy defeats a lexical dispute. Sola fide runs on three independent strands — Paul's ἔργα νόμου, Jesus' σέσωκέν σε at Luke 7:50, and Peter's refusal of the law's "yoke" at the Jerusalem council (Acts 15:10) — and no strand's disputed premise carries the argument alone. Only their disjunction does. An opponent must defeat all three readings, not one.

Before Acts 15 was encoded the argument had two strands, and defeating Paul's reading and Luke's together defeated it. That is no longer true, and the change is recorded as a result rather than left to be inferred from the old one's absence: apostolic_strand_survives_paul_and_luke. The apostolic premise is logically independent of the Pauline one but not dialectically: a reader who takes ἔργα νόμου as Israel's boundary markers will read Peter's yoke the same way, as Jervell does. The encoding cannot make that reader answer twice; it does show that there are two texts to answer.

The πίστις Χριστοῦ dispute was expected to add a strand of its own, and did not. Every text where the phrase occurs sets it against νόμος, so a route through the genitive still passes through what ἔργα νόμου denotes. Encoded honestly, it is a second disputed premise inside the Pauline strand. Deny it together with the other strands' premises and sola fide fails (pistisChristou_jointly_load_bearing); deny it alone and the other strands still carry the argument (pistisChristou_not_load_bearing). The genitive is the hinge of Paul's route, not of the conclusion, and it does not follow the Old/New Perspective line: Dunn holds the objective genitive and the New Perspective together.

A fourth strand, from John's Gospel, has the same shape and is encoded alongside the other three but not yet inside the Reformed case. "This is the work of God, that you believe in him whom he has sent" (John 6:29) delivers sola fide if its believing is trust, as Calvin reads it (johannine_strand_establishes), and not if it is faith living through charity, as Aquinas reads it (johannine_strand_rests_on_believing_as_trust). Luther answers that reading from Galatians 3:11–12 — charity is what the law commands, and the law is not of faith (luther_answers_aquinas_from_galatians) — though the texts alone do not settle it; his step does (luther_answer_rests_on_his_step). Folding it into the Reformed case changes every joint result above, so it is a step of its own (#86).

Sola fide's rivals deny different parts of it. The conclusion is three atoms — by grace, not by works, through faith — because a single atom could not say what a rival keeps. Trent denies the second, by merit. The apocalyptic reading denies the third and establishes the first two by its own route (apocalyptic_establishes_grace_not_works). And the split shows which part the strands are for: remove every lexical premise from every strand and grace and "not by works" still follow, from the texts that say so in terms and the answer to James (grace_and_works_rest_on_no_lexical_premise). The lexical disputes decide through faith alone — whether the texts that exclude works also name faith as the means — and, as encoded, nothing else.

The ἔργα νόμου dispute is a dispute about Judaism. The New Perspective's reading of Paul's phrase is not a bare premise but an inference, Dunn's, from Sanders' covenantal nomism; its critics answer by denying the ground, and derive the Reformed reading from the denial. On their history Paul alone carries sola fide (critics_carry_the_pauline_strand); on Sanders' he does not (sanders_costs_the_pauline_strand). What the lexical question turns on is a historical one about Second Temple soteriology. And what justification is — forensic, or Christ present in faith — turns out to be a separate question again: the Finnish reading of Luther denies the forensic account with Trent and still establishes sola fide (forensic_justification_not_load_bearing). What Trent's objection does rest on is its fuller definition — justification is the renewal of the inward man, which grows through good works — against the Reformed distinction of justification from the sanctification that follows it. Put the distinction in its place and Trent's case no longer denies "not by works" (trent_objection_rests_on_its_definition).

Jesus' own words decide less than either side cites them for (#122). Luke 18:9–14, where the tax collector "went down to his house justified", is Jesus' own teaching on justification and works, in Paul's word for it. The word pronounces a verdict there, and the tax collector brings no meriting works. Trent never cites Luke 18, but its case is consistent with every word of the parable (trent_grants_the_parable), since nothing before justification, "whether faith or works", merits it (Session VI, ch. 8). What divides them is the step to "faith suffices", which Trent's dispositions (ch. 6) and canon 9, applied to the parable, deny; so Luke 18 can be defended and is not forced (luke18_defensible, luke18_not_forced), meeting Trent where Luke 7:50 does (whyLukeEighteenStandsAgainstTrent). Matthew 7:21–23 and 19:16–22 are encoded as readings, never as what the text plainly says: the texts alone leave open whether obedience is a ground and whether the commandments are the way to life (matthew7_leaves_the_ground_open, matthew19_leaves_the_way_open), and each reading stands off against its rival. Heard together, Jesus' words force nothing (jesus_words_force_nothing); heard without Trent, Luke's two sayings are forced (without_trent_luke_is_forced) — that faith sufficed, not faith alone — and Matthew is still not.

Baptism, with its senses kept apart (#122). Trent makes water baptism the instrumental cause of justification, and chapter 4 qualifies it: "or the desire thereof". Water, the Spirit and "fire" are separate atoms, and the readings of the fire are encoded without a winner (the_baptist_leaves_the_fire_open). The dilemma whatTrentsInstrumentalCauseClaims finds that nobody on record holds the washing itself necessary for justification — even Feeney, who holds it necessary for salvation, grants that the desire justifies — and that Feeney's reading cannot be held with the thief read as Augustine reads him, nor with Rome's own teaching on the desire. Read in Trent's own words, the claim meets only the Reformed argument from the desire, at a step Aquinas contests. Of the readings of John 3:5's water (whatJohnThreeFiveMeans), only the baptismal one leaves Trent's step from the verse standing, and even then the step is disputed. Acts giving the Spirit before the water and after it is common ground (trent_grants_god_is_not_bound), not a Reformed win.

As a dispute, only Paul's word prevails; sola fide and Trent each stand, and neither is forced. Weighed as a dispute — the three strands argued separately, Trent, the apocalyptic reading, Sanders, the critics, Jervell, Paul's gospel in Galatians, Paul's word, and Trent read as a claim about that word — one thing prevails outright: Paul's word, that δικαιόω does not denote the renewal of the inward man (only_pauls_word_prevails). It prevails by two routes: lexically, from the forensic sense, Paul's own words for renewal and the rule of least meaning (Joos; Silva; Barr); and exegetically, from Romans 4:3–8, where Paul glosses the righteousness counted to the ungodly as sin not counted. Every link of each is rated wellSupported or better, so Trent read as a claim about the word cannot be defended (trent_on_pauls_word_indefensible) — nor can the Latin gloss it rests on, "being justified" as "being made righteous". Every other party's weakest link is disputed, and every attack between Trent and a Reformed party runs both ways, including a claim a party derives on the way to its conclusion. So Luke's case, Paul's gospel and Trent — as Trent states it, tied to neither reading — are each defensible and none forced (dominical_case_defensible, dominical_case_not_forced, gospel_defensible, gospel_not_forced, trent_defensible, trent_not_forced). The dilemma whatTrentsDefinitionClaims says why: read as a claim about Paul's word, Trent's definition cannot be held with the lexical and exegetical cases; read as a claim about what God does in justifying, nothing about the word reaches it, and it parts from Paul at the step from Galatians, that a verdict on a finished work excludes the renewal wrought in us (whereTrentPartsFromPaul), and at the step from Romans 4 — each rated disputed, because Augustine and Trent grant the texts and read them the other way. Two hearings answer narrower questions. Heard as Rome and the Reformers alone, only Paul's word is forced (reformation_dispute_forces_only_pauls_word). Heard without Trent, Luke's case, Paul's gospel and Paul's word are forced, but sola fide is still not — from Paul, because of Campbell's reading of πίστις Χριστοῦ, or from Peter, because of Jervell's reading of the yoke (sola_fide_from_paul_not_forced_without_trent, sola_fide_from_peter_not_forced_without_trent). Luke's case is attacked by no one but Trent, because no cited source argues that σῴζω at Luke 7:50 means healing. A search for one found none, so that premise is rated wellSupported; and the dominical case carries the Reformed reading of 7:47 — her love is the evidence of her forgiveness, not its ground — as a premise. That reading is cited to Osvaldo Padilla's narrative-critical study of Luke 7:36–50 and to Melanchthon's Apology of the Augsburg Confession, which reads 7:47 by 7:50; both read 7:50 as salvation received by faith.

Authorship is not a premise, and the encoding says what that costs. Ephesians, Titus and 1 and 2 Peter are each disputed, and each dispute is catalogued from both sides. Grant every critical conclusion and sola fide still follows (authorship_not_load_bearing), because the case reads them as canonical scripture rather than as an apostle's testimony. The cost is that they cannot then be evidence of what Paul meant by "works", so the premise that he meant works in general rests on Romans 4, 9 and 11, which nobody disputes.

The virgin-birth argument was the weaker one, and stopped being so. It began single-stranded, and the library's result then recorded that defeating עַלְמָה defeated it outright. Adding the protoevangelium (Genesis 3:15), Michean (Micah 5:2–3) and compositional (Isaiah 2–12) strands changed the structure, not the Isaianic evidence: almah_not_load_bearing now holds, while almah_is_load_bearing_alone preserves the original finding about the Isaianic strand taken by itself.

The same module carries a referential reply that answers the lexical dispute without entering it — עַלְמָה need not mean "virgin" for Mary to be one — and compatibility_does_not_establish_criterion records its price: the reply is purely defensive. The contrast between these arguments is a structural fact about them, not a matter of taste, and the library states it in a form either side can check.

A rival's circularity, shown rather than alleged (#13). Wegner's sharper form of the lexical objection — הָרָה at Isaiah 7:14 is a predicate adjective, so the עַלְמָה is already pregnant and therefore no virgin — is encoded at full strength, and wegner_establishes checks that it goes through. What the grammar does not supply is that the pregnancy is an ordinary one: that comes from the near-term reading of the sign, which the lexical conclusion was then wanted to support. With both legs in place, circle_leaves_the_lexical_conclusion_open and circle_leaves_the_denial_open show that neither end is settled either way, because a cycle of implications is satisfied outright by a valuation on which every node in it is false, and equally by one granting Wegner's conclusion. Postell's charge of circular reasoning becomes a checkable result rather than an accusation — and, like every result here, a conditional one: deny that the near-term reading needs the lexical conclusion and the circle is not there.

The oldest answer to the objection goes to the same premise (#73). Justin, Irenaeus and Origen argue that an ordinary conception would have been no sign. Encoded against its rival, that a sign need not be a miracle, sign_leaves_the_lexical_conclusion_open shows that it blocks Wegner and settles nothing about the word. As a dispute, the three positions tie (nothing_prevails_over_wegner), and the tie is a fact about two ratings. It turns on whether the sign of 7:14 must be the kind offered at 7:11, and on whether the reply's inference survives Rydelnik, who grants its grounds.

The Septuagint's "virgin", weighed rather than assumed. Irenaeus's argument — Jews translated Isaiah into Greek long before Christ and wrote παρθένος — is encoded at full strength, and three results say what it does. It rests on one claim, that παρθένος in the translator's Greek means a virgin (parthenos_is_load_bearing). Rico and Gentry hold that claim, and Bratcher with them; Wegner, Rhodea and Meade deny it, pointing to Genesis 34:3, where the Greek calls Dinah a παρθένος after Shechem has lain with her. The Greek Pentateuch, the corpus that verse comes from, uses the word in its laws where virginity is the point (Leviticus 21:13–14, Deuteronomy 22:13–21), and a new article of the ontology carries a sense found in a passage to the usage it belongs to (a_sense_in_a_usage_at_work), so the laws' sense excludes Wegner's "not yet 'virgin'" by what the words mean. Genesis 34:3 itself is read under the law of the seduced παρθένος (Exodus 22:15–16), which still calls the woman a man has lain with a παρθένος and owed "the bride-price of virgins"; Genesis 34 tells Shechem's act in that law's words. Weighed as a dispute, the Septuagint's side prevails (septuagint_prevails_over_wegner): that reading of Genesis 34:3 defeats Wegner, and he, on a step rated disputed, cannot answer it. The verdict turns on one rating, that reading's step, plausible because no reader found grants its grounds and denies it, and no higher because none found makes it; rated disputed, it would leave nothing prevailing, as before. The page says where the evidence lies, which the ratings do not weigh. A third standard, Scripture interprets Scripture, hears no dissent from a step grounded in Scripture alone unless the dissent rests on Scripture too; under it Matthew's reading of the Greek word, from his quotation of it of Mary, prevails over Wegner, and under the evidence standard the two stand off (matthew_step_turns_on_the_standard). Granted the word, the Septuagint shows that a pre-Christian Jewish reader took the woman of 7:14 to be a virgin, not what Isaiah's word means (septuagint_word_rests_on_its_inference), and its future tense leaves open whether she conceives as one (septuagint_leaves_the_conception_open). The two rival claims about παρθένος exclude each other by their meanings — Wegner's says the word meant a young woman and not yet a virgin — and the dispute's attacks are computed with that.

"Her seed", read two ways. The protoevangelium strand holds that Genesis 3:15, by naming the seed as the woman's, marks a birth with no human father. Read as what the wording itself signifies, that is Luther's argument, and it rests on his step (her_seed_rests_on_its_inference): Leupold and Keil grant every ground and deny it, and so does Lewis, on grounds that do not need the promise reading he doubts. Weighed against Leupold and Lewis, nothing prevails (nothing_prevails_over_her_seed), but the tie is nearer to breaking against Luther than for him: one rating, Lewis's step from Hagar and Rebekah, would break it against him, and two would be needed to break it for him. Read as what the wording fits once fulfilled, Leupold and Keil grant it, and it rests on the virginal conception rather than evidencing it (whatHerSeedMarks). The Septuagint's "he" for the neuter σπέρμα may show that its translator read one person (disputed: Philo, its earliest known reader, took it of the mind), and leaves the father open (the_greek_he_leaves_the_father_open). The promise is also weighed as a promise: every term of the verse is met as the New Testament names it (Galatians 4:4, Revelation 12:9, Hebrews 2:14, 1 Corinthians 15:3–4), and the fulfilment confirms that the verse was a promise, without needing the virgin birth (the_confirmation_does_not_need_the_virgin_birth); with it, the seed was of the woman alone (seed_of_the_woman_alone). Weighed against Westermann's denial that the verse is any promise, nothing prevails (nothing_prevails_over_the_promise): his "a line of descendants and not an individual" is answered from the Hebrew syntax of 3:15b, and that answer is disputed too. So is the reading of the scene as a whole, in which the speaking serpent is the instrument of a power the sentence falls on (its step plausible, its ground on the power disputed). Under the Scripture standard, which hears no dissent from a step grounded in Scripture alone unless it rests on Scripture too, Westermann is not heard and the fulfilment prevails (promise_turns_on_the_standard). A dissent now counts only on evidence the texts leave standing: Miller's "young widow" at Joel 1:8, a bride in the Greek, is struck from his dissent from the laws, which still stands on Genesis 34:3 (miller_survives_on_genesis) — but only with his premise that the noun there describes Dinah as she then was, which is his reading and not the text (miller_rests_on_the_noun). And a credible dissent now stops counting when it is overruled in a dispute that weighs the step at its floor: Miller's case from Genesis 34:3, a party in the dispute over the Septuagint's word, cannot be defended there (miller_indefensible), so the laws' step stands at its cited wellSupported under every standard (laws_step_ratings). On the way, the strand's Miravalle citations were corrected: Meet Mary, which could not be checked, gave way to the books where the passages are.

A corollary worth noting: because the New Perspective rejects the traditional reading of Paul's phrase while still affirming justification by faith, it establishes the conclusion too. Winning the ἔργα νόμου argument is not a defeat of sola fide.

The same reply, six times. The major objections to sola scriptura turn out to share a form: an authority outside scripture is needed to make scripture usable — to fix the canon, to supply the vocabulary Nicaea settled on, to identify which unwritten apostolic teaching is genuine, to license a development. And the reply is the same every time: so do you. Kruger on the canon, Mathison on interpretive authority, Athanasius answering the Arian charge that ὁμοούσιος is unscriptural, Whitaker on unwritten tradition, Geisler on who may interpret the Old Testament, Barrett on perspicuity — six instances across seventeen centuries, by people arguing against each other.

What the library adds is the price, and it has a name: a parity reply renders the disputed proposition independent of the premise set. Granted the reply's grounds, the proposition neither follows nor fails — two readings satisfy those grounds, one with it and one without. parity_leaves_the_canon_open and parity_leaves_the_distinction_open say exactly that, and saying it once is the whole finding: blocking the objection and establishing nothing are not two facts about the move but one fact seen from either side. It neutralises an objection and establishes nothing, because conceding a charge is not answering it. That is the lesson compatibility_does_not_establish_criterion already recorded for the virgin-birth argument, now shown to be a property of the move rather than of any one dispute.

And naming a shape finds the cases that do not fit it. The three parity replies in the sola scriptura argument were each written as a pair of results, "it blocks" and "it establishes nothing". Two of the pairs were genuine independence claims. The third was not: its halves asked about different propositions over the same premises — whether the circularity defeats Tradition I, and whether Tradition I's reasoning is circular — while being presented as complements. Nothing checked that, because nothing required the proposition to be named once. Under Independent it has to be, and the defect was visible immediately. Restated, the first half is parity_leaves_the_defeat_open and the second is stronger than it was: circle_parity_concedes_the_charge shows the reply does not merely fail to clear the charge but grants it outright, since the charge is one of its own grounds.

The notion is Foundation's — Independent φ there is 𝓢 ⊬ φ ∧ 𝓢 ⊬ ∼φ, over provability. Testimony.Logic.Independent is its semantic counterpart, over the entailment this library uses, and leaves_open proves one from the two readings the premises admit. Both readings stay named, for the same reason every countermodel here is named.

Answering an objection is two moves, and only one of them can win. Every reply in the library was written the same way, as the objection's own line with a ground replaced. Asked which of them contradict the ground and which merely decline it, they split. Kruger on the canon, Mathison on interpretive authority, the final-arbiter answer and both replies to Geisler's circle decline it: kruger_refuses_rather_than_denies shows Kruger's premises leave the requirement he refuses standing. Berry and Postell deny theirs, as do the classical answer to self-refutation and Barrett. A refusal takes a ground away, and its effect is the independence finding above. A denial is an attack, and an attack can defeat.

Entailment cannot say that one argument defeats another, because adding premises never removes a conclusion. A dispute can. The Isaiah 7:14 positions, taken as an argumentation framework with defeats proved from their premises and their cited confidences, show that against the scriptural reading alone nothing prevails (nothing_prevails_unanswered): each defeats the other. Once Berry and Postell are heard, the scriptural reading prevails (scriptural_reading_prevails_once_replies_are_heard), and the critic cannot be defended at all (critical_denial_indefensible). Two corrections got it there. The first draft rated the critic's exclusion premise wellSupported while recording, in the same argument, two scholars who contest it; rated as the library defines disputed, it became the critic's weakest link. Then the replies' inferences, unrated, had let each reply be weighed by its observations alone, so that where an encoding put a contested move — atom or step — decided who prevailed. Rated, Berry's and Motyer's steps are disputed and tie with the critic (nothing_prevails_on_motyer_alone). The verdict rests on Postell's inference — an oracle on the Assyrian timeline, read messianically, refutes the exclusion — rated plausible because no source cited grants its grounds and keeps the exclusion. He gives it two instances, Isaiah 9 and 11 and Micah 5: either suffices (scriptural_reading_prevails_without_postell), and without both nothing prevails (nothing_prevails_without_the_counterexamples). That makes the ratings premises of the result, and says which one to contest.

A premise can be load-bearing in one role and not another. The sola scriptura seed asserted in prose that the whole dispute reduces to whether scripture teaches the principle. Split into the two jobs that premise does, the claim is both weaker and sharper. It is not load-bearing for reaching the conclusion — hinge_not_load_bearing_for_conclusion strips it and the eliminative line still delivers — while hinge_is_load_bearing_within_classical_strand holds within that strand alone. Against the self-refutation objection it is one of two answers rather than the only one, since the objection's step is a conjunction and either conjunct may be denied: classical_answer_blocks_self_refutation denies one and scoping_blocks_self_refutation the other. "The dispute reduces to the hinge" was pointing at something true and describing it too broadly.

Jesus' rebuke of tradition settles less than it is cited for (#122). Mark 7 used to sit among sola scriptura's shared grounds, cited and read by no step. As a line of its own, it delivers a principle — God's word judges human tradition, and no commandment of men may be taught as God's word — and the principle is common ground while "God's word" is left as each side uses it: Rome's teaching office is "not above the word of God" (Dei Verbum 10), and Trent can hold every word of it (trent_grants_marks_principle). Weighed as a dispute, the principle prevails (marks_principle_prevails); sola scriptura from Mark 7 and Trent can each be defended, and neither is forced (mark7_case_defensible, mark7_case_not_forced, trent_defensible_against_mark7, trent_not_forced_against_mark7). The dilemma whatTrentsTraditionIs says why. Read as commandments of men, Trent's tradition is what Mark 7 condemns and cannot be defended (trent_as_mens_commandments_indefensible); heard against that reading alone, Mark 7's case is unopposed (mark7_forced_against_mens_commandments), though it still rests on two premises rated disputed that no party left in that hearing contests. Read as the apostolic word handed on unwritten — what Trent says it receives — Mark 7 does not reach it (mark7_does_not_reach_the_apostolic_word, against_the_apostolic_word_only_the_principle_is_forced), and the dispute moves to what the sola scriptura argument already turned on: whether any apostolic word survives outside Scripture, and whether the principle would then make Scripture the sole infallible rule. Weighing the dispute also moved a rating. Trent's claim that tradition is a coordinate source of revelation had been wellSupported. Geiselmann grants Session IV and denies that it canonised two coordinate sources, since the council replaced its draft's "partly … partly" with "and", and Congar judges that Trent left the question open. So it is disputed now, and the Tridentine party is named "Trent (Tradition II)" rather than by the reading in dispute.

A position its own cataloguer calls unworkable establishes the conclusion. Mathison files "solo scriptura" as Tradition 0 and judges it "unbiblical, illogical, and unworkable". tradition0_establishes shows that, stated by Geisler — who holds a version of it — rather than by its critic, it reaches sola scriptura by its own route. This is the second time the pattern has appeared; the New Perspective does the same for sola fide. Both results come from the same discipline: encode a rival from a source that holds it, never from a description of it.

Spirit baptism, a question among Protestants, is an argument of its own (#122). At conversion (Dunn, Stott), after it (the Assemblies of God; the Church of the Nazarene), or in baptism and confirmation (Rome; Lutherans hold the first half): weighed as a dispute, nothing is forced (spirit_baptism_forces_nothing). The conversion and sacramental views can be held together against a second baptism to seek, the two subsequence views can be held together for one, and each camp can be defended and is not forced (conversion_defensible, conversion_not_forced, pentecostal_defensible, pentecostal_not_forced). It turns on the Acts narratives: read for what its claims mean, the Pentecostal view must take them as a pattern, since Stott's "not a pattern" excludes its premise (pentecostal_cannot_read_acts_as_transitions), and read as a pattern they meet the variety of Acts itself. The holiness reading meets Wesley, who held the second work and declined to call it receiving the Holy Ghost, and the Nazarene seminary faculty, who keep entire sanctification and no longer hold the reading tenable. Tongues as initial evidence, and whether Paul and Luke mean the same by "baptized in the Spirit", are not yet encoded.

And one finding about the method rather than about an argument. Entails quantifies over the valuations satisfying the premises, so a premise set with no model entails everything. A package assembled from contradictory premises would establish its conclusion, the proof would close, and all four gates would pass — a claim simultaneously proved, axiom-clean and empty. Nothing checked for it, and Satisfiable did not exist. Twenty packages were audited, every one in the library carrying a positive Establishes result, and none was unsatisfiable: no result here was vacuous. Rule L11 now fails the build for a package that establishes a conclusion without exhibiting a model, so that is a standing check rather than a snapshot.

Near term

More messianic prophecies (#1, #2). The canonical dozen — Isaiah 53, Psalm 22, Zechariah 9:9, Daniel 9, Psalm 110 — each with competing packages. Then the first aggregate result: a MessiahDefinition with several criteria and a MeetsDefinition theorem, which will expose how sensitive a cumulative case is to its weakest link.

The remaining solas (#3). Sola gratia, solus Christus and soli Deo gloria. Sola scriptura is no longer a seed: it now carries four positions on tradition, three objections that do not reduce to one another, the two answers to the self-refutation objection, and a dispute over what Jesus' rebuke of tradition in Mark 7 decides.

Corpus grounding (#4). Importers so Passage values resolve against real text data (BHSA, OSHB, STEPBible). At that point linguistic premises can cite actual morphological annotation rather than a commentary's report of it — which matters most for exactly the lexical premises that keep turning out to be load-bearing.

Systematic theology

The natural extension. Doctrine is already structured the way this library wants: confessional standards state positions in numbered articles, and the relations between doctrinal loci are exactly the dependency structure the manifest machinery tracks.

• Confessional standards as versioned, citable axiom sets (#6) — the Nicene Creed, the Chalcedonian Definition, the Westminster Confession, the Catechism of the Catholic Church. Each becomes an ArgumentPackage whose atoms cite specific articles.
• Cross-locus consistency checking. Do a tradition's commitments on Christology, the atonement and justification cohere? This is a question about a set of formulas, and it is decidable for the propositional fragment.
• Dependency tracing. Which doctrines rest on which exegetical premises? If a reading of Romans 5 is abandoned, what else moves? Prose systematic theology cannot answer this; a generated manifest can.

The divinity of Christ is the obvious target and the hardest: it is a cumulative argument drawing on the Johannine prologue, the ego eimi sayings, worship texts, and the Chalcedonian settlement's reading of all of them. It should be attempted only once the aggregate machinery has been tested on the messianic prophecies, where the premises are simpler.

Philosophical theology

This is why the substrate choice matters — though not quite in the way this page used to claim. Foundation itself has no modal logic: its structure is Logic, Propositional, FirstOrder, SecondOrder, Meta and Vorspiel, and the FirstOrder/Kripke modules are Kripke semantics for intuitionistic first-order logic, with no □ and no ◇.

The modal logic is a sibling package, FormalizedFormalLogic/ModalLogic, which depends on Foundation and so shares the Semantics and Entailment interfaces this library already builds on. That is a smaller claim than the one this paragraph made before, and a true one: the arguments needing □ and ◇ are reachable by adding a dependency in the same family, not by changing foundations. The family also has neighbourhood semantics — which is what the omnipotence paradoxes usually want, normal modal logic being too strong for them — and a Lean 4 formalisation of Gödel's ontological argument. See #61 for the survey and #52 for the work, which begins with a toolchain reconciliation.

Nearer than the modal work, and currently invisible on this page: Foundation's FirstOrder is complete and unused here. Every argument so far is propositional, and SolaScriptura records what that costs — its doctrine/practice scope distinction "is carried by atom design and by this docstring, not by the logic", because a propositional fragment cannot quantify. That limitation is closable with no new dependency at all.

• Divine attributes and their alleged incompatibilities. The omnipotence paradoxes, and the foreknowledge/freedom problem — where the formal question is whether a set of attribute definitions is jointly satisfiable, which is precisely what a model-theoretic treatment settles.
• The classical arguments. Cosmological, ontological, moral. The ontological argument is the best-charted territory: Benzmüller and Woltzenlogel Paleo's machine-verified formalisation of Gödel's proof both demonstrates feasibility and illustrates the payoff, having discovered that Gödel's axioms collapse modal distinctions — a structural fact a century of prose commentary had missed.
• Theodicy structures. The logical problem of evil is a consistency claim about a premise set, which is the shape of problem this machinery handles best.

Infrastructure

• Premise-to-result cross-links (#7) on the docs site. lake exe argdoc already generates a page per argument that numbers every claim with its source and lists every package and result. Missing is the link from each result to the premises it rests on, and back from a premise to every result that would fall with it.
• Literate sources (#9). Prose and Lean interleaved in the .lean files, in the coqdoc tradition, rendering to PDF. This is currently blocked on tooling rather than on effort. Alectryon plus LeanInk was the path, and LeanInk is archived — last pushed in July 2024, pinned to Lean v4.6.0-rc1. Verso is actively developed and has a TeX backend, but it is HTML-first and inverts the model: documents embed Lean rather than Lean files carrying prose. Until one of those changes, lake exe argtex covers the part that matters most — the arguments themselves, typeset as logic.
• Probabilistic and evidential reasoning (#10), in a separate namespace, never conflated with deduction. Cumulative-case apologetics is Bayesian in structure, and pretending otherwise would misrepresent it.
• API documentation (#8). doc-gen4 arrives transitively via Foundation and the Testimony:docs facet works, but lake build Testimony:docs generates documentation for the entire Mathlib closure, which is far too slow to run in CI. Publishing API docs needs either a way to scope generation to this library's own modules, or a separately cached job. It is deliberately absent from the docs workflow until then.

Development environment

• A devcontainer (#11), so that the toolchain is consistent and not only the worktree layout. Contributors should not have to install elan and match Lean v4.33.1 by hand.

How deferred work is tracked

Everything above is a GitHub issue; the roadmap label marks the items seeded from this page, and infra the build and developer-environment ones. This page says why a thing is worth doing; the issue is where its state lives. When the two disagree, the issue is current.

What will not change

The conditional form of every result, the requirement that rivals be encoded with equal care, and the prohibition on undeclared axioms. These are what make the rest worth reading.