Weighing the positions on the procession

Three positions are parties to one dispute. LST holds only what it says the texts establish: the Spirit is related to the Son as well as to the Father. The West, with Aquinas, Florence and Westminster, holds that he proceeds from the Father and the Son. The East, with Photius and Ware, holds that he proceeds from the Father alone. Who defeats whom is computed from their premises and checked by the kernel.

How to read the verdicts

  • Defeats. One position contradicts another (it denies one of the other's 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. LST's weakest link is wellSupported. Each side rests on readings rated disputed, the lowest rating, so no rating breaks their standoff.
  • Forced. Accepted however every standoff is resolved.
  • Can be defended. Held by some consistent position that answers every attack on its members, by itself or through an ally.

What the weighing found

One standoff, and nothing else. The West and the East defeat each other over "and the Son", and neither attacks LST, because each grants every text LST cites and the relation LST draws from them. So what is forced is exactly LST's position (the_texts_prevail). The West can be defended, and so can the East, and neither is forced (western_defensible, western_not_forced, eastern_defensible, eastern_not_forced).

That is LST's grading of the question, reproduced given these ratings: the relation of the Spirit to the Son is settled, and "the exact eternal relation of the Spirit to the Son beyond what Scripture states is not demonstrated". It does not show that the question is idle, or that the two sides read equally well. It shows only that the weighing cannot choose, because every reading that divides them is rated disputed. A new, cited argument that one side's reading survives what the other side says against it could move a rating, and so the verdict. LST's own rating plays no part: nothing attacks its position, so it would prevail at any rating.

The standoff rests on reading "proceeds" the same way on both sides. The Pontifical Council for Promoting Christian Unity (1995) distinguishes the Greek ἐκπόρευσις, origin from the Father alone, from the Latin processio. On that distinction "and the Son" and "not from the Son" may not contradict each other, and the two defeats would not exist. The chapter on the procession says what testing that would take.

How this is checked

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

The dispute

partyNode

The package each party argues from.

def partyNode : Party → ArgumentPackage Claim :=
  fun x =>
    match x with
    | Party.lst => lstCase
    | Party.western => westernCase
    | Party.eastern => easternCase

processionDispute

The dispute over the procession: every party can be held without contradiction, delivers its conclusion, and has its steps rated.

def processionDispute : Dispute Claim Party :=
  { node := partyNode, consistent := processionDispute._proof_1,
    sound := processionDispute._proof_2,
    rated := processionDispute._proof_6 }

processionDispute_defeats

Who defeats whom, all 9 pairs: one standoff, the West and the East over "and the Son", and nothing else. Neither attacks LST, because each holds every premise LST holds. Every cell is checked by the kernel.

theorem processionDispute_defeats : ∀ (i j : Party), processionDispute.defeats
    i j ↔ (i, j) ∈ [(Party.western, Party.eastern), (Party.eastern,
    Party.western)]
-- axioms: propext, Classical.choice, Quot.sound

processionDispute_supports

Nothing supports anything, in all 9 pairs: no party's conclusion is a premise another party states. LST's relation is derived inside the other two positions, not assumed by them. Every cell is checked by the kernel.

theorem processionDispute_supports : ∀ (i j : Party),
    ¬processionDispute.supports i j
-- axioms: propext, Classical.choice, Quot.sound

processionDispute_partOf

LST's case is part of both the others', since each holds the texts and the step LST draws from them. Otherwise each case is part of its own only. Every cell is checked by the kernel.

theorem processionDispute_partOf : ∀ (i j : Party), processionDispute.partOf i
    j ↔ i = j ∨ (i, j) ∈ [(Party.lst, Party.western), (Party.lst,
    Party.eastern)]
-- axioms: propext, Classical.choice, Quot.sound

processionMap

The dispute over the procession drawn: who defeats whom, and whose case is part of whose.

1 2 3

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

#Party
1The texts: the Spirit sent by the Son and named for him
2From the Father and the Son (Aquinas; Florence; Westminster)
3From the Father alone (Photius; Ware)
FromToEdge
2 From the Father and the Son (Aquinas; Florence; Westminster)3 From the Father alone (Photius; Ware)defeats
3 From the Father alone (Photius; Ware)2 From the Father and the Son (Aquinas; Florence; Westminster)defeats
1 The texts: the Spirit sent by the Son and named for him2 From the Father and the Son (Aquinas; Florence; Westminster)is part of
1 The texts: the Spirit sent by the Son and named for him3 From the Father alone (Photius; Ware)is part of

The defeats are the cells of processionDispute_defeats, the supports the cells of processionDispute_supports and the parts the cells of processionDispute_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.

lst_stands_with_the_west

LST stands with the West: one reading satisfies both, the Western reading.

theorem lst_stands_with_the_west : processionDispute.StandTogether [Party.lst,
    Party.western]
-- axioms: propext, Classical.choice, Quot.sound

lst_stands_with_the_east

LST stands with the East too: the Eastern reading satisfies both. So LST's position takes no side, which is what it says of itself.

theorem lst_stands_with_the_east : processionDispute.StandTogether [Party.lst,
    Party.eastern]
-- axioms: propext, Classical.choice, Quot.sound

What the dispute decides

textsUnanswered

How far the dispute is settled, in one stage. Nothing defeats LST, so it comes first, and nothing joins it: the West has the East for a defeater, the East has the West, and LST answers neither.

What the dispute forces is exactly The texts: the Spirit sent by the Son and named for him.

  • Stage 1: The texts: the Spirit sent by the Son and named for him.
    • The texts: the Spirit sent by the Son and named for him is defeated by nothing.
  • Nothing else is forced:
    • From the Father alone (Photius; Ware) defeats From the Father and the Son (Aquinas; Florence; Westminster), and nothing forced defeats From the Father alone (Photius; Ware).
    • From the Father and the Son (Aquinas; Florence; Westminster) defeats From the Father alone (Photius; Ware), and nothing forced defeats From the Father and the Son (Aquinas; Florence; Westminster).

What this rests on. The reasons state 2 defeats and 5 absences of defeat, each a cell of the defeat table, processionDispute_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:

the_texts_prevail

What the texts establish prevails, and nothing more. What the dispute forces before any choice between rivals is exactly LST's position: the Spirit is related to the Son as well as to the Father. Nothing defeats it, because the West and the East both hold every premise it holds.

What this does not claim: that the Filioque is false, or that it is true. The West and the East are in a standoff, and neither is forced.

theorem the_texts_prevail : Framework.grounded processionDispute.defeats =
    Solver.toSet [Party.lst]
-- axioms: propext, Classical.choice, Quot.sound

westernWithTheTexts

Why the West can be defended: with LST, it answers the East itself.

From the Father and the Son (Aquinas; Florence; Westminster) is accepted on some resolution.

  • A position holding The texts: the Spirit sent by the Son and named for him, From the Father and the Son (Aquinas; Florence; Westminster) can be held.
  • None of The texts: the Spirit sent by the Son and named for him, From the Father and the Son (Aquinas; Florence; Westminster) defeats another, and each attack on them is answered from among them:
    • From the Father alone (Photius; Ware) defeats From the Father and the Son (Aquinas; Florence; Westminster), and From the Father and the Son (Aquinas; Florence; Westminster) defeats From the Father alone (Photius; Ware).

What this rests on. The reasons state 2 defeats and 5 absences of defeat, each a cell of the defeat table, processionDispute_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:

western_defensible

The Western position can be defended, together with LST's: some maximal defensible position, one no other party can join without losing that, holds both.

theorem western_defensible : Framework.CredulouslyAccepted
    processionDispute.defeats Party.western
-- axioms: propext, Classical.choice, Quot.sound

westernAnsweredByTheEast

Why the West is not forced: a defensible position holds the East, and the East defeats the West.

From the Father and the Son (Aquinas; Florence; Westminster) is not accepted on every resolution.

  • A position holding The texts: the Spirit sent by the Son and named for him, From the Father alone (Photius; Ware) can be held, and it holds From the Father alone (Photius; Ware); From the Father alone (Photius; Ware) conflicts with From the Father and the Son (Aquinas; Florence; Westminster): From the Father alone (Photius; Ware) defeats From the Father and the Son (Aquinas; Florence; Westminster), and From the Father and the Son (Aquinas; Florence; Westminster) defeats From the Father alone (Photius; Ware).
  • None of The texts: the Spirit sent by the Son and named for him, From the Father alone (Photius; Ware) defeats another, and each attack on them is answered from among them:
    • From the Father and the Son (Aquinas; Florence; Westminster) defeats From the Father alone (Photius; Ware), and From the Father alone (Photius; Ware) defeats From the Father and the Son (Aquinas; Florence; Westminster).

What this rests on. The reasons state 2 defeats and 5 absences of defeat, each a cell of the defeat table, processionDispute_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:

western_not_forced

Nor is it forced. A maximal defensible position holds LST's position and the East's, and cannot hold the West's with them.

theorem western_not_forced : ¬Framework.SkepticallyAccepted
    processionDispute.defeats Party.western
-- axioms: propext, Classical.choice, Quot.sound

easternWithTheTexts

Why the East can be defended: with LST, it answers the West itself.

From the Father alone (Photius; Ware) is accepted on some resolution.

  • A position holding The texts: the Spirit sent by the Son and named for him, From the Father alone (Photius; Ware) can be held.
  • None of The texts: the Spirit sent by the Son and named for him, From the Father alone (Photius; Ware) defeats another, and each attack on them is answered from among them:
    • From the Father and the Son (Aquinas; Florence; Westminster) defeats From the Father alone (Photius; Ware), and From the Father alone (Photius; Ware) defeats From the Father and the Son (Aquinas; Florence; Westminster).

What this rests on. The reasons state 2 defeats and 5 absences of defeat, each a cell of the defeat table, processionDispute_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:

eastern_defensible

The Eastern position can be defended, together with LST's.

theorem eastern_defensible : Framework.CredulouslyAccepted
    processionDispute.defeats Party.eastern
-- axioms: propext, Classical.choice, Quot.sound

easternAnsweredByTheWest

Why the East is not forced: a defensible position holds the West, and the West defeats the East.

From the Father alone (Photius; Ware) is not accepted on every resolution.

  • A position holding The texts: the Spirit sent by the Son and named for him, From the Father and the Son (Aquinas; Florence; Westminster) can be held, and it holds From the Father and the Son (Aquinas; Florence; Westminster); From the Father and the Son (Aquinas; Florence; Westminster) conflicts with From the Father alone (Photius; Ware): From the Father and the Son (Aquinas; Florence; Westminster) defeats From the Father alone (Photius; Ware), and From the Father alone (Photius; Ware) defeats From the Father and the Son (Aquinas; Florence; Westminster).
  • None of The texts: the Spirit sent by the Son and named for him, From the Father and the Son (Aquinas; Florence; Westminster) defeats another, and each attack on them is answered from among them:
    • From the Father alone (Photius; Ware) defeats From the Father and the Son (Aquinas; Florence; Westminster), and From the Father and the Son (Aquinas; Florence; Westminster) defeats From the Father alone (Photius; Ware).

What this rests on. The reasons state 2 defeats and 5 absences of defeat, each a cell of the defeat table, processionDispute_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:

eastern_not_forced

Nor is it forced. A maximal defensible position holds LST's position and the West's, and cannot hold the East's with them.

theorem eastern_not_forced : ¬Framework.SkepticallyAccepted
    processionDispute.defeats Party.eastern
-- axioms: propext, Classical.choice, Quot.sound