Weighing the four views

The four views as parties to one dispute: at conversion; after it, as the Pentecostals hold; after it, as the holiness tradition holds; and in baptism and confirmation, as Rome holds. The Pentecostal and holiness views are the subsequence views: both hold a second baptism in the Spirit, after conversion, to be sought. Who defeats whom is computed from their premises and checked by the kernel.

How to read the verdicts

  • Defeats. One position contradicts another — denies one of its premises, its conclusion, or a claim it derives on the way — and is not the weaker of the two. A defeat that runs both ways is a standoff.
  • Weakest link. A position is only as strong as its least-supported premise or step. Every party here rests on something rated disputed, the lowest rating, so no rating breaks a standoff.
  • Forced. Accepted however every standoff is resolved.
  • Can be defended. Held by some consistent position that answers every attack on its members, itself or through an ally.
  • Not forced. Some consistent position leaves it out — which is not the same as false.

What the weighing found

Four standoffs, and nothing else. The conversion view stands off against both subsequence views, and so does the sacramental view; the two subsequence views do not attack each other, and neither do the conversion and sacramental views. Nothing is forced (spirit_baptism_forces_nothing). Every view can be defended (conversion_defensible, pentecostal_defensible, holiness_defensible, sacramental_defensible), in one of two camps, and no position holds views from both: the conversion and sacramental views together, and the Pentecostal and holiness views together.

That is where the question stands in the literature, and the page says so rather than choosing. The conversion and sacramental views agree that there is no second baptism in the Spirit to seek, and differ over the rite, which this dispute does not weigh. What would decide between the two camps is argued, not weighed: what Luke's narratives are (pentecostal_cannot_read_acts_as_transitions says the Pentecostal view must read them as a pattern), and whether Paul's word at 1 Corinthians 12:13 and Luke's are the same baptism — a question not yet encoded.

How this is checked

The positions, steps and results behind this chapter, each with the formula or the Lean that checks it

The dispute

viewNode

The package each view argues from.

def viewNode : View → ArgumentPackage Claim :=
  fun x =>
    match x with
    | View.conversion => conversionCase
    | View.pentecostal => pentecostalCase
    | View.holiness => holinessCase
    | View.sacramental => sacramentalCase

spiritBaptismDispute

The dispute over Spirit baptism: every view can be held without contradiction, delivers its conclusion, and has its steps rated.

def spiritBaptismDispute : Dispute Claim View :=
  { node := viewNode,
    consistent := spiritBaptismDispute._proof_1,
    sound := spiritBaptismDispute._proof_2,
    rated := spiritBaptismDispute._proof_7 }

spiritBaptismDispute_defeats

Who defeats whom, all 16 pairs: four standoffs, and nothing else. The conversion view and each subsequence view defeat each other — "no second to seek" against "a second to seek" — and the Pentecostal view also denies the conversion reading of 1 Corinthians 12:13. The sacramental view and each subsequence view defeat each other on the same point. Every cell is checked by the kernel.

theorem spiritBaptismDispute_defeats : ∀ (i j : View),
    spiritBaptismDispute.defeats i j ↔ (i, j) ∈ [(View.conversion,
    View.pentecostal), (View.conversion, View.holiness), (View.pentecostal,
    View.conversion), (View.pentecostal, View.sacramental), (View.holiness,
    View.conversion), (View.holiness, View.sacramental), (View.sacramental,
    View.pentecostal), (View.sacramental, View.holiness)]
-- axioms: propext, Classical.choice, Quot.sound

spiritBaptismDispute_supports

Nothing supports anything, in all 16 pairs. Every cell is checked by the kernel.

theorem spiritBaptismDispute_supports : ∀ (i j : View),
    ¬spiritBaptismDispute.supports i j
-- axioms: propext, Classical.choice, Quot.sound

spiritBaptismDispute_partOf

Each view's case is part of its own and of no other's. Every cell is checked by the kernel.

theorem spiritBaptismDispute_partOf : ∀ (i j : View),
    spiritBaptismDispute.partOf i j ↔ i = j ∨ (i, j) ∈ []
-- axioms: propext, Classical.choice, Quot.sound

spiritBaptismMap

