Introduction
In August 2020 the Maverick Christian YouTube channel featured an interview on the Eternal Society paradox, something I’ve also talked about in article explaining why the past cannot be infinite. Here I’m going to dive into a symbolic logic approach to arguing for the premises of the Eternal Society paradox argument. This article is for logic nerds and less laypersonfriendly than most of my other blog articles.
Defining the Predicates
The domain of discourse are the years of the past.
 Py = the Eternal Society did the chant in a year prior to y.
 Cy = the chant was done in year y.
 Fy = the coin (indeterministic, probabilistically independent) was flipped in year y.
 Hy = the coin came up heads in year y.
 I = the past is infinite and beginningless.
 L = the coin came up heads last year.
 V = the coin came up heads every year.
 D = (I ∧ (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)])
 In English: the past is infinite and for every year y: if a flipped coin came up heads in year y and the society did not do the chant in a prior year, then the society does the chant in year y, otherwise they do not do the chant in year y.
 A = D ∧ ∀y[Fy]
 In English: the Eternal Society engages in the Annual CoinFlipping Tradition.
 E = the Eternal Society (roughly, a society that has existed throughout the infinite, beginningless past and in each year, they can do what we humans can do in contemporary society, e.g. in any year they can flip coins and do chants) obtains.
 S1 = Scenario S1 obtains (A is true and the coin comes up heads for the first time last year).
 S2 = Scenario S2 obtains (A is true and the coin comes up heads each year of the infinite past).
Argument 1: If ◊S1 then ◊S2
Where a possible world is the way the world is or could have been like, the modal operator □ is such that □P means that P is necessarily true (true in all possible worlds), and ◊P means that P is possibly true (true in at least one possible world).
Here is an argument that if Scenario S1 is possible then Scenario S2 is possible. The justification for premise (2) below is that in the Annual CoinFlipping Tradition the coinflips are probabilistically independent and so any particular permutation of coin clips is possible, including a permutation where the coin came up heads each year it was flipped.
 □(S1 → A)
 □(A → ◊(A ∧ V))
 □(S2 ↔ (A ∧ V))
 ◊S1 conditional proof assumption
 ¬◊S2 indirect proof assumption
 □¬S2 5, equivalence
 ¬S2 6, Treiteration
 S2 ↔ (A ∧ V) 3, Treiteration
 ¬(A ∧ V) 7, 8, biconditional elimination
 □¬(A ∧ V), 79, necessity intro
 □¬(A ∧ V) 10, S4reiteration
 ¬◊(A ∧ V) 11, equivalence
 A ↔ ◊(A ∧ V) 2, Treiteration
 ¬A 11, 12, biconditional elimination
 S1 → A 1, Treiteration
 ¬S1 14, 15, modus tollens
 □¬S1 1116 necessity intro
 ¬◊S1 17, equivalence
 ◊S1 ∧ ¬◊S1 5, 18, conjunction introduction
 ◊S2519, indirect proof
□ 

□ 

 ◊S1 → ◊S2420, conditional proof