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. I will, however, have at least rough English translations of symbolic logic for each of the premises right underneath the symbolic logic language. For those enterprising individuals who aren’t familiar with symbolic logic but want to try to understand it, I’ll explain some of the symbols in the next section.
Some Symbolic Logic
Some of the logic I will use (including the various names for the rules of logic) can be found in this introductory logic page. I won’t go into the various rules of logic here but I will explain what some symbols mean. First there are symbols of basic propositional logic:
Type of connective  English  Symbolic Logic  When it’s true/false 

Conjunction  p and q  p ∧ q  True if both are true; otherwise false 
Disjunction  p or q  p ∨ q  False if both are false; otherwise true 
Conditional  If p, then q  p → q  False if p is true and q is false; otherwise true 
Biconditional  p, if and only if q  p ↔ q  True if both have the same truthvalue (i.e. both are true or both are false); otherwise false 
Negation  Notp  ¬p  True if p is false; false if p is true 
To give an example of predicate logic, consider the following symbolization key:
B(x)  =  x is a Bachelor.  
U(x)  =  x is Unmarried. 
The letters B and M in these examples are predicates which say something about the element they are predicating. Sometimes parentheses aren’t used; e.g. Bx being used to mean “x is a bachelor.” The symbol; ∀ means “For All” or “For Any” such that the following basically means “All bachelors are unmarried:”
universal quantification  

In English  In Symbolic Logic 
For any x: [if x is B, then x is U]  ∀x[B(x) → U(x)] 
There’s also the existential quantifier ∃ that denotes the existence of something.
existential quantification  

In English  In Symbolic Logic 
There exists an x: [x is B and x is not U]  ∃x[B(x) ∧ ¬U(x)] 
Note that ∀x¬[Fx] = ¬∃[Fx].
In philosophy, a possible world is a complete description of the way reality is or could have been like. On possible world semantics, a proposition is possibly true if and only if it is true in at least one possible world, and a proposition is necessarily true if and only if it is true in all possible worlds.
English  Symbolic Logic  When it’s true/false 

p is possible  ◊p  True if p is true in at least on possible world; otherwise false 
p is necessary  □p  True if p is true in all possible worlds; otherwise false 
p is not possible  ¬◊p  True if p is false in all on possible worlds; otherwise true 
Note that ¬◊p is equivalent to □¬p. Indeed, the ◊ and □ operators can even be defined in terms of each other; e.g. one could define ◊ as “true in at least one possible world” and then define □ as this:
□p = ¬◊¬p
Eternal Society Paradox
Roughly, an Eternal Society is a society that has existed for a beginningless, infinite duration of time and has the abilities of ordinary human beings in each year of its existence; e.g. in each year people in the society can flip coins, write books, sing songs, and pass on information possessed in the current year to the next year. Because of the society’s extremely modest abilities, it seems like an Eternal Society would be possible if an infinite past were possible (note that by “possible” in this article I’ll be referring to metaphysical possibility, as opposed to e.g. physical possibility).
Now imagine the Eternal Society has the following Annual Coin Flipping Tradition: each year they flip a coin. If the coin comes up heads and they never did a particular chant in a prior year, then they do the chant; otherwise they do not do the chant for that year. The coin flips are probabilistically independent events, so any particular infinite permutation of coin flips is equally unlikely but also equally possible. Consider scenario S1 in which the coin came up heads for the first time last year for the Eternal Society practicing the aforementioned Annual Coin Flipping Tradition. The Eternal Society gets together to do the chant for the first time. This seems like it would be possible if an infinite past were possible (an eternal society with the ability of ordinary humans, by which I mean the society has the ability of ordinary humans in each year of its existence, could surely do something like this), but this scenario is provably not possible.
Again, the coin flips are probabilistically independent events, so if scenario S1 were possible, then another scenario, that we can call scenario S2, would be possible: the coin came up heads each year of the infinite past for the Eternal Society engaging in the Annual Coin Flipping Tradition. If the coin came up heads each year, did the Eternal Society ever do the chant? They would have had to have done the chant some year, because they would have done the chant last year if they hadn’t done it yet (since the coin came up heads last year). And yet any year you point to, there is a prior year in which they would have done the chant if they had not done the chant before. So they had to have done the chant (since the coin came up heads last year), yet they could not have done the chant (there is no year they could have done it), and so this scenario creates a logical contradiction.
Although scenario S1 is not directly selfcontradictory, scenario S1 is impossible because it implies the possibility of a logical contradiction. The Eternal Society argument against an infinite past goes like this:
 If an infinite past were possible, an Eternal Society would be possible.
 If an Eternal Society were possible, then scenario S1 would be possible.
 If S1 would be possible, then S2 would be possible.
 S2 is not possible.
 Therefore, an infinite past is not possible.