The dispute over Spirit baptism drawn: who defeats whom.

1 2 3 4

Solid red: defeats. Dashed green: supports. Dotted blue: one party's case is part of another's.

#Party
1At conversion (Dunn, Stott)
2After conversion (Assemblies of God; Menzies, Stronstad)
3A second work of grace (the holiness tradition)
4In baptism and confirmation (Catholic)
FromToEdge
1 At conversion (Dunn, Stott)2 After conversion (Assemblies of God; Menzies, Stronstad)defeats
1 At conversion (Dunn, Stott)3 A second work of grace (the holiness tradition)defeats
2 After conversion (Assemblies of God; Menzies, Stronstad)1 At conversion (Dunn, Stott)defeats
2 After conversion (Assemblies of God; Menzies, Stronstad)4 In baptism and confirmation (Catholic)defeats
3 A second work of grace (the holiness tradition)1 At conversion (Dunn, Stott)defeats
3 A second work of grace (the holiness tradition)4 In baptism and confirmation (Catholic)defeats
4 In baptism and confirmation (Catholic)2 After conversion (Assemblies of God; Menzies, Stronstad)defeats
4 In baptism and confirmation (Catholic)3 A second work of grace (the holiness tradition)defeats

The defeats are the cells of spiritBaptismDispute_defeats, the supports the cells of spiritBaptismDispute_supports and the parts the cells of spiritBaptismDispute_partOf, each computed from the parties' premises and checked by the kernel. The attacks derived through support and through parts are reported, not counted: every verdict is computed from the defeats alone. Every derived attack is already a defeat.

conversion_stands_with_the_sacraments

The conversion and sacramental views can be held together: one reading satisfies both — every believer baptized in the Spirit at conversion, the Spirit given in the sacraments, and no second baptism to seek.

It does not show that the two agree. They differ over what the rite does, which this dispute does not weigh, and the result says only that nothing encoded here makes them contradict each other.

theorem conversion_stands_with_the_sacraments :
    spiritBaptismDispute.StandTogether [View.conversion, View.sacramental]
-- axioms: propext, Classical.choice, Quot.sound

the_subsequence_views_stand_together

The two subsequence views can be held together: a second baptism to seek, whether read as empowerment or as the second work of grace. Whether it is the same second experience, the encoding does not say.

theorem the_subsequence_views_stand_together :
    spiritBaptismDispute.StandTogether [View.pentecostal, View.holiness]
-- axioms: propext, Classical.choice, Quot.sound

What the dispute decides

spiritBaptismSettlesNothing

Why nothing is forced: every view has a defeater. The conversion view has the Pentecostal, the Pentecostal and holiness views have the conversion view, and the sacramental view has the Pentecostal.

Nothing prevails outright: every party is defeated by another.

  • After conversion (Assemblies of God; Menzies, Stronstad) defeats At conversion (Dunn, Stott).
  • At conversion (Dunn, Stott) defeats After conversion (Assemblies of God; Menzies, Stronstad).
  • At conversion (Dunn, Stott) defeats A second work of grace (the holiness tradition).
  • After conversion (Assemblies of God; Menzies, Stronstad) defeats In baptism and confirmation (Catholic).

What this rests on. The reasons state 4 defeats and 0 absences of defeat, each a cell of the defeat table, spiritBaptismDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

spirit_baptism_forces_nothing

Nothing is forced. Every view is in a standoff the dispute cannot resolve, and every weakest link is disputed, so no rating breaks a tie.

It does not show that the question is idle. Each view can be defended, and what the dispute cannot do is choose between readings rated alike.

theorem spirit_baptism_forces_nothing : Framework.grounded
    spiritBaptismDispute.defeats = ∅
-- axioms: propext, Classical.choice, Quot.sound

conversionStandsWithTheSacraments

Why the conversion view can be defended: it stands with the sacramental view, and answers both subsequence views, itself.

