How to prove $2+2=4$ using Zermelo–Fraenkel Set Theory?

Clash Royale CLAN TAG#URR8PPP

up vote
3
down vote

favorite

2

I'm familiar with the famous excerpt from Principia Mathematica by Bertrand Russel and Alfred Whitehead. However, as Zermelo–Fraenkel Set Theory is today's most used foundation of mathematics (or ZF if you believe the axiom of Choice is implied), I was wondering if there is a postulation expressed in the symbolism of first-order logic for $2 + 2 = 4$ following ZFC. I'm not a logician, not even an undergraduate yet, and I was unable to find such a proof online, maybe I'm just overlooking some elementary understanding of what ZFC is.

elementary-set-theory logic set-theory first-order-logic

share|cite|improve this question

edited Jul 29 at 20:35

Taroccoesbrocco

3,48941431

asked Jul 23 at 13:08

John Miller

765

• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  In ZFC the natural numbers defined as ordinals, so by definition: $2+2=2+(1+1)=(2+1)+1=3+1=4$. Note that $A+1$ is defined as $S(A)$
  – Holo
  Jul 23 at 13:19
  
  

  
  
  
  

add a comment | 

up vote
3
down vote

favorite

2

I'm familiar with the famous excerpt from Principia Mathematica by Bertrand Russel and Alfred Whitehead. However, as Zermelo–Fraenkel Set Theory is today's most used foundation of mathematics (or ZF if you believe the axiom of Choice is implied), I was wondering if there is a postulation expressed in the symbolism of first-order logic for $2 + 2 = 4$ following ZFC. I'm not a logician, not even an undergraduate yet, and I was unable to find such a proof online, maybe I'm just overlooking some elementary understanding of what ZFC is.

elementary-set-theory logic set-theory first-order-logic

share|cite|improve this question

edited Jul 29 at 20:35

Taroccoesbrocco

3,48941431

asked Jul 23 at 13:08

John Miller

765

• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  In ZFC the natural numbers defined as ordinals, so by definition: $2+2=2+(1+1)=(2+1)+1=3+1=4$. Note that $A+1$ is defined as $S(A)$
  – Holo
  Jul 23 at 13:19
  
  

  
  
  
  

add a comment | 

up vote
3
down vote

favorite

2

up vote
3
down vote

favorite

2

2

I'm familiar with the famous excerpt from Principia Mathematica by Bertrand Russel and Alfred Whitehead. However, as Zermelo–Fraenkel Set Theory is today's most used foundation of mathematics (or ZF if you believe the axiom of Choice is implied), I was wondering if there is a postulation expressed in the symbolism of first-order logic for $2 + 2 = 4$ following ZFC. I'm not a logician, not even an undergraduate yet, and I was unable to find such a proof online, maybe I'm just overlooking some elementary understanding of what ZFC is.

elementary-set-theory logic set-theory first-order-logic

share|cite|improve this question

edited Jul 29 at 20:35

Taroccoesbrocco

3,48941431

asked Jul 23 at 13:08

John Miller

765

I'm familiar with the famous excerpt from Principia Mathematica by Bertrand Russel and Alfred Whitehead. However, as Zermelo–Fraenkel Set Theory is today's most used foundation of mathematics (or ZF if you believe the axiom of Choice is implied), I was wondering if there is a postulation expressed in the symbolism of first-order logic for $2 + 2 = 4$ following ZFC. I'm not a logician, not even an undergraduate yet, and I was unable to find such a proof online, maybe I'm just overlooking some elementary understanding of what ZFC is.

elementary-set-theory logic set-theory first-order-logic

share|cite|improve this question

edited Jul 29 at 20:35

Taroccoesbrocco

3,48941431

asked Jul 23 at 13:08

John Miller

765

share|cite|improve this question

share|cite|improve this question

edited Jul 29 at 20:35

Taroccoesbrocco

3,48941431

edited Jul 29 at 20:35

Taroccoesbrocco

3,48941431

edited Jul 29 at 20:35

Taroccoesbrocco

3,48941431

3,48941431

asked Jul 23 at 13:08

John Miller

765

asked Jul 23 at 13:08

John Miller

765

asked Jul 23 at 13:08

John Miller

765

765

• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  In ZFC the natural numbers defined as ordinals, so by definition: $2+2=2+(1+1)=(2+1)+1=3+1=4$. Note that $A+1$ is defined as $S(A)$
  – Holo
  Jul 23 at 13:19
  
  

  
  
  
  

add a comment | 

• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  In ZFC the natural numbers defined as ordinals, so by definition: $2+2=2+(1+1)=(2+1)+1=3+1=4$. Note that $A+1$ is defined as $S(A)$
  – Holo
  Jul 23 at 13:19
  
  

  
  
  
  

1

1

In ZFC the natural numbers defined as ordinals, so by definition: $2+2=2+(1+1)=(2+1)+1=3+1=4$. Note that $A+1$ is defined as $S(A)$
– Holo
Jul 23 at 13:19

In ZFC the natural numbers defined as ordinals, so by definition: $2+2=2+(1+1)=(2+1)+1=3+1=4$. Note that $A+1$ is defined as $S(A)$
– Holo
Jul 23 at 13:19

add a comment | 

5 Answers
5

active

oldest

votes

up vote
5
down vote



accepted

Zermelo–Fraenkel set theory is formulated in a language that has a binary relation $in$, and that's it. The symbols $1,2,3,4$ and $+$ make "no sense" from a syntactic point of view.

So first one needs to explain what is $2$ in the context of set theory. This means that you need to define some sets that will behave like you would expect of the natural numbers. Normally, these are the finite von Neumann ordinals, defined recursively as $0=varnothing$ and $n+1=ncupn$. There are other ways to define the natural numbers, or you could be thinking about the real numbers, and then you need to define those as well first, but for now let's stick with the von Neumann ordinals and see where it takes us.

Note that even in the case of Peano arithmetic or ring theory, the symbol for $2$ and the symbol for $4$ are not part of the language. They are used as shorthand for either repeated sums of $1$ or repeated application of the successor function to $0$, or so on.

So if $2$ is defined as $1+1$ and $4$ is defined as $((1+1)+1)+1$, and you have an axiom saying that $(x+y)+z=x+(y+z)$, then you're practically done: $(1+1)+(1+1)=((1+1)+1)+1$, so $2+2=4$. But okay, let's go back to set theory.

We have the natural numbers, so $2=varnothing,varnothing$ and $4$, well, let's just write $4$. After this you need to ask what is $+$. Do you think about $+$ as a recursive definition of applying the successor function? Even the Peano axioms which usually form the basis for arithmetic have $+$ as a standalone object, and there is a connection between $+$ and the successor function. There are two standard ways to define what is $+$ on the natural numbers in the context of set theory:

1. Successive application of the successor function, so $x+0=x$ and $x+S(y)=S(x+y)$. In that case, $2+2=S(1)+S(1)=S(S(0))+S(S(0))=dots=S(S(S(S(0))))$. And now we can also translate back into sets to get "a fully set theoretic statement". But it's awful, and I don't want to do it.



2. 
   

   Using cardinality of sets. Note that $n$ is a set with exactly $n$ elements. $0$ has no elements and $1$ has exactly one element (which is $0$, as it turns out). So we can define $n+m=k$ if and only if the number of elements in a disjoint union of a copy of $n$ and a copy of $m$, is $k$. Or, in modern terms, there is a bijection between the two sets.

   
   
   

   In that case, one needs to write down a function from $langle 0,0rangle,langle 0,1ranglecuplangle 1,0rangle,langle 1,1rangle$, or $0times2cup1times2$, and $4$ which is $0,1,2,3$. Of course, this starts with defining what is an ordered pair from a set theoretic view, what is a function, etc., and then write this as a set theoretic expression again. Which, as before, is an awful exercise in futility.

   
   

The easiest way, at the end, is to prove this "by blocks". First prove there is a way to formalize the natural numbers, then formalize addition, then show that no matter what formalization you chose, as long as it satisfies certain properties (which you would expect from the natural numbers), it has to be the case that the object corresponding to $2+2$ is the object corresponding to $4$.

---

Or just be annoying and declare that you interpret $2,+$ and $4$ in a non-standard way so $2+2=5neq 4$. Whatever floats your boat.

share|cite|improve this answer

answered Jul 23 at 13:38

Asaf Karagila

291k31402732

