Trent's claim, and two ways of taking it

trentOnBaptism — Trent: baptism the instrumental cause of justification

Trent's instrumental cause, as Trent states it: water baptism is the instrumental cause of justification.

No premise here rests on scripture alone.

feeneyReadsTrent

Taking the instrumental cause so that the washing itself is necessary for salvation. This is Feeney's reading. Rated disputed: Rome's own teaching denies it (Catechism 1258–1260).

def feeneyReadsTrent : Source :=
  { primary := Reference.work feeneyBreadOfLife,
    tradition := Tradition.romanCatholic, confidence := Confidence.disputed }

trentReadsItsOwnClaim

Taking the instrumental cause as Trent's chapter 4 qualifies it: the laver of regeneration, or the desire for it. Rated consensus, since it is what Trent says.

def trentReadsItsOwnClaim : Source :=
  { primary := Reference.work waterworthTrent (Bib.Locus.page 32),
    tradition := Tradition.romanCatholic, confidence := Confidence.consensus }

asTheWaterItself

The instrumental cause, taken so that the washing itself is necessary for salvation.

def asTheWaterItself : Reading Claim :=
  { name := "so that the washing itself is necessary for salvation",
    commits := p Claim.waterItselfNecessaryForSalvation,
    source := feeneyReadsTrent }

asBaptismOrItsDesire

The instrumental cause, taken as baptism or the desire for it.

def asBaptismOrItsDesire : Reading Claim :=
  { name := "as baptism or the desire of it",
    commits := p Claim.baptismOrItsDesire,
    source := trentReadsItsOwnClaim }

trentOnTheWaterItself — Trent: baptism the instrumental cause of justification, read so that the washing itself is necessary for salvation

Trent's instrumental cause, taken so that the washing itself is necessary.

No premise here rests on scripture alone.

trentOnBaptismOrDesire — Trent: baptism the instrumental cause of justification, read as baptism or the desire of it

Trent's instrumental cause, taken as baptism or the desire for it.

No premise here rests on scripture alone.

What each is set against

thiefToNotNecessary

From the thief to "the washing is not necessary": he was promised paradise unbaptised, and his case bears on salvation under the Gospel.

thiefCase — The thief on the cross (Luke 23:43), read with Augustine

The thief on the cross, as Augustine reads him: the washing itself is not necessary for salvation.

No premise here rests on scripture alone.

desireToNotNecessary

From what the desire brings to "the washing is not necessary".

desireCase — The desire for baptism (Catechism 1258–1259)

Rome's own teaching on the desire: it brings about the fruits of baptism, so the washing itself is not necessary for salvation.

No premise here rests on scripture alone.

desireToNotTheInstrument

The Reformed step from the desire. If justification needs only the laver or the desire for it, and the desire alone brings the fruits of baptism without the sacrament, then the sacrament is not the instrument of justification. Held by Westminster (XXVIII.5; XI.2). Rated disputed, because Aquinas accepts the starting points and denies the conclusion.

reformedOnTheDesire — What justifies where only the desire is present

The question the desire raises. Where only the desire is present, what justifies is not the washing, so the washing is not the instrument. This is the Reformed answer to Trent taken in its own words.

No premise here rests on scripture alone.

The positions, written out

romeOnBaptismReading

Rome's position. Baptism is the instrumental cause. The desire for it brings its fruits. The thief is saved. God is not bound to his sacraments. The water of John 3:5 is baptismal. And the washing itself is not necessary for salvation. Since baptism is a means of justification, faith is not the only means; and since justification includes sanctification, it is not a verdict only.

def romeOnBaptismReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.paulsJustifyDenotesRenewal => False
    | Claim.rev22_11BeJustifiedStill => False
    | Claim.sir18_22BeJustifiedToDeath => False
    | Claim.jamesUsesDikaioAsPaul => False
    | Claim.waterItselfNecessaryForSalvation => False
    | Claim.john3_5WaterIsNaturalBirth => False
    | Claim.john3_5WaterIsEzekielsCleansing => False
    | Claim.john3_5WaterIsTheSpiritsCleansing => False
    | Claim.justificationByFaithAlone => False
    | Claim.justificationIsForensicOnly => False
    | x => True

feeneyReading

A consistent way of holding Feeney's reading: baptism is the instrumental cause, and the washing itself is necessary for salvation. It has to deny that the thief's case bears on the Gospel, and that the desire brings the fruits that save. The first denial is what his reading requires; it is not a sentence quoted from him. With Trent, it denies that faith is the only means of justification, and that justification is a verdict only.

def feeneyReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.thiefBearsOnTheGospel => False
    | Claim.desireBringsFruitsWithoutTheSacrament => False
    | Claim.john3_5WaterIsNaturalBirth => False
    | Claim.john3_5WaterIsEzekielsCleansing => False
    | Claim.john3_5WaterIsTheSpiritsCleansing => False
    | Claim.justificationByFaithAlone => False
    | Claim.justificationIsForensicOnly => False
    | x => True

reformedOnBaptismReading

The Reformed position. Faith is the instrument, and baptism is not. Justification is the remission of sins, not sanctification. The desire brings the fruits, the thief is saved, and God is not bound to water. The water of John 3:5 is the Spirit's own cleansing, and the verse does not require water baptism.

def reformedOnBaptismReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.baptismIsInstrumentalCause => False
    | Claim.waterItselfNecessaryForSalvation => False
    | Claim.john3_5RequiresWaterBaptism => False
    | Claim.john3_5WaterIsBaptism => False
    | Claim.justificationIncludesSanctification => False
    | x => True

Each position holds together

trentOnBaptism_establishes

Trent's claim follows from its premises, trivially, since its one premise is the claim itself. This records the position. It does not argue for it.

theorem trentOnBaptism_establishes : Establishes trentOnBaptism
-- axioms: propext

trentOnBaptism_is_satisfiable

