I'm working on a species that is built around always making the most efficient available decisions as possible, and always trying to logically correlate events to make pattern sequences for how the world works. I've already decided they'll have two major religions, one built around societal ideals and the other around supporting a god. How should I design these?
What you describe actually exists in the world of First Order Logic (FOL) and its friends. In fact, what you describe is so mindbogglingly close to the work of Dan Willard that I really want to get to see where you take this in science fiction!
Let me preface this with an apology for the length. I have tried to condense this several times, and it falls flat without enough formality to make it profound. The paragraph above is as close as I can get to a Tl/Dr, other than to point out that the final outcome is that it is mathematically valid for both of your factions to look at the same evidence and come to radically different outcomes.
Logic, as far as mathematicians go, is all about proofs. Its about what you can argue is true based on the initial premises. Of course, you have to pick your rule set. There are dozens of rulesets out there. Maybe even hundreds. By there are a handful which are by far the most popular. I present them, ranked from least expressive to most expressive.
- Propositional Logic (PL). Propositional logic is how we handle sentences like "if it is raining, I will bring an umbrella." We see mathematical structures like
A ∧ B → C(if A and B then C) in this system. Most of us learn of it in school.
- First Order Logic (FOL). This is what happens when we extend propositional logic to talk about quantifiers over individuals like "for all" and "there exists." If we want to say "for every action there is an equal and opposite reaction," we might write
∀action. ∃reaction. isReactionOf (reaction, action) ∧ reaction = -1 * action. This permits a great deal of expressiveness that cannot be done in PL.
- Second Order Logic (SOL). This extends FOL to add quantifiers over relations. This is a very nuanced change, but surprisingly profound. For example, in SOL we can phrase one of the fundamental axioms used in logic, the principle of bivalence: "For every proposition, that proposition is true or false for every object" as
∀P∀x( P(x)∨¬P(x) ). This proves to be very powerful!
Now as I said, there are many many other systems, but over the years, these have been the ones that have been most accepted and most popular. They're the ones I'll focus on.
Another thing that has been enormously successful in mathematics is arithmetic. Being able to say 2+2=4 is a great thing for civilization. But what if someone disagrees, saying 2+2=5? How do you resolve this disagreement? The only way mathematicians know of, short of dukeing it out in the parking lot behind the dumpster, is to define a set of valid rules for what is and is not correct arithmetic.
Like logic, there are many variants, like Robinson arithmetic, each with its own peculiar quirks. However, by far the most popular is Peano arithmetic, and that is an understatement. Its so popular that most people don't even learn the other arithmetics until they are part way into an upper-graduate mathematics degree). It is the one you learned in school, whether you knew it or not. We called them "natural numbers," and it builds on the following rules (or a provably equivalent set):
- The number
0is a natural number
- Natural numbers have an equality function that is transitive, reflexive, symmetric, and closed. (read: our usual concept of equality)
- For every natural number
x, there exists a number
S(x), which is a natural number. This "S" function defines the successor for a number. 2 is the successor for 1, 5 is the successor for 4, so on and so forth. (we define the numbers
3... using this relationship)
∀m,n (m=n ↔ S(m)=S(n))- Two numbers are the same if and only if their successors are the same. This means we'll never find that 42 is the successor to both 41 and 7. It woudl be against the rules.
∀n ¬(S(n)=0)- Zero is not the successor of any number. In integers, zero would be the successor of -1, but natural numbers start with 0 and count up, so there's no predecessor of zero.
∀P P(0) ∧ (∀n P(n) → P(n + 1)) → ∀n P(n)- Woof! What a doozie! This one is the axiom of induction. It's what you learned in school as "mathematical induction" If you can prove that something is true for n=0 and you can prove that it is true for n+1 if you can prove it for n, then the statement is true for all natural numbers. You use the fact that it's true for 0 to prove it is true for 1, then use that to prove that it is true for 2, so and so forth, until infinity.
When you hear the joke about how a mathematician spends 4 years in college to learn to prove that 2+2=4, this is what they are referring to. Its a laborious way of going about things, but it is what we have all agreed "arithmetic" actually means under the hood. Now go memorize your multiplication tables, because you don't want to have to use this method on a timed test!
Now the axiom of induction is a problem. All of the other axioms can be expressed in FOL. But that one is written in SOL -- it said "for all predicates P..." We'd really like it if that could be rewritten in FOL. That would tidy this whole arithmetic bit up. As it turns out, we can't. At least we can't do it with a reasonable number of rules. We could always just have an infinite number of rules, one for each possible predicate P, but mathematicians aren't a fan of that.
The man who proved we can't was Kurt Gödel. He put together a fantastic proof, known as the Incompleteness Theorems. His incompleteness theorems basically proved that, were you ever to succeed at collapsing all of arithmetic into a finite set of rules (more formally, a "recursively enumerable" set of rules), your result must be inconsistent, and thus invalid. He did this by encoding said rules into numbers, similar to how this SE post is turned into 1's and 0's on a harddrive somewhere. He then showed that you could define a function, when fed the encoded version of itself, provide the wrong result.
It was a fascinating proof that basically showed that Peano arithmetic, as we know it, could not be completely expressed using the rules of FOL that we were comfortable with. It was decidedly unpopular in many cliques of mathematics, but has come to be accepted as a painful truth. I would argue it was the mathematical equivalent of the problem of evil.
The case was closed for a while, until recently Dan Willard started playing with it. In 2001 he released a fascinating paper on self-verifying systems -- FOL systems which could prove their own consistency. In it he showed a system which could prove all its own theories, and all of arithmetic except for one teeny-tiny detail. In his systems, multiplication was not provably total. This means his system could theoretically define two natural numbers,
b such that
a*b is not a natural number. In these systems, it is hypothetically possible that two numbers could be so large that, when multiplied together, they produce a result that is NaN - not a number.
Its a very small adjustment, but it proved sufficient to styme the particular tools needed to construct the lemmas (sub proofs) that Gödel needed to prove the system is inconsistent.
Okay, forgive me for geeking out for that long discussion of logic. Did you know you were getting into that when you chose to make a purely logical species? Its quite the subject! But all of that was important because it leads up to some fascinating disagreements on "what is arithmetic" that can lend itself to the religious split you seek.
Peano arithmetic starts from 0 and 1, and works its way up from there. Its like building a brick tower, one brick at a time. In theory, with infinite time, you can lay bricks for an infinitely tall tower. The Babble references here are intentional. Religion argues that such towers will be torn down by an angry god, as invalid.
But what if you made the tower larger at the bottom, so as to withstand the brunt of a god? What if the number of bricks in the bottom layer was infinite, to make it an infinitely large base, and then extended upwards infinitely high. Surely one would wish to use multiplication to see how many bricks you are going to need to produce!
Willard worlds are constructed differently. Instead of starting from 0 and 1 and then defining addition and subtraction, Willard worlds start from a infinity, and work their way down with subtraction and division. They start from a single infinity (a good starting point for your God), and define the individual from it.
Which one is right? Well, "right" is a linguistic judgement. We don't have to agree on what "arithmetic" means. You just keep calling Peano arithmetic "arithmetic," and I'll keep calling Willard arithmetic "arithmetic," and we will agree to disagree.
Fascinatingly, Willard's systems are self-verifying. A believer in such a world believes because they can prove they are right, using their own system. How fantastic is that?
And there's peculiarities that can be teased at. It turns out that it is possible to construct a number that is provably countably infinite outside of a Willard system, which is provably uncountably infinite inside the system. That's right: within a system you can prove that a number is unreachable, counting from 0, 1, 2, ..., even if you had infinite time to do so. And yet, outside of the system, you can prove otherwise.
This could be the basis for the God-believers to truly and honestly believe that there is a higher power more powerful than the sum of all creation, but to have the societal-ideals people to take the same evidence and find that there is not.
They celebrate the logical world via formal proofs.
In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically checkable
This is not outrageous. There are many who find beauty in math and especially logical sequences where each thing follows unambiguously from the thing before. Some music is thought to be like a mathematical proof in its symmetry and progression.
The only tricky thing: if you are going to write about people whose religion celebrates formal proofs it would help to have a thorough understanding of them yourself.
Religions are not specifically about gods. Religions are about cultural values that hold a society together. The deity figure is just that, a figure used to give the whole thing authority.
Religions are, fundamentally, memes. They grow, they mutate, they compete. Sometimes they die out. Humans tolerate them because they can (sometimes) be survival technology. They are how humans typically record and transmit their moral code. A good moral code, one that helps the individuals in society thrive, will help the religion to thrive and spread. So, quite sadly, will a seductive but harmful moral code.
Consider: The religion known as "Christian" is very different from the religion known as "Christian" even as recently as 2 centuries ago. And again very drastically different from the religion as it existed over the centuries from its first formation. From what is permitted on Sunday, to what is required to do with a witch, to how people are permitted or required to dress.
Consider such things as the bulk of symbols and decorations associated with Christmas. The tree, holly, wreath, yule log, mistletoe, etc., are all "borrowed" from Northern European traditions present before Christianity arrived.
I attend a pub night once a month. (When various virus measures don't prevent it.) And when somebody leaves for the evening, somebody nearly always says "Have fun storming the castle! Do you think it will work? It will take a miracle. Bye bye!" Such traditions are the seeds that may grow into a religion. Combine that with a moral code, and a societal model for things like romantic relations, raising children, caring for the elderly, choosing jobs, etc. and etc.
So what you need is a moral code that works for the society at the current tech level. And a bunch of accepted documents that illustrate this moral code. This behavior is exemplary, this good but unremarkable, this a little naughty, this monstrous. And a bunch of traditions that the followers use to mark themselves off as part of the religion. Funny hats, little phrases, specialty foods, ceremony, prohibitions, edicts.
The result is, practitioners of the religion can recognize each other and put just enough of a barrier up between "in" and "out" so that it is recognizable. The hat with what looks like miniature pool noodles sticking out of it marks the Pastafarian. The wish "May you be touched by his noodly appendage!" serves to remind everybody. The Book of Ramen and keeping September 19 (Talk Like a Pirate Day) remind everybody and bring them together.
If the ethics and morality prescribed make sense, so much the better.