• 
  
  
  

  
  

  
  
  
  
  
  

  
  Thank you for making it clear, so in Principia Mathematica what were they using to prove 1+1=2 because it seemed fairly abstract in terms of logic symbols?
  – John Miller
  Jul 23 at 14:15
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  I haven't read PM, because from a modern point of view, it's a ginormous waste of time unless you want to study some very specific things related to the text there. (I'm not, however, disparaging reading the book as a historical landmark of a huge undertaking to formalize mathematics, that was great.) So I can't quite help you with what and how they did things there. But if my memory serves me right, it takes them a couple hundred pages to finish formalizing the basics first so they can prove $1+1=2$. I think they use a type-theoretic approach, which is a different way to formalize mathematics
  – Asaf Karagila
  Jul 23 at 14:18
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  "and you have an axiom saying that (x+y)+z=x+(y+z)" I thought it was common to use axioms for Peano arithmetic where the associative law was not an axiom, but rather a theorem.
  – Doug Spoonwood
  Jul 29 at 21:42
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @Doug: I meant that in the context of the axioms of a field (or at least ring theory). In the case of PA you need to prove it, yes.
  – Asaf Karagila
  Jul 29 at 21:45
  
  

  
  
  
  

add a comment | 

up vote
3
down vote

In the ZFC axioms system, natural numbers are represented by sets. For example, $0$ is usually represented by the empty set $emptyset = $.

You can represent the successor of a number in different ways. One common way of doing so is representing any number greater than $0$ as the set of all smaller numbers. Thus, $1=emptyset$, $2=0,1 = emptyset,emptyset $.

This has the nice property that $a < b$ iff $a in b$ iff $asubset b$.

We can compute thus the successor of a number as $s(a) = acup a$. We note that the predecessor is also easy to compute.

Summation is defined recursively, such that $a+0 = a$, and $a+s(b) = s(a)+b$.

Applying these two rules repeatedly gives us that $2+2 = 3+1 = 4+0 = 4$

share|cite|improve this answer

answered Jul 23 at 13:29

Jsevillamol

3,01911124

• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  I would only add that $a<b$ is defined as $ain b$, it is not just equivalent
  – Holo
  Jul 23 at 13:38
  

  
  
  
  

add a comment | 

up vote
3
down vote

In ZFC you would usually construct the addition function by recursion, so by the general recursion theorem it would satisfy the recursion equations
$$ a + 0 = a \ a+S(b) = S(a+b) $$
where $S$ is the function that takes a natural number to its successor.

After proving that $2=S(S(0))$ and $4=S(S(S(S(0))))$ (which you may well have considered to be definitions in the first place), it is as simple as
$$ beginalign 2+2 &= 2 + S(S(0)) \
&= S(2+S(0)) \
&= S(S( 2+ 0 )) \
&= S(S( 2 )) \
&= S(S(S(S(0)))) \
&= 4 endalign $$

Depending on the underlying formalization of first-order logic, expressing this equational reasoning as a formal may be more or less cumbersome. In particular, doing it halfway readably depends on the ability to introduce new term notations (such as $x+y$) other than the ones present in the original logical language, and most proof systems for first-order logic are content to let that be handled by considering atomic formulas that involve the new terms to be abbreviations of a more complex nest of quantifiers.

So if you compare PM to the combination of orthodox textbook FOL + ZFC, the latter may not necessarily come out ahead.

On the other hand, modern proof assistants have shown that formal reasoning in first-order logic can be done much smoother than by the textbook proof systems -- e.g. by embedding FOL in a suitable higher-order system where the equational reasoning above can be done more or less directly, and then proving once and for all that this higher-order system is conservative over first-order logic.

share|cite|improve this answer

edited Jul 23 at 13:37

answered Jul 23 at 13:31

Henning Makholm

225k16290516

add a comment | 

up vote
1
down vote

First, you need to construct the numbers you are using. It can be the natural numbers set.
You can use the famous construction $emptyset$ for $0$, $emptyset$ for $1$, $emptyset, emptyset$ for $2$ and so on.
After that, you need to construct a $+$ operator. It can be a function $+:mathbbN^2rightarrowmathbbN$. This function can be constructed as a set of pairs $((a,b),c)$ satisfying some condition on $a$, $b$ and $c$. An ordered pair can be constructed with the Kuratowski definition.
Finally you can check if $2+2=4$.

Axiomatic Set Theory is an accepted foundations of mathematics, where you can construct all of mathematics(not sure of that). However, no one will ever do these constructions by hand.

Imagine you want to express the explicit construction of the tangent bundle of a smooth manifold. That would be huge and confusing.

share|cite|improve this answer

edited Jul 23 at 13:55

answered Jul 23 at 13:24

Cristhian Grundmann

765

• 
  
  
  

  
  

  
  
  
  
  
  

  
  First "construct all of mathematics" is a little too much for now, as contradiction free model has some problems with it(godel incompleteness theorem). Secondly how can you define $+$ using itself? The definition of $+$ in ZFC is:$$n+0=n\n+(m+1)=(n+m)+1\n+k=supn+mmid m<k$$ for $k$ limit ordinal and $A+1=S(A)$
  – Holo
  Jul 23 at 13:36
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  Oh, what I mean was not to use $a+b=c$ as a condition, but rather use some well defined condition. It would depend on the previous constructions.
  – Cristhian Grundmann
  Jul 23 at 13:54
  

  
  
  
  

add a comment | 

up vote
0
down vote

The existing answers are more or less talking about ordinal addition. In terms of cardinals: Say $|A|$ denotes the cardinality of the set $A$. Saying $2+2=4$ then means this:

Theorem. If $Acap B=emptyset$, $|A|=|B|=2$, then $|Acup B|=4$.
$newcommandtwo0,1$
$newcommandfour0,1,2,3$

Now let's write $Asim B$ to mean that there exists a bijection from $A$ onto $B$. Then $|A|=2$ means that $Asim0,1$ (where here it doesn't matter what $0$ and $1$ are, all that matters is $0ne 1$), and similarly $|A|=4$ means $Asimfour$.

We need a lemma:

Lemma. $twosim2,3$.

And now to prove the theorem: Suppose $Acap B=emptyset$ and $|A|=|B|=2$. The lemma shows that $Bsim2,3$. Since $twocap2,3=emptyset$ it follows that $$Acup Bsimtwocup2,3=four.$$

Note About "ordinal addition" versus "cardinal addition": They are two different things. In fact $2$ and $4$ are cardinals and ordinals, so the statement "$2+2=4$" is a priori ambiguous, since we haven't specified whether we're talking about ordinal addition or cardinal addition. In hopefully obvious notation, the other answers are showing that $2+_o2=4$, while here we show that $2+_c2=4$.

By the standard definitions, a finite ordinal is the same as a finite cardinal, annd the two notions of addition for finite ordinals/cardinals come out the same. But it's important to realize that they really are different for infinite ordinals and infinite cardinals.

For example, say $omega$ is the first infinite ordinal and $aleph_0$ is the first infinite cardinal. Then, as sets, $omega=aleph_0$, but, at least in the way the notation is usually interpreted, $omega+omeganeomega$ while $aleph_0+aleph_0=aleph_0$. That's not a contradiction because the two plus signs mean different things; in more careful notation that nobody actually uses, $omega+_oomeganeomega$ and $aleph_0+_caleph_0=aleph_0$.

So when you see "$+$" in set theory you need to consider the context to determine whether it means $+_o$ or $+_c$.

share|cite|improve this answer

edited Jul 23 at 15:21

answered Jul 23 at 14:40

David C. Ullrich

54.1k33481

• 
  
  
  

  
  

  
  
  
  
  
  

  
  Oh okay, so I'm starting to think to prove something through ZFC almost means nothing, as there are so many ways to do so. I think I had this preconception that it was a specific set of axioms to describe how to postulate modern mathematics, but is it more of a general framework in which one can theorise freely?
  – John Miller
  Jul 23 at 14:49
  
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @JohnMiller ZFC is certainly a specific set of axioms. The above is an informal proof "in ZFC", in that every step could be justified using those axioms. (If you're confused by the fact that what I proved is totally different from what the other answers prove, see the Note I'm about to add to the answer...)
  – David C. Ullrich
  Jul 23 at 15:02
  

  
  
  
  

add a comment | 

Your Answer

StackExchange.ifUsing("editor", function ()
return StackExchange.using("mathjaxEditing", function ()
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix)
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
);
);
, "mathjax-editing");

StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "69"
;
initTagRenderer("".split(" "), "".split(" "), channelOptions);

StackExchange.using("externalEditor", function()
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled)
StackExchange.using("snippets", function()
createEditor();
);

else
createEditor();

);

function createEditor()
StackExchange.prepareEditor(
heartbeatType: 'answer',
convertImagesToLinks: true,
noModals: false,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);



);

 

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2860346%2fhow-to-prove-22-4-using-zermelo-fraenkel-set-theory%23new-answer', 'question_page');

);

Post as a guest

Name Email

5 Answers
5

active

oldest

votes

5 Answers
5

active

oldest

votes

active

oldest

votes

active

oldest

votes