At conversion (Dunn, Stott) is accepted on some resolution.

  • A position holding At conversion (Dunn, Stott), In baptism and confirmation (Catholic) can be held.
  • None of At conversion (Dunn, Stott), In baptism and confirmation (Catholic) defeats another, and each attack on them is answered from among them:
    • After conversion (Assemblies of God; Menzies, Stronstad) defeats At conversion (Dunn, Stott), and At conversion (Dunn, Stott) defeats After conversion (Assemblies of God; Menzies, Stronstad).
    • A second work of grace (the holiness tradition) defeats At conversion (Dunn, Stott), and At conversion (Dunn, Stott) defeats A second work of grace (the holiness tradition).
    • After conversion (Assemblies of God; Menzies, Stronstad) defeats In baptism and confirmation (Catholic), and At conversion (Dunn, Stott) defeats After conversion (Assemblies of God; Menzies, Stronstad).
    • A second work of grace (the holiness tradition) defeats In baptism and confirmation (Catholic), and At conversion (Dunn, Stott) defeats A second work of grace (the holiness tradition).

What this rests on. The reasons state 6 defeats and 4 absences of defeat, each a cell of the defeat table, spiritBaptismDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

conversion_defensible

The conversion view can be defended, with the sacramental view: some maximal defensible position — one no other party can join without losing that — holds both.

theorem conversion_defensible : Framework.CredulouslyAccepted
    spiritBaptismDispute.defeats View.conversion
-- axioms: propext, Classical.choice, Quot.sound

conversionAnsweredByPentecost

Why the conversion view is not forced: a defensible position holds the Pentecostal view, and it defeats the conversion view.

At conversion (Dunn, Stott) is not accepted on every resolution.

  • A position holding After conversion (Assemblies of God; Menzies, Stronstad), A second work of grace (the holiness tradition) can be held, and it holds After conversion (Assemblies of God; Menzies, Stronstad); After conversion (Assemblies of God; Menzies, Stronstad) conflicts with At conversion (Dunn, Stott): After conversion (Assemblies of God; Menzies, Stronstad) defeats At conversion (Dunn, Stott), and At conversion (Dunn, Stott) defeats After conversion (Assemblies of God; Menzies, Stronstad).
  • None of After conversion (Assemblies of God; Menzies, Stronstad), A second work of grace (the holiness tradition) defeats another, and each attack on them is answered from among them:
    • At conversion (Dunn, Stott) defeats After conversion (Assemblies of God; Menzies, Stronstad), and After conversion (Assemblies of God; Menzies, Stronstad) defeats At conversion (Dunn, Stott).
    • In baptism and confirmation (Catholic) defeats After conversion (Assemblies of God; Menzies, Stronstad), and After conversion (Assemblies of God; Menzies, Stronstad) defeats In baptism and confirmation (Catholic).
    • At conversion (Dunn, Stott) defeats A second work of grace (the holiness tradition), and After conversion (Assemblies of God; Menzies, Stronstad) defeats At conversion (Dunn, Stott).
    • In baptism and confirmation (Catholic) defeats A second work of grace (the holiness tradition), and After conversion (Assemblies of God; Menzies, Stronstad) defeats In baptism and confirmation (Catholic).

What this rests on. The reasons state 6 defeats and 4 absences of defeat, each a cell of the defeat table, spiritBaptismDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

conversion_not_forced

Nor is it forced. A maximal defensible position holds the Pentecostal and holiness views, and cannot hold the conversion view with them.

theorem conversion_not_forced : ¬Framework.SkepticallyAccepted
    spiritBaptismDispute.defeats View.conversion
-- axioms: propext, Classical.choice, Quot.sound

pentecostalStandsWithHoliness

Why the Pentecostal view can be defended: it stands with the holiness view, and answers both the conversion and sacramental views itself.

After conversion (Assemblies of God; Menzies, Stronstad) is accepted on some resolution.

  • A position holding After conversion (Assemblies of God; Menzies, Stronstad), A second work of grace (the holiness tradition) can be held.
  • None of After conversion (Assemblies of God; Menzies, Stronstad), A second work of grace (the holiness tradition) defeats another, and each attack on them is answered from among them:
    • At conversion (Dunn, Stott) defeats After conversion (Assemblies of God; Menzies, Stronstad), and After conversion (Assemblies of God; Menzies, Stronstad) defeats At conversion (Dunn, Stott).
    • In baptism and confirmation (Catholic) defeats After conversion (Assemblies of God; Menzies, Stronstad), and After conversion (Assemblies of God; Menzies, Stronstad) defeats In baptism and confirmation (Catholic).
    • At conversion (Dunn, Stott) defeats A second work of grace (the holiness tradition), and After conversion (Assemblies of God; Menzies, Stronstad) defeats At conversion (Dunn, Stott).
    • In baptism and confirmation (Catholic) defeats A second work of grace (the holiness tradition), and After conversion (Assemblies of God; Menzies, Stronstad) defeats In baptism and confirmation (Catholic).