Defining the Predicates and Propositional Variables
With the domain of discourse being the years of the past, the predicates are defined as follows.
 Py = There exists a year y’ prior to year y in which the Eternal Society did the chant in year y’.
 Cy = the chant is done in year y.
 By = there exists a year before year y.
 PBy = Where y’ represents the year before y, Py’ is true (they did the chant in a year prior to y’).
 CBy = The chant is done in the year before y.
 Fy = the coin (indeterministic, probabilistically independent) is flipped in year y.
 Hy = the coin comes up heads in year y.
 I = the past is infinite and beginningless such that I entails ∀y[By].
 L = the flipped coin came up heads for the first time last year.
 V = ∀y[Hy].
 In English: the flipped 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 = ∀y[Fy] ∧ D = ∀y[Fy] ∧ (I ∧ (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)])
 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 = A ∧ L = ∀y[Fy] ∧ D ∧ L
 In English: Scenario S1 obtains.
 Note that it follows from this definition that S1 entails A.
 S2 = A ∧ V = ∀y[Fy] ∧ (I ∧ (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)]) ∧ ∀y[Hy]
 In English: 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 (7) below is that in the Annual CoinFlipping Tradition the coinflips are probabilistically independent and so any particular permutation of coin clips is possible for the Annual CoinFlipping Tradition, including a permutation where the coin came up heads each year it was flipped.
 □(S1 → A)
 Scenario S1 entails that the Annual CoinFlipping Tradition obtains.
 □(A → ◊(A ∧ V))
 Necessarily: if the Annual CoinFlipping Tradition obtains then heads coming up each year is a possible outcome.
 □(S2 ↔ (A ∧ V))
 Necessarily: the Annual CoinFlipping Tradition with the coin coming up heads each year obtains if and only if scenario S2 obtains. (Recall that scenario S2 is defined to be this way.
 ◊S1 conditional proof assumption
 ¬◊S2 indirect proof assumption
 □¬S2 10, equivalence
 ¬S2 10, Treiteration
 S2 ↔ (A ∧ V) 8, Treiteration
 ¬(A ∧ V) 12, 13, biconditional elimination
 □¬(A ∧ V) 1214, necessity intro
 □¬(A ∧ V) 15, S4reiteration
 ¬◊(A ∧ V) 16, equivalence
 A ↔ ◊(A ∧ V) 7, Treiteration
 ¬A 16, 17, biconditional elimination
 S1 → A 6, Treiteration
 ¬S1 19, 20, modus tollens
 □¬S1 1621 necessity intro
 ¬◊S1 22, equivalence
 ◊S1 ∧ ¬◊S1 9, 23, conjunction introduction
 ◊S21024, indirect proof
□ 

□ 

 ◊S1 → ◊S2925, conditional proof
Argument 2: If ◊I then ◊E, and if ◊E then ◊S1
Next is an argument for the idea that if an infinite past is possible, then an Eternal Society is possible and S1 is possible. Premises (2) and (3) can be derived rigorously from lines (27)(35) below:
 □(E → I)
 Necessarily: an Eternal Society existing implies the past is infinite.
 □(I → (I ∧ ∀y[Py ∨ ¬Py]))
 Necessarily: if the past is infinite, then (the past is infinite and for any year y, either the chant was done prior to year y or it is not the case that the chant was done prior to year y).
 □(I → (I ∧ ∀y[Fy → (Hy ∨ ¬Hy]))
 Necessarily: if the past is infinite, then (the past is infinite and for any year y, if the coin was flipped in y then either the coin landed heads in y or it is not the case that it landed heads in y.
 {◊I ∧ □(I → (I ∧ ∀y[Py ∨ ¬Py])) ∧ □(I → (I ∧ ∀[Fy → (Hy ∨ ¬Hy]))} → ◊E
 If [the infinite past is possible and necessarily: (if the past is infinite, then for any year y either the chant was done in a prior year or it is not the case the chant was done in a prior year) and necessarily (If the past is infinite, then for any year y if the coin was flipped then either it came up heads or it didn’t in year y)] then the Eternal Society is possible.
 ◊E → ◊(E ∧ (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)])
 If the Eternal Society is possible, then it is possible for that Eternal Society do the following in each year y: if there is a flipped coin that comes up heads and the chant was done in a prior year they do the chant, otherwise they don’t.
 □{D ↔ (I ∧ (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)])}
 Roughly, the letter D is defined as a placeholder letter to represent the following: the past is infinite and if for any year y there exists the flipped coin that comes up heads and the chant was not done in a prior year, then the chant is done in year y, otherwise the chant is not done in y.
 □(D ∧ E → ◊(D ∧ ∀y[Fy]))
 Necessarily: if the Eternal Society exists and D is true for that society (e.g. they do the chant depending on inter alia whether the coin came up heads), then it is possible for the Eternal Society to also actually flip a coin each year with D being true (thereby engaging in the Annual CoinFlipping Tradition).
 ◊(D ∧ ∀y[Fy]) → ◊(D ∧ ∀y[Fy] ∧ L)
 If the Annual CoinFlipping Tradition is possible (the probabilistically independent coin is flipped each year etc.), then it is possible for the coin to have come up heads for the first time last year.
 □((D ∧ ∀y[Fy] ∧ L) ↔ S1)
 Roughly: S1 is defined to be the scenario in which the Annual CoinFlipping Tradition is done and the coin comes up heads for the first time last year.
 ◊I conditional proof assumption
 ◊I ∧ □(I → (I ∧ ∀y[Fy → (Hy ∨ ¬Hy])) 28, 36, conjunction introduction
 ◊I ∧ □(I → (I ∧ ∀y[Fy → (Hy ∨ ¬Hy])) ∧ □(I → (I ∧ ∀y[Fy → (Hy ∨ ¬Hy]) 37, 29, conjunction introduction
 ◊E 30, 38, modus ponens
 ◊I → ◊E 3639, conditional proof
 □¬(D ∧ E) conditional proof assumption
 ¬(D ∧ E) 41, Treiteration
 E → I 27, Treiteration
 D ↔ (I ∧ (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)]) 32, Treiteration
 E ∧ (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)] indirect proof assumption
 E 45, conjunction elimination
 I 43, 46, modus tollens
 (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)] 45, conjunction elimination
 I ∧ (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)] 47, 48, conjunction introduction
 D 44, 49, biconditional elimination
 D ∧ E 46, 49, conjunction introduction
 (D ∧ E) ∧ ¬(D ∧ E) 42, 51, conjunction introduction
 ¬(E ∧ (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)]) 4552, indirect proof
 □¬(E ∧ (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)]) 4253, necessity intro