up vote
5
down vote



accepted

Zermelo–Fraenkel set theory is formulated in a language that has a binary relation $in$, and that's it. The symbols $1,2,3,4$ and $+$ make "no sense" from a syntactic point of view.

So first one needs to explain what is $2$ in the context of set theory. This means that you need to define some sets that will behave like you would expect of the natural numbers. Normally, these are the finite von Neumann ordinals, defined recursively as $0=varnothing$ and $n+1=ncupn$. There are other ways to define the natural numbers, or you could be thinking about the real numbers, and then you need to define those as well first, but for now let's stick with the von Neumann ordinals and see where it takes us.

Note that even in the case of Peano arithmetic or ring theory, the symbol for $2$ and the symbol for $4$ are not part of the language. They are used as shorthand for either repeated sums of $1$ or repeated application of the successor function to $0$, or so on.

So if $2$ is defined as $1+1$ and $4$ is defined as $((1+1)+1)+1$, and you have an axiom saying that $(x+y)+z=x+(y+z)$, then you're practically done: $(1+1)+(1+1)=((1+1)+1)+1$, so $2+2=4$. But okay, let's go back to set theory.

We have the natural numbers, so $2=varnothing,varnothing$ and $4$, well, let's just write $4$. After this you need to ask what is $+$. Do you think about $+$ as a recursive definition of applying the successor function? Even the Peano axioms which usually form the basis for arithmetic have $+$ as a standalone object, and there is a connection between $+$ and the successor function. There are two standard ways to define what is $+$ on the natural numbers in the context of set theory:

1. Successive application of the successor function, so $x+0=x$ and $x+S(y)=S(x+y)$. In that case, $2+2=S(1)+S(1)=S(S(0))+S(S(0))=dots=S(S(S(S(0))))$. And now we can also translate back into sets to get "a fully set theoretic statement". But it's awful, and I don't want to do it.



2. 
   

   Using cardinality of sets. Note that $n$ is a set with exactly $n$ elements. $0$ has no elements and $1$ has exactly one element (which is $0$, as it turns out). So we can define $n+m=k$ if and only if the number of elements in a disjoint union of a copy of $n$ and a copy of $m$, is $k$. Or, in modern terms, there is a bijection between the two sets.

   
   
   

   In that case, one needs to write down a function from $langle 0,0rangle,langle 0,1ranglecuplangle 1,0rangle,langle 1,1rangle$, or $0times2cup1times2$, and $4$ which is $0,1,2,3$. Of course, this starts with defining what is an ordered pair from a set theoretic view, what is a function, etc., and then write this as a set theoretic expression again. Which, as before, is an awful exercise in futility.

   
   

The easiest way, at the end, is to prove this "by blocks". First prove there is a way to formalize the natural numbers, then formalize addition, then show that no matter what formalization you chose, as long as it satisfies certain properties (which you would expect from the natural numbers), it has to be the case that the object corresponding to $2+2$ is the object corresponding to $4$.

---

Or just be annoying and declare that you interpret $2,+$ and $4$ in a non-standard way so $2+2=5neq 4$. Whatever floats your boat.

share|cite|improve this answer

answered Jul 23 at 13:38

Asaf Karagila

291k31402732

