[HN Gopher] What do we mean by "the foundations of mathematics"?
___________________________________________________________________
What do we mean by "the foundations of mathematics"?
Author : JoelMcCracken
Score : 54 points
Date : 2023-11-01 17:52 UTC (5 hours ago)
(HTM) web link (lawrencecpaulson.github.io)
(TXT) w3m dump (lawrencecpaulson.github.io)
| daoboy wrote:
| A good opportunity to break out my favorite Bertrand Russell
| quote:
|
| "Everything is vague to a degree you do not realize till you have
| tried to make it precise."
| hiAndrewQuinn wrote:
| Category theory is a pretty good one. But I think a lot of people
| would get a surprising amount of value from reading Halmos's slim
| _Naive Set Theory_, to see just how much work we can create using
| sets alone.
| btilly wrote:
| We can't define "foundations of mathematics" without defining
| mathematics. My favorite stab at this is from Thurston's On Proof
| and Progress in Mathematics. Which may be read in full at
| https://www.math.toronto.edu/mccann/199/thurston.pdf: Could the
| difficulty in giving a good direct definition of mathematics be
| an essential one, indicating that mathematics has an essential
| recursive quality? Along these lines we might say that
| mathematics is the smallest subject satisfying the following:
|
| - Mathematics includes the natural numbers and plane and solid
| geometry.
|
| - Mathematics is that which mathematicians study.
|
| - Mathematicians are those humans who advance human understanding
| of mathematics.
|
| In other words, as mathematics advances, we incorporate it into
| our thinking. As our thinking becomes more sophisticated, we
| generate new mathematical concepts and new mathematical
| structures: the subject matter of mathematics changes to reflect
| how we think.
|
| The foundations of mathematics then refers to the essential core
| that we have based our mathematical thinking on. Which is
| something that most of us only wish to think about when our
| thinking has run into problems and we need a better foundation.
| vlovich123 wrote:
| Is mathematics just the study of all possible languages that
| are constructed from strict internally consistent rules?
| saalweachter wrote:
| Mathematics is the study of things you can convince people
| are true without physical evidence.
| btilly wrote:
| No, because some possible languages are far more interesting
| than others.
| bmacho wrote:
| I don't think that's a problem: if there are uninteresting
| languages, then you must _study_ them, then _work hard_ to
| _prove_ that they are uninteresting first. That is,
| mathematics indeed does study uninteresting languages.
|
| .. mathematics is the same for me as GP said: you have a
| set of symbols, a set of rules, now derive true statements.
| (Or at least this is a good view, but other views can be
| also good.)
| Someone wrote:
| > Mathematics includes the natural numbers and plane and solid
| geometry.
|
| That, to me, feels similar to Euclid's fifth postulate, in the
| sense that it isn't something you'd want to include in a
| definition.
|
| Maybe, the similarity doesn't end there, and we have multiple
| mathematics, just as pure mathematicians don't talk about
| _algebra_ , but about _an algebra_ , with some of them being
| more interesting than others, and it not always being easy to
| show that two algebras are different from each other.
|
| For example, we have mathematics without the law of the
| excluded middle and with it, ones without the axiom of choice
| and with it, etc.
| westurner wrote:
| https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t... :
|
| > _Today, Zermelo-Fraenkel set theory [ZFC], with the
| historically controversial axiom of choice (AC) included, is the
| standard form of axiomatic set theory and as such is the most
| common_ foundation of mathematics.
|
| Foundation of mathematics:
| https://en.wikipedia.org/wiki/Foundations_of_mathematics
|
| Implementation of mathematics in set theory:
| https://en.wikipedia.org/wiki/Implementation_of_mathematics_... :
|
| > _The implementation of a number of basic mathematical concepts
| is carried out in parallel in ZFC (the dominant set theory) and
| in NFU, the version of Quine 's New Foundations shown to be
| consistent by R. B. Jensen in 1969 (here understood to include at
| least axioms of Infinity and Choice)._
|
| > _What is said here applies also to two families of set
| theories: on the one hand, a range of theories including Zermelo
| set theory near the lower end of the scale and going up to ZFC
| extended with large cardinal hypotheses such as "there is a
| measurable cardinal"; and on the other hand a hierarchy of
| extensions of NFU which is surveyed in the New Foundations
| article. These correspond to different general views of what the
| set-theoretical universe is like_
|
| IEEE-754 specifies that float64s have +-infinity and specify
| ZeroDivisionError. Symbolic CAS with MPFR needn't be limited to
| float64s.
|
| HoTT in CoQ: Coq-HoTT: https://github.com/HoTT/Coq-HoTT
|
| What is the relation between Coq-HoTT & Homotopy Type Theory and
| Set Theory with e.g. ZFC?
|
| Homotopy Type Theory:
| https://en.wikipedia.org/wiki/Homotopy_type_theory :
|
| > _" Cartesian Cubical Computational Type Theory: Constructive
| Reasoning with Paths and Equalities" (2018)_
|
| https://scholar.google.com/scholar?cites=9763697449338277760...
| and sorted by date:
| https://scholar.google.com/scholar?hl=en&as_sdt=5,43&sciodt=...
|
| What does Mathlib have for SetTheory, ZFC, NFU, and HoTT?
|
| leanprover-community/mathlib4// Mathlib/SetTheory:
| https://github.com/leanprover-community/mathlib4/tree/master...
| nyc111 wrote:
| Mathematics is built on definitions. There are definitions on the
| foundations of mathematics. Axioms are definitions that are kept
| constant by consensus.
|
| Euclid starts with definitions. If you don't like Euclid's
| definitions you make your own definitions. You create your own
| geometry etc.
| smokel wrote:
| For those who like to read biographies of the brilliant minds,
| instead of the actual mathematics they produced, I can highly
| recommend "Journey to the Edge of Reason: The Life of Kurt Godel"
| (2021) by Stephen Budiansky, which is nice.
| wisnesky wrote:
| A foundation for mathematics is any formalism sufficient to prove
| the results typically taken as axioms in practical mathematics.
| For example, in ZFC you can define numbers as sets in many
| different ways and prove that 1+1=2 for each of them - other
| foundations include higher order logic, topos theory, other set
| theories, etc.
| wubrr wrote:
| Is it also possible to define set theory in terms of
| arithmetic?
| wisnesky wrote:
| Yes, at least with a strong enough arithmetic (such as
| Peano's), but that is usually more complicated; for example,
| you might have to create a Godel numbering or some other
| "deep embedding" to represent each set as a number. There's
| also so-called "reverse mathematics", which tries to
| determine the weakest axiom system capable of establishing a
| particular result.
| wubrr wrote:
| Interesting, thanks!
| Kranar wrote:
| You can certainly define some set theories using arithmetic
| but arithmetic as formalized by first-order Peano arithmetic
| can not define a set theory powerful enough to prove results
| about uncountable sets, such as large cardinal axioms or even
| properties of real numbers.
| wubrr wrote:
| Any links/examples of why this isn't possible? My thinking
| is - if all existing set theory and set theoretic proofs
| are expressed in finite set-theoretic
| statements/expressions - can't we 'encode' these
| expressions within the system of arithmetic?
| Kranar wrote:
| Do I have links off the top of my head that directly
| address this, no unfortunately I do not. I do have links
| to different pieces that you can use to understand this,
| however. First is the notion of the consistency strength
| of a formal system which basically is the ability of one
| formal system to prove the consistency of another formal
| system [1].
|
| ZFC is strictly stronger than PA in the sense in that ZFC
| can prove the consistency of PA [2].
|
| From this, however, it follows that PA can not prove the
| consistency of ZFC. If PA could prove the consistency of
| ZFC then ZFC would be able to prove the consistency of
| itself, which we know from Godel's incompleteness theorem
| would mean that ZFC is inconsistent [3].
|
| So this gives one concrete proof that ZFC can produce
| that PA can not produce, namely the consistency of PA
| itself.
|
| [1] https://en.wikipedia.org/wiki/Equiconsistency#Consist
| ency_st...
|
| [2] https://mathoverflow.net/questions/66121/is-pa-
| consistent-do...
|
| [3] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incomple
| teness_...
| nitwit005 wrote:
| You're getting at the problem with saying "foundation". If you
| can reach the same conclusions from a large number of starting
| points, there isn't any special set of ideas on which
| everything rests.
| epgui wrote:
| Why does the foundation need to be unique? It seems intuitive
| to me that they must not be unique.
| tromp wrote:
| Jeremy Avigad made available a 54-page draft chapter on
| mathematical logic and foundations [1]. Quoting from the
| abstract:
|
| > The formal foundation of a proof assistant is the formal
| deductive system with respect to which the correctness of the
| proof assistant's implementation is judged. The foundation
| specifies a language for defining objects and saying things about
| them, and it determines the means that can be used to prove that
| such statements are true. This chapter presents some general
| background in logic that is helpful for thinking and reasoning
| about formal systems, and it describes the three main families of
| foundations that are commonly used in proof assistants today.
|
| [1] https://arxiv.org/abs/2009.09541
| 1equalsequals1 wrote:
| Thank you friend
| cjfd wrote:
| I have a project to write a proof assistant that is as simple as
| possible while still usable. A kind of turing tar pit but for
| proofs instead of programs. Some early attempts did not quite
| work out. I try to get it off the ground using the calculus of
| constructions (not the calculus of inductive constructions)
| together with a small set of axioms. As axioms I aim, at the
| moment, to use a hilbert epsilon operator to contstruct objects
| from theorems that state their existence, proof irrelevance and
| an infinity axiom that states that an infinite set exists. Also I
| do use an infinite hierarchy of Types a bit like the universes of
| coq. I am still debating with myself whether I also should
| provide the luxury of not having to specify universe levels and
| just keep constraints between them like in coq.
|
| The article proposes the calculus of inductive constructions but
| I think that is just too big and complicated to be a good
| candidate for a foundation of mathematics. I think it makes more
| sense to use a more concise foundation and maybe attempt to prove
| that the calculus of inductive constructions is a conservative
| extension of that.
| bvssvni wrote:
| Is your goal to have as few axioms as possible, or as few
| syntactic constructions as possible?
| zarzavat wrote:
| The calculus of inductive constructions is not very big? It
| seems simpler than ZFC to me. The version that Coq uses is
| quite large, but that's the difference between theory and
| practice: Coq is designed to be maximally usable not minimally
| simple.
| lacker wrote:
| Once you have an infinite hierarchy of types, including
| universe levels, can the proof assistant really be "as simple
| as possible"?
|
| I feel like a simple-as-possible proof assistant would be more
| like, proving things about programs written in a minimal Lisp
| dialect, where the proof validator is itself written in that
| Lisp dialect.
|
| That said, I personally would rather have an extremely usable
| proof assistant, rather than a simple-as-possible one. In many
| ways those things point in opposite directions; consider the
| usability and simplicity of Python vs the lambda calculus.
| blueberry87 wrote:
| What are your other options? A type-based proof system
| implies dependent types, implies universe levels if you want
| it to be consistent.
| lacker wrote:
| You would have to not use a type-based proof system. I
| think those are not going to be the "as simple as possible"
| ones. Consider metamath for example.
| aaimnr wrote:
| Reminds me of Wilfrid Sellars: "The aim of philosophy, abstractly
| formulated, is to understand how things in the broadest possible
| sense of the term hang together in the broadest possible sense of
| the term".
|
| "Hanging together" doesn't impose as many assumptions as "having
| specific foundation". It's a very distinct philosophical stance
| to assume that any kind of human knowledge has a specific
| foundation, and a naive one at that.
| wannabebarista wrote:
| For those interested in recent systematic discussions of
| foundations, I find Penelope Maddy's recent work compelling. For
| instance, see the paper "What do we want a foundation to do?" [0]
|
| [0]
| https://sites.socsci.uci.edu/~pjmaddy/bio/What%20do%20we%20w...
| practal wrote:
| > That the solution could lie in something as simple as Zermelo's
| separation axiom and the conception of the cumulative hierarchy
| of sets was seemingly not anticipated. It was a miracle.
|
| If you are a Platonist (I am), then it is not really a miracle.
| Mathematical objects are real, and logic is a tool to study them.
| The paradoxes can only exist, because math is real: a paradox
| shows that something is not real, and if there were no real
| mathematical objects to begin with, paradoxes would be
| meaningless. As it stands, a paradox is a tool to distinguish
| reality from that which is not real.
|
| Have fun making any kind of sense if you are a formalist or
| intuitionist (hint: you can't).
|
| It is indeed cool that something as simple as set theory covers
| so much. But it doesn't cover everything. The Banach-Tarski
| Paradox shows that sets are not what we imagine them to be (but
| they are still real): we need to add the property of
| measurability, which acts then as an additional axiom, to get
| closer to that. And in order to solve BB(748), ZFC is not enough
| [0, theorem 7]. So, one set theory is not enough. Depending on
| which properties we ascribe to sets, or in other words, which
| axioms we add to set theory, we also get different set theories.
|
| > I give up.
|
| Set theory is cool, but it is not special. In the end it
| describes a fragment of the (real) mathematical universe, but
| there is more to this universe than just set theory. And
| depending on which properties you pick for your sets, you get
| different fragments.
|
| It is interesting that Larry says that Automath is not a
| Foundation, and that neither is Isabelle, which he created. Maybe
| I am putting words in his mouth here, but that is how I interpret
| his "Isabelle/Pure is in the same spirit". I think he is right.
| BUT, Isabelle is SO close to a foundation. All you have to do is
| to drop the types :-D. All of them. That's what I did, and you
| then basically get Abstraction Logic [1]. Abstraction Logic makes
| no assumptions whatsoever about your mathematical universe,
| except that it is non-empty, and it better have more than 1
| object in it. It doesn't assume that sets exist, or types, or
| anything else. It doesn't force you to define natural numbers or
| other mathematical objects as sets. You can define any operator
| you want, and with each choice of axioms you are exposed to the
| risk of doing nonsense and creating paradoxes. And therefore I
| believe it is the right foundation for mathematics, and I think
| it is the only right one. Yes, there is a single logical
| foundation. Sounds too simple? So did set theory. Yes, I think
| Abstraction Logic is a miracle, but on the other hand, it simply
| manifests logic as it is.
|
| [0] https://www.scottaaronson.com/papers/bb.pdf, page 12, theorem
| 7
|
| [1] http://abstractionlogic.com
| drdeca wrote:
| > Abstraction Logic makes no assumptions whatsoever about your
| mathematical universe, except that it is non-empty, and it
| better have more than 1 object in it. It doesn't assume that
| sets exist, or types, or anything else.
|
| This sounds kind of similar to something I've thought about,
| but which makes approximately one fewer assumption, while also
| remaining closer to set theory.
|
| Namely, the theory of first order logic (without equality),
| with one binary relation symbol, and no axioms (unless you
| count the laws of inference of FOL, which you shouldn't).
|
| If you name this binary relation symbol \in_0 , and are willing
| to use a "definition schema" to define, for each natural number
| in your meta-theory, binary relations \in_n and =_n (any
| sentence using these \in_n and =_n can be expanded out to a
| longer sentence in FOL using just quantifiers and \in_0), then,
| in the meta theory, you can prove a fair number of nice things
| about "for all natural numbers n, it is provable in the object
| theory that [some statement which uses relations \in_n and/or
| =_n]".
|
| For example, you can show that, for all n, you can show in the
| object-theory that =_n is transitive and reflexive, and that if
| x =_n y, then x =_{n+1} y as well, and that for all A, B, if A
| \subseteq_n B , then A \subseteq_{n+1} B, and you can define
| notions of one object being a power set of another object at
| level n (and any two power sets of an object at level n, will
| be equal at level n), and can show that, for all n, it is
| provable in the object theory that if A \subseteq_n B , and if
| PA is a powerset of A at level n, and PB is a powerset of B at
| level n, then PA \subseteq_n PB , and all sorts of similar
| things.
|
| I'm a little skeptical of the "something between 1st order
| logic and 2nd order logic" claim, but I haven't looked closely.
|
| Are you familiar with the metamath project? aiui, metamath is
| based in string rewrite rules, and is therefore fully general
| in the way it sounds like you are going for?
| lacker wrote:
| 100 years ago everyone was worrying about whether the foundations
| of mathematics were consistent. We figured out some details that
| we had been taking for granted, like the axiom of choice, how to
| prevent Russell's paradox, and the inevitable difference between
| "true" and "provable" (ie Godel's incompleteness). Now that part
| is pretty much solved, we are fairly confident that the
| foundations of mathematics are consistent.
|
| IMHO the problem now is that the foundations of mathematics are
| _impractical_. Most mathematicians don 't actually do mathematics
| that can be tied back to the foundational axioms. It seems like
| it should be possible, in theory, but it takes too much work. So
| most mathematicians prefer communicating their proofs in PDFs
| rather than in a more rigorous format.
| bvssvni wrote:
| One thing I would like point out with Godel's incompleteness
| theorems, is that there are different notions of provability.
| Godel uses the notion of "provability" you get from Provability
| Logic, which is a modal logic where you introduce terms from
| e.g. Sequent Calculus.
|
| Recently I found another notion of "provability" where Lob's
| axiom, required in Provability Logic, is absurd. It turns out
| that this notion fits better with Intuitionistic Propositional
| Logic than Provability Logic. This allows integrating the meta-
| language into object-language. This is pretty recent, so I
| think we still have much to learn about the foundations of
| mathematics.
| layer8 wrote:
| > Recently I found another notion of "provability"
|
| Any pointers to that alternative notion?
| bvssvni wrote:
| I'm implementing it in this project:
| https://crates.io/crates/hooo
| drdeca wrote:
| This makes it kind of sound as if Lob's axiom is used in the
| proof of Godel's incompleteness theorems, but Godel was
| working in (I think) PA, not in Provability Logic?
|
| I guess you just meant "the notion of provability is the same
| as the one that would later be described in Provability
| logic" ?
|
| I viewed the page you linked, but I don't see anywhere where
| you describe the alternate notion of "provability" you have
| in mind.
|
| "Provability" in the sense of Godel's incompleteness
| theorems, is just, "There exists a proof of it in [the chosen
| system of axioms + rules of inference]", yes? I don't see how
| any other notion would be fitting of the name "provability".
| "provable" , "possible to prove", "a proof exists", all the
| same thing?
|
| Oh, I guess, if you want to use "there exists" in a
| specifically constructive/intuitionistic way? (so that to
| prove "[]P" you would have to show that you _can produce_ a
| proof of P?)
|
| I think I've seen other people try to do away with the need
| for a meta-language / make it the same as the object-
| language, and, I think this generally ends up being
| inconsistent in the attempts I've seen?
|
| edit: I see you have written 'Self quality a ~~ a is
| equivalent to ~a, which is called a "qubit".'
|
| I don't know quite what you mean by this, but, _please_ do
| not call this a qubit, unless you literally mean something
| whose value is a vector in a 2d Hilbert space.
| bvssvni wrote:
| > I guess you just meant "the notion of provability is the
| same as the one that would later be described in
| Provability logic" ?
|
| yes
|
| > I viewed the page you linked, but I don't see anywhere
| where you describe the alternate notion of "provability"
| you have in mind.
|
| See section "HOOO EP"
|
| >Oh, I guess, if you want to use "there exists" in a
| specifically constructive/intuitionistic way? (so that to
| prove "[]P" you would have to show that you can produce a
| proof of P?)
|
| This would be `|- p` implies `#p`, which is the N axiom in
| modal logic (used by Provability Logic).
|
| In Provability Logic, you can't prove `#false => false`. If
| you can prove this, then Lob's axiom implies `false`, hence
| absurd. `#p => p` for all `p` is the T axiom in modal
| logic. In IPL, if have `true |- false`, then naturally you
| can prove `false`. So, you can only prove `#false => false`
| if you already have an inconsistent theory.
|
| Provability Logic is biased toward languages that assume
| that the theory is consistent. However, if you want to
| treat provability from a perspective of any possible
| theory, then favoring consistency at meta-level is
| subjective.
|
| > I think I've seen other people try to do away with the
| need for a meta-language / make it the same as the object-
| language, and, I think this generally ends up being
| inconsistent in the attempts I've seen?
|
| I have given this some thought before and I think it is
| based on fix-point results of predicates of one argument in
| Provability Logic. For example, in Godel's proof, he needs
| to encode a predicate without arguments in order to create
| the Godel sentence. In a language without such fix-points,
| this might not be a problem.
|
| > I don't know quite what you mean by this, but, _please_
| do not call this a qubit, unless you literally mean
| something whose value is a vector in a 2d Hilbert space.
|
| The name "qubit" comes from the classical model, where you
| generate a random truth table using the input bit vector as
| seed. So, the proposition is in super-position of all
| propositions and hence behaves like a "qubit" in a
| classical approximation of a quantum circuit.
| deltasepsilon wrote:
| I'm attempting to understand you, so:
|
| Are you saying that Lob's axiom, which states that the
| provability of "the provability of p implies p" implies the
| provability of p, necessarily prejudices some implicit
| assumption of consistency to the meta-language?
|
| How so, and/or, what are the axioms, or derived properties,
| of this new notion of provability you have uncovered?
| libraryofbabel wrote:
| > IMHO the problem now is that the foundations of mathematics
| are impractical. Most mathematicians don't actually do
| mathematics that can be tied back to the foundational axioms.
|
| I suppose my followup to that is, _why_ is this a problem? Does
| it lead to bad mathematics? (For what definition of "bad"?)
| Would we be able to solve unsolved problems if we tied things
| back to foundations more? Mathematicians have never really done
| much mathematics that ties back to the foundational axioms --
| why change? Rigor is not really much of an end in itself -
| surely people do mathematics because it is useful or beautiful,
| or both?
| jimwhite42 wrote:
| And you can apply it, when you do, it really works.
| lacker wrote:
| I think AI for mathematics will help us solve unsolved
| problems. There should be a virtuous cycle during its
| development.
|
| 1. More formalized training data makes the math AI better
|
| 2. Better math AI helps us formalize more known mathematics
|
| But right now math AI is not very useful. It isn't at the
| point where ChatGPT is for programming, where the AI is
| really helpful for a lot of programming tasks even if it
| isn't superhuman yet. So the virtuous cycle hasn't started
| yet. But I think we will get there.
| jimwhite42 wrote:
| > It seems like it should be possible, in theory, but it takes
| too much work.
|
| The definition of a valid mathematical proof that I've heard
| mathematicians use is if it convinces other mathematicians. I
| think there's integrity in depth in mathematical proofs for
| lots of reasons, tying back to an axiomatic basis is a lot of
| extra work for likely no benefit.
|
| On formal mathematics, almost no mathematicians pay attention
| to this afaik. It's something that lives in philosophy
| departments, not mathematics.
| bvssvni wrote:
| I think the most exciting work in mathematics today is in the
| formal foundations. However, I can also understand
| mathematicians who are thinking like this:
|
| 1. I only need normal congruence
|
| 2. I only need perfect information games
|
| Under problems that are solvable using these two assumptions,
| there is little benefit in tying proofs back to an axiomatic
| basis. Once you drop one of these two assumptions, proofs get
| much harder and a solid foundation gets more important.
| bvssvni wrote:
| The foundations of mathematics are all about language design.
|
| To answer this question, one must say something about which
| language a foundation of mathematics is using. For example, Set
| Theory is formalized in First Order Logic. However, First Order
| Logic uses Propositional Logic, so to build an alternative
| foundation to Set Theory, you might consider starting with
| Propositional Logic and extending it another way.
|
| First Order Logic extends Propositional Logic with predicates.
| This might seem like a good design at first, until you try to
| reason about uniqueness. In Set Theory, one requires an equality
| operator in addition to set membership, in order to be able to
| reason about uniqueness, at all. This equality operator is ugly,
| because you have to rebuild objects that are isomorphic but using
| different encodings.
|
| Predicates causes problems because they are unconstrained. For
| easier formalizing of advanced theories, I suggested Avatar
| Logic, which replaces predicates with binary relations, avatars
| and roles. You can try it here: https://crates.io/crates/avalog
|
| Also, most theories assume congruence for all predicates, which
| is bad for e.g. foundations of randomness.
|
| The next crisis in "the foundations of mathematics" will be
| "tautological congruence". Luckily, this is already being worked
| on, by extending Intuitionistic Propositional with exponential
| propositions. This theory is known as "HOOO EP" and is
| demonstrated here: https://crates.io/crates/hooo
| tutfbhuf wrote:
| I'm a bit sad the he doesn't mention univalent foundations, which
| is based on [?]-groupoids instead of sets.
| graycat wrote:
| (1) Common K-12 math.
|
| (2) A text on set theory, especially _axiomatic_ set theory.
|
| (3) Abstract algebra, i.e., the natural numbers, the rationals,
| the reals, the complex numbers, the basic properties, and some on
| groups, rings, fields, and vector spaces.
|
| That's enough for the _foundations_.
___________________________________________________________________
(page generated 2023-11-01 23:02 UTC)