Trent's instrumental cause, as stated, can be held without contradiction.

theorem trentOnBaptism_is_satisfiable : Satisfiable trentOnBaptism.premises
-- axioms: propext, Quot.sound

trentOnTheWaterItself_is_satisfiable

The first way of taking it is fair. By itself, Trent taken Feeney's way contradicts nothing, so it is not a position invented to be knocked down.

theorem trentOnTheWaterItself_is_satisfiable : Satisfiable
    trentOnTheWaterItself.premises
-- axioms: propext, Quot.sound

trentOnBaptismOrDesire_is_satisfiable

The second is fair too. Trent taken in its own words can be held without contradiction.

theorem trentOnBaptismOrDesire_is_satisfiable : Satisfiable
    trentOnBaptismOrDesire.premises
-- axioms: propext, Quot.sound

thiefCase_establishes

Grant that the thief was promised paradise unbaptised, and that his case bears on the Gospel. It follows that the washing itself is not necessary for salvation.

theorem thiefCase_establishes : Establishes thiefCase
-- axioms: propext, Quot.sound

thiefCase_is_satisfiable

The thief's case can be held without contradiction.

theorem thiefCase_is_satisfiable : Satisfiable thiefCase.premises
-- axioms: propext, Quot.sound

desireCase_establishes

Grant Rome's own teaching that the desire brings the fruits of baptism, and the same follows.

theorem desireCase_establishes : Establishes desireCase
-- axioms: propext, Quot.sound

desireCase_is_satisfiable

The desire's case can be held without contradiction.

theorem desireCase_is_satisfiable : Satisfiable desireCase.premises
-- axioms: propext, Quot.sound

reformedOnTheDesire_establishes

The Reformed answer reaches its conclusion, given its step: the sacrament is not the instrument of justification.

theorem reformedOnTheDesire_establishes : Establishes reformedOnTheDesire
-- axioms: propext, Quot.sound

reformedOnTheDesire_is_satisfiable

The Reformed answer can be held without contradiction.

theorem reformedOnTheDesire_is_satisfiable : Satisfiable
    reformedOnTheDesire.premises
-- axioms: propext, Quot.sound

the_thief_does_not_reach_the_desire

The thief does not count against Trent taken in its own words. Trent's instrumental cause, as baptism or the desire for it, can be held with everything the thief's case says: the thief had the desire, and the desire saves.

theorem the_thief_does_not_reach_the_desire : Satisfiable (thiefCase.premises
    ++ trentOnBaptismOrDesire.premises)
-- axioms: propext, Quot.sound

Where each fails

whereTheThiefMeetsFeeney

Why the thief stands against Feeney's reading. Everything turns on the step from the thief: he was promised paradise unbaptised, and his case bears on the Gospel, so the washing itself is not necessary for salvation. What that contradicts is Trent's claim taken Feeney's way, and nothing else.

Why The thief on the cross (Luke 23:43), read with Augustine stands against Trent: baptism the instrumental cause of justification, read so that the washing itself is necessary for salvation.