What this rests on. The reasons state 6 defeats and 4 absences of defeat, each a cell of the defeat table, spiritBaptismDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

pentecostal_defensible

The Pentecostal view can be defended, with the holiness view.

theorem pentecostal_defensible : Framework.CredulouslyAccepted
    spiritBaptismDispute.defeats View.pentecostal
-- axioms: propext, Classical.choice, Quot.sound

pentecostalAnsweredByConversion

Why the Pentecostal view is not forced: a defensible position holds the conversion view, and it defeats the Pentecostal view.

After conversion (Assemblies of God; Menzies, Stronstad) is not accepted on every resolution.

  • A position holding At conversion (Dunn, Stott), In baptism and confirmation (Catholic) can be held, and it holds At conversion (Dunn, Stott); At conversion (Dunn, Stott) conflicts with After conversion (Assemblies of God; Menzies, Stronstad): At conversion (Dunn, Stott) defeats After conversion (Assemblies of God; Menzies, Stronstad), and After conversion (Assemblies of God; Menzies, Stronstad) defeats At conversion (Dunn, Stott).
  • None of At conversion (Dunn, Stott), In baptism and confirmation (Catholic) defeats another, and each attack on them is answered from among them:
    • After conversion (Assemblies of God; Menzies, Stronstad) defeats At conversion (Dunn, Stott), and At conversion (Dunn, Stott) defeats After conversion (Assemblies of God; Menzies, Stronstad).
    • A second work of grace (the holiness tradition) defeats At conversion (Dunn, Stott), and At conversion (Dunn, Stott) defeats A second work of grace (the holiness tradition).
    • After conversion (Assemblies of God; Menzies, Stronstad) defeats In baptism and confirmation (Catholic), and At conversion (Dunn, Stott) defeats After conversion (Assemblies of God; Menzies, Stronstad).
    • A second work of grace (the holiness tradition) defeats In baptism and confirmation (Catholic), and At conversion (Dunn, Stott) defeats A second work of grace (the holiness tradition).

What this rests on. The reasons state 6 defeats and 4 absences of defeat, each a cell of the defeat table, spiritBaptismDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

pentecostal_not_forced

Nor is it forced. A maximal defensible position holds the conversion and sacramental views, and cannot hold the Pentecostal view with them. What would decide is argued, not weighed: what the Acts narratives are (pentecostal_cannot_read_acts_as_transitions).

theorem pentecostal_not_forced : ¬Framework.SkepticallyAccepted
    spiritBaptismDispute.defeats View.pentecostal
-- axioms: propext, Classical.choice, Quot.sound

holinessStandsWithPentecost

Why the holiness view can be defended: it stands with the Pentecostal view, which answers the conversion and sacramental views.

A second work of grace (the holiness tradition) is accepted on some resolution.

  • A position holding After conversion (Assemblies of God; Menzies, Stronstad), A second work of grace (the holiness tradition) can be held.
  • None of After conversion (Assemblies of God; Menzies, Stronstad), A second work of grace (the holiness tradition) defeats another, and each attack on them is answered from among them:
    • At conversion (Dunn, Stott) defeats After conversion (Assemblies of God; Menzies, Stronstad), and After conversion (Assemblies of God; Menzies, Stronstad) defeats At conversion (Dunn, Stott).
    • In baptism and confirmation (Catholic) defeats After conversion (Assemblies of God; Menzies, Stronstad), and After conversion (Assemblies of God; Menzies, Stronstad) defeats In baptism and confirmation (Catholic).
    • At conversion (Dunn, Stott) defeats A second work of grace (the holiness tradition), and After conversion (Assemblies of God; Menzies, Stronstad) defeats At conversion (Dunn, Stott).
    • In baptism and confirmation (Catholic) defeats A second work of grace (the holiness tradition), and After conversion (Assemblies of God; Menzies, Stronstad) defeats In baptism and confirmation (Catholic).

