Mathematicist Genesis
I just thought up a fun philosophical forum game for those well-versed in either mathematics or the natural sciences to play, and those interested in learning more about them to watch. This game will make one core philosophical assumption: mathematicism, the view that the physical universe is identical with some mathematical structure. This assumption should only come in to play at one step in the game though, and if you really hate mathematicism, you can interpret everything after that step to be talking about a simulation of the universe instead of the actual universe, and it shouldn't make any difference.
The game is to start with the most elementary of mathematical structures, and build from there up to the structure that is (on our best current understanding of physics) identical to (or if you really prefer, the perfect model of) our physical universe, and then build up from the most elementary physical elements of our universe to, let's say, a human being, or human civilization, or something thereabouts.
More or less one step of the process per turn, more or less one turn in a row per player (unless the thread is dying and you want to revive it), try to make your explanations understandable to people who don't already know the thing you're explaining, and for extra style points, try to make it sound dramatic, vaguely like a creation myth, as you do it.
Also feel free to correct anyone who plays a step wrong, or ask for clarification if you can't follow a step.
I'll start us off:
----------------
To begin with, there is the empty set, and the empty set is without contents and void.
And the joint negation or complement operation is the sole sufficient operation, which returns the set of everything that is not any of the arguments fed into it, i.e. the complement operation on a set is equivalent to the negation of all the things in that set: the complement of {a, b, c, ...} is all that is not-a and not-b and not-c and ...
And the complement of the empty set, all that is not nothing, is everything. The end.
...No wait, let's go back and take things a little slower this time around. Or a lot slower, as the case may be.
The negation or complement of the joint negation or complement operation is the disjunction or union operation, which returns all that is at least one of the arguments fed into it: the complement of the complement of {a, b, c, ...}, which is to say not(not-a and not-b and not-c and ...), is all that is a or b or c or ...
Call the union of something and the set containing that thing the successor of that thing. The successor of the empty set is thus the union of it and a set containing itself, which union is just a set containing the empty set, since the empty set contained nothing to begin with.
Thus the negation of the joint negation of the empty set and the set containing the empty set is the first successor.
And the empty set we call zero, and the successor to that set we call one. And thus are the first numbers.
And the successor to one we call two, and the successor to two we call three, and so on ad infinitum.
And thus the empty set and its successors are the natural numbers. And they are good.
----------------
(Suggested next steps: construction of addition from set operations, then multiplication; then subtraction, necessitating the construction of integers... and so on until we get up to SU(3)xSU(2)xU(1) or such, where the physicists can take over from the mathematicians).
The game is to start with the most elementary of mathematical structures, and build from there up to the structure that is (on our best current understanding of physics) identical to (or if you really prefer, the perfect model of) our physical universe, and then build up from the most elementary physical elements of our universe to, let's say, a human being, or human civilization, or something thereabouts.
More or less one step of the process per turn, more or less one turn in a row per player (unless the thread is dying and you want to revive it), try to make your explanations understandable to people who don't already know the thing you're explaining, and for extra style points, try to make it sound dramatic, vaguely like a creation myth, as you do it.
Also feel free to correct anyone who plays a step wrong, or ask for clarification if you can't follow a step.
I'll start us off:
----------------
To begin with, there is the empty set, and the empty set is without contents and void.
And the joint negation or complement operation is the sole sufficient operation, which returns the set of everything that is not any of the arguments fed into it, i.e. the complement operation on a set is equivalent to the negation of all the things in that set: the complement of {a, b, c, ...} is all that is not-a and not-b and not-c and ...
And the complement of the empty set, all that is not nothing, is everything. The end.
...No wait, let's go back and take things a little slower this time around. Or a lot slower, as the case may be.
The negation or complement of the joint negation or complement operation is the disjunction or union operation, which returns all that is at least one of the arguments fed into it: the complement of the complement of {a, b, c, ...}, which is to say not(not-a and not-b and not-c and ...), is all that is a or b or c or ...
Call the union of something and the set containing that thing the successor of that thing. The successor of the empty set is thus the union of it and a set containing itself, which union is just a set containing the empty set, since the empty set contained nothing to begin with.
Thus the negation of the joint negation of the empty set and the set containing the empty set is the first successor.
And the empty set we call zero, and the successor to that set we call one. And thus are the first numbers.
And the successor to one we call two, and the successor to two we call three, and so on ad infinitum.
And thus the empty set and its successors are the natural numbers. And they are good.
----------------
(Suggested next steps: construction of addition from set operations, then multiplication; then subtraction, necessitating the construction of integers... and so on until we get up to SU(3)xSU(2)xU(1) or such, where the physicists can take over from the mathematicians).
Comments (149)
1. If you are aiming at some fundamental physics, such as QFT, that still leaves out every non-fundamental theory that is not reducible to fundamental physics - which means pretty much everything, from solid state physics to derivative trading. Now, it is plausible, though still controversial, that, to the extent that they are accurate, those "special sciences" supervene on fundamental physics. However, it looks ever more certain that they cannot be built from the ground up, the way you suggest - there will be a discontinuity where you have to jump from one level to another, with no analytical bridge between the two.
2. You realize that there isn't a unique construction, even for something as basic as the integers, right? Even with set theory there's more than one way to do it.
Interested in filling out parts of the story that I know.
Quoting SophistiCat
I was thinking about this issue. If we want to arrive at a general description of... well, everything maths oriented as it pertains to modelling physical systems with deterministic laws, we'd probably need to have extremely abstract foundations. The end result of that would look more like the nlab than an accessible thread on a philosophy forum.
So I propose that whoever wants to fill out parts of the story, we limit the scope and split it into a bunch of subtopics.
Set theory -> Definition Algebraic Structure (DAS) of the Naturals -> DAS Rationals -> DAS reals -> Analytic structure of the reals -> calculus of real functions -> differential equations -> specific examples of physical laws.
Linear algebra (if required) would fit somewhere after the DAS of the reals (the field construction and the vector space over a field construction).
That's a simplified version of the story that misses out a lot; like action formulations of physical laws, complex analysis and Hilbert spaces, which would limit the quantum parts of the story we can tell. We're also missing a more general structure for the calculus and analytic structure of the reals (need more general topological/differential geometric notions) that allow tensor equations to be written.
If you read the OP you’d see that that’s just the midpoint. We build up to something like QFT, and then build from there to something like a human. I’m not specifying the exact route we must take or how far we can go but that’s the rough idea.
Quoting SophistiCat
I always forget that even among physicalists the reducibility of everything to fundamental physics in contentious. So I suppose that’s another presumption of this thread, and the thread itself can serve as the debate on that, as players put forward constructions of higher levels from lower ones and others challenge the accuracy of those.
Quoting SophistiCat
That’s fine. Any construction will do.
An approachable simplified story is what I’m aiming for. Something like the version I tell of it in my essay On Logic and Mathematics, but hopefully better. (I’m hoping to learn from this thread myself). The construction of numbers, spaces, groups, manifolds, Lie groups, special unitary groups, and then quantum fields from those, particles from those, atoms from those, molecules from those, cells from those, organisms from those, etc.
I don't think you realise how big a project just getting to differential equations of real variables would be. It's a lot of work.
We should put the logic in the background then, except where it's completely necessary to go into it. I'm guessing that we'll need to set it up so that binary relations make sense; for equivalence relations in setting up algebraic operations on the rationals and reals and for order relations when we need the ordered field construction and the convergence/continuity/differentiability stuff that relies upon the completeness of the real line.
Buzz. Wrong. There's no universal set. Russell's paradox. You can't take the complement of the empt set except with respect to some given enclosing set.
The part you quoted isn't talking about taking the complement of the empty set specifically, it's just talking about how joint negation (NOR) is a sole sufficient operator: you can build all the other logical operators out of it. Specifically, in that post, I trivially build OR out of it, which as I understand it is the equivalent of union, which I use to build the successor function. The thought that we can start out with empty sets and joint negation and with that build everything out of "negations of nothing" (operations built out of negation on operands built out of empty sets) was the inspiration for this little game.
I could use a little clarification though, because as I understand it the logical operations are all equivalent to set operations, and as I understand it complement is the set-theoretic equivalent of negation, but negation isn't quite the same as joint negation though it can trivially be made to function as such (just feed an operand into both arguments of NOR instead of the single argument of NOT), so I'm not entirely sure if complement can be treated as the set-theoretic equivalent of joint negation too, or just plain unary negation, and in the latter case, what actually is the set-theoretic equivalent of joint negation?
So, we are going to build the Theory of Everything from scratch, starting from an empty virtual inference machine (VM).
Of course, we'd better load the propositional-logic language-extension pack, along with first-order extensions (universal quantifiers). Language must of course be "pluggable". Still, if we load the propositional-logic language extension pack, we must also load its axiom pack with the 14 basic rules of propositional logic. Language packs and axiomatic packs are not entirely independent.
(According to Wolfram, we also need to load a few first-order logic axioms too. Not sure, though.)
So, our two extension types are: language packs and axiom packs, i.e first-principle packs.
Not sure, though, that the elusive ToE is a first-order logic theory. We assume already quite a bit by saying a thing like that!
Ok. Now our VM can reason in first-order logic.
Quoting Pfhorrest
So, you have already decided that we are supposed to load something like the ZFC axiomatic extension pack?
In my intuition, I would rather load the PA number theory pack. It can certainly "see" everything that ZFC considers to be provable, but it does not trust quite a bit of it. I do not consider ZFC to be necessarily more powerful than PA. ZFC could just be more gullible!
Quoting Pfhorrest
Operator symbols must be mentioned in the language pack, but some of their invariants will have to be mentioned in the axiomatic pack. The other invariants can be derived. So, yes, do we load the logic operator rules from the logic pack or do we use a translation layer running on top of the ZFC pack?
Aren't we trying to rebuild Isabelle or Coq from scratch now?
It increasingly starts looking like an exercise in reinventing the wheel ... ;-)
Microsoft Research recently did exactly that. Apparently dissatisfied with Coq and Isabelle, they ended up concocting their own lean theorem prover. They probably consider Coq and Isabelle to be "bloated".
Still, myself, I have unlearned to give in to the temptation to rewrite from scratch. It is always a lot of work while the final result will probably end up being as bloated as the thing it was going to replace, once you add all the intricate bug fixes that may at first glance appear to be superfluous. If you don't know why all that shit is there, then unceremoniously stripping it away, is rarely the solution ...
To be clear, the contention isn't necessarily metaphysical. The prospects for Nagelian inter-theory reduction - the derivability of "phenomenological" theories from more "fundamental" ones - has been robustly challenged on mathematical grounds. See for instance Robert Batterman's Emergence, Singularities, and Symmetry Breaking (2010)
I'd be willing to contribute to a more modest, though still quite ambitious, project, where we go from say, sets to simple harmonic motion when we can handwave too arduous technical requirements.
I think I realized that a little later but didn't go back and update my post.
Quoting Pfhorrest
Ok so there is no complement of the empty set, but the negation of T is F and vice versa, is that what you mean? I think you want negation in a Boolean algebra, not in set theory at large, if you're trying to formalize negation. I'm not sure why NOR is important to you, it's somewhat obscure in logic although I believe it's more important in computer chip design. Or actually I'm probably thinking of NAND gates.
LOL I just checked it out on Wiki and it says, "The NOR operator is also known as Peirce's arrow ..."
That Peirce really gets around!
https://en.wikipedia.org/wiki/Logical_NOR
Someone else please check this because I don't trust alcontali's word on this for various reasons, and my understanding is that from set theory you can build predicate logic, which serves as an extension of propositional logic (anything you can say in propositional logic you can say in predicate logic), so if you start with sets you don't need to "manually" include propositional logic, it's one of the things you can build along the way.
Quoting fdrake
Yeah no this thread is not supposed to be demonstrating mathematicism, it's just assuming it, and as I said in the OP you can instead assume we're building a simulation of the universe instead, if that makes you more comfortable.
Quoting fdrake
Well the former is what I'm aiming for, but if you only want to play along up to the latter end that's fine with me. As I said in the OP, I expect mathematicians to contribute more to the first half of the project and scientists to contribute more to the latter half. (Or rather, people with extensive math and science knowledge, not necessarily professionals in such fields).
Also as I said in the OP, as I understand it QFT takes SU(3)xSU(2)xU(1) to be the mathematical model of quantum fields, which in turn are where we can stop with the math and pick up with sciences instead. So for the math segment of the game, we're aiming to build up to special unitary groups, for which we need Lie groups, for which we need both groups generally, and differentiable manifolds, for which we need topoligical spaces, for which we need points, and so on. I'm probably skipping a lot of steps along the way, but that's generally the course I'm expecting this to take to get to the point where physics can take over. Then from quantum fields we can build fundamental particles, build atoms out of those, molecules out of those, cells out of those, and so on. I thought I already sketched an expected trajectory like this in the OP.
Quoting fishfry
Because it's a sole sufficient operator. You can start with just that one operator and build all the others from there, so it's a great starting place. (NAND would work too, but I like the symmetry of starting with the empty set and joint negation). You can trivially build NOT(x) with NOR(x,x), then OR(x,y) with NOT(NOR(x,y)) and AND(x,y) with NOR(NOT(x),(NOT(y)), NAND(x,y) with NOT(AND(x,y)) obviously, IF(x,y) with OR(x,NOT(y)), ONLY-IF(x,y) with OR(y,NOT(x)), IFF(x,y) with AND(IF(x,y),ONLY-IF(x,y)), XOR with NOR(AND(x,y),NAND(x,y)), and so on...
Yes, predicate logic gets loaded automatically by first-order logic. I don't think it comes with a separate axiom pack. It is just additional language grammar. In my impression, the entire axiom pack of logic is already attached to propositional logic.
Quoting Pfhorrest
Yes, and anything you can say in predicate logic you can say in first-order logic, which is what you need for PA or ZFC. Predicate logic is not sufficient. You need the universal quantifiers too (again, supposedly language-only).
Quoting Pfhorrest
It would be fantastic if it were possible to derive the 14 axioms of propositional logic as theorems in ZFC, but I have not run into any documentation that confirms this or clarifies how to do that. I am absolutely not sure that it can be built along the way on top of ZFC. All documentation that I have seen up till now suggests that it is simply another, additional axiom pack.
You need logical symbols to state set axioms. You also need them for Peano arithmetic (and the Von Neumann version you presented in the OP). You don't have any tools to reason about sets without putting the reasoning system in the background - roughly, positing inference rules to output theorem statements from axiom statements.
With more rigour you need to specify a whole formal language to specify the logical connection of statements, typically a Hilbert system with first or second order quantification, AFAIK you only need first order to specify everything in the plan I posted up until you get to the analytic properties of the reals, in which case in the standard treatment you need second order quantification to axiomatise the completeness property of an ordering (quantifying over upper and lower bounds of a set is a second order logical statement).
Regardless, if you actually try to reason about objects in derived theories (like naturals from sets) using only the set and logical axioms, you'll find that the proofs for every statement get intolerably long, and at that point you switch to natural language and appeal to intuition (which is translatable to the inference rules if you do it right).
Quoting alcontali
Considering you need to axiomatise the behaviour of quantifiers to state ZF axioms (eg extensionality) or Peano axioms (eg the successor function being injective)... It's kinda redundant to start from sets then derive quantifiers (like for some being arbitrary disjunction over set elements, or for all being infinite conjunction over set elements).
The LEAN documentation (Microsoft Research) says that they fully support set theory but that their core axiomatization is actually dependent type theory:
Quoting LEAN on Dependent Type Theory
It is certainly not the first time that I see them switching to type theory in the context of proof assistants and theorem provers (Coq does that too), even though type theory is so much less straightforward (at a basic level) than set theory ...
This statement seems confused. First-order logic is a form of predicate logic: the first form of it, before you get to higher-order predicate logics. I think you may be confusing propositional logic with predicate logic.
In any case, you've both made the case that you at least need a quantification operation in addition to the truth-functional joint negation operation I started with, though since existential and universal quantification are DeMorgan duals of each other, you can start with just one (or its negation) and build all the others from that. So I guess to start with we need NOR (or NAND), and a quantifier (pick one; I would start with the negation of the existential, for aesthetic reasons, but logically it doesn't matter), and then we can say what a set is, and from the empty set proceed as previously described.
But the thread evolved into arguments of conceptual pontifications, it seems.
Why can't people just play along? People lost their child-like sense of play-dough. What I blame is an insidious ugly thing, called "maturity".
Well, since first-order logic is a predicate logic (extended by quantifiers), I did not mention predicate logic separately. All the axioms of logic, however, are (supposedly) already included at the level of propositional logic.
Wolfram insists, however, that first-order logic adds two new axiom schemata.
Quoting Wolfram on first-order logic
Do you know why this is needed? In my impression, these schemata are not mentioned in Wikipedia's page on first-order logic. I could not find other relevant documentation for this problem ...
By the way, Wolfram also describes first-order (predicate) logic as an extension to propositional logic. They do not see zeroth-order predicate logic as something that needs to be mentioned separately ...
No, we'll get to those eventually... if anybody actually plays the game instead of arguing about the premise of it. I mean, I can build you the integers, rationals, reals, and complex numbers in my next post if you like, though I'm not up to building arithmetic out of set operations alongside it, so I was hoping someone else would do that.
Quoting alcontali
I don't, and if I'm reading them correctly, they together contradict my understanding of predicate logic, wherein "for all x, F(x)" does not entail "there exists some x such that F(x)", but only "there does not exist any x such that not-F(x)". Which makes me think I'm not reading that passage correctly.
Quoting alcontali
According to Wikipedia, zeroth-order predicate logic is sometimes used as a synonym for propositional logic.
Well, I guess that we'll figure it out later. In the meanwhile, there's a bigger snag. The documentation (LEAN and Coq) suggests that we will regret using set theory as a foundation, because they went with type theory instead, even though all of type theory can be phrased as set-theoretical theorems. Any idea why? Is this just practical or so?
Don't know enough about type theory to comment.
Quoting Pfhorrest
Might as well start then. I'm largely going to assume that we can have a classical logic in the background with whatever rules we need (so it's non-constructive as in the usual way people do math), and proceed in the less formal manner of mathematical proof. If you want to try to translate the arguments into formally valid ones, give it a go, but you will almost certainly give up when you realise how insane it is to try and prove everything like in a logic textbook.
Beginnings - An Overview Of Some Of The Crap In The Background to Even Get Set Theory Going
Informally, sets are collections of objects.
When you start building up a mathematical theory axiomatically, unfortunately the word "informally" means "a miracle occurs" or "lots of abstractions are at work in the background to make what I'm saying true".
If you want to remove the miracles, the only recourse is formalisation; that is, to specify how to make a structure of elements you can reason about (like propositions), and specify the ways you can reason your way about in the structure (like rules of inference).
Underneath this is a question of the language that you're using - when you no longer take reason's intervention in language for granted, why should you be able to take the language itself for granted either? So you also need to be able to specify exactly the kind of symbols that you're using and how they relate, and what it means to be a statement.
This specification consists of two components:
(1) A formal language (a syntax).
(2) A way of providing interpretations of that formal language (a semantics).
A formal language is a formal system. It consists of a set of symbols that you define a grammar for. Like the symbols in logical arguments: [math]A \implies B[/math]. You stipulate a bunch of symbols and ways of combining them. The bunch of symbols are building blocks of the language. The ways of combining them are how you build things with them. The bunch of symbols in a language are called primitives, and the ways of combining and replacing them are called production rules.
When you have a formal language, you have a way of combining symbols with other symbols to produce valid formulas in the language. When you apply stipulated production rules to stipulated starting symbols, you end up with a well formed formula. If you mess up, you end up with something that is no longer part of the formal language. Drawing special emphasis - a formal language consists solely of well formed formulas, things which can be built from applying production rules to primitives.
If we have a language consisting solely of:
Symbols: A, B
Production Rules: (R1) Whenever you have a symbol, you can replace it with two copies of the symbol.
(R2) Whenever you have A, you can join B to its right.
(R3) Whenever you have B, you can join A to its right.
(A): We start with A.
We refer to the collection of all these things together as TOY.
We can make sequences of formulae like [math]A \rightarrow AA \rightarrow AAB[/math], which starts with A, applies R1, then applies R2 to the second A. But we can never produce BAA, why? Because the only way we can produce formulas requires that the first B is always to the right of the first A. The only way we can introduce a B is by joining it to the right of an A, and we can only start with A. BAA is then not a well formed formula of the language, whereas AAB is.
If we adjoined another rule (R4); that we can reverse any formula and obtain a new formula, we can now obtain BAA. What this highlights is that what counts as a well formed formula of a formal language depends entirely on how you set up the rules for the formal language; you can only get out consequences of what you put in.
For any sufficiently interesting formal system, there will be a gap between what counts as an element of the language and what is a derivable consequence. This is a distinction, roughly, between what is sayable and what is demonstrable. As may be obvious, to furnish this distinction we need a distinction between a well formed formula and a derivable consequence. This ultimately turns on there being a difference between how well formed formulae are produced and how consequences are derived; and this is fleshed out in a distinction between the formal language (like TOY, or the language of propositional logic) and a system of inference on its elements (to be introduced).
So we're going to talk about propositional logic now. Propositional logic has such a distinction; between its well formed formulae and its derivable consequences.
This sets out what it means for a formula to be well formed in propositional logic:
We need an alphabet of propositional symbols.
We need an alphabet of logical connectives on those propositional symbols - this is like negation, implication, and, or, xor and so on.
(1) Every element of the alphabet of propositional symbols is a well formed formula.
(2) If [math]x[/math] is a well formed formula, then [math]\lnot x[/math] is a well formed formula.
(3) If [math]x,y[/math] are well formed formulae, then [math]f(x,y)[/math] is a well formed formula, where [math]f(x,y)[/math] is any binary logical connective (like or or and).
Analogously to TOY, (1) gives us the set of starting points (any individual propositional symbol) and (2),(3) are the production rules.
Per @Pfhorrest's comment, if you want to be very conservative you can have a single binary logical connective in your domain - nor - and generate all the logical connectives. But from the perspective of building up the larger structures desired in this thread, such parsimony is not required or desirable (IMO anyway).
This is just like TOY, but the rules are different. Let's have an example: denote logical conjunction by [math]\cap[/math]. A sequence like we built in TOY goes:
[math]\displaystyle x \rightarrow \lnot x \rightarrow \lnot x \cap x[/math]
This starts with [math]x[/math], assumed to be a propositional symbol of the language which is thereby a well formed formula by rule (1), we then apply rule (2), we then apply rule (3) with conjunction and [math]x[/math]. This well formed formula is "x and not x". Perhaps why it is silly to require every step in a demonstration to be done explicitly with stated rules becomes obvious at this point; it is easy to construct things which are obviously well formed formulae:
[math]\displaystyle x \cap (y \implies x) \cap \lnot (x \implies (y \cup \lnot z))[/math]
where [math]\cup[/math] is logical disjunction, but demonstrating that this is so based off the rules is tedious and uninformative.
If someone wants to start talking about the inferential theory of propositional logic from here that would be fine, if not I'll make the post later.
I have accidentally run into a comment on this issue:
Quoting Wikipedia on type theory
It seems to suggest that your remark would be true for type theory but not for set theory.
People more familiar with the material will probably be trolled extremely hard by my cavalier attitude to equality and the formal status of arguments, but I hope that it provides enough of a flavour of logic to proceed from. I'm happy to receive comments/criticisms/corrections and rewrite things to be more formally valid, but only if the corrections don't sacrifice (or even improve!) the post being intuitive and introductory.
For a given formal language, we can construct the collection of all possible well formed formulae that can be produced from it. This collection of well formed formulae is the vocabulary with which we will express a system of inference on such a formal language.
For the propositional calculus, the set of well formed formulae is obtainable through the following rules:
An alphabet of propositional symbols.
An alphabet of logical connectives on those propositional symbols - this is like negation, implication, and, or, xor and so on.
(1) Every element of the alphabet of propositional symbols is a well formed formula.
(2) If [math]x[/math] is a well formed formula, then [math]\lnot x[/math] is a well formed formula.
(3) If [math]x,y[/math] are well formed formulae, then [math]f(x,y)[/math] is a well formed formula, where [math]f(x,y)[/math] is any binary logical connective (like or or and).
[math]\lnot[/math] is negation.
We want to augment this language with more rules of a different flavour; a more restrictive collection of ways of linking well formed formulae that embeds intuitions regarding demonstrating propositions given assumptions - deduction proper - rather than constructing new grammatically sound propositions based on old ones. We need to know more than the lexicology of a language to be able to reason using it.
To reason formally using a language, the first step is to formalise and stipulate the rules by which well formed formulas can be reasonably linked to others. These formalised stipulations embed intuitions about what a system of inference should be able to do.
What this entails is letting some variables range over the set of well formed formulas defined above, then stipulating linking statements between the variables using logical connectives. Stated abstractly, it isn't particularly intuitive, so I'll proceed with (some of one way of doing) the specifics for propositional calculus.
All of this is still spelling out the syntax language, so we're still discussing (1) in the previously linked post.
In an introductory symbolic logic class, you'll be introduced to a natural deduction system and asked to prove things in it. This is going to be a very abbreviated form of that.
We're going to introduce a few more rules that allow us to produce well formed formulas given other well formed formulas; except these encode inference rather than grammaticality, these are not an exhaustive list. Given that [math]x[/math] and [math]y[/math] are well formed formulae of the language of propositional calculus, we introduce some axioms to relate them inferentially.
(some) Inference Rules:
Conjunction (how [math]\cap[/math] "and/conjunction" works):
(CE1) [math]x \cap y[/math] lets us produce [math]x[/math]
(CE2) [math]x \cap y[/math] lets us produce [math]y[/math]
(CI) If we have [math]x[/math] and [math]y[/math], this lets us produce [math]x \cap y[/math].
These just say that if two things can be assumed together independently, this means that we can conclude each of the things independently from assuming them together. "There are 2 apples and 3 pears on this shopping list" therefore "there are 2 apples on this shopping list" and "there are 3 pears on this shopping list". These are called conjunction elimination (CE1 and CE2) and conjunction introduction (CI).
Modus ponens (how [math]\implies[/math], "implication" works):
(MP) If we have [math]x[/math] and we have [math]x \implies y[/math], then we can produce [math]y[/math].
This tells you that implication lets you transmit assumptions into conclusions whenever those assumptions imply those conclusions.
Now we have to introduce two symbols, [math]\top[/math] and [math]\perp[/math], which are logical constants (0th order logical connectives)... They will suspiciously resemble true and false respectively for good reason.
Disjunction (how [math]\cup[/math], "or/disjunction" works:
(DI) If we have [math]x[/math], we can produce [math]x \cup y[/math]
(DS) If we have [math]x \cup y[/math] and [math]x=\perp[/math], then we can produce [math]y[/math]
Informally - since we've not introduced truth or falsity as notions yet - the first says that if we know something is true, we know that either that thing is true or something else is true (which might be quite silly depending on the context, but it's fine here. "1+1=2 therefore 1+1=2 or Santa exists", it's rather artificial from the perspective of reasoning in natural language. The second says that if we know at least one of two things is true, and one of those things is false, then we know the other is true.
A common feature of all these rules is that they have an "if, then" form, given a bunch of inputs, we can produce (a bunch of) outputs. They are production rules that work on well formed formulae that capture a notion of inference. If we have a bunch of inputs [math]\Gamma[/math], and they let us produce the conclusion [math]\phi[/math], we write [math]\Gamma \vdash \phi[/math]. The distinct elements of the bunch of inputs will be separated with commas (and canny readers will probably notice that comma separation before [math]\vdash[/math] does exactly the same thing as making a conjunction of the separate elements).
As a sample of how to use this notation, we can write out some rules involving negation:
(DNE) [math] \lnot \lnot x \vdash x[/math]
(PBC) [math] x \implies \perp \vdash \lnot x[/math]
These say "not not x lets us produce x" and "if x implies the falsehood symbol, then we can produce not x". Rephrasing them (informally at this point) in terms of truth and falsity. If we know that not X is false, then X is true; this is double negation elimination (DNE). The second one says that if x implies a falsehood, we can conclude that x is false, this is proof by contradiction.
Some curious features of the formalism are that we don't need to stipulate anything at all to derive (anything which is equal to) [math]\top[/math], IE [math] \{\} \vdash \top[/math] (this is writing that there's no premises to the argument, and that the system derives the conclusion with no stipulations). And that if we start with (anything which is equal to) [math]\perp[/math] we can derive anything - [math]\perp \vdash x[/math]. Any statement which is provable from no assumptions is called a tautology (it is equivalent to [math]\top[/math] in some sense). The latter is called the principle of explosion.
Two examples of a proofs (using the stated axioms):
We want to show that [math]\perp \vdash x[/math].
(1) Assume [math]\perp[/math].
(2) [math]\perp \cup x[/math] (DI)
(3) [math]x[/math] (DS).
We want to show that [math]A \cap B, A \implies C, B \implies D \vdash C \cap D[/math]:
(1) [math]A[/math] (CE1)
(2) [math]B[/math] (CE2)
(3) [math]C[/math] (using [math]A \implies C[/math] and MP)
(4) [math]D[/math] (using [math]B \implies D[/math] and MP)
(5) [math]C \cap D[/math] (3,4, CI).
A canny and sufficiently pedantic reader will have noticed that in each of these proofs I've made assumptions, then used those assumptions to derive conclusions. This is called a conditional proof. But if we're being extremely pedantic about the foundations, even that can't be taken for granted (it either has to be some assumption of the system itself or provable from/about the system).
Formally, this looks like:
(CP) If we have that [math] \Gamma \cap x \vdash y[/math], then this means [math]\Gamma \vdash x \implies y[/math].
or
[math] x \vdash y[/math] implies [math] \{ \} \vdash x \implies y[/math].
This is called the deduction theorem, it's what's lets you link the ability to produce a well formed formula using the inference rules to the overall ability of the system to produce that well formed formula as a conclusion.
At this point, notice that there are four things kicking about in the discussion that look a lot like entailment:
(1) The rules that produce well formed formulae from other well formed formulae.
(2) The implication symbol internal to the formal language [math]\implies[/math]
(3) The statement that the rules that produce an inference from a set of assumptions [math]\vdash[/math]
(4) Some further sense of entailment that lets us say [math] x \vdash y[/math] implies [math] \{ \} \vdash x \implies y[/math], the middle "implies"; this is some 'meta theoretical' entailment, as it's entailment about the formal language under consideration.
All of these are formally distinct entities! They aren't the same thing and don't mean the same thing. But when reasoning about mathematical structures, so long as the context is sufficiently clear, we don't need to keep track of all the distinctions; when reasoning about objects that are sufficiently far removed from what spelling out reasoning even means, we don't have to pay so much attention to all the internal distinctions between entailment types.
But for now we do.
So far we've defined a collection of well formed formulas for propositional logic; then we've defined a bunch of ways of linking well formed formulas together. Now we're going to develop an idea of what it means for a well formed formula to be true or false. Truth and falsity are semantic properties; specifying how they behave over the well formed formulae of a language specifies the semantics of that language.
It's probably strange to consider all the things we've done so far as 'meaningless', insofar as they don't have any formal semantic properties, but nevertheless seem to behave quite a lot like how we reason logically. The trick here is that semantic properties of a formal language and system of inference rules on top of it is a different structure again: we need some way of interpreting what we've done so far.
[hide]I don't think it's a coincidence that the systems we use and study do indeed have tight relations between the syntax and the semantics, as does natural language (if you're not Chomskybot). We set things up in a formal language to the syntax and semantics relate well.[/hide]
An interpretation is just a mapping of well formed formulae to true or false. How a well formed formula of propositional logic is mapped to true or false completely determines the interpretation of that well formed formula. Interpretations in propositional logic are done truth functionally. If we have a well formed formula of logical connectives over propositional symbols, how that formula evaluates to True or False is completely determined by what happens when its propositional symbols are True (T) or False (F)
These are typically spelled out with truth tables for the primitive logical connectives. A truth table specifies the argument propositions on the left and the formula containing them on the right, the truth values on the left lead to the truth value of the well formed formula on the right. For example, [math]\cup[/math] and [math]\implies[/math].
[math]\begin{array}{c|c|c}A & B & A \cup B\\T &T&T\\T & F & T\\F& T & T\\F& F & F\end{array}[/math]
[math]\begin{array}{c|c|c}A & B & A \implies B\\T &T&T\\T & F & F\\F& T & T\\F& F & T\end{array}[/math]
The truth value of a complex formula is defined as the truth value obtained by iteratively evaluating all its logical connectives from the propositional symbols up. EG for [math](A \cup \lnot B) \implies (B \implies A)[/math], we set out all the combinations for [math]A,B[/math] evaluate [math]\lnot B[/math] as a function of [math]B[/math], then use that to evaluate [math]A \cup \lnot B[/math]. We then evaluate [math]B \implies A[/math] as a function of [math]B[/math] and [math]A[/math] and then finally the whole thing. If you do this as an exercise, you should see that it's always true.
Two well formed formulae are semantically equivalent when and only when they evaluate to the same truth value on every single assignment of truth values of their constituent propositions. A well formed formula which always evaluates as true is equivalent to [math]\top[/math], a well formed formula which always evaluates to false is equivalent to [math]\perp[/math].
A well formed formula which always evaluates as true is called a tautology, and if a collection of propositions linked by logical connectives - an element of the propositional logic [math]x[/math] - always evaluates as true under every truth value assignment, we write [math]{ } \vDash x[/math]. This is read "the system (propositional logic) semantically derives x". In contrast, [math]\vdash[/math] from the previous posts is read as "syntactically derives". This is a distinction between "if this is true then that is true" (semantic entailment) and "if this is produced then that is produced" (syntactic entailment).
I believe this is quite perverse, but I think it serves the point of hammering home the wedge driven between syntax and semantics which we're beginning to bridge; we can write:
[math]\begin{array}{c|c}\perp & F\end{array}[/math]
[math]\begin{array}{c|c}\top & T\end{array}[/math]
Since [math]\perp[/math] and [math]\top[/math] were syntactic elements, we still need to interpret them to true or false. Even though we've set them up to behave just like true and false, and to represent tautologies and necessary falsehoods when appropriate in the syntax, we still need to map them to their semantic analogues to complete the picture; that is, to provide a means of interpretation for all our well formed formulae.
It's easy to lose track of why the truth tables were introduced; so I'll spend some more words on it. When we're setting up a logic, we want to ensure that if we what we assume is true, what we can produce from it is true. "What we assume" is a well formed formula, "is true" is stipulated by assuming it, "what we can produce from it" are the inference rules applied to the well formed formula. It would be nice if all these notions coincided, but it is not guaranteed to hold.
So it is an open question, given the interpretation of symbols, whether we can produce all and only true well formed formulae given the use of the inference rules. The constructions are quite different, no? We have a bunch of rules that produce well formed formulae, and we have a way of assigning truth values to well formed formulae - do the inference rules play well with the truth value assignment? What are the relations between syntactic and semantic derivation in a logic?
These are important questions to answer for a logic. The possible gap between what is true statement of the system - the well formed formulae which evaluate as true - and what well formed formulae the system can produce through the inference rules is the site of the famous incompleteness theorems. This gap is closed by a few properties, soundness, completeness, consistency, compactness and decidability which are necessary for a logic to behave in all the ways we pre-theoretically expect, but famously completeness and consistency together are guaranteed not to hold for almost all mathematical structures of interest (with a classical logic).
To discuss these issues in more depth, we need to introduce the idea of a model and relate it to the truth value assignments. The idea of a model of a system of axioms and inference rules will turn out to be how we can turn a constructed object in the language into an object that behaves how we specify with the specification of axioms (using the inference rules).
But I haven't been following the discussion and you may be into something else.
Thanks, fixed.
The presentation is very non-standard. If and when you've read it I'd appreciate you pointing out flaws and errors as I'm mostly winging it but checking sources to make sure I'm not doing something completely insane.
The one bit I'm already skeptical about is putting in syntactic copies of contradiction and tautology as logical connectives (of 0th order, constants), then feeding them into the semantics to get false and true. I don't think it does anything to the overall logic, despite being redundant. The only place I've used the syntactic copy of the falsehood symbol is in presenting the disjunctive syllogism as an axiom (I think I've seen this somewhere before, Gentzen?).
I'm trying to stress in the presentation that there are a lot of ways to end up in the same place, so I've not defined a system with primitive logical connectives, just let them be whatever.
I'm a lot less competent on the details for quantifiers, so I expect to write many more batshit insaanities if I end up writing that bit.
I remember my logic professor telling us about the Scheffer stroke, which can be used to define all the other logical operations. It's equivalent to NAND. So NAND is as good as NOR for your purposes. But isn't it mostly a curiosity? We can define all the other logical relations in terms of a single one. Ok. But why make it a focus of interest?
I think it's a fetish for parsimony. I vaguely recall that having a single logical connective simplifies proofs and the well formed formulae definitions (you just nand or nor stuff). But I think that this is more relevant if you're ball deep proving things about formal logics than providing an overview of them.
Would appreciate it, if you've read what I've written, to point out bullshit where I've said it.
you’ve built all the other connectives, it’s just part of the game to show that you can start with just NOT and don’t need to start with anything else as given.
Feel free to intervene in the bits I've written to add further detail if you like.
Quoting Pfhorrest
Define the hand wave operator H as a function on the cartesian product of the axiom set of a formal system with its theory... The language with the hand wave operator is equivalent to the language without the hand wave operator when and only when for all axioms A and for all theorems B H(A,B) is true when and only when the system has A implies B as a tautology...
Will do once I have time to read them. When I’m away from home I only have brief moment like bathroom breaks to read and write short things like this.
Fair. Would you be interested in doing the more detailed version I had in mind?
Quoting Pfhorrest
It is likely that we imagine different things by rigorous proof. To me, what I've written is still highly informal and suggestive.
I agree.
I would be very interested in reading it, but I doubt I have the competence to contribute to it.
I'm afraid I won't be of much help in developing the detailed aspects of your game. Russell and Whitehead began their Universe of Discourse with Set Theory as the foundation of Logic, but ended-up running into the impassible boundary (incompleteness theorem) of space-time limitations.
So, in the interest of surpassing that inherent constraint on human reasoning, I'd recommend starting with something that transcends the actual Universe, such as the Greek notion of LOGOS. Of course, our knowledge of Logos is limited to imaginary abstractions such as the concepts of Eternity and Infinity. But, at least, the game will acknowledge that the game-board has its limitations. So that all moves will be <= ?. :nerd:
Logicism failed, but set theory is nevertheless the foundations of contemporary mathematics. That's not identical with logicism.
I wasn't referring to the Logicism of Analytic philosophy, but to the Greek notion that there is some absolute Truth, equivalent to Ideal Proportions, which can be expressed mathematically in ratios. I don't know how that might apply to your forum game, except to serve as an ideal goal, approachable but never attainable --- I.e. asymptotic to infinity. It's a barrier, but it also leaves a lot of room for experimentation.
PS___Sorry to butt-in with irrelevant comments. But I had been thinking about the relationship of Logic to Math. My personal pragmatic definition of philosophical Logic has been "mathematics with words". Which means that it is less pure & abstract & absolute. So, maybe the Greek Logos was actually referring to the mathematics of Proportion (e.g. positive vs negative; good vs evil), and its association with human language is secondary. I'll leave you alone now. :yikes:
To discuss these questions with a bit more detail, we need the notion of a theory. A theory is just the collection of derivable consequences from a stipulated set of rules; the collection of all theorems; derivable consequences; of the language. Notably, a theory is closed under the application of the inference rules to its constituents - this means that you can't get extra consequences by applying the inference rules to something which we call a theory.
Accompanying the notion of a theory is the notion of a model; a model of a theory (or of a collection of stipulated well formed formulae and rules) is a collection of objects in which every element of the theory interprets as true.
EG if we have the rule "every element of a set has to have a strictly bigger element", any finite set violates the rule and so is not a model. If we have the rule [math]A \implies B[/math], a model of that formula has [math]A[/math] false and [math]B[/math] true, or [math]A[/math] true and [math]B[/math] true. Models typically are not unique.
In propositional logic, a model of a formula is just a row of a truth table under which that formula evaluates as true; assignments of truth/falsity to the proposition which make it true. A model of a collection of formulae is an assignment of truth/falsity to propositions which make them all true.
This lets us restate some things: eg [math]\vDash x[/math] occurs when every model of propositional logic has [math]x[/math] evaluate as true; that is, [math]\vDash x[/math] denotes a semantic tautology - something which is necessarily true.
(Soundness) If a well formed formula can be produced through syntactic operations without stipulating any assumptions, is it the case that the semantics will always evaluate such a statement as true? Stated more briefly, is every theorem (syntax) of the system a tautology (semantics) of the system? If something is provable, is therefore true? When this property holds of the logic, it is called sound.
This can be written [math]\Gamma \vdash x[/math] implies [math]\Gamma \vDash x[/math].
Propositional logic is sound.
(Completeness) If a well formed formula always evaluates as true under every possible assignment of truth values (semantics) to its propositions, is it the case that the system can derive the formula using its rules of inference (syntax)? If something is true, is it therefore provable? When this property holds of the logic, it is called complete.
This can be written [math]\Gamma \vDash x[/math] implies [math]\Gamma \vdash x[/math].
Propositional logic is complete.
(Consistency) If a collection of well formed formulae can all be true at the same time, then that collection is called consistent. If the theory of a system of inference is consistent, then that theory is consistent.
This can be written: not [math]\Gamma \vDash \perp[/math] where [math]\Gamma[/math] is a theory. Conversely, inconsistency says "no model exists for this theory", and "its elements can't be jointly true together/satisfied".
Propositional logic is consistent.
(Decidability) Does an algorithm exist that lets you check whether an arbitrary well formed formula of propositional logic belongs to the theory of propositional logic?
Propositional logic is decidable.
These are all nice properties to have, but we still couldn't write an argument like:
"Every number has a square, therefore two has a square".
We're missing quantifiers, and just by introducing them we gain a lot of expressive power but lose decidability in almost every context of interest for mathematical reasoning. We also complicate the idea of a model; "every natural number has a square" must range over infinite collections - the truth table method of checking whether something is a tautology just won't work any more.
2 has a prime factor.
3 has a prime factor.
...
We'd need to do that infinitely many times. This would mean we would need to write down infinitely many statements to formalise extremely elementary properties of numbers. Also, within the statement "has a prime factor" there is another subtlety: a prime factor of a number is a number that is prime that divides the number. IE, "has a prime factor" means "there is some number which is prime that divides the number".
The device which implements the "every number" part of "every number greater than 1 has a prime factor" is called the universal quantifier, written [math]\forall[/math] and read "for all". The device which implements the "there is some number" part of the statement is called the existential quantifier, written [math]\exists[/math] and read "for some" or "there exists".
There's another element of that statement which we could not render without additional vocabulary; a number being prime, or having a prime factor, is a property of some number. Moreover, say, 12 having 3 as a prime factor is a relation between 12 and 3. Propositional calculus alone does not have the resources to talk about properties or relations, so we need to augment the language with resources for that. We'd like to be able to have a condensed notation that reads "12 has 3 as a prime factor" and "3 is prime" and so on. The latter might be written as [math]P(3)[/math], the former might be written as [math]PF(12,3)[/math]. Generally, these are called predicates; properties, relations, functions and so on.
This means the extra principles that need to be added to propositional logic to be able to implement these kinds of statements are:
(1) Quantifiers, [math]\forall,\exists[/math]
(2) Predicates: properties, relations, functions etc.
In addition we would like to be able to have all of propositional calculus as valid formulae of whatever language we set up. So this gives us:
Predicate logic = Propositional logic + quantifiers + predicates.
These are required changes in the syntax, and they will induce changes in the semantics appropriate for them. EG: we can't just evaluate a truth table to see if "Every number has a prime factor" is true.
So we need to specify what the building blocks (called terms) of predicate logic are:
(T1) An alphabet of symbols; here called variables. Every variable is a term. EG, x,y
(T2) Functions on those symbols: eg, if x and y are variables, then P(x,y) is a term. This holds for every function independent of the number of things that go into it, eg Q(x,y,z)... All of these function expressions are terms. Functions without any arguments are called constants, and these are also terms.
[hide]It helps to throw in functions into the terms to make it so that function evaluations can have predicates applied to them without applying predicates to predicates. Helps in the sense of keeping the theory first order.[/hide]
Functions take terms and map them to other terms. They are like replacement rules in in the first post. They take an input and produce an output. EG the function defined by [math]f(x)=t[/math] takes any input [math]x[/math] and produces the term [math]t[/math].
These define the objects of the theory of predicate calculus; the alphabet which its well formed formulae will be written with.
On top of these term notions we need well formed formulae notions; ways of producing well formed formulae given other well formed formulae, like with propositional logic and TOY in the first post.
(W1) If [math]P[/math] is a predicate, then [math]P[/math] of it arguments is a well formed formula. EG if P is "is prime" and x is "2" then P(x) is a well formed formula. EG if D is "divides" and x is 2 and y is 4, D(x,y) is "2 divides 4". As before, D(y,x) is also a well formed formula, it just happens to be false.
(W2) If [math]x[/math] and [math]y[/math] are terms, then [math]x=y[/math] is a well formed formula.
(W3) If [math]x[/math] is a well formed formula, so is [math]\lnot x[/math].
(W4) If [math]f[/math] is a binary connective and [math]x[/math] and [math]y[/math] are well formed formulae, then [math]f(x,y)[/math] is a well formed formulae.
(W5) If [math]g[/math] is a formula and [math]x[/math] is a variable in it, then [math]\forall x g[/math] and [math]\exists x g[/math] are well formed formulae.
These set out the basic grammar; the rules of well formed formula production in predicate logic. An example sequence of produced well formed formulae is:
[math]x=y \rightarrow \forall x (x=y) \rightarrow \exists y \forall x (x=y) \rightarrow ( \exists y \forall x (x=y) )\cup (x=y)[/math]
Where x and y are terms. This uses W2, then W5, then W5, then W4 with [math]\cup[/math] for logical disjunction.
Function terms let us write things like:
[math]\forall x L(x,f(x))[/math]
For things like "every number x is less than f(x)=x+1" with L(x,f(x)) being x is less than f(x).
Note; the only things which can be quantified over to produce well formed formulae are variables in formulae, not predicates or function symbols. This is what makes the predicate logic first order; first order means quantification only over terms (term symbols), not over predicates applied to terms (predicate symbols).
EG: "All colours are sensory properties of objects" is not a first order statement, since colours are properties. Whereas "all natural numbers have at least one number which is larger than them" is a first order statement, as the "all" works on natural numbers and the "at least" also works on natural numbers.
It remains, again, to build a system of inference on top of these grammatical rules of the formal language.
What kind of math is this and who did you learn it from
Asking for a friend lol
Thanks for the continuing posts! Haven't found time to read them yet but I hope to soon.
I'm a mathematician who studied a decent amount of logic. The material I've presented here is recapitulating stuff from 2 undergraduate courses in logic. I've checked Stanford Encyclopedia of Philosophy, the Internet Encyclopedia of Philosophy and Wikipedia on what I've written to make sure what I've written isn't completely insane.
Your friend might want to study "natural deduction", "first order logic" and "formal languages".
(1)"Every number has a prime factor"
[math]\forall n \exists x : (x|n) \& P(x)[/math]
where | is "divides" and P is "is prime" and & is conjunction.
(2)"There is no largest prime"
[math]\forall p \exists q: q\gt p[/math]
where p and q are prime numbers and [math]\gt[/math] is greater than.
(3)"Every fraction can be multiplied by some other fraction to obtain the number 1 and that fraction is unique"
[math]\forall x \exists y : (x \times y = 1 \hphantom{...} \& \hphantom{...} \forall z : x \times z = 1 \implies z=y)[/math]
where x is a fraction, y is some other fraction, [math]x \times y[/math] is a function term which corresponds to multiplication.
(4) "If a is on the same landmass as b, and b is on the same landmass as c, then a is on the same landmass as c"
[math]\forall a \forall b \forall c:\hphantom{...}R(a,b) \& R(b,c) \implies R(a,c)[/math]
(5)"[math]\forall a \forall b \forall c:a \times (b+c) = a\times b + a\times c[/math]"
(the distributive law of multiplication and addition).
[hide]equality, [math]=[/math] is assumed to just be part of the logic, it occurs when the term on the left and the term on the right are different names for the same term, or the term itself like in [math]x=x[/math] or [math]f(x,g(x)) = f(x, g(x))[/hide]
One trick here is that things like [math]+,-,\times[/math] above are functions; f(x,y) = x+y, if you input x and input y, you get x+y out, so f(1,2)=1+2=3. Subtraction and multiplication work similarly. All the elementary operations in mathematics can be inputted into a first order language as function symbols of their argument terms, and their output interpreted as another term!
Within the above statements, there is an implicitly assumed domain in the background and an implicitly assumed interpretation of the function and predicate symbols.
Regarding the domains: in the first statement, the domain is the numbers 1,2,3,4... . In the second statement, the domain is the primes 2,3,5,7,... . In the third statement, the domain is the fractions. In the fourth statement, the domain is the landmasses (of Earth). In the fifth statement, the domain is something like the naturals or fractions or reals where multiplication and addition interact.
Regarding the function and predicate symbols: in each of these cases, the formal language requires extra symbols to augment the domain with to make sense of the statement. In the first, we add a binary predicate (relation) symbol | for "divides" and a unary predicate (property) symbol P for "is prime". In the second we add a relation symbol [math]\gt[/math] for "greater than". In the third we add the multiplication symbol [math]\times[/math]. In the fourth we add the relation symbol [math]R[/math]. In the fifth we add the multiplication symbol [math]\times[/math] and the addition symbol [math]+[/math].
All of these contexts are very different, but first order logic lets you express things about all of them. In that regard, we need to pay attention to precisely what we're talking about; what domain of discourse and predicates and functions make sense on it, and how those predicates and functions interact. And in terms of formalisation, set out exactly what we're talking about to begin with; have an interpretation in mind, an intended semantics.
[hide]"intended semantics" is not a standard term, though by it I mean intended interpretation. As we saw with the rows of truth tables, it is quite rare that models that satisfy our stipulations are unique, and the same holds for first order theories.[/hide]
Due to the expressive power of the predicate symbols and function symbols, we can posit much different structures depending on what predicate symbols and function symbols we augment the domain with. For an example, consider the natural numbers equipped with addition; the only statements which make sense in this context are natural numbers added together and equations between sums of natural numbers. Like 5+2=3+4=7, or "if 5+2 = 3+4 and 3+4 = 7, then 5+2=7", but no statements including multiplication.
If we then add multiplication to this "natural numbers with addition" structure, we can start talking about equations involving addition and multiplication.
This is to say, while in propositional logic, the system of inference (the theories of propositional logic) depended entirely on the logical structure of argument (the valid ways of using logical connectives between elements of he domain), the theories of first order logic depend on stipulated rules of functions and predicates as well as the rules of propositional logic + quantifier rules.
A propositional logic argument, modus ponens, detailed here goes like:
[math]P \implies Q, \hphantom{..} P \vdash Q[/math]
"If P then Q, P, therefore Q"
Much the same thing in predicate logic is:
[math]P(x) \implies Q(x), \phantom{..} P(x) \vdash Q(x)[/math]
"If P holds of x this implies Q holds of x, P holds of x, therefore Q holds of x".
Similar structures apply for conjunction, disjunction etc:
EG:
(Conjunction Elimination) [math] P(x) \cap Q(x) \vdash P(x)[/math] and [math] P(x) \cap Q(x) \vdash Q(x)[/math]
(Disjunction) [math] P(x) \cup Q(x)[/math] implies [math]P(x) \cup Q(x) \vdash P(x)[/math] or [math]P(x) \cup Q(x) \vdash Q(x)[/math]
[hide]The logical connectives range over well formed formulae as arguments, rather than just predicates applied to x, but the same behaviour applies - the logical connectives work for arbitrarily complicated formulae, eg:
[math]\forall x \exists y P(x,y) \cap \forall x \exists y \forall z Q(x,y,z) \vdash \forall x \exists y \forall z Q(x,y,z)[/math] and so on[/hide]
where [math]\vdash[/math] works as before (but now with the well formed formulae of first order predicate logic).
There are also rules for quantifiers: universal instantiation and universal introduction - which define how for all [math]\forall[/math] works and existential instantiation and existential introduction - which define how [math]\exists[/math] works, these read:
[math]\forall[/math]
(Universal instantiation) For every well formed formula [math] \phi [/math], [math]\forall x :\phi x \vdash \phi c[/math] for every [math]c[/math] in the domain. This says "if a statement holds of everything, it holds of each particular thing".
(Universal introduction) If for the well formed formula [math]\phi [/math] involving arbitrary variable [math]x[/math] holds/is stipulated , then [math]\forall x :\phi x[/math]
This says "if a statement holds of each particular thing/an arbitrary thing, then it holds for everything".
[math]\exists[/math]
(Existential instantiation) If [math]\exists x: \phi x[/math] then in particular [math]\phi c[/math] for some c in the domain. This reads "if a thing holds of something in the domain, it (at least) holds of a particular we can label as c".
(Existential introduction) If for some constant element of the domain [math] c[/math] some well formed formula [math]\phi[/math] holds/is stipulated, then [math]\exists x: \phi x[/math] holds, where x is a variable. This says "if something holds of a specified particular thing, it holds of something in general".
The rules for quantifiers also include two descriptive notions which are important; free and bound variables. A variable occurrence is bound in a well formed formula if some quantifier acts on it in that well formed formula and free otherwise. EG
[math]P(x) \implies Q(x)[/math] has [math]x[/math] free.
[math](\forall x P(x) ) \implies Q(x)[/math] has [math]x[/math] bound in the first part and free in the second.
[math]\forall x (P(x) \implies Q(x))[/math] has [math]x[/math] bound alone.
Only well formed formulas where every variable is bound can evaluate unambiguously to true or false; otherwise they depend on the variables instantiating the claim. Well formed formulae solely involving constants need not be bound in this manner to be true or false. EG:
[hide]Well, constants can't be quantified over, formally speaking anyway, only variables can be.[/hide]
"Socrates is a man" is true when speaking of philosophers since Socrates is a fixed term of the domain of philosophers and is a man.
"x is a man" might be true or false when speaking of philosophers, because x might be Elisabeth Anscombe who is a fixed term of the domain of philosophers and is a woman. In this case x is free.
"There exists an x such that x is a man" is true when speaking of philosophers because (at least) Socrates exists. In this case x is bound.
"Every x is a man" is false when speaking of philosophers because (at least) Elizabeth Anscombe exists In this case x is bound.
Expressions involving constants and variables at the same time are common, eg:
"For all natural numbers x, if x is even and x is prime then x = 2"
the constant 2 shows up, the variable x shows up, the predicate symbols "is even" and "is prime" show up, all variables are bound so this statement is either true or false, and it turns out to be true since 2 is the only even prime.
Given all this, we can weave the inference rules (this post) and the predicate/function behaviour together to start talking about formal semantics of first order logic; theories and models of stipulated function/predicate rules.
This is, finally, when we get to start talking about axiomatic systems like the Peano Arithmetic and ZF( C ).
I'm one who hasn't. Complex analysis here. And you? :cool:
Statistics! This is all very pure for me.
I think maybe you meant to write “inconsistency” there?
Fixed, thank you.
Last post we saw that the overall behaviour of a first order theory depends on the function symbols and predicate symbols and their stipulated relationships; eg how the natural numbers work with addition alone vs how the natural numbers work with multiplication alone; and in this regard, all the function symbols and predicate symbols need to have an interpretation.
To set out the building blocks of a first order theory, a device called a signature is used. A signature has the following symbolic components:
SYMBOLS (SIGNATURE, SYNTAX)
(SIGNATURE 1) A collection of constant symbols.
(SIGNATURE 2) A collection of function symbols
(SIGNATURE 3) A collection of predicate symbols..
Everything which goes into the syntax of a first order theory is a labelled element of a signature, except for the assumed logical connectives, quantifiers and variable symbols. We can also stipulate behaviour for the constants, functions and predicates.
An example is:
[math]\{\mathbb{N},+\}[/math]
which has the set symbolised with [math]\mathbb{N}[/math] of constants (which are intended to be natural numbers) and the function symbol [math]+[/math] (which is intended to be addition). If we stipulate that the set is the natural numbers and + is addition - assigning the symbols with their usual meaning - this becomes the usual natural numbers we're familiar with and the usual addition we're familiar with and we can write things like 1+1=2 in the language. Such an assignment is how a first order formal language obtains a syntax!
MEANING (ASSIGNMENT, SEMANTICS)
(ASSIGNMENT 1) A collection of constants - called the domain.
(ASSIGNMENT 2) A collection of functions - called functions on the domain.
(ASSIGNMENT 3) A collection of predicates - called predicates on the domain.
Variable symbols can also be included, but behave differently.
An interpretation of a first order theory takes each element of the signature (SYMBOLS) and associates it uniquely (assigns it) with a part of the assignment. Constants symbols go to constants, variable symbols go to a range of constants, function symbols go to functions, predicate symbols go to predicates.
All an interpretation of a first order theory does is associate all the parts of the signature list to a unique part of the assignment list. Note that there are variable symbols but no part of the signature has variables in it, so variables require a slightly different treatment.
The distinguishing feature of variables is that they can be reassigned to other constants. This range of assignments is what makes them variable. Their labels don't matter very much. EG "For all natural x, x is either prime or composite" means just the same thing as "For all natural a, a is either prime or composite". For any formula, you can replace a variable label with another variable label and not change the meaning of the formula so long as the variables belong to exactly the same object. EG, "for all a, a is either prime or composite" might be false if for some reason we've specified that the symbol a must be a fraction. The intuition this embodies relates to the basic behaviour of the two quantifies:
(1) For some x P(x) is true when and only when we can assign x to some value a and P(a) is true.
(2) For all x P(x) is true when and only when all assignments of x have P(x) as true.
The difference between variables and constants, then, is that variables are defined relative to their ability to be reassigned other elements of the domain and constants cannot be reassigned. The number 2 is the number 2 is the number 2, the number x is... well whatever x could be. The only important thing for using variables appropriately is to use them consistently once you've introduced them.
Setting out how variables, constants, functions and predicate SYMBOLS associate with the ASSIGNMENT list sets out what variables, constants, functions and predicates mean in the language! And once we've set up what they all mean; once we've assigned all the (non-variable) symbols to a unique part of the signature; we can begin looking at what is true and what is false in the language.
Consider the domain:
FOODWEB={grass, sheep, wolves}
we are going to assign these words to their usual meanings; grass, sheep, wolves.
And the relation "eats" as it applies to FOODWEB.
sheep eat grass
wolves eat sheep
We can characterise the relation "eats" as the collection of pairs:
{sheep, grass}, read "sheep eat grass"
and
{wolves, sheep}, read "wolves eat sheep"
We then collect all the pairs into a single object:
{ {sheep, grass}, {wolves, sheep} }
This is what we assign to "eats" to flesh out its meaning.
So the assignment of "eats" is { {sheep, grass}, {wolves, sheep} }.
The signature is then {FOODWEB, eats}
FOODWEB is assigned to {grass, sheep, wolves}
eats is assigned to { {sheep, grass}, {wolves, sheep} }
We can prove theorems about FOODWEB now.
Theorem: "nothing eats wolves"
Proof: Let x be in FOODWEB, then x is grass or x is sheep or x is wolves (definition of FOODWEB)
A (Disjunct 1) Assume x is grass, then x does not eat wolves (definition of eats)
B (Disjunct 2) Assume x is sheep, then x does not eat wolves (definition of eats)
C (Disjunct 3) Assume x is wolves, then x does not eat wolves (definition of eats)
D (Disjunction Elimination) Then x does not eat wolves (disjunction elimination/proof by cases). (using lines A,B,C).
E (UI) Since x was arbitrary, then for all x, x does not eat wolves (line D, universal introduction/universal generalisation, introduced in thread here).
What this shows is that {FOODWEB,eats} [math]\vDash[/math] "nothing eats wolves".
In this case, the entailment is semantic because it follows from the assignment (and the logic rules assumed in the background).
We could turn question around: "find a signature and an assignment in which nothing eats wolves is satisfied", and in that case we find that {FOODWEB, eats} with the above assignment works. This is how models work for first order logic - {FOODWEB, eats} models the claim "nothing eats wolves".
There are other domains and assignments that satisfy this! {grass, wolves}, {sheep, wolves}, {vegetarians, sheep}... with the usual meaning of "eats". It is rare that if we start off with the theorems we'd like, that there is a unique model which satisfies the theorems.
Logicism did not fail. It just hasn't achieved its goals.
Logicism would have "failed" if someone had provided proof that the 10 axioms of ZFC set theory (or even the 9 axioms of PA number theory) cannot possibly be derived from the 14 axioms of propositional logic. I have never seen such proof.
It would have "succeeded" if they had successfully been able to build set theory (and/or number theory) as a dependency inside logic theory. They haven't been able to do that either.
Therefore, the status of logicism is not "failed" nor "succeeded", but "undecidable".
Properties are assigned to lists. EG: "even" = {0,2,4,6,8,...}
Relations are assigned to lists of pairs: EG: "eats" from the last post.
...
Restating something: properties and relations are predicates. Predicates are assigned a number called an arity, which tells you how many things go into them. Properties have arity 1, relations have arity 2. Predicate logic allows you to deal with predicates of arbitrary arity.
Properties are assigned to lists of single objects (arity 1 predicate, list of single elements)
Relations are assigned to lists of pairs (arity 2 predicate, list of paired elements)
This pattern continues indefinitely.
Properties are assigned to lists of single objects (arity 1 predicate, list of single elements)
Relations are assigned to lists of pairs (arity 2 predicate, list of paired elements)
Predicates with arity three are assigned to lists of triples (arity 3 predicate, list of triples)
Predicates with arity x are assigned to lists of x-tuplets (arity x predicate, list of elements of length x).
Functions are constructed similarly.
The function f(x)=x+1 on the natural numbers is exhaustively determined by the list:
1->2
2->3
3->4
...
n->n+1
...
This can be rewritten as the list of pairs
{1,2}
{2,3}
{3,4}
...
{n,n+1}
...
And then aggregated into a single object as with predicates
{ {1,2}, {2,3}, {3,4}, ... , {n,n+1}, ... }
A function of two arguments: f(x,y) = x+y works like
(1,2)->1+2->3
(3,4)->3+4->7
...
Equivalently
{1,2} -> 3
{3,4} -> 7
...
Which is rewritten as:
{1,2,3}
{3,4,7}
...
The number of arguments a function has is also called its arity. A function of arity n is associated with a list of elements of length n+1, representing the n inputs in order and then the output as the last element.
It is convenient to have a structure which compiles all the objects types: "lists of single elements", "list of pairs", "list of triples", ... , "list of x-tuples" together. This is called a Cartesian product [hide](most generally a product object[/hide].
A list of pairs of all pairs of elements from a domain [math]U[/math] is written as the Cartesian product [math] U \times U[/math].
A list of all triples of elements from a domain [math]U[/math] is written as the Cartesian product [math]U \times U \times U[/math].
And so on.
Generally:
A predicate [math]P[/math] of arity [math]k[/math] on a domain [math]U[/math] must be assigned to some subset (sub-list, some part) of the Cartesian product of [math]U[/math] with itself [math]k[/math] times.
Functions are similar, but more constrained:
A function [math]f[/math] of arity [math]k[/math] on a domain [math]U[/math] must be assigned to some subset (sub-list, some part) of the Cartesian product of [math]U[/math] with itself [math]\mathbf{k+1}[/math] times. Additionally this subset must satisfy the property that each element of [math]U[/math] Cartesian product-ed with itself [math]k[/math] times occurs once in the subset (every input list must produce a unique output - a unique term of [math]U[/math]).
(Technical reason) Without that restriction, a term could transform into a collection of terms, and a statement like [math]\forall x: x \lt f(x)[/math] would both require a lot more effort to make sense of (what would it mean for a number to be less than a collection of numbers, say?) and "for all x, x < (some set)(x)" is equivalent (I think) to quantifying over a predicate (a collection of domain items dependent on x) - it breaks the first order-ness of the theory.
(Expressive reason) It means that you have a way of describing ways of transforming a term into another term. To reiterate: you can describe properties and relations of ways of transforming terms into other terms. These are incredibly important ideas, functions let you talk about change and transformation, in addition to relation and property. The concepts this allows the logic to express are much broader.
Signatures also let us stipulate properties (strictly: well formed formulae that can be true involving) their constituent elements (domain elements, functions, predicates), EG, if we have [math]\{\mathbb{N},+,\times\}[/math] (have in mind "natural numbers when you can add them and multiply them and nothing else"), we can stipulate that [math]+[/math] and [math]\times[/math] obey:
[math]\forall x \forall y \forall z : x \times (y+z) = x \times y + x \times z[/math], which is the (left) distributive law.
Stipulating the distributive law lets you derive this as a theorem:
[math](a+b)\times (c+d) = a\times (c+d) + b \times (c+d) = a \times c + a \times d + b \times c + b \times d[/math]
The first and second equalities follow from the distributive law. This is, hopefully, the familiar FOIL (firsts, outsides, insides last) or "smiley face" method of multiplying binomials together from high school algebra.
This can be written formally as [math]\{\mathbb{N},+,\times\} \vdash \\ \forall a \forall b \forall c \forall d : (a+b)\times (c+d) = a \times c + a \times d + b \times c + b \times d[/math]
when [math]+,\times[/math] are understood as obeying the distributive law.
Usually the signature and the axioms which define the properties and relations of its predicates and functions will be the intended meaning of just writing down the signature. This is a notational convenience, it does no harm. We could introduce an extra list of axioms for the operations and add them to the signature (analogous to building a system of inference over well formed formula production rules), but usually in other areas of mathematics this is omitted.
When you leave this regime of mathematical logic it is extremely convenient to just assume that whenever we write down a signature, we implicitly give it its intended interpretation. This specifies the structure of interest for mathematical investigations/theorem proving in terms of what can be proved and what we hold to be true, but it does not block people from analysing other models; called non-standard models; of the same signature.
Because of the waning relevance of the distinction between syntax and semantics for our purposes, I am not going to go into all the formal details of linking an arbitrary signature to an arbitrary interpretation; but I will state some general things about models to conclude, and end our discussion of them with a mathematical justification for why set theory is in some sense the "most fundamental" part of (lots of) mathematics.
(1) Signatures do not necessarily, and usually do not, have unique models. More than one object can satisfy the stipulated properties of a signature. This applies as much for things like arithmetic as it does for my contrived examples.
(2) Models can be different, but not be interestingly different. If we decided to write all the natural numbers upside down, we would obtain a different set that satisfies all the usual properties of the natural numbers; a formally distinct set anyway. If we started calling what we mean by "1" what we mean by "2" and vice versa, we would have a formally distinct model. But these models are entirely the same for our purposes. In this regard, models are equivalent when each truth of one obtains just when an equivalent corresponding truth obtains in the other. EG, if we relabelled the numbers 1,2 by a,b,c, we would have:
[math]a + a = b[/math] holds in our new labelling when and only when [math]1 + 1 = 2[/math] holds in the usual labelling.
When this property holds between models, they are called isomorphic.
(3) Models are extremely informative about the syntax of a formal system, for example, you can prove that the truth value of a statement is independent from a system of axioms (neither it nor its negation are derivable) by finding a model of that system where the statement is true and finding a model of that system where the statement is false. Alternatively, one can assume the statement along with the formal system under study and show that it entails no contradiction (IE that it is consistent) and then assume the negation of the statement along with the formal system under study and show that this too entails no contradiction. This proof method was what showed that the continuum hypothesis was independent of the axioms of set theory ZFC; a result partially proved by Godel and then the rest by Cohen.
Lastly, you have no doubt noticed (if you've been paying attention) that the discussion of first order logic required us to talk about collections of objects; eg for the domains, for the definition of functions and predicates, for how the quantifiers worked... It showed up pretty much everywhere. If it were somehow possible to make a bunch of axioms of a privileged few symbols and bind them together with a signature that captured how collections of objects behave, whatever modelled such a theory would be an extremely general object. It would contain things like natural numbers, groups in algebra, functions in analysis... It would contain pretty much everything... And in that regard, the theory that expressed such a structure would serve as a foundation for mathematics.
This happened. It's called ZFC, for Zermelo Fraenkel set theory with the axiom of choice. So that's what we'll discuss (very briefly, considering the complexity of the topic and my more limited knowledge of it) next.
Would it be fair to say that thus far, we have only discussed the language by which we would reason about any kinds of objects, but (other than for examples) we have not yet formally introduced any objects about which to reason? And that's what we're about to start doing with sets?
IMHO you can start wherever you like, the "existence" of any object that satisfies some property is really only relative to some other object. Like "the naturals exist inside the reals" or "the continuous functions exist inside the differentiable functions". "Existence" is just a question of whether an object exists inside another one.
You can "introduce" an object without it existing. "imagine a signature with these rules, then this follows", this is like the deduction theorem (with a big abuse of notation):
If you have [math]\{\mathbb{N},+\}\vdash \Gamma[/math] then you have [math]\vdash \{\mathbb{N},+\} \implies \Gamma[/math] .
There is an object with the structure, so it has these properties.
vs
If there was an object with this structure, it would have these properties
In this regard, the reason I've waited to talk about set theory is that the model of set theory contains sub objects which model all the structures we've talked about. If you want to start from "something fundamental", this "contained object" or "the theory of ZFC is a supertheory of the theory of natural numbers", say, is a good intuition for why ZFC is in some sense "fundamental".
But yes, thinking about it again, what you've said is accurate. I've not written down what sets are, natural numbers are, rational numbers are etc; but I've gone some way of showing a system in which you can talk about them formally.
Quoting fdrake
As I understand it, we’re really saying “all objects with this structure have these properties”, but that’s technically true whether or not there “really” are any objects with that structure at all. All bachelors are unmarried, even if there are no bachelors.
I think this is about right. Though it's clearly true that not every first order structure has the empty domain as a model; eg "There exists an x such that x+1 = 2" is not true in the empty domain, but it is true in the naturals with addition.
Something that gives me that Pascal feeling of infinity vertigo is that we can say things like:
"If you interpret the the Peano axioms in the usual way, then..."
Which conjures up a meta language to talk about an implication from a meta-language item to an object language item. It seems the formalism always has to stop at some point, but the reason (and conceptual content) doesn't.
Yep.
Yeah, this is what I really take the truth of mathematical or more generally logical statements to be about. “All bachelors are unmarried” isn’t really a necessary truth by itself, but “If bachelor means ‘unmarried man of marriageable age’ then all bachelors are unmarried” is. I take mathematical truths to be truths about the implications from axioms to theorems. None of the theorems are themselves necessarily true, but it’s necessarily true that they are implied by their axioms.
So it is only necessarily true that some axioms imply the existence of the natural numbers with their usual properties including some natural number x such that x+1=2, but that is a conditional statement that is therefore equivalent to some “all A are B” statement that I don’t care to reconstruct right now, and is thus true even in an empty universe.
Only once you've fixed the underlying logic, I think. I'm not too happy with bringing in an exterior sense of modality to the theorems. If we're in a context sufficiently abstract to start playing around with the rules of logic, then necessity and possibility ideas might be perturbed too.
Edit: though, again, I generally agree with what you've said. I might just be being pedantic here.
Regarding the sense of necessity thing, maybe this helps spell out my suspicions that it doesn't tell us much.
Define that a given statement x is possible with respect to a given axiomatic system z if and only if (the theory of z & x) is consistent.
Define that a given statement x is necessary with respect to a given axiomatic system z if and only if (the theory of z & not(x)) is inconsistent.
If we have a list of axiomatic systems as the set of possible worlds, with the same underlying logic, and we fix a theory like arithmetic, arithmetic will be possible for axiomatic systems that don't make any of its theorems false (IE, possible worlds look like augmented arithmetic with rules consistent with all of its rules, or weakened arithmetic by deleting rules or modifying them to weaker versions), and arithmetic will be necessary for axiomatic systems that make all of the theorems of arithmetic true (IE, the axiomatic system under consideration contains all theorems of arithmetic in its theory, like set theory or Russel's type theory).
If we have a list of possible worlds that contained all satisfiable combinations of well formed formulae of the logic, the only statements true in all possible worlds would be those that we can derive from any world; the tautologies of the underlying logic.
Are the theorems concerning natural numbers necessary in the above sense? Well no, for example the rational numbers and how to manipulate fractions are in the above list of possible worlds; and for the fractions, it's false that every fraction is the successor of some other fraction (under their usual ordering).
(It's false that every element of the structure [math]\{\mathbb{Q},+,-,\times,\lt \}[/math] is the successor of some other number, but it is true for its sub-structure [math]\{\mathbb{N},+,-,\times,\lt \}[/math], in the arithmetic of fractions there will be a sub-arithmetic of naturals that has the successor function behaving normally, but this weakens the [math]\forall x[/math] in successor axiom statements about natural numbers to [math]\forall x \in \mathbb{N}[/math], in some sense they're the same statement since they're about the same object, but the universality of the successor property still breaks for the larger object of all fractions.)
If we go back one layer and allow the rules of logic to vary (over the set of well formed formulae); the only necessities would be the shared tautologies of every logic under consideration.
If we can vary the set of logics to include just one logic which has, say [math]\lnot(P \leftrightarrow \lnot \lnot P)[/math] as satisfiable, not even all the consequences of propositional logic would be necessary (because there exists a satisfiable theory/possible world which is inconsistent with double negation elimination).
The argument for the problem was that it seems like an inference like "P, if P then Q, therefore Q" depends on a hidden premise, "if (P and if P then Q) then Q", which in turn depends on yet another hidden nested conditional premise, and so on ad infinitum. Whenever you have some premises from which you think you can derive a conclusion, you're implicitly using a hidden premise that says you can derive that conclusion from those premises, but even once you've explicated that hidden premise you still have the same problem and need to add another hidden premise, on and on forever.
This sounds like that problem in that, say, a theorem of arithmetic may be necessitated by ZFC, but ZFC is not necessitated by propositional logic, you can use other axiomatic systems that maybe don't necessitate that theorem; and even if ZFC were necessitated by propositional logic, that may not be necessitated by anything, as there are for example paraconsistent logics. You keep falling back on earlier and earlier sets of rules that say that you're allowed to use the rules you tried to use earlier, but who says you can use those earlier rules?
This also reminds me of Kripkean relative modality, where something can be be necessary inasmuch as it is true in all worlds accessible from a reference world, even if it's not true in absolutely every world.
I don't have much more well-sorted thoughts on the topic now besides those comparisons to other problems.
I think that's the general picture involved with it, yeah. When you fix a starting point (of assumptions), you fix what is necessary for it (what can't fail to be true given the assumptions), what's consistent/possible with it (what can be true at the same time as the assumptions) and what's necessarily not for it (what can't be true at the same time as the assumptions).
Anyway, onto ZFC.
What's the purpose of ZFC? Well, historically, it arises at the time a foundation for mathematics was a popular research program. What it does is attempt to provide an axiomatic system in which all the usual theorems of mathematics are provable. How it does this is by showing that all these usual mathematical statements are secretly statements about sets; or rather, we can construct sets (in accordance with the axioms of ZFC) which interpret the theory of other structures (like continuous functions, arithmetic, fractions, etc).
How does ZFC achieve this? It forms an axiomatisation of sensible rules for combining, comparing and transforming collections of objects. One important property of all the rules is a notion of closure. Closure is a general mathematical property that says that "every way we can act on something in ways described by our stipulated rules produces something which obeys those rules". In the abstract, this maybe doesn't make much sense, but here are some examples:
[hide]Of course, studying it has its own merits, but for our purposes all we need are the tools to build sets.[/hide]
When we add two numbers in {0,1,2,3,...}, we're guaranteed to get another number. This says that {0,1,2,3,...} is closed under addition.
When we multiply two numbers in {0,1,2,3,...}, we're guaranteed to get another number. This says {0,1,2,3,...} is closed under multiplication.
But when we divide a number by another in {0,1,2,3,...}, we might get a fraction, like 0.5, which is not a number in {0,1,2,3,...}, and so {0,1,2,3,...} is not closed under division.
The axioms of ZFC give us various things we can do to sets to produce other sets. That is to say, if we follow the axioms of ZFC, we will stay within the structure; we'll still be talking about sets. Axiomatising something generally requires that the structure is closed under its stipulated rules and if the structure is not closed, that's seen as a defect/opportunity to introduce further axioms and/or objects.
ZFC stipulates rules that we can use to make and transform sets and get other sets out in a way that is sufficiently flexible to interpret usual mathematical objects as objects of ZFC - as sets.
[hide]Some of you familiar with types might notice a correspondence; the closure of an object under some rules induces an object type of belonging to the object.[/hide]
[hide]We've already seen two incidences of closure before, with regard to the construction of well formed formulae (you can't make a non-well formed formula from a well formed formula using the production rules) and with regard to the theory of an axiomatic system; a theory of an axiomatic system is a closure of that axiomatic system under syntactic derivation; the collection of all consequences of a bunch of axioms is closed under inference.[/hide]
[math]1 \in \{1,2\}[/math]
says "1 is a member of the set containing 1 and 2". The bracket notation means "the set consisting of the elements inside the brackets { }"
It also needs a symbol for the empty set, the set containing no elements. This is [math]\emptyset[/math]. With the previous membership relation, the emptyset can be characterised as:
[math]\emptyset = \forall x \{x \notin \emptyset \} [/math]
Which says the empty set is the name for the set with no elements - for all sets x, x is not in the empty set. [math] \notin [/math] is the negation of [math]\in[/math]. EG [math] 3 \notin \{1,2\} [/math] since 3 is not an element of the set {1,2}.
This makes the signature of ZFC [math]\{X, \in, \emptyset \}[/math]. The existence of the empty set can be entailed by other axioms, so it doesn't really need to be thrown into the signature as a constant, but I'll do it anyway. We could also include a symbol for equality of sets [math]=[/math], but since I've left that out of the previous discussions I'll leave it out here too.* Furthermore, we're going to postpone discussion of precisely what "X" is, but suffice now to say that it's a collection of (names of) all the sets.
[hide=*]It certainly makes things a bit fuzzier to equivocate between the ideas of equality in the underlying logic and equality in the first order theory using the logic, but considering that the only context this distinction is likely to crop up in is in distinguishing equal objects of the logic from equal objects of the theory, I'm going to just assume that the context will be sufficient to disambiguate the use of the symbol.[/hide]
The first rule we'll need to talk about sets is a criterion for when they're equal - how can we tell whether two sets are actually the same set? This principle is encoded in the axiom of extensionality, which states "two sets are equal when and only when they share all and only the same elements", eg {1,2} = {1,2}, or {2-1,2}={1,2}, since they share all and only the same elements. {1,2} isn't equal to {1,2,3} even though all the elements of {1,2} are in {1,2,3} because {1,2,3} has the additional element 3 (which is not in {1,2}). Prosaically, a set is the same as another if the other contains no more, no less, and no different elements from the first.
Formally, the axiom can be written as:
[math] (A = B) \leftrightarrow (\forall x (x \in A \leftrightarrow x \in B))[/math]
"For two given sets A and B, and for all sets x, a set A is equal to a set B when (if an x is in A when and only when it is also B)". "All and only the same elements" is what is formalised here.
The first bit says [math]A = B[/math] is logically equivalent to the rest... the [math]\forall x [/math] formalises the "All sets", the [math] (x \in A \leftrightarrow x \in B) [/math] formalises A having x as a member if B has it and vice versa. This posits what it means for two sets to be equal.
Better now?
An analogy - shopping lists. Two shopping lists are the same if they have the same items in them.
The next axiom is the axiom of pairing, which states that if you have two sets, you can make a another set which contains only those two sets as elements.
Shopping list wise - this means that if you have two shopping lists for different shops, you could make a shopping list for both shops by combining them.
Then there's the axiom of (restricted) comprehension - if you have a set, you can take a subset of it whose elements are the only elements which satisfy some property. If A = {1,2,3,4}, we can construct the set.
{x in A, x is even}
and get {2,4}. All the axiom of comprehension does is ensure the existence of a subset of a set which satisfies a specified property. It's called the axiom of restricted comprehension because it requires that we begin with a set (like A) then apply a property to it to get a subset (like {2,4}). If we could 'conjure up' a set into the language of set theory solely by specifying a property:
{x , x satisfies P}
Then we can make P whatever we like. Notoriously, this gives
[math]\{x, x \notin x\}[/math]
The Russel set. This must exist if we stipulated "we can conjure up a set through a property", and P is a property of set theory since it's a well formed formula of the language of set theory. If something belongs to the set, it doesn't belong to it, if something does not belong to the set, then it belongs to it. The reason why mathematicians rejected this axiom was because it entails a contradiction, and through the principle of explosion (discussed earlier), makes the theory prove everything it can state, even the falsehoods. Restricted comprehension saves the theory from the paradox by making sure you start with a set to apply properties to, rather than conjuring up a set from the logic using a property. If you change the underlying logic to one that is more resistant to contradictions, you might still want the unrestricted version (like in a paraconsistent logic).
Shopping list wise - this says that we can select sub lists by specifying elements. "What vegetables will we buy?" is answered by the sub list of vegetables.
The next is the axiom of union. This says that for every collection of sets, there's a set which consists of the elements of all of them taken together.
Shopping list wise, this says that you can make a larger shopping list out of any collection of shopping lists. A shopping list of meat items taken with a shopping list of vegetables becomes another shopping list which consists of the meat items and the vegetables.
The next is the axiom of powerset. This says that for every set, there exists a set which consists of all the subsets of that set.
Shopping list wise, if we have the list:
Carrots
Potatoes
Eggs
This says we must be able to construct the lists
Carrots, Potatoes, Eggs, {Carrots, Potatoes}, {Carrots, Eggs}, {Potatoes, Eggs},
{Carrots, Potatoes, Eggs}, and the empty list (what you would buy if you bought everything on a blank page).
Then make a list of all those shopping lists and the blank bit of paper. That whole new list is the powerset of the original shopping list.
The powerset of a set is always larger than the original set. If you had a set of infinite size (to be introduced later), this makes there be more than one size of infinity. If we considered an object which would be a model of set theory, because of the power set axiom, intuitively it would have to have a size larger than any set, in particular larger than the natural numbers! Unfortunately this does not hold, there are countable models of ZFC (called Skolem's Paradox). Such a model does not satisfy the intuition, but entails no contradictions; a model in some sense sets out a meaning of terms, a countable model of ZFC doesn't have the statements in it mean precisely the same thing.
The axiom of infinity states that:
"There is a set [math]N[/math] such that [math]\emptyset[/math] is in [math]N[/math], and if the set [math]x[/math] is in [math]N[/math] then [math]S(x)[/math] is in [math]N[/math]". Where [math]S(x)[/math] is defined as [math]x \cup \{x\}[/math].
This looks like:
[math]N=\{ \emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\} \}, ... \}[/math]
If we define the symbols [math]0=\emptyset[/math], [math]1 = S(\emptyset)[/math],
[math]2 = S(1)[/math]... ,[math]n = S(n-1)[/math]
we can see that [math]N[/math] looks suspiciously like the natural numbers. This is true. It is the natural numbers. Arithmetic can be defined on this set by defining an operation [math]+[/math] ( a function from [math] N \times N[/math] to [math]N[/math] ) which is given by:
[math]\forall a (a+0=a)[/math]
[math]\forall a \forall b (a + S(b) = S(a+b))[/math]
This lets us prove [math]1+1 = 2 [/math] in [math]\{N,+\}[/math].
Theorem: [math]1+1=2[/math]
Proof: Let [math]a[/math] be in [math]N[/math], then [math]a+1 = a+S(0) = S(a+0) = S(a)[/math]. Then set [math]a=1[/math], this gives [math]1+1=S(1) = 2[/math].
Is it possible to write "1 + 1 = 2" entirely in terms of sets and set operations? Like, if I understand correctly, we can say that 0 = ? = {}, and that 1 = {?} = {{}}, no? So 2 = {{},{{}}}, right?
So {{}} + {{}} = {{},{{}}}
But is there a way to write that "+" in terms of things like ?, entirely set-theoretic operations?
(1) Show that some statement [math]\phi[/math] is true of some number [math]f(1)[/math]
(2) Show that if [math]\phi[/math] is true of [math]f(x)[/math], then [math]\phi[/math] is true of [math]f(S(x))[/math].
(3) Conclude: therefore [math]\phi[/math] is true of [math]f(x)[/math] for all [math]x[/math].
EG: Theorem: "Given a sequence [math]f(n) = a + b \times (n-1)[/math] for [math]n[/math] in [math]\{1,2,3,...,\}[/math], show that the sum [math]P(n)[/math] of the first [math]n[/math] terms of this sequence is [math]P(n) = \frac{n}{2}(2f(1) + (n-1)b)[/math].
Proof:
(1) Initial statement: [math]f(1)=a[/math] then [math]P(1) = a+b\times 0 = a = f(1)[/math].
Now how do we show (2)? We can use the strategy of conditional proof detailed earlier, simply assume that [math]P(n)[/math] is true and then show that [math]P(n+1)[/math] is true on this basis. "Assuming [math]P(n)[/math] is true" is called the induction hypothesis. So we make that induction hypothesis.
Assume [math]P(n) = \frac{n}{2}(2f(0) + (n-1)b)[/math], then [math]P(n+1)[/math] is [math]f(n+1)+P(n)[/math], which is [math](a+(n+1)b+\frac{n}{2}(2f(1) + (n-1)b)[/math], which after some tedious algebra is [math]P(n+1)[/math].
(3) The combination of (1) and (2) shows that this is true for all the numbers.
Quoting Pfhorrest
Yes. The definition of addition lets you do this, it's just an exercise of translation.
[math]a + S(b) = S(a+b)[/math] and [math]a+0 = a[/math]. Gives you that if [math]x[/math] is a set which represents a natural number and so is [math]S(y)[/math], [math]x+S(y)=S(x+y)[/math]. Working out the details for [math]x+1[/math] is [math]x \cup \{x\}[/math], working out the details for [math]x+2[/math] is [math]x+2= (x \cup \{x\})\cup \{(x \cup \{x\})\}[/math]. Defining [math]+[/math] without the inductive definition gives you "take the thing on the left and write it as its set, take the thing on the right and write it as its set, define the sum as the successor function applied to 0 as many times as the thing on the left plus the thing on the right".
Or alternatively "take the thing on the left, and successor function it the number of times required to reach the thing on the right from 0", equivalently "union the thing on the left with the successor function applied to it as many times as the number on the right"
[math]x+y = x \cup_{i \in y} S^i (x)=S^{x+y}(\emptyset)[/math]
The strategy for showing that ZFC contains within it a copy of the natural numbers and arithmetic is to show that you can define a collection of sets [math]N[/math] and the relevant operations/functions [math]S[/math], [math]+[/math] (and subtraction, multiplication, division, inequalities on natural numbers etc etc...) such that the overall structure [math]\{N,S,+\}[/math] satisfies an axiomatisation of arithmetic like (first order) Peano arithmetic [math]\{\mathbb{N},S,+\}[/math].
What this does formally is show that [math]\{N,S,+\}[/math] (the set theory construction) models [math]\{\mathbb{N},S,+\}[/math] (the Peano arithmetic axioms defining natural numbers and addition). The successor in Peano arithmetic is interpreted as the successor in the set theory construction, the numbers in Peano arithmetic are interpreted by their corresponding number in the set theory construction, addition in Peano arithmetic is interpreted by addition in the set theory construction and so on for however many functions/operations/relations you throw into the Peano arithmetic structure and the set theory structure.
Recapitulating a previous point: the power of set theory is that it provides a way of defining lots of structures, so that you can take some other structure (like Peano arithmetic) and interpret it as a set theory object (collection of sets).
An equation in a variable [math]x[/math] in a structure (with [math]f[/math] defined) is an expression of the form [math]f(x)=t[/math], and where [math]f[/math] is a function defined in the structure from its constants to its constants and [math]t[/math] is a constant element. A solution for a given equation is a substitution of [math]x[/math] for a constant term in the equation expression which makes [math]f(x)=t[/math] true.
EG: [math]f(x)=x+1[/math], [math]t=2[/math] substituted into the above formula gives [math]x+1=2[/math], and a solution is then [math]x=1[/math] since the substitution [math]x \rightarrow 1[/math] makes [math]f(1) = 1 + 1 = 2 = t[/math] true.
This?
Quoting Pfhorrest
Lack of one is cool for inscriptionalism. No sign of a consensus on wiki.
EG: [math]x+1 = 2 [/math] is true implies [math]x = 2 - 1[/math] is true implies [math]x = 1[/math] is true implies [math]1[/math] is a solution of [math]x+1=2[/math].
What we'd need is a way of substituting equivalent expressions for equivalent expressions, and in order to do this we can define what it means for two expressions to be equivalent.
We'd really like something like [math]2 = 3-1 = 1+1 = 4-2 = ...[/math], so that all ways of obtaining [math]2[/math] from operations of arithmetic are in some way equivalent. This can be set up for addition as follows:
[math][t]=\{x,y \in \mathbb{N} : x+y = t\}[/math]
which is to be read "the set of all expressions defined as [math][t][/math] such that every expression within [math]t[/math] is the sum of two numbers which equal [math]t[/math].
If we took some other number, say [math]u[/math], and defined the same thing: [math][z]=\{v,w \in \mathbb{N} : v+w = z\}[/math]
We could ask "under what conditions is [math][t]=[z][/math]?", the answer there is:
[math][ z ] = [ t ] \leftrightarrow \{v,w \in \mathbb{N} : v+w = z\} = \{x,y \in \mathbb{N} : x+y = t\}[/math]
Under what conditions does this equation of sets have a (non-empty collection of) solutions? Well, whenever [math]z=t[/math]. That is, whenever the expressions in the two sets equal the same number. This gives us a perspective from which equations can be manipulated.
Notice that if we define [math][x]+[y] = [x+y][/math], this also respects the above. (For example, any expressions which evaluate to 2 plus any expressions which evaluate to 3 equal any expressions which evaluate to 5, this is 2+3=5 if and only if [2]+[3]=[5]).
If we have that [math]x+y=t[/math], then we also have that [math][x]+[y]=[t][/math], this means we can substitute in anything in [math][x][/math] for [math]x[/math] in the equation and obtain another equivalent equation. Substituting equivalent expressions is how equations can be solved through algebra. Imagine that we've done the same thing for subtraction and so on, eg:
[math][0]_- = \{x,y \in \mathbb{N} : x-y = 0 \}[/math]
For example:
[math]\begin{align}x+1=2\\ \leftrightarrow [x+1]=[2]\\ \leftrightarrow [x+1-1] = [2-1]\\\leftrightarrow[x]+[1-1] = [1] \\\leftrightarrow [x+0]=[1]\\ \leftrightarrow [x]=[1]\\\leftrightarrow x = 1\end{align}[/math]
What this highlights is that you can leverage the equality defined between sets to define an equivalence between expressions that equal the same constant. This (kind of thing, but for all the operations) is the construction that formalises the algebra used in solving equations.
The first has the benefit of telling a story from the "objects" points of view, how do we build up more complicated objects from simpler objects, the second has the benefit of telling the story from the "structures" point of view, which presents the integers as "solving a problem regarding addition and subtraction in the naturals", the fractions as "solving a problem regarding multiplication and division in the integers" and the real numbers as "solving a problem regarding sequences in the fractions".
Input?
So what's a relation? A relation on a set is a collection of pairs of elements from that set where the order matters. EG the set {1,2,3} can have the relation R={ (1,2), (2,3) } on it. This says that "1 is related to 2" and "2 is related to 3". The pairs can be written as 1R2, 2R3. Note that 1R2 is different from 2R1! An equivalence relation has three properties which characterise it:
(1) Reflexivity: for all x; xRx
(2) Symmetry: for all x for all y : xRy implies yRx
(3) Transitivity: for all x for all y for all z : xRy & yRz imply xRz.
The relation defined above satisfies these properties.
(1) Reflexivity: eg; 3+1 = 3+1
(2) Symmetry; eg; 3+1 = 4 implies 4 = 3+1
(3) Transitivity; 3+1 = 4 and 4 = 5-1 implies 3+1 = 5-1
Equivalence relations defined on some set divide that set up into non-overlapping parts. These are called equivalence classes. The equivalence class of x is written [x]. EG [4] contains 3+1 and 5-1. But it does not contain 3, or anything that adds up to 3, like 2+1. The equivalence classes on a set divide it up into distinct parts which are somehow equivalent. The above construction divides the set of expressions of the form x+y up into the various sets [t]={x+y = t}.
Note that [2] = [1+1]. When an equivalence class can be written in the form [x], x is called a representative of that equivalence class.
The properties of equivalence classes (for arithmetic) exhibited above give you [x]+[y]=[x+y]. The same applies for every way of obtaining x from arithmetic operations on any collection of numbers. This means that the arithmetic operations defined on numbers transfer to arithmetic operations defined on equivalence classes. Numerical equality of what arithmetic expressions evaluate to (3+1 evaluates to 4) transfers to set equality of these equivalence classes ([3+1]=[4]). Once you get arithmetic expressions evaluating to terms functionally (which they always will, they will have unique outputs per input set by definition), you can always leverage this to define equivalence classes of expressions on whatever structure you have defined the operations on.
This technique is used over and over again; once operations are defined on a structure, equivalence classes of evaluation (like 3+1 evaluates to 4) can be used to motivate algebraic substitution/solving things by algebra on that structure. The same will apply to rational numbers (fractions); they will be built as equivalence classes of naturals. Then real numbers will be built as equivalence classes of fractions!
Different senses of identity can be thought of as equivalence classes under different relations. Numerical identity is like 2=2, predicative identities like "crimson = scarlet" (insofar as they are both red colours) are equivalence relations of a different sort. This makes some sense so long as the idea can be understood extensionally without simplification. Something can be understood extensionally when the concept is completely expressible by collecting all terms that the concept applies to.
EG: "foot " is an element of the equivalence class of nouns in English. Two words are related when and only when they are of the same grammatical type.
EG: "foot" is an element of the equivalence class of "foot" under the equivalence relation of string (character sequence) identity.
Not all concepts behave extensionally.
EG: "pile of rocks" has ambiguous boundaries, at what point does a collection of stones become a pile?
EG: "hot". at what point does a temperature become hot? Does a temperature become hot in the same way as a human body feels hot?
Expressions in natural language rarely only leverage extensional concepts to furnish their understanding, most expressions are confused jumbles. This provides lots of interpretive issues, but what we lose in rigidity and precision we gain in expressive power.
In general, this is phrased "X up to equivalence relation R", and is written X/R. You can think of equivalence relations as gluing terms together into meaningful chunks, for a prescribed sense of meaning set out in the definition of the equivalence relation.
EG: "identify the natural numbers up to their remainder upon division by 2", the equivalence relation there is characterised as xRy iff x-y 's remainder upon division by 2 is 0. This gives you that 0 is related to all the even numbers and that 1 is related to all the odd numbers. This is called "the integers modulo (mod) 2".
When you glue parts of a structure together, the glued parts tend to inherit the operations of the original structure. EG, two numbers: 3 and 7, 3+7 = 10. If you map this expression to their equivalence classes mod 2, [3] = [1], [7]=[1], [10]=[0], [3+7]=[3]+[7]=[1]+[1]=[1+1]=[2]=[0]=[10]. Everything works out.
For the remainder of the discussion; whenever a structure with some operations on it (like natural numbers with addition etc) is introduced, assume that we have identified the terms of the structure up to equivalence of evaluating expressions. So for example, 22/7 will be identified with 44/14, or [math]\sqrt{2} = 2^{0.5}[/math]. Explicitly setting out how this works in every case is extremely tedious and unenlightening, so I'm just going to assume that once the structure has been defined the (collection of) equivalence relations upon its terms I just described the nature of have been set up appropriately. This means I will be abusing the equality symbol a lot, but the meaning should be clear from the context (and if I don't think it is I'll make a reminder).
There's a pretty obvious problem with defining subtraction in the system to work in precisely the same way we're taught in school, like 1-2 = ... what? -1, says school. But -1 isn't a natural number at all. What this means is that for any sense of subtraction which works exactly like the one we have in school, the natural numbers don't let you do it in the general case.
You can define subtraction between two natural numbers a,b whenever b is greater than or equal to a and have it work exactly as expected in that case, but being able to subtract any number from any other and obtain something that we've already defined is extremely desirable. In other words, whatever structure we define subtraction in, it has to be closed under subtraction to work as expected in every case.
An observation that's extremely useful in setting up subtraction in the above way is the following list:
1-1 = 0
2-2=0
3-3=0
4-4=0
...
1+0=1
2+0=2
3+0=3
4+0=4
...
Which demonstrates the, probably obvious, property of subtraction that a number minus itself is always zero. And that any number plus zero is itself.
Imagine, now, that you're not looking at familiar numbers, and instead you're looking at symbols. There is some operation such that for any x (say 2), there exists some y (say 2) that when you combine them together with the operation, you get 0. What would be nice would be to be able to take the original operation we defined, addition, and define additional elements into the structure of natural numbers so that for any number x we can guarantee the existence of some y so that we can have:
x+y=0=y+x
We want to ape the ability of subtraction to take any x and ensure that we can subtract x from it and get 0, but make it a property of addition instead. This property is called the existence of an additive inverse for every element of the structure, or more generally the existence of an inverse for every element under an operation.
Predictably, the additive inverse of 2 is (-2), the additive inverse of 1 is (-1)... the additive inverse of x is (-x).
So the first list can be rewritten as:
1+(-1) = 0
2+(-2)=0
3+(-3)=0
4+(-4)=0
2 * x = 1
Has no solutions when x is a natural number. That is, there are no multiplicative inverses in the natural numbers (or the integers). But there's more conceptual issues to work out here.
For addition, it made a lot of sense to copy all the natural numbers, append - to them, then simply define -x as the additive inverse of x. Geometrically, this can be thought of as mirroring the positive number line into the negative one, inducing a copy.
I'm going to call the natural numbers with additive inverses "the integers".
Positive numbers
0------->
Negative numbers
<------0
Integers
<-------0------>
But division is a bit more tricky; we need to define a new structure to somehow "mix" natural numbers with each other to produce parts of natural numbers which are not natural numbers.
As always, the use of fractions preceded their axiomatization. So we can go from the use and try to guess axioms.
When we write a fraction, it's something like 1/2, or 22/7, or 22+3/5, or 1 - 1/2 (ignoring decimals because they mean the same thing). Cases like 22+3/5 reduce to cases like 1/2; 22+3/5 = 113/5.
What we have to work with then are pairs of numbers. We could write 113/5 as (113,5) to signify this. So we will. So all fractions can be written as a pair of integers like that. Now we've got a way of writing all the fractions, we can define operations on them.
Multiplication and division of fractions are actually easier to define in this way than addition and subtraction.
We want 1/2 * 4/7 to be 2/7, so if we have two fractions (a,b) and (c,d), (a,b)*(c,d) = (ab,cd), where ab is a times b as natural numbers and cd is c times d as natural numbers.
Division follows with a minor tweak. (a,b)/(c,d) = (ad,bc); dividing by a fraction is the same as multiplying by 1/ that fraction.
Addition is a bit harder.
(a,b)+(c,d) = ?
Go by example.
We have that 2/7 + 3/5, as in school the first thing to do is write them over a common denominator. One way of getting that is just to multiply the bottom numbers together, then times each top number by the top number in the other fraction. This gives us two fractions numerically equal to the starting ones, so the sum will be the same.
In symbols:
2/7 + 3/5 = (5*2)/(5*7) + (7*3)/(7*5) = 20/35 + 21/35
Then the tops can be added together as they're over a common bottom.
2/7 + 3/5 = (5*2)/(5*7) + (7*3)/(7*5) = 20/35 + 21/35 = (20+21)/35 = 41/35
If we replace 2,7 by a,b and 3,5 by c,d:
(a,b) + (c,d) = (d*a,d*b)+(b*c,b*d) = (ad+bc,bd)
Careful reading shows that we've not introduced an axiom for combining the pairs through addition rigorously. Especially since it requires the common denominator trick.
One way of making this rigorous is to make the axiom for all integer a, (a,a) = 1 (with the assumptions that 1 behaves like it should, 1 times anything is itself). Now with that, you can simply define addition as what would result only when the fractions are expressed in terms of a common denominator. Why does this work?
(a,b) + (c,d) = by definition = (ad+cb,bd)
Now imagine that we have two representations of the same thing - this is called a well definition proof.
Let's set (e,f)=(a,b) and (g,h) = (c,d). The question is, if we compute (e,f)+(g,h), do we end up at the same result as computing (a,b) + (c,d) ? How can we turn e's into a's, as it were?
Well, we could try and say that two fractions are equal; (a,b) = (c,d), then a=c and b=d... Again, there's a but:
Note that 1 has lots of representations, (1,1), (2,2), (-2,-2), and so on. But they all equal 1 when written as fractions, but 1 isn't equal to 2. What gives? They're clearly "morally equal", but strict equality in the last paragraph is too restrictive to get the job done.
We were in a similar situation before; with expressions like 1+3 and 2+2, we want them to be equal, but they contain different things. We want to take collections of representations of things and glue them together.
We actually have enough here to do the work. If we define two fractions (a,b) and (c,d) as equivalent when (c,d) = (e*a,e*b) for some integer e... Does this do the job?
Instead of stipulating:
(a,b) = (c,d), then a=c and b=d
we instead stipulate
(a,b) = (c,d), then c=e*a and d=e*b for some integer e.
Now we can try and complete the well definition proof; if we start off with two sums of fractions, will their results necessarily match? I'm just going to write = here to mean equivalent. Two fractions will be equal (equivalent) when one is a representation of 1 (like (2,2)) times the other.
(a,b) = (e,f), (c,d) = (g,h)
Question: (a,b)+(c,d) = (equivalent) = (e,f)+(g,h)?
From the equivalences, we have:
e=ka
f=kb
g=lc
h=ld
Then using these and the definition of addition above
(e,f)+(g,h) = (eh+gf,fh) = ( [ka][ld] + [lc][kb], [kb][ld] )
You can rearrange the square brackets inside using the rules of natural number (and integer) arithmetic:
(e,f)+(g,h) = (eh+gf,fh) = ( [ka][ld] + [lc][kb], [kb][ld] ) = ( [kl]ad+[kl]cb, [kl]bd)
That last one, there's a common factor on top and bottom:
( [kl]ad+[kl]cb, [kl]bd) = ( [kl](ad+cb), [kl]bd )
The common factor is the same. So we can pull it out (by the definition of multiplication of factions) as
( [kl](ad+cb), [kl]bd )
= (kl,kl)*(ad+cb,bd)
So by: two fractions will be equal (equivalent) when one is a representation of 1 (like (2,2)) times the other, the two representations come out the same, completing the proof.
Collections of sets have an ordering on them, the subset relationship. If we have the collection of sets:
{1,2,3}, {1,}, {2}, {3}, {1,2}, {1,3} , {2,3}
You can call one set X smaller than another Y if X is a subset of Y. So {1} would be less than {1,3}, since the first is a subset of the second. When there are orderings, there comes an associated idea of biggest and smallest with respect to the ordering. In the above list, {1,2,3} is the biggest element, since every element is a subset of it.
But the sets {2} and {3} are not comparable, since neither is a subset of the other.
Contrast natural numbers. Consider the set of natural numbers {1,2,3}. The number 3 is the biggest there; 3 is bigger than 2, 2 is bigger than 1. Every natural number is comparable to every other natural number with the usual idea of how to order them by size, but not every set is comparable to every other set when comparing them by the subset relationship.
Setting out the ordering on the natural numbers, you can call one natural number x greater than some natural number y if and only if (definitionally) x = S^n ( y ) for some n. IE, x is bigger than y if you can apply the successor function to y a few times and get x. This immediately ensures that all natural numbers are comparable; since every natural number is a successor of 0. [hide](equivalently, if one natural number x represented as a collection of sets is a subset of another y then x
It's pretty clear that the way we compare fraction sizes resembles the way we compare natural numbers in some ways; for any two fractions, you can tell which is bigger or if they're the same. The way we compare fraction sizes does not resemble the way we compare sets by the subset relationship; there aren't pairs of fractions which are incomparable like {2} and {3} are.
But they have differences too, any pair of fractions has a fraction inbetween them, whereas natural numbers do not. Natural numbers come in lumps of 1, the smallest positive difference between two natural numbers. Fractions don't come in smallest differences at all.
It's also pretty clear that there's more than one way of ordering things; the kind of ordering sets have by the subset relation is not the kind of ordering natural numbers (or fractions) have by the usual way we compare them.
What this suggests is that it's important to make axioms for the different types of ordering relationships as suits our interest. One intuitive property the ordering on the natural numbers has but the subset one lacks is that the ordering on the natural numbers appears to represent something about magnitudinal quantities; the mathematical objects numbers /are/ are sizes, and those sizes can be compared.
Whereas, the subset relation breaks this intuition; it doesn't represent comparison of a magnitudinal property, it represents something like nesting or containedness. The UK contains Scotland and England and Northern Ireland, but Scotland doesn't contain England or Northern Ireland, and England doesn't contain Scotland or Northern Island, and Northern Island doesn't contain Scotland or England; Scotland, England and Northern Ireland can only be compared to the UK in that manner, and not to each other. Another example is that Eukaryotes contains Animals and Fungi, but Animals don't contain Fungi and Fungi don't contain animals.
What properties then characterise the ordering of naturals and fractions, and distinguish them from the ordering of province and country or the ordering of classifications of biological kinds?
Also of interest, the next essay in my Codex Quarentis series of threads will be closely related to this thread, since the writing of it was the inspiration for creating this thread. I'd love your input on it when I post it early next week.
Mathematics is essentially just the application of pure logic: a mathematical object is defined by fiat as whatever obeys some specified rules, and then the logical implications of that definition, and the relations of those kinds of objects to each other, are explored in the working practice of mathematics. Numbers are just one such kind of objects, and there are many others, but in contemporary mathematics, all of those structures have since been grounded in sets.
The natural numbers, for instance, meaning the counting numbers {0, 1, 2, 3, ...}, are easily defined in terms of sets. First we define a series of sets, starting with the empty set, and then a set that only contains that one empty set, and then a set that only contains those two preceding sets, and then a set that contains only those three preceding sets, and so on, at each step of the series defining the next set as the union of the previous set and a set containing only that previous set. We can then define some set operations (which I won't detail here) that relate those sets in that series to each other in the same way that the arithmetic operations of addition and multiplication relate natural numbers to each other.
We could name those sets and those operations however we like, but if we name the series of sets "zero", "one", "two", "three", and so on, and name those operations "addition" and "multiplication", then when we talk about those operations on that series of sets, there is no way to tell if we are just talking about some made-up operations on a made-up series of sets, or if we were talking about actual addition and multiplication on actual natural numbers: all of the same things would be necessarily true in both cases, e.g. doing the set operation we called "addition" on the set we called "two" and another copy of that set called "two" creates the set that we called "four". Because these sets and these operations on them are fundamentally indistinguishable from addition and multiplication on numbers, they are functionally identical: those operations on those sets just are the same thing as addition and multiplication on the natural numbers.
All kinds of mathematical structures, by which I don't just mean a whole lot of different mathematical structures but literally every mathematical structure studied in mathematics today, can be built up out of sets this way. The integers, or whole numbers, can be built out of the natural numbers (which are built out of sets) as equivalence classes (a kind of set) of ordered pairs (a kind of set) of natural numbers, meaning in short that each integer is identical to some set of equivalent sets of two natural numbers in order, those sets of two natural numbers in order that are equal when one is subtracted from the other: the integers are all the things you can get by subtracting one natural number from another. Similarly, the rational numbers can be defined as equivalence classes of ordered pairs of integers in a way that means that the rationals are the things you can get by dividing one integer by another.
The real numbers, including irrational numbers like pi and the square root of 2, can be constructed out of sets of rational numbers in a process too complicated to detail here (something called a Dedekind-complete ordered field, where a field is itself a kind of set). The complex numbers, including things like the square root of negative one, can be constructed out of ordered pairs of real numbers; and further hypercomplex numbers, including things called quaternions and octonions, can be built out of larger ordered sets of real numbers, which are built out of complicated sets of rational numbers, which are built out of sets of integers, which are built out of sets of natural numbers, which are built out of sets built out of sets of just the empty set. So from nothing but the empty set, we can build up to all complicated manner of fancy numbers.
But it is not just numbers that can be built out of sets. For example, all manner of geometric objects are also built out of sets as well. All abstract geometric objects can be reduced to sets of abstract geometric points, and a kind of function called a coordinate system maps such sets of points onto sets of numbers in a one-to-one manner, which is hence reversible: a coordinate system can be seen as turning sets of numbers into sets of points as well. For example, the set of real numbers can be mapped onto the usual kind of straight, continuous line considered in elementary geometry, and so the real numbers can be considered to form such a line; similarly, the complex numbers can be considered to form a flat, continuous plane. Different coordinate systems can map different numbers to different points without changing any features of the resulting geometric object, so the points, of which all geometric objects are built, can be considered the equivalence classes (a kind of set) of all the numbers (also made of sets) that any possible coordinate system could map to them. Things like lines and planes are examples of the more general type of object called a space.
Spaces can be very different in nature depending on exactly how they are constructed, but a space that locally resembles the usual kind of straight and flat spaces we intuitively speak of (called Euclidian spaces) is an object called a manifold, and such a space that, like the real number line and the complex number plane, is continuous in the way required to do calculus on it, is called a differentiable manifold. Such a differentiable manifold is basically just a slight generalization of the usual kind of flat, continuous space we intuitively think of space as being, and it, as shown, can be built entirely out of sets of sets of ultimately empty sets.
Meanwhile, a special type of set defined such that any two elements in it can be combined through some operation to produce a third element of it, in a way obeying a few rules that I won't detail here, constitutes a mathematical object called a group. A differentiable manifold, being a set, can also be a group, if it follows the rules that define a group, and when it does, that is called a Lie group. Also meanwhile, another special kind of set whose members can be sorted into a two-dimensional array constitutes a mathematical object called a matrix, which can be treated in many ways like a fancy kind of number that can be added, multiplied, etc.
A square matrix (one with its dimensions being of equal length) of complex numbers that obeys some other rules that I once again won't detail here is called a unitary matrix. Matrices can be the "numbers" that make up a geometric space, including a differentiable manifold, including a Lie group, and when a Lie group is made of unitary matrices, it constitutes a unitary group. And lastly, a unitary group that obeys another rule I won't bother detailing here is called a special unitary group. This makes a special unitary group essentially a space of the kind we would intuitively expect a space to be like — locally flat-ish, smooth and continuous, etc — but where every point in that space is a particular kind of square matrix of complex numbers, that all obey certain rules under certain operations on them, with different kinds of special unitary groups being made of matrices of different sizes.
I have hastily recounted here the construction of this specific and complicated mathematical object, the special unitary group, out of bare, empty sets, because that special unitary group is considered by contemporary theories of physics to be the fundamental kind of thing that the most elementary physical objects, quantum fields, are literally made of.
You probably need to qualify this. Take the circle x^2+y^2=1 in the standard Euclidean plane and lengthen the scale on the x-axis, so that the circle becomes an ellipse. That's a "different coordinate system".
Amazing how the physicists can use those groups. :cool:
Interesting thread. Ambitious too.
I'm not sure I understand what you mean here. You can describe the same circle with different coordinates in a distorted coordinate system like that; or you can describe a different ellipse with the same coordinates in that different coordinate system. I'm not sure which of those scenarios you're referring to.
I'm talking about the first scenario: the circle is unchanged, but different numbers map to its points in the different coordinate system, and the points can each be considered the equivalence classes of all different sets of numbers that can map to them from all coordinate systems.
Quoting Kenosha Kid
Yeah @fdrake is awesome and I would love to see him continue what he was doing in this thread; or for someone else to take over where he left off.
of me.
@fdrake is far more up to date and knowledgeable.
I can do some more of the basic axiomatic maths, but I've been cheating and looking ahead at axiomatic QFT and decided that I really need to study more mathematics. I don't know C*-algebra from a 32C-wonderbra
Lots of people asked me to help them with their homework when I was at school and uni! Never could say outright no to it. Unless someone wanted me to do it for them rather than get help learning it. Have no sympathy for the first motivation.
Quoting Pfhorrest
Thank you!
I've been thinking about going back to it for some time now. I probably will. It would be nice to have one way of telling the story in one place.
I only really know the story up until "this is a differential equation with real variables". Complex analysis stuff and actual physics is mostly above my pay grade. It'd be pretty cool if @Kenosha Kid, @jgill and I could actually get up to something like the Schrodinger equation rather than f=ma, which is what I planned to stop at (but stopped just short of the ordering of the reals).
Quoting Kenosha Kid
There should be a sound effect for a field flying over another mathematician's head. [math] ? ? ? WHOOSH[/math]
I have no idea!
I'm a huge fan of discrete maths; I know your proof by heart!
Have you thought about machine learning?
The models can predict our behavior, meaning that their inner logic, which is always based on math, try to accomplish what you suggest.
The problem is that they're not explicit/comprehensible by humans. They're sort of black boxes, like functions.
What do you think about this?
I know how to get from simple fields to wavefunctions and from densities to wavefunctions uniquely -- that's simple enough.
Are you talking physics field or mathematics field? Field as a mapping from, say, the plane to vectors in the plane (physics field), or field as a commutative ring with multiplicative inverses (mathematics field)?
I’m especially curious about the steps between SU groups, and excitations of quantum fields into particles. Like, I have a vague understanding that an SU group is a kind of space with a particular sort of matrix of complex numbers at every point in it, and I imagine that that space is identified with a quantum field and so what’s happening in those matrices at each point is what’s happening with the quantum field at that point, but I have no clue what the actual relationship between the quantum field states and the complex matrices is.
You've said it yourself. Math is our ever-evolving language for modeling anything.
If you really want to get down to detail, I suggest focusing on particular areas.
For example, language is an interesting one.
And you build from there.
Chomsky worked hard on this theory, but I'm no expert. What I can attest to is art and creation , but I'm not ready at this moment to lay out a fitting mathematical approach.
I wish you the best of fates!
So you'd need linear operators on vector spaces, differentiation+integration, complex numbers... If I gave you definitions of those things, would you be able to to do what you needed to do with them? Can you do the thing where you go from linear operators on vector spaces to linear operators on modules if required?
The vector space construction needs mathematical fields (commutative rings with multiplicative inverses), which needs groups.
That's roughly where I started - gesturing in the direction of formal languages (production rules on a collection of strings).
[math]\left [\begin{matrix}{{\alpha }_{k}} & -{{{\bar{\beta }}}_{k}} \\{{\beta }_{k}} & {{{\bar{\alpha }}}_{k}} \\\end{matrix} \right][/math]
Corresponds to
[math]{{t}_{k}}(z)=\frac{{{\alpha }_{k}}z-{{{\bar{\beta }}}_{k}}}{{{\beta }_{k}}z+{{{\bar{\alpha }}}_{k}}}[/math]
And multiplication is the following
[math]{{t}_{k}}({{t}_{k+1}}(z))=\frac{{{\alpha }_{k}}{{t}_{k+1}}-{{{\bar{\beta }}}_{k}}}{{{\beta }_{k}}{{t}_{k+1}}+{{{\bar{\alpha }}}_{k}}}[/math]
edit: But the matrix represents a quaternion, primarily. I.e., extending the complex numbers to a higher dimension. In the above, alpha=a+bi and beta=-c+di to give the quaternion a+bi+cj+dk.
SU(2) seems to associate with spin. The multiplication of two such 2X2 matrices may give the Hamiltonian product, or maybe not. Too much work involved.
Yes to all of the above. I'm still catching up, I can do complex numbers if need be, I've done it before. The other thing we need is category theory. I don't think we need to do any integrals but we need to know about them. I guess a good aim atm is continuum mathematics.
I'll be in quarantine for a couple of weeks soon. I shall try and get the field of real numbers with its order defined in that time.
Oh are you or a loved one I'll? Sorry to hear. Be safe!
Nah. Couldn't see my partner for a while, travelled to see her, quarantine restrictions got reimposed while I was here!
Look forward to this! Next, well-order an uncountable set of reals. :cool: :up:
Ah okay. That actually sounds quite nice.
Mostly because fdrake majorly upped the ante on the level of rigor I expected. I had hoped for a dozen or two posts about the size (and level of detail) of my OP, but instead he started giving us so much more.
That's one of those books which is in dire need of a Miracle operator.
(vague description of mathematics)
A miracle occurs.
Now you try!
On the first day of ordering, the Lord said let [math]\mathbb{N}[/math] be the set of all natural numbers, then for any pair of natural numbers x and y, y is the greatest and cometh after x if and only if x is contained within y and, conversely, y is the lesser of x and cometh earlier if and only if x containeth y:
[math]\forall x,y \in \mathbb{N}[/math]
[math]y > x \leftrightarrow x \in y[/math]
and
[math]y < x \leftrightarrow y \in x[/math]
And thus the natural numbers were ordered and it was good.
On the second day of ordering, the Lord said let [math]\mathbb{Z}[/math] be the set of integers, then for any pair of integers x=(a,b) and y=(c,d), y be greater than x if and only if c+b > a+d:
[math]\forall x=(a,b) \in [x], y=(c,d) \in [y], [x],[y] \in \mathbb{Z} [/math]
[math][y] > [x] \leftrightarrow c+b > a+d[/math]
and [y] be equivalent of [x] if and only if c+b = a+d. And thus the integers were ordered and it was good.
On the third day of ordering, the Lord said let [math]\mathbb{Q}[/math] be the set of all rationals, then for any pair of rationals x=(a,b) and y=(c,d), y be greater than x if and only if c*b > a*d:
[math] \forall x=(a,b) \in [x],y=(c,d) \in [y], [x],[y] \in \mathbb{Q} [/math]
[math][y] > [x] \leftrightarrow c*b > a*d[/math]
and [y] be equivalent of [x] if and only if c*b = a*d. And lo the rationals were ordered and it was good.
On the fourth day of ordering, the Lord realised that Dedekind was late producing the reals and verily he flipped his fucking lid. He spake unto Dedekind:
And Dedekind heard the Lord and said it would be done. He took the set of rationals and a saw, and he ordered the rationals as the Lord had commanded and he took his saw and he cut them in half and he spake to the Lord:
and the Lord looked upon the two sets, which he named A and B, and saw that A was infinite in number and that for any rational x in A, there was always a higher rational, for between any pair of rationals there exist an infinity of intermediate rationals as spaketh by @fdrake. But no matter which x he took, he could find no element y in B that was the equal or the lesser of it. The Lord sought for the smallest rational in B but found that, for any he looked upon, he could find a lesser. And the Lord spake unto Dedekind:
and Dedekind confessed to the Lord that he did not know because he did not look. And the Lord spake to him that had Dedekind cut exactly at a rational x, then x would be either the greatest rational in A with none greater, or the least rational in B with none lesser, and that since neither A had a greatest rational nor B a lesser, the number at which Dedekind had cut could not be a rational. And he spake further unto Dedekind:
And he bade Dedekind make his cuts upon the set of rationals an infinite number of times and also bade him to be finished before midnight lest they run into a fifth day of ordering, and Dedekind did saw impossibly and created the set of real numbers, [math]\mathbb{R}[/math].
The Lord looked upon the set and said, Let A be the set of lesser rationals and B the set of greater, and (A,B) be a real number greater than the greatest of A and less than or the equal of the least of B. And let (C, D) be another such real. Then if A is a subset of C, then (A,B) is the lesser of (C,D):
[math]\forall x=(A,B),y=(C,D) \in \mathbb{R}[/math]
[math]y > x \leftrightarrow A \in C[/math]
and if A and C be brethren, then the two reals are as one. And he looked upon the ordering of the reals and it was good. Actually better than the ordering of the rationals.
*I'm figuring we covered union as part of generators.
That's the kind of post I was hoping this whole thread would be. I didn't want to complain since fdrake was producing such good informative content, but it was the combination of that content with Biblical style that I was really hoping for in this thread, and you nailed it!
I haven't really taken care to enumerate the axioms. For instance, I've dealt with selecting numbers from infinite sets without stating an axiom of choice. This is mostly because I haven't really unpicked the axioms covered so far. Might make a good summary post.
I'm also thinking that category theory has been handwaved a bit, but that can be put on a more formal footing once morphisms are covered in group theory. Technically that goes rather against the bottom-up approach you wanted but there's always something isn't there.
Quoting Kenosha Kid
[math]\left( c,d \right)\in Z'=N\times N[/math]
Do you mean x is in Z and y in Z'? I thought the above was okay but I'm not used to it tbh.
Calling fishfry! :cool:
Quoting Kenosha Kid
MathType works well - it's WYSIWYG - using the Wikipedia cut and paste option. You only have to replace
Yes, that's right.
https://www.math.uchicago.edu/~may/VIGRE/VIGRE2011/REUPapers/Lian.pdf
Not a big deal. You are to be applauded for wading into this.
It's worth getting right. You're quite right. The set was Z not Z', but I was representing the elements of Z as ordered pairs which is invalid, since they are sets, specifically equivalence classes. Further, rightly, I should have said y is equivalent to x, not equal to, when defining the equivalence relation.
I have edited the above. Can you check this? I'm not that practised at this.
[math]\forall x=(a,b) \in [x], y=(c,d) \in [y], [x],[y] \in \mathbb{Z} [/math]
[math][y] > [x] \leftrightarrow c+b > a+d[/math]
is supposed to read, for each ordered pair x = (a,b) (from the set Z') in the integer [x] and y = (c,d) in the integer [y], where [x] and [y] are in Z, [y] is greater than [x] if and only if c+b > a+d.
The Lord looked upon the naturals once more, reminding Himself that:
[math]a \cdot 0 = 0[/math]
[math]a \cdot S(b) = a + (a \cdot b)[/math]
and He said, let S(b) = a, and thus
[math]a \cdot a = a + (a \cdot (a-1)) = a + (a + a\cdot (a-2)) = ... [/math]
[math] = \sum_{i=1}^a a[/math]
And he said, Let this be denoted as [math]a^2[/math], and Me denote [math]a^3 = a \cdot a \cdot a[/math] and [math]a^n = \prod_{i=1}^n a[/math].
Then he asked, What then is [math]a^{m+n}[/math]? And seeing that he could write [math]\prod_{i=1}^{m+n} a[/math] as
[math]a^{m+n} = \prod_{i=1}^m a \cdot \prod_{i=1}^m a[/math]
he saw that [math]a^{m+n} = a^m a^n[/math].
And thus on that day the Lord created [math]a^m a^n[/math]. And he said, Let n=d, and thus He named him [math]a^d a^m[/math].
He then asked, what is the exponent k such that [math]a^{m+n+k} = a^n[/math]? And He remembered he had fought this devil before, for the answer lay not in the set of naturals, but in the integers.
Thus, he said, let k, m, n be integers and not naturals such that [math]m+n+k = n \rightarrow k=-m[/math], and therefore:
[math]a^{-m} \cdot (a^m a^n) = a^n[/math]
such that [math]a^{-m}[/math] be the inverse of [math]a^m[/math]. And further that since division be the inverse of multiplication, [math]a^{-m} = \frac{1}{a^m}[/math]. And thus [math]a^0 = a^n a^{-n} = 1[/math].
Then He asked, what is [math](a^n)^m[/math]? From the above, He knew that [math](a^n)^0 = 1 = a^0[/math] and [math](a^n)^1 = a^n[/math], and He conjectured that [math](a^n)^m = a^{m*n}[/math] and saw that it was true, since:
[math](a^n)^m = (a^n)^{m-1} \cdot a^n = a^{n(m-1)} \cdot a^n = a^{nm - n + n} = a^{nm}[/math]
(proceeding by induction).
Then He asked, what is m such that [math](a^n)^m = a[/math] and saw that the answer lay not in the integers but in the rationals, since it must from the above be that [math]m=\frac{1}{n} [/math] such that [math](a^n)^m = a^{mn} = a^{n/n} = a[/math].
Thus He turned his eye (for he had but one) to the rationals and he named these inverses of exponents roots.
And finally He turned his eye to the reals and asked, What is x such that [math]x^2 = -1[/math]? And He looked but did not see among the reals an answer to this question, for [math]x^2 \ge 0 (\forall x \in \mathbb{R})[/math].
And knowing that for closure under subtraction He had to put aside the naturals for the integers, and for closure under division He had to put aside the integers for the rationals, He knew once again that he had been failed by his creations, and must create anew for His work to be good.
And he spake:
(quotes butcher mathjax but you know what I mean)
:rofl: :clap: :up: :fire:
Whoa, not so fast! Where is the link between complex numbers and the existence of man?
Inquiring minds want to know. :chin:
Which fulfills @Pfhorrest 's original goal. Thread complete.
Morphisms: Book I
And the Lord spake unto Morph and said:
And Morph did take the set of natural numbers, and the first thing he did was to take two elements from it and form of them an ordered pair as he had seen the Lord do:
[math]f(x, y \in \mathbb{N}) = (x, y)[/math]
The second thing he did was to remove 0 and to put it back, then repeat for 1 and 2 and so on:
[math]f: \mathbf{N} \rightarrow \mathbf{N}[/math]
The third thing he did was to swap 0 and 1:
[math]f: \mathbf{N} \rightarrow \mathbf{N} (f(0)=1, f(1)=0, f(n>1) = n)[/math]
The fourth thing he did was to take an element at random and add it to all of the other elements and itself, and he saw that he had kept all the elements greater than or equal to the random element:
[math]f_{y \in \mathbf{N}}: \mathbf{N} \rightarrow \mathbf{N} + y = \mathbf{N'} \subset \mathbf{N} [/math]
The fifth thing he did was to take an element > 0 at random and multiply with it all of the other elements and itself, and he saw that the sum of two such fiddles was the equal of the fiddle of the sum:
[math]f_{y \in \mathbf{N}}: \mathbf{N} \rightarrow y \cdot \mathbf{N} = \mathbf{N'} \subset \mathbf{N}[/math]
The sixth thing he did was to take the element 0 = {} and multiply with it all of the other elements and itself, and he saw that he was left with unity:
[math]f_{0}: \mathbf{N} \rightarrow 0 \cdot \mathbf{N} = 1 \subset \mathbf{N}[/math]
And thus Morph spent his days, fiddling with the natural numbers and noting the achievements of his fiddling, and he spake unto the Lord:
And the Lord heard Morph and said:
And He instructed Morph to continue to explore this set, and the other sets, and he spake:
And Morph heard this and said:
And the Lord in rage did smite Morph upon his head, causing Morph such pain and anguish that the Lord did feel sorry for him and gave him two white pills and a glass of water. And Morph swallowed the pills with the water and his head did heal and he was glad. And Morph did ask of the Lord:
and the Lord said, We shall call it the cocodomain and the Lord was booed for it was not good.
You crack me up.... Best nerd jokes I ever read. :rofl:
Such as Odd Perfect Numbers https://medium.com/cantors-paradise/eulers-odd-perfect-numbers-theorem-82a393baa883