You said you want to model “in a non-formal, non-rigorous set-theoretic manner.” That’s fine by me, but since you also say “Something about the way I constructed the interval below bothers me”, I’m going to go ahead and approach this in a fully formal way, since it can help give you new ideas about how to model the idea.
I’ll start with the formal system “Zermelo-Fraenkel set theory with the axiom of choice”. This is a collection of sentences written in the language of “first-order logic”.
First, let’s begin by stating we have the following (and we won’t worry about where they came from):
- A bunch of symbols which we will call constants.
- A bunch of symbols which we will call variables.
- A bunch of symbols we will call functions.
- A bunch of symbols we will call predicates.
Each of the above categories of symbol will be given its own set of rules; they act differently than each other, in our ruleset.
On this symbolic language, we also define some more special symbols, which are the more familiar elements of logic:
¬ (negation), ∧ (conjunction), ∨ (disjunction), → (implication), ↔ (biconditional), ∀ (universal quantifier), ∃ (existential quantifier). And we’ll define their rules below, too.
(There are also punctuation symbols like commas that I don’t see the need to define.)
In this language, the function symbols so far are meaningless. They are just a symbolic rule we have, where if you have a variable x, or a constant c, you can always make up function expressions using them, like f(c, x, y). This is just a way of generating new strings of symbols.
Anything that represents an object that we are talking about, is called a term. First-order logic is a language for talking about some things. The cool thing is, it can be used to talk about different things, since it’s abstract. Whatever we are using it to talk about, we call the domain of discourse.
In general, the constant symbols represent specific things in our domain of discourse. The variables are special placeholders. With further rules about to be defined, we can have a variable say “I refer to a certain thing, but you don’t know which one it is,” for example.
These are called terms. Terms represent things in the domain of discourse. Constants represent specific things. Variables are a way for us to talk about the things without being as specific. Functions represent some way of grouping the things together (which depends on the kind of thing).
Predicates are meant to represent statements about things. They take terms, and they judge if the statement (proposition) about the thing (term) is “true” or “false”.
This language is used to define a system of mathematics - set theory. You write certain claims, or facts, about “some things” (which we can refer to as sets, since this intuitively captures the behavior of the things we are describing). These are the claims:
- ∀x ∀y (∀z (z ∈ x ↔ z ∈ y) → x = y)
- ∃x ∀y (y ∉ x)
- ∀x ∀y ∃z ∀w (w ∈ z ↔ (w = x ∨ w = y))
- ∀x ∃y ∀z (z ∈ y ↔ ∃w (z ∈ w ∧ w ∈ x))
- ∀x ∃y ∀z (z ∈ y ↔ ∀w (w ∈ z → w ∈ x))
- ∃x (∅ ∈ x ∧ ∀y (y ∈ x → y ∪ {y} ∈ x))
- ∀x ∃y ∀z (z ∈ y ↔ (z ∈ x ∧ φ(z)))
- ∀x ((∀y ∈ x ∃!z φ(y, z)) → ∃w ∀y ∈ x ∃z ∈ w φ(y, z))
- ∀x (x ≠ ∅ → ∃y (y ∈ x ∧ ∀z (z ∈ y → z ∉ x)))
- ∀x (∀y ∈ x ∀z ∈ x (y ≠ z → y ∩ z = ∅) → ∃f (f: x → ⋃x ∧ ∀y ∈ x (f(y) ∈ y)))
There are some symbols we did not mention in the explanation of the language, above. The most important one is ‘∈’. This is a predicate. (We said above we had a bunch of predicate symbols. So this is one we took from that bunch and chose to write some rules using.)
[I have to come back here later and flesh out the rest of my presentation of set theory. I’m still learning and I need to move on to the main point now.]
Below I am assuming an ordered set with each element being a year of the past (except for the current year).
Basically, when you have the axioms of ZFC, you use them, along with certain defined rules of inference, to prove the existence of a certain set. When you assume an ordered set of all past years, let’s assume (for now) we actually are taking the elements of some ordered set - which are actually sets - and interpreting them with our human subjectivity to “denote” or stand for the conceptual thing called “years”, we know in our experiential, ontological world.
We need to define “ordered set”, using the axioms of ZFC. I am going to skip the full proof for now. The idea is, an ordered set is a bijective function from an ordinal set to any other set. A bijective function is a function meeting certain conditions that can be expressed in the language of FOL. You can prove the existence of “the set of all ordered sets” (I think), then state that your set of “years up to now” is some element in that set.
If the past is infinite, then the current year is at the very least in the ordinal position ω, yet we do not know if its ordinal position is “further” than this, so we represent the index of the current year with ω + (x), with x being any ordinal value greater than or equal to 0.
I think one problem with this formalization is you claim x, a variable, is an element in a particular set: the set of all sets greater than ω. I believe it is not possible to prove the existence of such a set in ZFC, but I could be wrong. It might relate to Russell’s paradox. (Intuitively, consider that this succession of sets never ends. Well, according to your definition, that infinite succession of sets is itself contained by some enclosing set - the set of all such sets. Assuming this set is larger than any of the sets it contains, it follows that that succession of sets eventually must include that containing set; a contradiction since the set cannot be larger than itself.)
Please consider this “Part 1”, I’ll be back later to deliver Part 2. Thanks.
It seems like in the rest of your post you also came to the conclusion that there is something paradoxical, but in a different way. I’ll come back to try to help you find a non-paradoxical formulation.