□ 

 □¬(D ∧ E) → □¬(E ∧ (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)]) 4154, conditional proof
 ¬◊(D ∧ E) → ¬◊(E ∧ (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)]) 55, equivalence
 ◊(E ∧ (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)]) → ◊(D ∧ E) 56, transposition
 ◊E → ◊(D ∧ E) 28, 52, hypothetical syllogism
 □¬(D ∧ ∀y[Fy]) conditional proof assumption
 □¬(D ∧ ∀y[Fy]) 59, S4reiteration
 ¬◊(D ∧ ∀y[Fy]) 60, equivalence
 (D ∧ E) → ◊(D ∧ ∀y[Fy]) 33, Treiteration
 ¬(D ∧ E) 61, 62, modus tollens
 □¬(D ∧ E) 6568, necessity intro
□ 

 □¬(D ∧ ∀y[Fy]) → □¬(D ∧ E) 5964, conditional proof
 ¬◊(D ∧ ∀y[Fy]) → ¬◊(D ∧ E) 65, equivalence
 ◊(D ∧ E) → ◊(D ∧ ∀y[Fy]) 66, transposition
 ◊E → ◊(D ∧ ∀y[Fy]) 58, 67, hypothetical syllogism
 ◊E → ◊(D ∧ ∀y[Fy] ∧ L) 34, 68, hypothetical syllogism
 □¬S1 conditional proof assumption
 ¬S1 70, Treiteration
 (D ∧ ∀y[Fy] ∧ L) ↔ S1 35, Treiteration
 ¬(D ∧ ∀y[Fy] ∧ L) 71, 72 biconditional elimination
 □¬(D ∧ ∀y[Fy] ∧ L) 7173, necessity intro