• The crux: \((\href{claims.html#claim-72}{P_{72}} \land \href{claims.html#claim-73}{P_{73}}) \rightarrow \lnot \href{claims.html#claim-69}{P_{69}}\), a premise of The thief on the cross (Luke 23:43), read with Augustine.
• What it does: its conclusion does not follow without it.
• Granted: \(\href{claims.html#claim-72}{P_{72}}\), \(\href{claims.html#claim-73}{P_{73}}\), which the break also needs.
• Where the rival breaks: \(\href{claims.html#claim-68}{P_{68}}\), \(\href{claims.html#claim-68}{P_{68}} \rightarrow \href{claims.html#claim-69}{P_{69}}\) cannot be held together with \((\href{claims.html#claim-72}{P_{72}} \land \href{claims.html#claim-73}{P_{73}}) \rightarrow \lnot \href{claims.html#claim-69}{P_{69}}\) and \(\href{claims.html#claim-72}{P_{72}}\), \(\href{claims.html#claim-73}{P_{73}}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(\href{claims.html#claim-72}{P_{72}}\) Luke 23:43 — the thief, unbaptised, is promised paradise — consensus: Luke 23:43; Schaff 1887, §On Baptism IV.23.31
  • \(\href{claims.html#claim-73}{P_{73}}\) The thief's case bears on salvation under the Gospel — well supported: Schaff 1887, §On Baptism IV.22.30–23.31; Aquinas 1920, §III q.66 a.11
  • the step itself — well supported: Schaff 1887, §On Baptism IV.23.31; Aquinas 1920, §III q.66 a.11

whereTheDesireMeetsFeeney

Why Rome's own teaching stands against Feeney's reading. Everything turns on the step from what the desire brings: if the desire brings about the fruits of baptism, the washing itself is not necessary for salvation. Feeney denies the starting point. Whoever accepts it, as the Catechism does, cannot hold his reading.

Why The desire for baptism (Catechism 1258–1259) stands against Trent: baptism the instrumental cause of justification, read so that the washing itself is necessary for salvation.

• The crux: \(\href{claims.html#claim-71}{P_{71}} \rightarrow \lnot \href{claims.html#claim-69}{P_{69}}\), a premise of The desire for baptism (Catechism 1258–1259).
• What it does: its conclusion does not follow without it.
• Granted: \(\href{claims.html#claim-71}{P_{71}}\), which the break also needs.
• Where the rival breaks: \(\href{claims.html#claim-68}{P_{68}}\), \(\href{claims.html#claim-68}{P_{68}} \rightarrow \href{claims.html#claim-69}{P_{69}}\) cannot be held together with \(\href{claims.html#claim-71}{P_{71}} \rightarrow \lnot \href{claims.html#claim-69}{P_{69}}\) and \(\href{claims.html#claim-71}{P_{71}}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(\href{claims.html#claim-71}{P_{71}}\) The desire for baptism brings about its fruits without being a sacrament — consensus: Catholic Church 2000, §1258; Aquinas 1920, §III q.69 a.4 ad 2
  • the step itself — well supported: Catholic Church 2000, §1259

whereTheDesireMeetsTrent

Why the Reformed answer stands against Trent taken in its own words. Everything turns on the step from the desire: where the desire alone brings the fruits, what justifies is not the washing, so the washing is not the instrument. What that contradicts is the instrumental cause itself. The step is rated disputed: Aquinas accepts that the desire brings grace, and holds that it does so as a desire for the sacrament, which then gives a fuller grace.

Why What justifies where only the desire is present stands against Trent: baptism the instrumental cause of justification, read as baptism or the desire of it.

• The crux: \((\href{claims.html#claim-70}{P_{70}} \land \href{claims.html#claim-71}{P_{71}}) \rightarrow \lnot \href{claims.html#claim-68}{P_{68}}\), a premise of What justifies where only the desire is present.
• What it does: its conclusion does not follow without it.
• Granted: \(\href{claims.html#claim-70}{P_{70}}\), \(\href{claims.html#claim-71}{P_{71}}\), which the break also needs.
• Where the rival breaks: \(\href{claims.html#claim-68}{P_{68}}\) cannot be held together with \((\href{claims.html#claim-70}{P_{70}} \land \href{claims.html#claim-71}{P_{71}}) \rightarrow \lnot \href{claims.html#claim-68}{P_{68}}\) and \(\href{claims.html#claim-70}{P_{70}}\), \(\href{claims.html#claim-71}{P_{71}}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(\href{claims.html#claim-70}{P_{70}}\) Justification cannot be effected without the laver of regeneration, or the desire thereof — consensus: Council of Trent 1848, p. 32; Aquinas 1920, §III q.68 a.2
  • \(\href{claims.html#claim-71}{P_{71}}\) The desire for baptism brings about its fruits without being a sacrament — consensus: Catholic Church 2000, §1258; Aquinas 1920, §III q.69 a.4 ad 2
  • the step itself — disputed: Westminster Assembly 1647, §XXVIII.5; Westminster Assembly 1647, §XI.2; disputed: Aquinas 1920, §III q.69 a.4 ad 2

whatTrentsInstrumentalCauseClaims

What Trent's instrumental cause claims, taken both ways.

Taken so that the washing itself is necessary for salvation, Feeney's reading, it cannot be held with the thief as Augustine reads him, nor with Rome's own teaching that the desire brings the fruits of baptism. Each fails at a step rated wellSupported. Both answers are Catholic ones.

Taken in Trent's own words, baptism or the desire for it, the thief does not count against it. It cannot be held with the Reformed answer, that where only the desire is present what justifies is not the washing. But that step is disputed, by Aquinas.

Each way of taking it is fair. By itself it contradicts nothing, so it is not a position invented to be knocked down. It fails only when joined to what the positions set against it hold.

Every reading of \(\href{claims.html#claim-68}{P_{68}}\), answered. Trent: baptism the instrumental cause of justification holds \(\href{claims.html#claim-68}{P_{68}}\). It is read 2 ways here, and each reading is checked; none can be left out.

1. Read so that the washing itself is necessary for salvation. The claim commits Trent: baptism the instrumental cause of justification to \(\href{claims.html#claim-69}{P_{69}}\) — so read by Feeney 1952 (disputed).

Against The thief on the cross (Luke 23:43), read with Augustine, it cannot be held. Where it breaks:

Why The thief on the cross (Luke 23:43), read with Augustine stands against Trent: baptism the instrumental cause of justification, read so that the washing itself is necessary for salvation.

• The crux: \((\href{claims.html#claim-72}{P_{72}} \land \href{claims.html#claim-73}{P_{73}}) \rightarrow \lnot \href{claims.html#claim-69}{P_{69}}\), a premise of The thief on the cross (Luke 23:43), read with Augustine.
• What it does: its conclusion does not follow without it.
• Granted: \(\href{claims.html#claim-72}{P_{72}}\), \(\href{claims.html#claim-73}{P_{73}}\), which the break also needs.
• Where the rival breaks: \(\href{claims.html#claim-68}{P_{68}}\), \(\href{claims.html#claim-68}{P_{68}} \rightarrow \href{claims.html#claim-69}{P_{69}}\) cannot be held together with \((\href{claims.html#claim-72}{P_{72}} \land \href{claims.html#claim-73}{P_{73}}) \rightarrow \lnot \href{claims.html#claim-69}{P_{69}}\) and \(\href{claims.html#claim-72}{P_{72}}\), \(\href{claims.html#claim-73}{P_{73}}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(\href{claims.html#claim-72}{P_{72}}\) Luke 23:43 — the thief, unbaptised, is promised paradise — consensus: Luke 23:43; Schaff 1887, §On Baptism IV.23.31
  • \(\href{claims.html#claim-73}{P_{73}}\) The thief's case bears on salvation under the Gospel — well supported: Schaff 1887, §On Baptism IV.22.30–23.31; Aquinas 1920, §III q.66 a.11
  • the step itself — well supported: Schaff 1887, §On Baptism IV.23.31; Aquinas 1920, §III q.66 a.11

Against The desire for baptism (Catechism 1258–1259), it cannot be held. Where it breaks:

Why The desire for baptism (Catechism 1258–1259) stands against Trent: baptism the instrumental cause of justification, read so that the washing itself is necessary for salvation.

• The crux: \(\href{claims.html#claim-71}{P_{71}} \rightarrow \lnot \href{claims.html#claim-69}{P_{69}}\), a premise of The desire for baptism (Catechism 1258–1259).
• What it does: its conclusion does not follow without it.
• Granted: \(\href{claims.html#claim-71}{P_{71}}\), which the break also needs.
• Where the rival breaks: \(\href{claims.html#claim-68}{P_{68}}\), \(\href{claims.html#claim-68}{P_{68}} \rightarrow \href{claims.html#claim-69}{P_{69}}\) cannot be held together with \(\href{claims.html#claim-71}{P_{71}} \rightarrow \lnot \href{claims.html#claim-69}{P_{69}}\) and \(\href{claims.html#claim-71}{P_{71}}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(\href{claims.html#claim-71}{P_{71}}\) The desire for baptism brings about its fruits without being a sacrament — consensus: Catholic Church 2000, §1258; Aquinas 1920, §III q.69 a.4 ad 2
  • the step itself — well supported: Catholic Church 2000, §1259

2. Read as baptism or the desire of it. The claim commits Trent: baptism the instrumental cause of justification to \(\href{claims.html#claim-70}{P_{70}}\) — so read by Council of Trent 1848, p. 32 (consensus).

Against The thief on the cross (Luke 23:43), read with Augustine, it is not reached: The thief on the cross (Luke 23:43), read with Augustine holds, and can be held together with it.

Against What justifies where only the desire is present, it cannot be held. Where it breaks:

Why What justifies where only the desire is present stands against Trent: baptism the instrumental cause of justification, read as baptism or the desire of it.

• The crux: \((\href{claims.html#claim-70}{P_{70}} \land \href{claims.html#claim-71}{P_{71}}) \rightarrow \lnot \href{claims.html#claim-68}{P_{68}}\), a premise of What justifies where only the desire is present.
• What it does: its conclusion does not follow without it.
• Granted: \(\href{claims.html#claim-70}{P_{70}}\), \(\href{claims.html#claim-71}{P_{71}}\), which the break also needs.
• Where the rival breaks: \(\href{claims.html#claim-68}{P_{68}}\) cannot be held together with \((\href{claims.html#claim-70}{P_{70}} \land \href{claims.html#claim-71}{P_{71}}) \rightarrow \lnot \href{claims.html#claim-68}{P_{68}}\) and \(\href{claims.html#claim-70}{P_{70}}\), \(\href{claims.html#claim-71}{P_{71}}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(\href{claims.html#claim-70}{P_{70}}\) Justification cannot be effected without the laver of regeneration, or the desire thereof — consensus: Council of Trent 1848, p. 32; Aquinas 1920, §III q.68 a.2
  • \(\href{claims.html#claim-71}{P_{71}}\) The desire for baptism brings about its fruits without being a sacrament — consensus: Catholic Church 2000, §1258; Aquinas 1920, §III q.69 a.4 ad 2
  • the step itself — disputed: Westminster Assembly 1647, §XXVIII.5; Westminster Assembly 1647, §XI.2; disputed: Aquinas 1920, §III q.69 a.4 ad 2

John 3:5

johnThreeFiveToWater

Trent's step from John 3:5: the verse requires water baptism. Rated disputed: Calvin accepts the verse and denies the step.

trentOnJohnThreeFive — Trent on John 3:5: born of water, so water baptism required

Trent on John 3:5: born of water and the Spirit, so the verse requires water baptism for entry into the kingdom.

No premise here rests on scripture alone.

waterReadAsBaptism

Who reads the water of John 3:5 as baptismal water: Trent (Session VII, On Baptism, canon 2), and "Chrysostom, with whom the greater part of expounders agree", as Calvin reports.

def waterReadAsBaptism : Source :=
  { primary := Reference.work waterworthTrent (Bib.Locus.page 56),
    supporting := [Reference.work calvinJohn (Bib.Locus.page 110)],
    tradition := Tradition.romanCatholic, confidence := Confidence.disputed }

waterReadAsBirth

Who reads it as natural birth: Oliver, who argues for it as his own reading. The water "could be a reference to the amniotic fluid that surrounds the baby in the womb".

def waterReadAsBirth : Source :=
  { primary := Reference.work oliverWaterJohn,
    tradition := Tradition.criticalScholarship,
    confidence := Confidence.disputed }

waterReadAsEzekiel

Who reads it as the cleansing of Ezekiel 36: Carson, who finds there "a transformative new beginning, characterized by spectacular cleansing symbolized by water".

def waterReadAsEzekiel : Source :=
  { primary := Reference.work carsonBornOfWater,
    supporting := [Reference.work oliverWaterJohn],
    tradition := Tradition.christianHistoricalGrammatical,
    confidence := Confidence.disputed }

waterReadAsTheSpirit

Who reads it as the Spirit's own cleansing: Calvin, "By 'water and the Spirit,' therefore, I simply understand the Spirit, which is water" (Institutes IV.xvi.25).

def waterReadAsTheSpirit : Source :=
  {
    primary :=
      Reference.work Bib.calvinInstitutes (Bib.Locus.sectionRef "IV.xvi.25"),
    supporting := [Reference.work calvinJohn (Bib.Locus.pages 110 111)],
    tradition := Tradition.reformedProtestant,
    confidence := Confidence.disputed }

waterAsBaptism

The water of John 3:5, read as baptismal water.

def waterAsBaptism : Reading Claim :=
  { name := "with its water as baptismal water",
    commits := p Claim.john3_5WaterIsBaptism,
    source := waterReadAsBaptism }

waterAsBirth

The water of John 3:5, read as natural birth.

def waterAsBirth : Reading Claim :=
  { name := "with its water as natural birth",
    commits := p Claim.john3_5WaterIsNaturalBirth,
    source := waterReadAsBirth }

waterAsEzekiel

The water of John 3:5, read as the cleansing of Ezekiel 36.

def waterAsEzekiel : Reading Claim :=
  { name := "with its water as Ezekiel's cleansing",
    commits := p Claim.john3_5WaterIsEzekielsCleansing,
    source := waterReadAsEzekiel }

waterAsTheSpirit

The water of John 3:5, read as the Spirit's own cleansing.

def waterAsTheSpirit : Reading Claim :=
  { name := "with its water as the Spirit's own cleansing",
    commits := p Claim.john3_5WaterIsTheSpiritsCleansing,
    source := waterReadAsTheSpirit }

birthToNoWater

If the water is natural birth, the verse does not require water baptism.

ezekielToNoWater

If the water is Ezekiel's cleansing and not baptism, the verse does not require water baptism.

spiritToNoWater

If the water is the Spirit's own cleansing, the verse does not require water baptism.

spiritToNotBaptism

And if the water is the Spirit's own cleansing, it is not baptismal water.

birthOnJohnThreeFive — John 3:5, the water as natural birth (Oliver)

The natural-birth reading, as a position: the water is natural birth, so the verse does not require water baptism.

No premise here rests on scripture alone.

ezekielOnJohnThreeFive — John 3:5, the water as Ezekiel's cleansing (Carson)

The Ezekiel reading, as a position.

No premise here rests on scripture alone.

calvinOnJohnThreeFive — John 3:5, the water as the Spirit's own cleansing (Calvin)

Calvin's reading, as a position: water and Spirit are one, so the water is not baptismal water, and the verse does not require water baptism.

No premise here rests on scripture alone.

noWaterInJohnThreeFiveReading

A reading on which all three non-baptismal readings hold at once: the water is natural birth, Ezekiel's cleansing and the Spirit's own cleansing, and not baptism, and the verse does not require water baptism. Nobody holds this, since the three readings are rivals. It is used only to show that each position's premises can be true together.

def noWaterInJohnThreeFiveReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.john3_5RequiresWaterBaptism => False
    | Claim.john3_5WaterIsBaptism => False
    | x => True

trentOnJohnThreeFive_establishes

Grant the verse and Trent's step from it, and the requirement of water baptism follows. The step is disputed.

theorem trentOnJohnThreeFive_establishes : Establishes trentOnJohnThreeFive
-- axioms: propext, Quot.sound

trentOnJohnThreeFive_is_satisfiable

Trent on John 3:5 can be held without contradiction, on Rome's position.

theorem trentOnJohnThreeFive_is_satisfiable : Satisfiable
    trentOnJohnThreeFive.premises
-- axioms: propext, Quot.sound

birthOnJohnThreeFive_establishes

The natural-birth reading reaches its conclusion.

theorem birthOnJohnThreeFive_establishes : Establishes birthOnJohnThreeFive
-- axioms: propext, Quot.sound

birthOnJohnThreeFive_is_satisfiable

The natural-birth reading can be held without contradiction.

theorem birthOnJohnThreeFive_is_satisfiable : Satisfiable
    birthOnJohnThreeFive.premises
-- axioms: propext, Quot.sound

ezekielOnJohnThreeFive_establishes

The Ezekiel reading reaches its conclusion.

theorem ezekielOnJohnThreeFive_establishes : Establishes
    ezekielOnJohnThreeFive
-- axioms: propext, Quot.sound

ezekielOnJohnThreeFive_is_satisfiable

The Ezekiel reading can be held without contradiction.

theorem ezekielOnJohnThreeFive_is_satisfiable : Satisfiable
    ezekielOnJohnThreeFive.premises
-- axioms: propext, Quot.sound

calvinOnJohnThreeFive_establishes

Calvin's reading reaches its conclusion.

theorem calvinOnJohnThreeFive_establishes : Establishes calvinOnJohnThreeFive
-- axioms: propext, Quot.sound

calvinOnJohnThreeFive_is_satisfiable

Calvin's reading can be held without contradiction.

theorem calvinOnJohnThreeFive_is_satisfiable : Satisfiable
    calvinOnJohnThreeFive.premises
-- axioms: propext, Quot.sound

trentWithBaptismalWater — Trent on John 3:5: born of water, so water baptism required, read with its water as baptismal water

Trent on John 3:5, with the water read as baptism.

No premise here rests on scripture alone.

trentWithNaturalBirth — Trent on John 3:5: born of water, so water baptism required, read with its water as natural birth

Trent on John 3:5, with the water read as natural birth.

No premise here rests on scripture alone.

trentWithEzekielsCleansing — Trent on John 3:5: born of water, so water baptism required, read with its water as Ezekiel's cleansing

Trent on John 3:5, with the water read as Ezekiel's cleansing.

No premise here rests on scripture alone.

trentWithTheSpiritsCleansing — Trent on John 3:5: born of water, so water baptism required, read with its water as the Spirit's own cleansing

Trent on John 3:5, with the water read as the Spirit's own cleansing.

No premise here rests on scripture alone.

trentReadingOfJohnThreeFive

The verse read Trent's way and no other: its water is baptismal water, and not natural birth, Ezekiel's cleansing or the Spirit's own cleansing.

def trentReadingOfJohnThreeFive : Valuation Claim :=
  fun a =>
    match a with
    | Claim.john3_5WaterIsNaturalBirth => False
    | Claim.john3_5WaterIsEzekielsCleansing => False
    | Claim.john3_5WaterIsTheSpiritsCleansing => False
    | x => True

trentWithBirthReading

The verse read with its water as natural birth, and Trent's step kept. By itself this contradicts nothing. It fails only when that reading's own step is added: then the verse does not require water baptism.

def trentWithBirthReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.john3_5WaterIsEzekielsCleansing => False
    | Claim.john3_5WaterIsTheSpiritsCleansing => False
    | x => True

trentWithEzekielReading

Trent's step, with the water read as Ezekiel's cleansing.

def trentWithEzekielReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.john3_5WaterIsNaturalBirth => False
    | Claim.john3_5WaterIsTheSpiritsCleansing => False
    | x => True

trentWithSpiritReading

Trent's step, with the water read as the Spirit's own cleansing.

def trentWithSpiritReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.john3_5WaterIsNaturalBirth => False
    | Claim.john3_5WaterIsEzekielsCleansing => False
    | x => True

trentWithBaptismalWater_is_satisfiable

The baptismal reading of Trent's step can be held without contradiction.

theorem trentWithBaptismalWater_is_satisfiable : Satisfiable
    trentWithBaptismalWater.premises
-- axioms: propext, Quot.sound

trentWithNaturalBirth_is_satisfiable

The natural-birth reading of Trent's step can be held without contradiction.

theorem trentWithNaturalBirth_is_satisfiable : Satisfiable
    trentWithNaturalBirth.premises
-- axioms: propext, Quot.sound

trentWithEzekielsCleansing_is_satisfiable

The Ezekiel reading of Trent's step can be held without contradiction.

theorem trentWithEzekielsCleansing_is_satisfiable : Satisfiable
    trentWithEzekielsCleansing.premises
-- axioms: propext, Quot.sound

trentWithTheSpiritsCleansing_is_satisfiable

The Spirit's-cleansing reading of Trent's step can be held without contradiction.

theorem trentWithTheSpiritsCleansing_is_satisfiable : Satisfiable
    trentWithTheSpiritsCleansing.premises
-- axioms: propext, Quot.sound

whereCalvinMeetsTheBaptismalReading

Why Calvin's reading stands against Trent with the water read as baptism. Everything turns on Calvin's step: if water and Spirit are one thing, the water is not baptismal water. What that contradicts is the baptismal reading itself. The step is wellSupported. But Calvin's reading, which it starts from, is disputed, and Trent condemns it (Session VII, On Baptism, canon 2).

Why John 3:5, the water as the Spirit's own cleansing (Calvin) stands against Trent on John 3:5: born of water, so water baptism required, read with its water as baptismal water.

• The crux: \((\href{claims.html#claim-77}{P_{77}} \land \href{claims.html#claim-82}{P_{82}}) \rightarrow \lnot \href{claims.html#claim-79}{P_{79}}\), a premise of John 3:5, the water as the Spirit's own cleansing (Calvin).
• What it does: its conclusion follows without it — the crux is its answer to Trent on John 3:5: born of water, so water baptism required, read with its water as baptismal water.
• Granted: \(\href{claims.html#claim-77}{P_{77}}\), \(\href{claims.html#claim-82}{P_{82}}\), which the break also needs.
• Where the rival breaks: \(\href{claims.html#claim-77}{P_{77}} \rightarrow \href{claims.html#claim-79}{P_{79}}\) cannot be held together with \((\href{claims.html#claim-77}{P_{77}} \land \href{claims.html#claim-82}{P_{82}}) \rightarrow \lnot \href{claims.html#claim-79}{P_{79}}\) and \(\href{claims.html#claim-77}{P_{77}}\), \(\href{claims.html#claim-82}{P_{82}}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(\href{claims.html#claim-77}{P_{77}}\) John 3:5 — unless one is born of water and the Spirit, he cannot enter the kingdom — consensus: John 3:5; Oliver 2022
  • \(\href{claims.html#claim-82}{P_{82}}\) The water of John 3:5 is the Spirit's own cleansing: water and Spirit are one — disputed: Calvin 1847, pp. 110–111; Calvin 1960, §IV.xvi.25
  • the step itself — well supported: Oliver 2022; Calvin 1960, §IV.xvi.25

whereBirthMeetsTrentsStep

Why the natural-birth reading cannot keep Trent's step. If the water is natural birth, the verse does not require water baptism. So Trent's step from the verse, with the verse read that way, fails, at a step rated wellSupported.

Why John 3:5, the water as natural birth (Oliver) stands against Trent on John 3:5: born of water, so water baptism required, read with its water as natural birth.

• The crux: \(\href{claims.html#claim-80}{P_{80}} \rightarrow \lnot \href{claims.html#claim-78}{P_{78}}\), a premise of John 3:5, the water as natural birth (Oliver).

• What it does: its conclusion does not follow without it.

• Where the rival breaks: \(\href{claims.html#claim-77}{P_{77}}\), \(\href{claims.html#claim-77}{P_{77}} \rightarrow \href{claims.html#claim-78}{P_{78}}\), \(\href{claims.html#claim-77}{P_{77}} \rightarrow \href{claims.html#claim-80}{P_{80}}\) cannot be held together with \(\href{claims.html#claim-80}{P_{80}} \rightarrow \lnot \href{claims.html#claim-78}{P_{78}}\); each is needed for the break, and without the crux they stand.

• What this rests on:

  • the step itself — well supported: Oliver 2022; Calvin 1960, §IV.xvi.25

whereEzekielMeetsTrentsStep

Why the Ezekiel reading cannot keep Trent's step. If the water is Ezekiel's cleansing and not baptism, the verse does not require water baptism.

Why John 3:5, the water as Ezekiel's cleansing (Carson) stands against Trent on John 3:5: born of water, so water baptism required, read with its water as Ezekiel's cleansing.

• The crux: \(\href{claims.html#claim-81}{P_{81}} \rightarrow \lnot \href{claims.html#claim-78}{P_{78}}\), a premise of John 3:5, the water as Ezekiel's cleansing (Carson).

• What it does: its conclusion does not follow without it.

• Where the rival breaks: \(\href{claims.html#claim-77}{P_{77}}\), \(\href{claims.html#claim-77}{P_{77}} \rightarrow \href{claims.html#claim-78}{P_{78}}\), \(\href{claims.html#claim-77}{P_{77}} \rightarrow \href{claims.html#claim-81}{P_{81}}\) cannot be held together with \(\href{claims.html#claim-81}{P_{81}} \rightarrow \lnot \href{claims.html#claim-78}{P_{78}}\); each is needed for the break, and without the crux they stand.

• What this rests on:

  • the step itself — well supported: Oliver 2022; Calvin 1960, §IV.xvi.25

whereTheSpiritMeetsTrentsStep

Why Calvin's reading cannot keep Trent's step. If the water is the Spirit's own cleansing, the verse does not require water baptism.

Why John 3:5, the water as the Spirit's own cleansing (Calvin) stands against Trent on John 3:5: born of water, so water baptism required, read with its water as the Spirit's own cleansing.

• The crux: \(\href{claims.html#claim-82}{P_{82}} \rightarrow \lnot \href{claims.html#claim-78}{P_{78}}\), a premise of John 3:5, the water as the Spirit's own cleansing (Calvin).

• What it does: its conclusion does not follow without it.

• Where the rival breaks: \(\href{claims.html#claim-77}{P_{77}}\), \(\href{claims.html#claim-77}{P_{77}} \rightarrow \href{claims.html#claim-78}{P_{78}}\), \(\href{claims.html#claim-77}{P_{77}} \rightarrow \href{claims.html#claim-82}{P_{82}}\) cannot be held together with \(\href{claims.html#claim-82}{P_{82}} \rightarrow \lnot \href{claims.html#claim-78}{P_{78}}\); each is needed for the break, and without the crux they stand.

• What this rests on:

  • the step itself — well supported: Oliver 2022; Calvin 1960, §IV.xvi.25

whatJohnThreeFiveMeans

What John 3:5 means, read four ways. What can be taken more than one way is the verse Trent cites, not Trent. Trent argues: unless one is born of water and the Spirit, he cannot enter the kingdom of God; therefore water baptism is required. Each of the four readings is a reading of the verse's "water", held by the reader named. For each, the question is whether Trent's step from the verse still stands once the verse is read that way.

Read with its water as baptismal water, Trent's step stands. That reading cannot be held with Calvin's, at a wellSupported step from Calvin's reading, which is itself disputed. Even so, Trent's step stays disputed.

Read with its water as natural birth, as Ezekiel's cleansing, or as the Spirit's own cleansing, Trent's step cannot be kept, each time at a wellSupported step.

So only the baptismal reading leaves Trent's step standing. Which reading is right is not decided here: each is cited, and each is disputed. Each is fair. By itself it contradicts nothing, and it fails only when joined to the step its own holders draw from it.

Every reading of \(\href{claims.html#claim-77}{P_{77}}\), answered. Trent on John 3:5: born of water, so water baptism required holds \(\href{claims.html#claim-77}{P_{77}}\). It is read 4 ways here, and each reading is checked; none can be left out.

1. Read with its water as baptismal water. The claim commits Trent on John 3:5: born of water, so water baptism required to \(\href{claims.html#claim-79}{P_{79}}\) — so read by Council of Trent 1848, p. 56; Calvin 1847, p. 110 (disputed).

Against John 3:5, the water as the Spirit's own cleansing (Calvin), it cannot be held. Where it breaks:

Why John 3:5, the water as the Spirit's own cleansing (Calvin) stands against Trent on John 3:5: born of water, so water baptism required, read with its water as baptismal water.

• The crux: \((\href{claims.html#claim-77}{P_{77}} \land \href{claims.html#claim-82}{P_{82}}) \rightarrow \lnot \href{claims.html#claim-79}{P_{79}}\), a premise of John 3:5, the water as the Spirit's own cleansing (Calvin).
• What it does: its conclusion follows without it — the crux is its answer to Trent on John 3:5: born of water, so water baptism required, read with its water as baptismal water.
• Granted: \(\href{claims.html#claim-77}{P_{77}}\), \(\href{claims.html#claim-82}{P_{82}}\), which the break also needs.
• Where the rival breaks: \(\href{claims.html#claim-77}{P_{77}} \rightarrow \href{claims.html#claim-79}{P_{79}}\) cannot be held together with \((\href{claims.html#claim-77}{P_{77}} \land \href{claims.html#claim-82}{P_{82}}) \rightarrow \lnot \href{claims.html#claim-79}{P_{79}}\) and \(\href{claims.html#claim-77}{P_{77}}\), \(\href{claims.html#claim-82}{P_{82}}\); each is needed for the break, and without the crux they stand.
• What this rests on:
  • \(\href{claims.html#claim-77}{P_{77}}\) John 3:5 — unless one is born of water and the Spirit, he cannot enter the kingdom — consensus: John 3:5; Oliver 2022
  • \(\href{claims.html#claim-82}{P_{82}}\) The water of John 3:5 is the Spirit's own cleansing: water and Spirit are one — disputed: Calvin 1847, pp. 110–111; Calvin 1960, §IV.xvi.25
  • the step itself — well supported: Oliver 2022; Calvin 1960, §IV.xvi.25

2. Read with its water as natural birth. The claim commits Trent on John 3:5: born of water, so water baptism required to \(\href{claims.html#claim-80}{P_{80}}\) — so read by Oliver 2022 (disputed).

Against John 3:5, the water as natural birth (Oliver), it cannot be held. Where it breaks:

Why John 3:5, the water as natural birth (Oliver) stands against Trent on John 3:5: born of water, so water baptism required, read with its water as natural birth.

• The crux: \(\href{claims.html#claim-80}{P_{80}} \rightarrow \lnot \href{claims.html#claim-78}{P_{78}}\), a premise of John 3:5, the water as natural birth (Oliver).

• What it does: its conclusion does not follow without it.

• Where the rival breaks: \(\href{claims.html#claim-77}{P_{77}}\), \(\href{claims.html#claim-77}{P_{77}} \rightarrow \href{claims.html#claim-78}{P_{78}}\), \(\href{claims.html#claim-77}{P_{77}} \rightarrow \href{claims.html#claim-80}{P_{80}}\) cannot be held together with \(\href{claims.html#claim-80}{P_{80}} \rightarrow \lnot \href{claims.html#claim-78}{P_{78}}\); each is needed for the break, and without the crux they stand.

• What this rests on:

  • the step itself — well supported: Oliver 2022; Calvin 1960, §IV.xvi.25

3. Read with its water as Ezekiel's cleansing. The claim commits Trent on John 3:5: born of water, so water baptism required to \(\href{claims.html#claim-81}{P_{81}}\) — so read by Carson 2019; Oliver 2022 (disputed).

Against John 3:5, the water as Ezekiel's cleansing (Carson), it cannot be held. Where it breaks:

Why John 3:5, the water as Ezekiel's cleansing (Carson) stands against Trent on John 3:5: born of water, so water baptism required, read with its water as Ezekiel's cleansing.

• The crux: \(\href{claims.html#claim-81}{P_{81}} \rightarrow \lnot \href{claims.html#claim-78}{P_{78}}\), a premise of John 3:5, the water as Ezekiel's cleansing (Carson).

• What it does: its conclusion does not follow without it.

• Where the rival breaks: \(\href{claims.html#claim-77}{P_{77}}\), \(\href{claims.html#claim-77}{P_{77}} \rightarrow \href{claims.html#claim-78}{P_{78}}\), \(\href{claims.html#claim-77}{P_{77}} \rightarrow \href{claims.html#claim-81}{P_{81}}\) cannot be held together with \(\href{claims.html#claim-81}{P_{81}} \rightarrow \lnot \href{claims.html#claim-78}{P_{78}}\); each is needed for the break, and without the crux they stand.

• What this rests on:

  • the step itself — well supported: Oliver 2022; Calvin 1960, §IV.xvi.25

4. Read with its water as the Spirit's own cleansing. The claim commits Trent on John 3:5: born of water, so water baptism required to \(\href{claims.html#claim-82}{P_{82}}\) — so read by Calvin 1960, §IV.xvi.25; Calvin 1847, pp. 110–111 (disputed).

Against John 3:5, the water as the Spirit's own cleansing (Calvin), it cannot be held. Where it breaks:

Why John 3:5, the water as the Spirit's own cleansing (Calvin) stands against Trent on John 3:5: born of water, so water baptism required, read with its water as the Spirit's own cleansing.

• The crux: \(\href{claims.html#claim-82}{P_{82}} \rightarrow \lnot \href{claims.html#claim-78}{P_{78}}\), a premise of John 3:5, the water as the Spirit's own cleansing (Calvin).

• What it does: its conclusion does not follow without it.

• Where the rival breaks: \(\href{claims.html#claim-77}{P_{77}}\), \(\href{claims.html#claim-77}{P_{77}} \rightarrow \href{claims.html#claim-78}{P_{78}}\), \(\href{claims.html#claim-77}{P_{77}} \rightarrow \href{claims.html#claim-82}{P_{82}}\) cannot be held together with \(\href{claims.html#claim-82}{P_{82}} \rightarrow \lnot \href{claims.html#claim-78}{P_{78}}\); each is needed for the break, and without the crux they stand.

• What this rests on:

  • the step itself — well supported: Oliver 2022; Calvin 1960, §IV.xvi.25

Acts, both orders

actsToUnbound

From Samaria and Caesarea: the Spirit comes after the water and before it, so God is not bound to water baptism. Rated consensus: Calvin and the Catechism both accept that much, though Calvin's own sentence goes further.

actsCase — Acts 8 and 10: the Spirit after the water, and before it

Acts, both orders: the Spirit given after the water in Samaria and before it at Caesarea, so God is not bound to water baptism.

No premise here rests on scripture alone.

actsCase_establishes

Grant the two orders in Acts, and it follows that God is not bound to water.

theorem actsCase_establishes : Establishes actsCase
-- axioms: propext, Quot.sound

actsCase_is_satisfiable

Acts' case can be held without contradiction.

theorem actsCase_is_satisfiable : Satisfiable actsCase.premises
-- axioms: propext, Quot.sound

trent_grants_god_is_not_bound

Trent's instrumental cause is consistent with God not being bound to it. Rome holds both: "God has bound salvation to the sacrament of Baptism, but he himself is not bound by his sacraments" (Catechism 1257). So what Acts shows is accepted on both sides, and is not a point won by the Reformed. What remains in dispute is the first half of that sentence, that God has bound salvation to the sacrament, and Trent's further claim that the sacrament is the instrument of justification.

theorem trent_grants_god_is_not_bound : Grants trentOnBaptism (p
    Claim.godNotBoundToWater)
-- axioms: propext, Quot.sound

"And fire": three readings, and none chosen

fireAsJudgmentReading

A reading on which the fire is judgement, and neither of the other readings holds. This is enough to show that the verse does not require them. Many readers take the fire as both judging and purifying; nothing here says the readings exclude each other.

def fireAsJudgmentReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.fireIsPurification => False
    | Claim.fireIsPentecost => False
    | x => True

fireAsPurificationReading

A reading on which the fire is purification, and neither of the other readings holds. This is enough to show that the verse does not require them.

def fireAsPurificationReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.fireIsJudgment => False
    | Claim.fireIsPentecost => False
    | x => True

the_baptist_leaves_the_fire_open

John the Baptist's words leave open whether the fire is judgement. "He will baptize you with the Holy Spirit and fire" is kept alike by Gregory Nazianzen, who reads the fire as the burning of the chaff, and by Calvin, who reads it as the Spirit's purifying. The text does not settle it either way.

theorem the_baptist_leaves_the_fire_open : Independent [p
    Claim.matthew3_11SpiritAndFire] (p Claim.fireIsJudgment)
-- axioms: propext, Quot.sound

the_baptist_leaves_purification_open

Nor whether it is purification.

theorem the_baptist_leaves_purification_open : Independent [p
    Claim.matthew3_11SpiritAndFire] (p Claim.fireIsPurification)
-- axioms: propext, Quot.sound

the_baptist_leaves_pentecost_open

Nor whether it is Pentecost, as Cyril of Jerusalem reads it: "because the descent of the Holy Ghost was in fiery tongues".

theorem the_baptist_leaves_pentecost_open : Independent [p
    Claim.matthew3_11SpiritAndFire] (p Claim.fireIsPentecost)
-- axioms: propext, Quot.sound