What this rests on. The reasons state 6 defeats and 4 absences of defeat, each a cell of the defeat table, spiritBaptismDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

holiness_defensible

The holiness view can be defended, with the Pentecostal view. Not forced, for the same reason the Pentecostal view is not.

theorem holiness_defensible : Framework.CredulouslyAccepted
    spiritBaptismDispute.defeats View.holiness
-- axioms: propext, Classical.choice, Quot.sound

sacramentalStandsWithConversion

Why the sacramental view can be defended: it stands with the conversion view, which answers both subsequence views.

In baptism and confirmation (Catholic) is accepted on some resolution.

  • A position holding At conversion (Dunn, Stott), In baptism and confirmation (Catholic) can be held.
  • None of At conversion (Dunn, Stott), In baptism and confirmation (Catholic) defeats another, and each attack on them is answered from among them:
    • After conversion (Assemblies of God; Menzies, Stronstad) defeats At conversion (Dunn, Stott), and At conversion (Dunn, Stott) defeats After conversion (Assemblies of God; Menzies, Stronstad).
    • A second work of grace (the holiness tradition) defeats At conversion (Dunn, Stott), and At conversion (Dunn, Stott) defeats A second work of grace (the holiness tradition).
    • After conversion (Assemblies of God; Menzies, Stronstad) defeats In baptism and confirmation (Catholic), and At conversion (Dunn, Stott) defeats After conversion (Assemblies of God; Menzies, Stronstad).
    • A second work of grace (the holiness tradition) defeats In baptism and confirmation (Catholic), and At conversion (Dunn, Stott) defeats A second work of grace (the holiness tradition).

What this rests on. The reasons state 6 defeats and 4 absences of defeat, each a cell of the defeat table, spiritBaptismDispute_defeats, computed from the two parties' premises and checked by the kernel. Whether an attack survives turns on the attacker's weakest link and on the rating of what it attacks, so a changed rating can change the verdict. The weakest links:

sacramental_defensible

The sacramental view can be defended, with the conversion view. Not forced, for the same reason the conversion view is not.

theorem sacramental_defensible : Framework.CredulouslyAccepted
    spiritBaptismDispute.defeats View.sacramental
-- axioms: propext, Classical.choice, Quot.sound

What the Pentecostal view can read Acts as

pentecostal_cannot_read_acts_as_transitions

The Pentecostal view cannot read Acts as transitions. Its own premise is that Luke's narratives are a pattern for believers today, and Stott's reading says, in its own words, that they are "not a pattern" (TestimonyArguments.Meanings.SpiritBaptism.joins). So what the view holds, read for what its claims mean, denies the transitions reading outright.

So the Pentecostal view must read the Acts narratives as a pattern, because the other reading is not open to it. It does not show that the pattern reading is right. Read as a pattern, the narratives still meet the variety of Acts (whereTheVarietyMeetsThePattern), at a step the Assemblies of God contest.

Before the two readings were joined by meaning, this was a dilemma with two horns, and the transitions horn broke only at Stott's step from transitions to no norm. Joined, the horn is not there to break: no reader can hold the Pentecostal view and read Acts as transitions.

theorem pentecostal_cannot_read_acts_as_transitions : Entails
    pentecostalCase.held (notP Claim.actsEpisodesAreTransitions)
-- axioms: propext, Quot.sound

stott_undermines_the_pattern

Stott's reading meets the Pentecostal view at its premise. Read for what its claims mean, Acts as transitions denies that the narratives are a pattern, and that is one of the Pentecostal view's premises. Before the join it met the view only at Stott's step, as a reason not to seek a second baptism; now it contradicts what the view rests on. Whether that attack is a defeat is a question of ratings, and this argument's dispute does not seat Stott's reading as a party.

theorem stott_undermines_the_pattern : UnderminesOn transitionCase
    pentecostalCase (p Claim.actsNarrativesAreNormative)
-- axioms: propext, Quot.sound