□ 

 □¬S1 → □¬(D ∧ ∀y[Fy] ∧ L) 7074, conditional proof
 ¬◊S1 → ¬◊(D ∧ ∀y[Fy] ∧ L) 75, equivalence
 ◊(D ∧ ∀y[Fy] ∧ L) → ◊S1 76, transposition
 ◊E → ◊S1 69, 77 hypothetical syllogism
Argument 3: ¬◊S2
Odd as it may seem, I’ve even seen some question premise (4), even though theoretically it should be an uncontroversial premise. In addition to the definition of scenario S2 applied in premise (81) I make use of several necessary truths that apply to this situation, such as the beginningless, infinite past entailing that each year has a year before it (line (79)); that where y’ is the year right before some arbitrary year y, if the chant was done in y’ then the chant was done in a year prior to y (line (84)); and that if there exists a year y where the chant was done in a year prior to y, then there exists a year in which the chant was done (line 85).
 □(I → ∀y[By])
 The past being beginningless and infinite entails that for every y there exists a year before y.
 □(I → (∃y[Cy] ∨ ∃y[¬Cy]))
 The past being beginningless and infinite entails that either there exists a year in which the chant is done or there exists a year in which it is not the case that the chant was done.
 □(S2 → (∀y[Fy] ∧ I ∧ (∀y[((Hy ∧ ¬Py) → Cy) ∧ (¬(Hy ∧ ¬Py) → ¬Cy)]) ∧ ∀y[Hy]))
 Roughly, scenario S2 is defined such that: the Annual CoinFlipping Tradition in which the coin comes up heads each year. (Note that scenario S2 is in fact defined this way.)
 □(∀y[¬Py → Cy] → ∀y[By → (¬PBy → CBy)])
 Necessarily: if (for every year y, if the chant is not done in a year prior to y then the chant is done in y) then (if there exists year y’ before y, if the chant is not done in a year prior to y’ then the chant is done in y’)
 □(∀y[PBy → Py])
 Necessarily: for any year y if there exists a year y’ right before y and the chant was done prior to year y’ then the chant was done prior to year y.
 □(∀y[CBy → Py])
 Necessarily: for any year y if there exists a year y’ right before y and the chant was done in y’, then the chant was done prior to year y.
 □(∃y[Py] → ∃y[Cy])
 Necessarily: if there exists a year y in which the chant was done in a year prior to y, then there exists a year in which the chant was done.
□ 

 □¬S2 86146, necessity intro
 ¬◊S2 147, equivalence