• 
  
  
  

  
  

  
  
  
  
  
  

  
  Thank you for making it clear, so in Principia Mathematica what were they using to prove 1+1=2 because it seemed fairly abstract in terms of logic symbols?
  – John Miller
  Jul 23 at 14:15
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  I haven't read PM, because from a modern point of view, it's a ginormous waste of time unless you want to study some very specific things related to the text there. (I'm not, however, disparaging reading the book as a historical landmark of a huge undertaking to formalize mathematics, that was great.) So I can't quite help you with what and how they did things there. But if my memory serves me right, it takes them a couple hundred pages to finish formalizing the basics first so they can prove $1+1=2$. I think they use a type-theoretic approach, which is a different way to formalize mathematics
  – Asaf Karagila
  Jul 23 at 14:18
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  "and you have an axiom saying that (x+y)+z=x+(y+z)" I thought it was common to use axioms for Peano arithmetic where the associative law was not an axiom, but rather a theorem.
  – Doug Spoonwood
  Jul 29 at 21:42
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @Doug: I meant that in the context of the axioms of a field (or at least ring theory). In the case of PA you need to prove it, yes.
  – Asaf Karagila
  Jul 29 at 21:45
  
  

  
  
  
  

add a comment | 

up vote
5
down vote



accepted

Zermelo–Fraenkel set theory is formulated in a language that has a binary relation $in$, and that's it. The symbols $1,2,3,4$ and $+$ make "no sense" from a syntactic point of view.

So first one needs to explain what is $2$ in the context of set theory. This means that you need to define some sets that will behave like you would expect of the natural numbers. Normally, these are the finite von Neumann ordinals, defined recursively as $0=varnothing$ and $n+1=ncupn$. There are other ways to define the natural numbers, or you could be thinking about the real numbers, and then you need to define those as well first, but for now let's stick with the von Neumann ordinals and see where it takes us.

Note that even in the case of Peano arithmetic or ring theory, the symbol for $2$ and the symbol for $4$ are not part of the language. They are used as shorthand for either repeated sums of $1$ or repeated application of the successor function to $0$, or so on.

So if $2$ is defined as $1+1$ and $4$ is defined as $((1+1)+1)+1$, and you have an axiom saying that $(x+y)+z=x+(y+z)$, then you're practically done: $(1+1)+(1+1)=((1+1)+1)+1$, so $2+2=4$. But okay, let's go back to set theory.

We have the natural numbers, so $2=varnothing,varnothing$ and $4$, well, let's just write $4$. After this you need to ask what is $+$. Do you think about $+$ as a recursive definition of applying the successor function? Even the Peano axioms which usually form the basis for arithmetic have $+$ as a standalone object, and there is a connection between $+$ and the successor function. There are two standard ways to define what is $+$ on the natural numbers in the context of set theory:

1. Successive application of the successor function, so $x+0=x$ and $x+S(y)=S(x+y)$. In that case, $2+2=S(1)+S(1)=S(S(0))+S(S(0))=dots=S(S(S(S(0))))$. And now we can also translate back into sets to get "a fully set theoretic statement". But it's awful, and I don't want to do it.



2. 
   

   Using cardinality of sets. Note that $n$ is a set with exactly $n$ elements. $0$ has no elements and $1$ has exactly one element (which is $0$, as it turns out). So we can define $n+m=k$ if and only if the number of elements in a disjoint union of a copy of $n$ and a copy of $m$, is $k$. Or, in modern terms, there is a bijection between the two sets.

   
   
   

   In that case, one needs to write down a function from $langle 0,0rangle,langle 0,1ranglecuplangle 1,0rangle,langle 1,1rangle$, or $0times2cup1times2$, and $4$ which is $0,1,2,3$. Of course, this starts with defining what is an ordered pair from a set theoretic view, what is a function, etc., and then write this as a set theoretic expression again. Which, as before, is an awful exercise in futility.

   
   

The easiest way, at the end, is to prove this "by blocks". First prove there is a way to formalize the natural numbers, then formalize addition, then show that no matter what formalization you chose, as long as it satisfies certain properties (which you would expect from the natural numbers), it has to be the case that the object corresponding to $2+2$ is the object corresponding to $4$.

---

Or just be annoying and declare that you interpret $2,+$ and $4$ in a non-standard way so $2+2=5neq 4$. Whatever floats your boat.

share|cite|improve this answer

answered Jul 23 at 13:38

Asaf Karagila

291k31402732

• 
  
  
  

  
  

  
  
  
  
  
  

  
  Thank you for making it clear, so in Principia Mathematica what were they using to prove 1+1=2 because it seemed fairly abstract in terms of logic symbols?
  – John Miller
  Jul 23 at 14:15
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  I haven't read PM, because from a modern point of view, it's a ginormous waste of time unless you want to study some very specific things related to the text there. (I'm not, however, disparaging reading the book as a historical landmark of a huge undertaking to formalize mathematics, that was great.) So I can't quite help you with what and how they did things there. But if my memory serves me right, it takes them a couple hundred pages to finish formalizing the basics first so they can prove $1+1=2$. I think they use a type-theoretic approach, which is a different way to formalize mathematics
  – Asaf Karagila
  Jul 23 at 14:18
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  "and you have an axiom saying that (x+y)+z=x+(y+z)" I thought it was common to use axioms for Peano arithmetic where the associative law was not an axiom, but rather a theorem.
  – Doug Spoonwood
  Jul 29 at 21:42
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @Doug: I meant that in the context of the axioms of a field (or at least ring theory). In the case of PA you need to prove it, yes.
  – Asaf Karagila
  Jul 29 at 21:45
  
  

  
  
  
  

add a comment | 

up vote
5
down vote



accepted

up vote
5
down vote



accepted

Zermelo–Fraenkel set theory is formulated in a language that has a binary relation $in$, and that's it. The symbols $1,2,3,4$ and $+$ make "no sense" from a syntactic point of view.

So first one needs to explain what is $2$ in the context of set theory. This means that you need to define some sets that will behave like you would expect of the natural numbers. Normally, these are the finite von Neumann ordinals, defined recursively as $0=varnothing$ and $n+1=ncupn$. There are other ways to define the natural numbers, or you could be thinking about the real numbers, and then you need to define those as well first, but for now let's stick with the von Neumann ordinals and see where it takes us.

Note that even in the case of Peano arithmetic or ring theory, the symbol for $2$ and the symbol for $4$ are not part of the language. They are used as shorthand for either repeated sums of $1$ or repeated application of the successor function to $0$, or so on.

So if $2$ is defined as $1+1$ and $4$ is defined as $((1+1)+1)+1$, and you have an axiom saying that $(x+y)+z=x+(y+z)$, then you're practically done: $(1+1)+(1+1)=((1+1)+1)+1$, so $2+2=4$. But okay, let's go back to set theory.

We have the natural numbers, so $2=varnothing,varnothing$ and $4$, well, let's just write $4$. After this you need to ask what is $+$. Do you think about $+$ as a recursive definition of applying the successor function? Even the Peano axioms which usually form the basis for arithmetic have $+$ as a standalone object, and there is a connection between $+$ and the successor function. There are two standard ways to define what is $+$ on the natural numbers in the context of set theory:

1. Successive application of the successor function, so $x+0=x$ and $x+S(y)=S(x+y)$. In that case, $2+2=S(1)+S(1)=S(S(0))+S(S(0))=dots=S(S(S(S(0))))$. And now we can also translate back into sets to get "a fully set theoretic statement". But it's awful, and I don't want to do it.



2. 
   

   Using cardinality of sets. Note that $n$ is a set with exactly $n$ elements. $0$ has no elements and $1$ has exactly one element (which is $0$, as it turns out). So we can define $n+m=k$ if and only if the number of elements in a disjoint union of a copy of $n$ and a copy of $m$, is $k$. Or, in modern terms, there is a bijection between the two sets.

   
   
   

   In that case, one needs to write down a function from $langle 0,0rangle,langle 0,1ranglecuplangle 1,0rangle,langle 1,1rangle$, or $0times2cup1times2$, and $4$ which is $0,1,2,3$. Of course, this starts with defining what is an ordered pair from a set theoretic view, what is a function, etc., and then write this as a set theoretic expression again. Which, as before, is an awful exercise in futility.

   
   

The easiest way, at the end, is to prove this "by blocks". First prove there is a way to formalize the natural numbers, then formalize addition, then show that no matter what formalization you chose, as long as it satisfies certain properties (which you would expect from the natural numbers), it has to be the case that the object corresponding to $2+2$ is the object corresponding to $4$.

---

Or just be annoying and declare that you interpret $2,+$ and $4$ in a non-standard way so $2+2=5neq 4$. Whatever floats your boat.

share|cite|improve this answer

answered Jul 23 at 13:38

Asaf Karagila

291k31402732

Zermelo–Fraenkel set theory is formulated in a language that has a binary relation $in$, and that's it. The symbols $1,2,3,4$ and $+$ make "no sense" from a syntactic point of view.

So first one needs to explain what is $2$ in the context of set theory. This means that you need to define some sets that will behave like you would expect of the natural numbers. Normally, these are the finite von Neumann ordinals, defined recursively as $0=varnothing$ and $n+1=ncupn$. There are other ways to define the natural numbers, or you could be thinking about the real numbers, and then you need to define those as well first, but for now let's stick with the von Neumann ordinals and see where it takes us.

Note that even in the case of Peano arithmetic or ring theory, the symbol for $2$ and the symbol for $4$ are not part of the language. They are used as shorthand for either repeated sums of $1$ or repeated application of the successor function to $0$, or so on.

So if $2$ is defined as $1+1$ and $4$ is defined as $((1+1)+1)+1$, and you have an axiom saying that $(x+y)+z=x+(y+z)$, then you're practically done: $(1+1)+(1+1)=((1+1)+1)+1$, so $2+2=4$. But okay, let's go back to set theory.

We have the natural numbers, so $2=varnothing,varnothing$ and $4$, well, let's just write $4$. After this you need to ask what is $+$. Do you think about $+$ as a recursive definition of applying the successor function? Even the Peano axioms which usually form the basis for arithmetic have $+$ as a standalone object, and there is a connection between $+$ and the successor function. There are two standard ways to define what is $+$ on the natural numbers in the context of set theory:

1. Successive application of the successor function, so $x+0=x$ and $x+S(y)=S(x+y)$. In that case, $2+2=S(1)+S(1)=S(S(0))+S(S(0))=dots=S(S(S(S(0))))$. And now we can also translate back into sets to get "a fully set theoretic statement". But it's awful, and I don't want to do it.



2. 
   

   Using cardinality of sets. Note that $n$ is a set with exactly $n$ elements. $0$ has no elements and $1$ has exactly one element (which is $0$, as it turns out). So we can define $n+m=k$ if and only if the number of elements in a disjoint union of a copy of $n$ and a copy of $m$, is $k$. Or, in modern terms, there is a bijection between the two sets.

   
   
   

   In that case, one needs to write down a function from $langle 0,0rangle,langle 0,1ranglecuplangle 1,0rangle,langle 1,1rangle$, or $0times2cup1times2$, and $4$ which is $0,1,2,3$. Of course, this starts with defining what is an ordered pair from a set theoretic view, what is a function, etc., and then write this as a set theoretic expression again. Which, as before, is an awful exercise in futility.

   
   

The easiest way, at the end, is to prove this "by blocks". First prove there is a way to formalize the natural numbers, then formalize addition, then show that no matter what formalization you chose, as long as it satisfies certain properties (which you would expect from the natural numbers), it has to be the case that the object corresponding to $2+2$ is the object corresponding to $4$.

---

Or just be annoying and declare that you interpret $2,+$ and $4$ in a non-standard way so $2+2=5neq 4$. Whatever floats your boat.

share|cite|improve this answer

answered Jul 23 at 13:38

Asaf Karagila

291k31402732

share|cite|improve this answer

share|cite|improve this answer

answered Jul 23 at 13:38

Asaf Karagila

291k31402732

answered Jul 23 at 13:38

Asaf Karagila

291k31402732

answered Jul 23 at 13:38

Asaf Karagila

291k31402732

291k31402732

• 
  
  
  

  
  

  
  
  
  
  
  

  
  Thank you for making it clear, so in Principia Mathematica what were they using to prove 1+1=2 because it seemed fairly abstract in terms of logic symbols?
  – John Miller
  Jul 23 at 14:15
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  I haven't read PM, because from a modern point of view, it's a ginormous waste of time unless you want to study some very specific things related to the text there. (I'm not, however, disparaging reading the book as a historical landmark of a huge undertaking to formalize mathematics, that was great.) So I can't quite help you with what and how they did things there. But if my memory serves me right, it takes them a couple hundred pages to finish formalizing the basics first so they can prove $1+1=2$. I think they use a type-theoretic approach, which is a different way to formalize mathematics
  – Asaf Karagila
  Jul 23 at 14:18
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  "and you have an axiom saying that (x+y)+z=x+(y+z)" I thought it was common to use axioms for Peano arithmetic where the associative law was not an axiom, but rather a theorem.
  – Doug Spoonwood
  Jul 29 at 21:42
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @Doug: I meant that in the context of the axioms of a field (or at least ring theory). In the case of PA you need to prove it, yes.
  – Asaf Karagila
  Jul 29 at 21:45
  
  

  
  
  
  

add a comment | 

• 
  
  
  

  
  

  
  
  
  
  
  

  
  Thank you for making it clear, so in Principia Mathematica what were they using to prove 1+1=2 because it seemed fairly abstract in terms of logic symbols?
  – John Miller
  Jul 23 at 14:15
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  I haven't read PM, because from a modern point of view, it's a ginormous waste of time unless you want to study some very specific things related to the text there. (I'm not, however, disparaging reading the book as a historical landmark of a huge undertaking to formalize mathematics, that was great.) So I can't quite help you with what and how they did things there. But if my memory serves me right, it takes them a couple hundred pages to finish formalizing the basics first so they can prove $1+1=2$. I think they use a type-theoretic approach, which is a different way to formalize mathematics
  – Asaf Karagila
  Jul 23 at 14:18
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  "and you have an axiom saying that (x+y)+z=x+(y+z)" I thought it was common to use axioms for Peano arithmetic where the associative law was not an axiom, but rather a theorem.
  – Doug Spoonwood
  Jul 29 at 21:42
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @Doug: I meant that in the context of the axioms of a field (or at least ring theory). In the case of PA you need to prove it, yes.
  – Asaf Karagila
  Jul 29 at 21:45
  
  

  
  
  
  

Thank you for making it clear, so in Principia Mathematica what were they using to prove 1+1=2 because it seemed fairly abstract in terms of logic symbols?
– John Miller
Jul 23 at 14:15

Thank you for making it clear, so in Principia Mathematica what were they using to prove 1+1=2 because it seemed fairly abstract in terms of logic symbols?
– John Miller
Jul 23 at 14:15

1

1

I haven't read PM, because from a modern point of view, it's a ginormous waste of time unless you want to study some very specific things related to the text there. (I'm not, however, disparaging reading the book as a historical landmark of a huge undertaking to formalize mathematics, that was great.) So I can't quite help you with what and how they did things there. But if my memory serves me right, it takes them a couple hundred pages to finish formalizing the basics first so they can prove $1+1=2$. I think they use a type-theoretic approach, which is a different way to formalize mathematics
– Asaf Karagila
Jul 23 at 14:18

I haven't read PM, because from a modern point of view, it's a ginormous waste of time unless you want to study some very specific things related to the text there. (I'm not, however, disparaging reading the book as a historical landmark of a huge undertaking to formalize mathematics, that was great.) So I can't quite help you with what and how they did things there. But if my memory serves me right, it takes them a couple hundred pages to finish formalizing the basics first so they can prove $1+1=2$. I think they use a type-theoretic approach, which is a different way to formalize mathematics
– Asaf Karagila
Jul 23 at 14:18

"and you have an axiom saying that (x+y)+z=x+(y+z)" I thought it was common to use axioms for Peano arithmetic where the associative law was not an axiom, but rather a theorem.
– Doug Spoonwood
Jul 29 at 21:42

"and you have an axiom saying that (x+y)+z=x+(y+z)" I thought it was common to use axioms for Peano arithmetic where the associative law was not an axiom, but rather a theorem.
– Doug Spoonwood
Jul 29 at 21:42

1

1

@Doug: I meant that in the context of the axioms of a field (or at least ring theory). In the case of PA you need to prove it, yes.
– Asaf Karagila
Jul 29 at 21:45

@Doug: I meant that in the context of the axioms of a field (or at least ring theory). In the case of PA you need to prove it, yes.
– Asaf Karagila
Jul 29 at 21:45

add a comment | 

up vote
3
down vote

In the ZFC axioms system, natural numbers are represented by sets. For example, $0$ is usually represented by the empty set $emptyset = $.

You can represent the successor of a number in different ways. One common way of doing so is representing any number greater than $0$ as the set of all smaller numbers. Thus, $1=emptyset$, $2=0,1 = emptyset,emptyset $.

This has the nice property that $a < b$ iff $a in b$ iff $asubset b$.

We can compute thus the successor of a number as $s(a) = acup a$. We note that the predecessor is also easy to compute.

Summation is defined recursively, such that $a+0 = a$, and $a+s(b) = s(a)+b$.

Applying these two rules repeatedly gives us that $2+2 = 3+1 = 4+0 = 4$

share|cite|improve this answer

answered Jul 23 at 13:29

Jsevillamol

3,01911124

• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  I would only add that $a<b$ is defined as $ain b$, it is not just equivalent
  – Holo
  Jul 23 at 13:38
  

  
  
  
  

add a comment | 

up vote
3
down vote

In the ZFC axioms system, natural numbers are represented by sets. For example, $0$ is usually represented by the empty set $emptyset = $.

You can represent the successor of a number in different ways. One common way of doing so is representing any number greater than $0$ as the set of all smaller numbers. Thus, $1=emptyset$, $2=0,1 = emptyset,emptyset $.

This has the nice property that $a < b$ iff $a in b$ iff $asubset b$.

We can compute thus the successor of a number as $s(a) = acup a$. We note that the predecessor is also easy to compute.

Summation is defined recursively, such that $a+0 = a$, and $a+s(b) = s(a)+b$.

Applying these two rules repeatedly gives us that $2+2 = 3+1 = 4+0 = 4$

share|cite|improve this answer

answered Jul 23 at 13:29

Jsevillamol

3,01911124

• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  I would only add that $a<b$ is defined as $ain b$, it is not just equivalent
  – Holo
  Jul 23 at 13:38
  

  
  
  
  

add a comment | 

up vote
3
down vote

up vote
3
down vote

In the ZFC axioms system, natural numbers are represented by sets. For example, $0$ is usually represented by the empty set $emptyset = $.

You can represent the successor of a number in different ways. One common way of doing so is representing any number greater than $0$ as the set of all smaller numbers. Thus, $1=emptyset$, $2=0,1 = emptyset,emptyset $.

This has the nice property that $a < b$ iff $a in b$ iff $asubset b$.

We can compute thus the successor of a number as $s(a) = acup a$. We note that the predecessor is also easy to compute.

Summation is defined recursively, such that $a+0 = a$, and $a+s(b) = s(a)+b$.

Applying these two rules repeatedly gives us that $2+2 = 3+1 = 4+0 = 4$

share|cite|improve this answer

answered Jul 23 at 13:29

Jsevillamol

3,01911124

In the ZFC axioms system, natural numbers are represented by sets. For example, $0$ is usually represented by the empty set $emptyset = $.

You can represent the successor of a number in different ways. One common way of doing so is representing any number greater than $0$ as the set of all smaller numbers. Thus, $1=emptyset$, $2=0,1 = emptyset,emptyset $.

This has the nice property that $a < b$ iff $a in b$ iff $asubset b$.

We can compute thus the successor of a number as $s(a) = acup a$. We note that the predecessor is also easy to compute.

Summation is defined recursively, such that $a+0 = a$, and $a+s(b) = s(a)+b$.

Applying these two rules repeatedly gives us that $2+2 = 3+1 = 4+0 = 4$

share|cite|improve this answer

answered Jul 23 at 13:29

Jsevillamol

3,01911124

share|cite|improve this answer

share|cite|improve this answer

answered Jul 23 at 13:29

Jsevillamol

3,01911124

answered Jul 23 at 13:29

Jsevillamol

3,01911124

answered Jul 23 at 13:29

Jsevillamol

3,01911124

3,01911124

• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  I would only add that $a<b$ is defined as $ain b$, it is not just equivalent
  – Holo
  Jul 23 at 13:38
  

  
  
  
  

add a comment | 

• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  I would only add that $a<b$ is defined as $ain b$, it is not just equivalent
  – Holo
  Jul 23 at 13:38
  

  
  
  
  

1

1

I would only add that $a<b$ is defined as $ain b$, it is not just equivalent
– Holo
Jul 23 at 13:38

I would only add that $a<b$ is defined as $ain b$, it is not just equivalent
– Holo
Jul 23 at 13:38

add a comment | 

up vote
3
down vote

In ZFC you would usually construct the addition function by recursion, so by the general recursion theorem it would satisfy the recursion equations
$$ a + 0 = a \ a+S(b) = S(a+b) $$
where $S$ is the function that takes a natural number to its successor.

After proving that $2=S(S(0))$ and $4=S(S(S(S(0))))$ (which you may well have considered to be definitions in the first place), it is as simple as
$$ beginalign 2+2 &= 2 + S(S(0)) \
&= S(2+S(0)) \
&= S(S( 2+ 0 )) \
&= S(S( 2 )) \
&= S(S(S(S(0)))) \
&= 4 endalign $$

Depending on the underlying formalization of first-order logic, expressing this equational reasoning as a formal may be more or less cumbersome. In particular, doing it halfway readably depends on the ability to introduce new term notations (such as $x+y$) other than the ones present in the original logical language, and most proof systems for first-order logic are content to let that be handled by considering atomic formulas that involve the new terms to be abbreviations of a more complex nest of quantifiers.

So if you compare PM to the combination of orthodox textbook FOL + ZFC, the latter may not necessarily come out ahead.

On the other hand, modern proof assistants have shown that formal reasoning in first-order logic can be done much smoother than by the textbook proof systems -- e.g. by embedding FOL in a suitable higher-order system where the equational reasoning above can be done more or less directly, and then proving once and for all that this higher-order system is conservative over first-order logic.

share|cite|improve this answer

edited Jul 23 at 13:37

answered Jul 23 at 13:31

Henning Makholm

225k16290516

add a comment | 

up vote
3
down vote

In ZFC you would usually construct the addition function by recursion, so by the general recursion theorem it would satisfy the recursion equations
$$ a + 0 = a \ a+S(b) = S(a+b) $$
where $S$ is the function that takes a natural number to its successor.

After proving that $2=S(S(0))$ and $4=S(S(S(S(0))))$ (which you may well have considered to be definitions in the first place), it is as simple as
$$ beginalign 2+2 &= 2 + S(S(0)) \
&= S(2+S(0)) \
&= S(S( 2+ 0 )) \
&= S(S( 2 )) \
&= S(S(S(S(0)))) \
&= 4 endalign $$

Depending on the underlying formalization of first-order logic, expressing this equational reasoning as a formal may be more or less cumbersome. In particular, doing it halfway readably depends on the ability to introduce new term notations (such as $x+y$) other than the ones present in the original logical language, and most proof systems for first-order logic are content to let that be handled by considering atomic formulas that involve the new terms to be abbreviations of a more complex nest of quantifiers.

So if you compare PM to the combination of orthodox textbook FOL + ZFC, the latter may not necessarily come out ahead.

On the other hand, modern proof assistants have shown that formal reasoning in first-order logic can be done much smoother than by the textbook proof systems -- e.g. by embedding FOL in a suitable higher-order system where the equational reasoning above can be done more or less directly, and then proving once and for all that this higher-order system is conservative over first-order logic.

share|cite|improve this answer

edited Jul 23 at 13:37

answered Jul 23 at 13:31

Henning Makholm

225k16290516

add a comment | 

up vote
3
down vote

up vote
3
down vote

In ZFC you would usually construct the addition function by recursion, so by the general recursion theorem it would satisfy the recursion equations
$$ a + 0 = a \ a+S(b) = S(a+b) $$
where $S$ is the function that takes a natural number to its successor.

After proving that $2=S(S(0))$ and $4=S(S(S(S(0))))$ (which you may well have considered to be definitions in the first place), it is as simple as
$$ beginalign 2+2 &= 2 + S(S(0)) \
&= S(2+S(0)) \
&= S(S( 2+ 0 )) \
&= S(S( 2 )) \
&= S(S(S(S(0)))) \
&= 4 endalign $$

Depending on the underlying formalization of first-order logic, expressing this equational reasoning as a formal may be more or less cumbersome. In particular, doing it halfway readably depends on the ability to introduce new term notations (such as $x+y$) other than the ones present in the original logical language, and most proof systems for first-order logic are content to let that be handled by considering atomic formulas that involve the new terms to be abbreviations of a more complex nest of quantifiers.

So if you compare PM to the combination of orthodox textbook FOL + ZFC, the latter may not necessarily come out ahead.

On the other hand, modern proof assistants have shown that formal reasoning in first-order logic can be done much smoother than by the textbook proof systems -- e.g. by embedding FOL in a suitable higher-order system where the equational reasoning above can be done more or less directly, and then proving once and for all that this higher-order system is conservative over first-order logic.

share|cite|improve this answer

edited Jul 23 at 13:37

answered Jul 23 at 13:31

Henning Makholm

225k16290516

In ZFC you would usually construct the addition function by recursion, so by the general recursion theorem it would satisfy the recursion equations
$$ a + 0 = a \ a+S(b) = S(a+b) $$
where $S$ is the function that takes a natural number to its successor.

After proving that $2=S(S(0))$ and $4=S(S(S(S(0))))$ (which you may well have considered to be definitions in the first place), it is as simple as
$$ beginalign 2+2 &= 2 + S(S(0)) \
&= S(2+S(0)) \
&= S(S( 2+ 0 )) \
&= S(S( 2 )) \
&= S(S(S(S(0)))) \
&= 4 endalign $$

Depending on the underlying formalization of first-order logic, expressing this equational reasoning as a formal may be more or less cumbersome. In particular, doing it halfway readably depends on the ability to introduce new term notations (such as $x+y$) other than the ones present in the original logical language, and most proof systems for first-order logic are content to let that be handled by considering atomic formulas that involve the new terms to be abbreviations of a more complex nest of quantifiers.

So if you compare PM to the combination of orthodox textbook FOL + ZFC, the latter may not necessarily come out ahead.

On the other hand, modern proof assistants have shown that formal reasoning in first-order logic can be done much smoother than by the textbook proof systems -- e.g. by embedding FOL in a suitable higher-order system where the equational reasoning above can be done more or less directly, and then proving once and for all that this higher-order system is conservative over first-order logic.

share|cite|improve this answer

edited Jul 23 at 13:37

answered Jul 23 at 13:31

Henning Makholm

225k16290516

share|cite|improve this answer

share|cite|improve this answer

edited Jul 23 at 13:37

edited Jul 23 at 13:37

edited Jul 23 at 13:37

answered Jul 23 at 13:31

Henning Makholm

225k16290516

answered Jul 23 at 13:31

Henning Makholm

225k16290516

answered Jul 23 at 13:31

Henning Makholm

225k16290516

225k16290516

add a comment | 

add a comment | 

up vote
1
down vote

First, you need to construct the numbers you are using. It can be the natural numbers set.
You can use the famous construction $emptyset$ for $0$, $emptyset$ for $1$, $emptyset, emptyset$ for $2$ and so on.
After that, you need to construct a $+$ operator. It can be a function $+:mathbbN^2rightarrowmathbbN$. This function can be constructed as a set of pairs $((a,b),c)$ satisfying some condition on $a$, $b$ and $c$. An ordered pair can be constructed with the Kuratowski definition.
Finally you can check if $2+2=4$.

Axiomatic Set Theory is an accepted foundations of mathematics, where you can construct all of mathematics(not sure of that). However, no one will ever do these constructions by hand.

Imagine you want to express the explicit construction of the tangent bundle of a smooth manifold. That would be huge and confusing.

share|cite|improve this answer

edited Jul 23 at 13:55

answered Jul 23 at 13:24

Cristhian Grundmann

765

• 
  
  
  

  
  

  
  
  
  
  
  

  
  First "construct all of mathematics" is a little too much for now, as contradiction free model has some problems with it(godel incompleteness theorem). Secondly how can you define $+$ using itself? The definition of $+$ in ZFC is:$$n+0=n\n+(m+1)=(n+m)+1\n+k=supn+mmid m<k$$ for $k$ limit ordinal and $A+1=S(A)$
  – Holo
  Jul 23 at 13:36
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  Oh, what I mean was not to use $a+b=c$ as a condition, but rather use some well defined condition. It would depend on the previous constructions.
  – Cristhian Grundmann
  Jul 23 at 13:54
  

  
  
  
  

add a comment | 

up vote
1
down vote

First, you need to construct the numbers you are using. It can be the natural numbers set.
You can use the famous construction $emptyset$ for $0$, $emptyset$ for $1$, $emptyset, emptyset$ for $2$ and so on.
After that, you need to construct a $+$ operator. It can be a function $+:mathbbN^2rightarrowmathbbN$. This function can be constructed as a set of pairs $((a,b),c)$ satisfying some condition on $a$, $b$ and $c$. An ordered pair can be constructed with the Kuratowski definition.
Finally you can check if $2+2=4$.

Axiomatic Set Theory is an accepted foundations of mathematics, where you can construct all of mathematics(not sure of that). However, no one will ever do these constructions by hand.

Imagine you want to express the explicit construction of the tangent bundle of a smooth manifold. That would be huge and confusing.

share|cite|improve this answer

edited Jul 23 at 13:55

answered Jul 23 at 13:24

Cristhian Grundmann

765

• 
  
  
  

  
  

  
  
  
  
  
  

  
  First "construct all of mathematics" is a little too much for now, as contradiction free model has some problems with it(godel incompleteness theorem). Secondly how can you define $+$ using itself? The definition of $+$ in ZFC is:$$n+0=n\n+(m+1)=(n+m)+1\n+k=supn+mmid m<k$$ for $k$ limit ordinal and $A+1=S(A)$
  – Holo
  Jul 23 at 13:36
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  Oh, what I mean was not to use $a+b=c$ as a condition, but rather use some well defined condition. It would depend on the previous constructions.
  – Cristhian Grundmann
  Jul 23 at 13:54
  

  
  
  
  

add a comment | 

up vote
1
down vote

up vote
1
down vote

First, you need to construct the numbers you are using. It can be the natural numbers set.
You can use the famous construction $emptyset$ for $0$, $emptyset$ for $1$, $emptyset, emptyset$ for $2$ and so on.
After that, you need to construct a $+$ operator. It can be a function $+:mathbbN^2rightarrowmathbbN$. This function can be constructed as a set of pairs $((a,b),c)$ satisfying some condition on $a$, $b$ and $c$. An ordered pair can be constructed with the Kuratowski definition.
Finally you can check if $2+2=4$.

Axiomatic Set Theory is an accepted foundations of mathematics, where you can construct all of mathematics(not sure of that). However, no one will ever do these constructions by hand.

Imagine you want to express the explicit construction of the tangent bundle of a smooth manifold. That would be huge and confusing.

share|cite|improve this answer

edited Jul 23 at 13:55

answered Jul 23 at 13:24

Cristhian Grundmann

765

First, you need to construct the numbers you are using. It can be the natural numbers set.
You can use the famous construction $emptyset$ for $0$, $emptyset$ for $1$, $emptyset, emptyset$ for $2$ and so on.
After that, you need to construct a $+$ operator. It can be a function $+:mathbbN^2rightarrowmathbbN$. This function can be constructed as a set of pairs $((a,b),c)$ satisfying some condition on $a$, $b$ and $c$. An ordered pair can be constructed with the Kuratowski definition.
Finally you can check if $2+2=4$.

Axiomatic Set Theory is an accepted foundations of mathematics, where you can construct all of mathematics(not sure of that). However, no one will ever do these constructions by hand.

Imagine you want to express the explicit construction of the tangent bundle of a smooth manifold. That would be huge and confusing.

share|cite|improve this answer

edited Jul 23 at 13:55

answered Jul 23 at 13:24

Cristhian Grundmann

765

share|cite|improve this answer

share|cite|improve this answer

edited Jul 23 at 13:55

edited Jul 23 at 13:55

edited Jul 23 at 13:55

answered Jul 23 at 13:24

Cristhian Grundmann

765

answered Jul 23 at 13:24

Cristhian Grundmann

765

answered Jul 23 at 13:24

Cristhian Grundmann

765

765

• 
  
  
  

  
  

  
  
  
  
  
  

  
  First "construct all of mathematics" is a little too much for now, as contradiction free model has some problems with it(godel incompleteness theorem). Secondly how can you define $+$ using itself? The definition of $+$ in ZFC is:$$n+0=n\n+(m+1)=(n+m)+1\n+k=supn+mmid m<k$$ for $k$ limit ordinal and $A+1=S(A)$
  – Holo
  Jul 23 at 13:36
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  Oh, what I mean was not to use $a+b=c$ as a condition, but rather use some well defined condition. It would depend on the previous constructions.
  – Cristhian Grundmann
  Jul 23 at 13:54
  

  
  
  
  

add a comment | 

• 
  
  
  

  
  

  
  
  
  
  
  

  
  First "construct all of mathematics" is a little too much for now, as contradiction free model has some problems with it(godel incompleteness theorem). Secondly how can you define $+$ using itself? The definition of $+$ in ZFC is:$$n+0=n\n+(m+1)=(n+m)+1\n+k=supn+mmid m<k$$ for $k$ limit ordinal and $A+1=S(A)$
  – Holo
  Jul 23 at 13:36
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  Oh, what I mean was not to use $a+b=c$ as a condition, but rather use some well defined condition. It would depend on the previous constructions.
  – Cristhian Grundmann
  Jul 23 at 13:54
  

  
  
  
  

First "construct all of mathematics" is a little too much for now, as contradiction free model has some problems with it(godel incompleteness theorem). Secondly how can you define $+$ using itself? The definition of $+$ in ZFC is:$$n+0=n\n+(m+1)=(n+m)+1\n+k=supn+mmid m<k$$ for $k$ limit ordinal and $A+1=S(A)$
– Holo
Jul 23 at 13:36

First "construct all of mathematics" is a little too much for now, as contradiction free model has some problems with it(godel incompleteness theorem). Secondly how can you define $+$ using itself? The definition of $+$ in ZFC is:$$n+0=n\n+(m+1)=(n+m)+1\n+k=supn+mmid m<k$$ for $k$ limit ordinal and $A+1=S(A)$
– Holo
Jul 23 at 13:36

Oh, what I mean was not to use $a+b=c$ as a condition, but rather use some well defined condition. It would depend on the previous constructions.
– Cristhian Grundmann
Jul 23 at 13:54

Oh, what I mean was not to use $a+b=c$ as a condition, but rather use some well defined condition. It would depend on the previous constructions.
– Cristhian Grundmann
Jul 23 at 13:54

add a comment | 

up vote
0
down vote

The existing answers are more or less talking about ordinal addition. In terms of cardinals: Say $|A|$ denotes the cardinality of the set $A$. Saying $2+2=4$ then means this:

Theorem. If $Acap B=emptyset$, $|A|=|B|=2$, then $|Acup B|=4$.
$newcommandtwo0,1$
$newcommandfour0,1,2,3$

Now let's write $Asim B$ to mean that there exists a bijection from $A$ onto $B$. Then $|A|=2$ means that $Asim0,1$ (where here it doesn't matter what $0$ and $1$ are, all that matters is $0ne 1$), and similarly $|A|=4$ means $Asimfour$.

We need a lemma:

Lemma. $twosim2,3$.

And now to prove the theorem: Suppose $Acap B=emptyset$ and $|A|=|B|=2$. The lemma shows that $Bsim2,3$. Since $twocap2,3=emptyset$ it follows that $$Acup Bsimtwocup2,3=four.$$

Note About "ordinal addition" versus "cardinal addition": They are two different things. In fact $2$ and $4$ are cardinals and ordinals, so the statement "$2+2=4$" is a priori ambiguous, since we haven't specified whether we're talking about ordinal addition or cardinal addition. In hopefully obvious notation, the other answers are showing that $2+_o2=4$, while here we show that $2+_c2=4$.

By the standard definitions, a finite ordinal is the same as a finite cardinal, annd the two notions of addition for finite ordinals/cardinals come out the same. But it's important to realize that they really are different for infinite ordinals and infinite cardinals.

For example, say $omega$ is the first infinite ordinal and $aleph_0$ is the first infinite cardinal. Then, as sets, $omega=aleph_0$, but, at least in the way the notation is usually interpreted, $omega+omeganeomega$ while $aleph_0+aleph_0=aleph_0$. That's not a contradiction because the two plus signs mean different things; in more careful notation that nobody actually uses, $omega+_oomeganeomega$ and $aleph_0+_caleph_0=aleph_0$.

So when you see "$+$" in set theory you need to consider the context to determine whether it means $+_o$ or $+_c$.

share|cite|improve this answer

edited Jul 23 at 15:21

answered Jul 23 at 14:40

David C. Ullrich

54.1k33481

• 
  
  
  

  
  

  
  
  
  
  
  

  
  Oh okay, so I'm starting to think to prove something through ZFC almost means nothing, as there are so many ways to do so. I think I had this preconception that it was a specific set of axioms to describe how to postulate modern mathematics, but is it more of a general framework in which one can theorise freely?
  – John Miller
  Jul 23 at 14:49
  
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @JohnMiller ZFC is certainly a specific set of axioms. The above is an informal proof "in ZFC", in that every step could be justified using those axioms. (If you're confused by the fact that what I proved is totally different from what the other answers prove, see the Note I'm about to add to the answer...)
  – David C. Ullrich
  Jul 23 at 15:02
  

  
  
  
  

add a comment | 

up vote
0
down vote

The existing answers are more or less talking about ordinal addition. In terms of cardinals: Say $|A|$ denotes the cardinality of the set $A$. Saying $2+2=4$ then means this:

Theorem. If $Acap B=emptyset$, $|A|=|B|=2$, then $|Acup B|=4$.
$newcommandtwo0,1$
$newcommandfour0,1,2,3$

Now let's write $Asim B$ to mean that there exists a bijection from $A$ onto $B$. Then $|A|=2$ means that $Asim0,1$ (where here it doesn't matter what $0$ and $1$ are, all that matters is $0ne 1$), and similarly $|A|=4$ means $Asimfour$.

We need a lemma:

Lemma. $twosim2,3$.

And now to prove the theorem: Suppose $Acap B=emptyset$ and $|A|=|B|=2$. The lemma shows that $Bsim2,3$. Since $twocap2,3=emptyset$ it follows that $$Acup Bsimtwocup2,3=four.$$

Note About "ordinal addition" versus "cardinal addition": They are two different things. In fact $2$ and $4$ are cardinals and ordinals, so the statement "$2+2=4$" is a priori ambiguous, since we haven't specified whether we're talking about ordinal addition or cardinal addition. In hopefully obvious notation, the other answers are showing that $2+_o2=4$, while here we show that $2+_c2=4$.

By the standard definitions, a finite ordinal is the same as a finite cardinal, annd the two notions of addition for finite ordinals/cardinals come out the same. But it's important to realize that they really are different for infinite ordinals and infinite cardinals.

For example, say $omega$ is the first infinite ordinal and $aleph_0$ is the first infinite cardinal. Then, as sets, $omega=aleph_0$, but, at least in the way the notation is usually interpreted, $omega+omeganeomega$ while $aleph_0+aleph_0=aleph_0$. That's not a contradiction because the two plus signs mean different things; in more careful notation that nobody actually uses, $omega+_oomeganeomega$ and $aleph_0+_caleph_0=aleph_0$.

So when you see "$+$" in set theory you need to consider the context to determine whether it means $+_o$ or $+_c$.

share|cite|improve this answer

edited Jul 23 at 15:21

answered Jul 23 at 14:40

David C. Ullrich

54.1k33481

• 
  
  
  

  
  

  
  
  
  
  
  

  
  Oh okay, so I'm starting to think to prove something through ZFC almost means nothing, as there are so many ways to do so. I think I had this preconception that it was a specific set of axioms to describe how to postulate modern mathematics, but is it more of a general framework in which one can theorise freely?
  – John Miller
  Jul 23 at 14:49
  
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @JohnMiller ZFC is certainly a specific set of axioms. The above is an informal proof "in ZFC", in that every step could be justified using those axioms. (If you're confused by the fact that what I proved is totally different from what the other answers prove, see the Note I'm about to add to the answer...)
  – David C. Ullrich
  Jul 23 at 15:02
  

  
  
  
  

add a comment | 

up vote
0
down vote

up vote
0
down vote

The existing answers are more or less talking about ordinal addition. In terms of cardinals: Say $|A|$ denotes the cardinality of the set $A$. Saying $2+2=4$ then means this:

Theorem. If $Acap B=emptyset$, $|A|=|B|=2$, then $|Acup B|=4$.
$newcommandtwo0,1$
$newcommandfour0,1,2,3$

Now let's write $Asim B$ to mean that there exists a bijection from $A$ onto $B$. Then $|A|=2$ means that $Asim0,1$ (where here it doesn't matter what $0$ and $1$ are, all that matters is $0ne 1$), and similarly $|A|=4$ means $Asimfour$.

We need a lemma:

Lemma. $twosim2,3$.

And now to prove the theorem: Suppose $Acap B=emptyset$ and $|A|=|B|=2$. The lemma shows that $Bsim2,3$. Since $twocap2,3=emptyset$ it follows that $$Acup Bsimtwocup2,3=four.$$

Note About "ordinal addition" versus "cardinal addition": They are two different things. In fact $2$ and $4$ are cardinals and ordinals, so the statement "$2+2=4$" is a priori ambiguous, since we haven't specified whether we're talking about ordinal addition or cardinal addition. In hopefully obvious notation, the other answers are showing that $2+_o2=4$, while here we show that $2+_c2=4$.

By the standard definitions, a finite ordinal is the same as a finite cardinal, annd the two notions of addition for finite ordinals/cardinals come out the same. But it's important to realize that they really are different for infinite ordinals and infinite cardinals.

For example, say $omega$ is the first infinite ordinal and $aleph_0$ is the first infinite cardinal. Then, as sets, $omega=aleph_0$, but, at least in the way the notation is usually interpreted, $omega+omeganeomega$ while $aleph_0+aleph_0=aleph_0$. That's not a contradiction because the two plus signs mean different things; in more careful notation that nobody actually uses, $omega+_oomeganeomega$ and $aleph_0+_caleph_0=aleph_0$.

So when you see "$+$" in set theory you need to consider the context to determine whether it means $+_o$ or $+_c$.

share|cite|improve this answer

edited Jul 23 at 15:21

answered Jul 23 at 14:40

David C. Ullrich

54.1k33481

The existing answers are more or less talking about ordinal addition. In terms of cardinals: Say $|A|$ denotes the cardinality of the set $A$. Saying $2+2=4$ then means this:

Theorem. If $Acap B=emptyset$, $|A|=|B|=2$, then $|Acup B|=4$.
$newcommandtwo0,1$
$newcommandfour0,1,2,3$

Now let's write $Asim B$ to mean that there exists a bijection from $A$ onto $B$. Then $|A|=2$ means that $Asim0,1$ (where here it doesn't matter what $0$ and $1$ are, all that matters is $0ne 1$), and similarly $|A|=4$ means $Asimfour$.

We need a lemma:

Lemma. $twosim2,3$.

And now to prove the theorem: Suppose $Acap B=emptyset$ and $|A|=|B|=2$. The lemma shows that $Bsim2,3$. Since $twocap2,3=emptyset$ it follows that $$Acup Bsimtwocup2,3=four.$$

Note About "ordinal addition" versus "cardinal addition": They are two different things. In fact $2$ and $4$ are cardinals and ordinals, so the statement "$2+2=4$" is a priori ambiguous, since we haven't specified whether we're talking about ordinal addition or cardinal addition. In hopefully obvious notation, the other answers are showing that $2+_o2=4$, while here we show that $2+_c2=4$.

By the standard definitions, a finite ordinal is the same as a finite cardinal, annd the two notions of addition for finite ordinals/cardinals come out the same. But it's important to realize that they really are different for infinite ordinals and infinite cardinals.

For example, say $omega$ is the first infinite ordinal and $aleph_0$ is the first infinite cardinal. Then, as sets, $omega=aleph_0$, but, at least in the way the notation is usually interpreted, $omega+omeganeomega$ while $aleph_0+aleph_0=aleph_0$. That's not a contradiction because the two plus signs mean different things; in more careful notation that nobody actually uses, $omega+_oomeganeomega$ and $aleph_0+_caleph_0=aleph_0$.

So when you see "$+$" in set theory you need to consider the context to determine whether it means $+_o$ or $+_c$.

share|cite|improve this answer

edited Jul 23 at 15:21

answered Jul 23 at 14:40

David C. Ullrich

54.1k33481

share|cite|improve this answer

share|cite|improve this answer

edited Jul 23 at 15:21

edited Jul 23 at 15:21

edited Jul 23 at 15:21

answered Jul 23 at 14:40

David C. Ullrich

54.1k33481

answered Jul 23 at 14:40

David C. Ullrich

54.1k33481

answered Jul 23 at 14:40

David C. Ullrich

54.1k33481

54.1k33481

• 
  
  
  

  
  

  
  
  
  
  
  

  
  Oh okay, so I'm starting to think to prove something through ZFC almost means nothing, as there are so many ways to do so. I think I had this preconception that it was a specific set of axioms to describe how to postulate modern mathematics, but is it more of a general framework in which one can theorise freely?
  – John Miller
  Jul 23 at 14:49
  
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @JohnMiller ZFC is certainly a specific set of axioms. The above is an informal proof "in ZFC", in that every step could be justified using those axioms. (If you're confused by the fact that what I proved is totally different from what the other answers prove, see the Note I'm about to add to the answer...)
  – David C. Ullrich
  Jul 23 at 15:02
  

  
  
  
  

add a comment | 

• 
  
  
  

  
  

  
  
  
  
  
  

  
  Oh okay, so I'm starting to think to prove something through ZFC almost means nothing, as there are so many ways to do so. I think I had this preconception that it was a specific set of axioms to describe how to postulate modern mathematics, but is it more of a general framework in which one can theorise freely?
  – John Miller
  Jul 23 at 14:49
  
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @JohnMiller ZFC is certainly a specific set of axioms. The above is an informal proof "in ZFC", in that every step could be justified using those axioms. (If you're confused by the fact that what I proved is totally different from what the other answers prove, see the Note I'm about to add to the answer...)
  – David C. Ullrich
  Jul 23 at 15:02
  

  
  
  
  

Oh okay, so I'm starting to think to prove something through ZFC almost means nothing, as there are so many ways to do so. I think I had this preconception that it was a specific set of axioms to describe how to postulate modern mathematics, but is it more of a general framework in which one can theorise freely?
– John Miller
Jul 23 at 14:49

Oh okay, so I'm starting to think to prove something through ZFC almost means nothing, as there are so many ways to do so. I think I had this preconception that it was a specific set of axioms to describe how to postulate modern mathematics, but is it more of a general framework in which one can theorise freely?
– John Miller
Jul 23 at 14:49

1

1

@JohnMiller ZFC is certainly a specific set of axioms. The above is an informal proof "in ZFC", in that every step could be justified using those axioms. (If you're confused by the fact that what I proved is totally different from what the other answers prove, see the Note I'm about to add to the answer...)
– David C. Ullrich
Jul 23 at 15:02

@JohnMiller ZFC is certainly a specific set of axioms. The above is an informal proof "in ZFC", in that every step could be justified using those axioms. (If you're confused by the fact that what I proved is totally different from what the other answers prove, see the Note I'm about to add to the answer...)
– David C. Ullrich
Jul 23 at 15:02

add a comment | 

 

draft saved

draft discarded

 

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2860346%2fhow-to-prove-22-4-using-zermelo-fraenkel-set-theory%23new-answer', 'question_page');

);

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Name Email

Name

Email

Name Email

Name

Email