Peano Arithmetic Puns

Some statements, like arithmetic on the natural numbers, seem too trivial to prove. In this video I explore how we can prove these statements using the peano axioms, and explain how the peano axioms give rise to arithmetic on the natural numbers. I made this video for 3Blue1Brown's Summer of Math Exposition.

Link: https://youtu.be/TQpHVtlXuyc

I'm reading https://plato.stanford.edu/entries/definitions/#DefNorFor and they have the following paragraph:

>Here the first equation—called the base clause—defines the value of the function when the exponent is 0. And the second clause—called the recursive clause—uses the value of the function when the exponent is n to define the value when the exponent is n+1. This is perfectly legitimate, according to the traditional account, because a theorem of Peano Arithmetic establishes that the above definition is equivalent to one in normal form.

Now what is that theorem and where can I find an article or book on it?

The reference they give is Moschovakis, Y., 1974, Elementary Induction on Abstract Structures, which is anything but elementary and doesn't seem to cover normal forms of definitions at all, at least at a level I can understand. I've been reading Suppes, P., 1957, Introduction to Logic which covers the normal forms of everything but inductive definitions at a level I can understand relatively easily. Ideally I'm looking for something at a similar level.

Say that P1(I) is an arbitrary predicate in Peano Arithmetic (PA), which accepts one argument I as a natural number.

Say that evalsP1(⎡P⎤,I) is a two-argument predicate that accepts the source code ⎡P⎤ of any arbitrary predicate P as a natural number, i.e. Gödel number, along with any arbitrary natural number I as input.

The predicate evalsP1 returns true if predicate P evaluates predicate P1 for argument I, and false if it does not.

Say that predicate P2(⎡P⎤) is defined as following:

P2(⎡P⎤) ⇔ ( ¬evalsP1(⎡P⎤,⎡P⎤) ⇒ P1(⎡P⎤) )

P2 accepts the source code ⎡P⎤ of any arbitrary predicate P as a natural number.

Now apply P2(⎡P2⎤) to itself:

¬evalsP1(⎡P2⎤,⎡P2⎤) ⇒ P1(⎡P⎤)

Case 1: Assume evalsP1(⎡P2⎤,⎡P2⎤) is false

In this case, according to evalsP1, P2 does not evaluate P1. However:

¬evalsP1(⎡P2⎤,⎡P2⎤) ⇒ P1(⎡P⎤)

¬false ⇒ P1(⎡P⎤)

true ⇒ P1(⎡P⎤)

P1(⎡P⎤)

So, unlike what evalsP1 reports on ⎡P2⎤, P2 does evaluate P1.

Case 2: Assume evalsP1(⎡P2⎤,⎡P2⎤) is true

In this case, according to evalsP1, P2 evaluates P1. However:

¬evalsP1(⎡P2⎤,⎡P2⎤) ⇒ P1(⎡P⎤)

¬true ⇒ P1(⎡P⎤)

false ⇒ P1(⎡P⎤)

false

So, unlike what evalsP1 reports on ⎡P2⎤, P2 does not evaluate P1.

Therefore, it is not possible to define in PA a predicate evalsP1(⎡P⎤,I) that will correctly determine from the source code ⎡P⎤ of any arbitrary predicate P and argument I if it evaluates a given predicate P1 or not.

Turing's halting problem is a special case of Rice theorem. We define halts2(⎡P⎤) as following:

halts2(⎡P⎤) ⇔ ( halts1(⎡P⎤,⎡P⎤) ⇒ loopForever(⎡P⎤) )

Apply halts2(⎡halts2⎤) to itself:

halts1(⎡halts2⎤,⎡halts2⎤) ⇒ loopForever(⎡halts2⎤)

Case 1: Assume halts1(⎡halts2⎤,⎡halts2⎤) is false

false ⇒ loopForever(⎡halts2⎤)

false

When halts1 reports that halts2 will not halt, then halt2 will halt with result false.

Case 2: Assume halts1(⎡halts2⎤,⎡halts2⎤) is true

true ⇒ loopForever(⎡halts2⎤)

loopForever(⎡halts2⎤)

When halts1 reports that halts2 halts, then halts2 loops forever.

Therefore, it is not possible to define in PA the predicate halts1(⎡P⎤,I) that will correctly determine from the source code ⎡P⎤ of any arbitrary predicate P if it halts on argument I.

Conclusion

Rice theorem and Turing's halting problem can be expressed an

By 'basic rules of arithmetic,' I mean addition and its commutative and associative properties, subtraction and its anticommuttative and antiassociative properties, multiplication and its properties, and division and its properties.

PS -- A few days ago I asked about an intuitive proof of PEMDAS, and today I'm asking this question. The reason is that I'm tutoring a struggling algebra student, and she seems to be struggling because she doesn't understand the 'why' behind it all. I'm hoping to show her the beauty of math, and I believe that starts with intuitively knowing the 'why' and not just following the teacher's rules. I hope these questions aren't bothering anyone!

There are proofs of PA's consistency using other sets of axioms that are not proven to be consistent.

So it's possible that PA is inconsistent, yes?

What if it is? What would it be possible to prove in PA? What would the implications be for mathematics in general? What would mathematicians have to do to "fix" this?

Hi. As a challenge, I tried to prove commutativity of addition in Peano arithmetic without first proving associativity. Could you please take a look and tell me if the proof is OK like this? I'm also open to criticism of proof style, writing, and rigor. Thanks in advance!

Careful: the proof has been updated, some of the discussion below refers to an earlier version.

Part 1

Part 2

Edit: Corrected Typos

I sometimes read the sentence “xx is provable in PA”(or ZFC). I knew about ZFC but didn’t know about PA so I looked it up. From what I have found, PA is a theory that relies on the Peano Axiom. The one that tells about natural numbers. But... Peano axiom uses terms from set theory like “set” or “map”, right? If PA is different from ZFC, then how are they even defined in PA?

A friend just pointed me to this: http://www.cs.nyu.edu/pipermail/fom/2011-September/015816.html

Was wondering if anyone who works in this field knows what the chances are that this is true and what the implications would be. My friend suggests that this would imply that ZFC is inconsistent. That doesn't sound right to me but foundations is not my field.

(Let's say, for concreteness, that our world was based on a non-standard model of arithmetic where PA was inconsistent.)

What would we do if, today, an inconsistency in the peano axioms was found?

Basically, set theory as we know it would be borked, since ZFC would also be inconsistent. Could we fix it somehow? How would other fields be affected?

EDIT: This apparently is examined in Pudlak's “Life in an Inconsistent World” https://math.stackexchange.com/q/706095/49592

Amateur mathematician here. I have read about formal logic and axiomatic systems and have encountered several axiomatic systems that have been proposed to "explain" all of mathematics. We are all familiar with Whitehead and Russell's Principia Mathematica, Zermelo-Fraenkel Set Theory, Peano Arithmetic, Lambda Calculus, and Second Order Arithmetic. Each of these systems attempts to form the basis of mathematics, but which one is truly the basis for mathematics? Are there any noticeable differences between them? Does it even matter whether which axiomatic system forms the basis for math? Although I have seen literature that cites ZFC as the basis, many other sources also use Peano Arithmetic or Second Order Arithmetic, especially for formal logic.

Are there any reasons to not accept Gentzen's use of transfinite induction in order to prove the consistency of PA? In particular, what is the cost of accepting transfinite induction in order to prove Con(PA), and do mathematical logicians/philosophers of mathematics tend to accept Gentzen's proof?

Thanks.

Hey everyone, I'm doing inductive proofs for some Theorems in Peano Arithmetic and I'm stuck on 2 of them.

AT30: x × y = y × x

Here's what I've gotten so far:

1. x × 0 = 0 AA8

2. 0 × x = 0 AT28

3. 0 = 0 × x 2, IR2

4. x × 0 = 0 × x 1, 3 IR3

5. Assume x × k = k × x

And I really am not sure how to proceed from here. I tried a few different ways but none of them panned out and I haven't been able to figure out the proof.

The second proof is:

AT35: x+y=x+v --> y=v

1. Assume 0+y=0+v

2. 0+y=y AT22

3. 0+v=v AT22

4. y=0+y 2, IR2

5. y=v 1,3,4 IR3

6. Then 0+y=0+v --> y=v

7. Assume k+y=k+v --> y=v

The way I progressed from here initially was to then assume k'+y=k'+v and work to get y=v from that and then close out the conditional proofs to get (k+y=k+v --> y=v) --> (k'+y=k'+v --> y=v). I don't know if that was the right way to go about it, but if it is I can't figure out how to prove y=v and if not I have no idea how to progress from here.

Any help would be greatly appreciated, thank you!

I was reading about complexity when I stumbled upon Presburger arithmetic. I was a bit surprised to read that it was decidable; while I have not formally been taught that much complexity theory, I was under the impression that Godel's Incompleteness Theorems said that this was not possible.

The wiki articles discuss the differences but I can only tell that it's due to a difference between axioms of Peano arithmetic and axioms of Presburger arithmetic. Could someone please explain to me why Godel's applies for one and not the other?

I have to do the following using these axioms PA1-7, the others below it are previously proved results I can use too.

[Sa] means the successor of a.

http://i39.tinypic.com/263c5ee.png

Base Case: y = S0

x.S0 = S0

→ x.0 + x = S0

→ 0 + x = S0

→ x = S0 & y=S0

Now the induction step is usually y=a to y=Sa, however this does not work here, I assume I need to take a new y and it's successor to proceed. Would anyone know how to proceed and which y to take?

Thanks

I know that Peano arithmetic is stronger than Robinson arithmetic and Presburger arithmetic. But I don't understand how primitive recursive arithmetic relates to those systems. How do the axioms differ and why is there a distinction between the two?

Show that an extension T for Peano arithmetic there exists closed formulae E and F in the language such that |-E <-> Bx[k#F] and |-F <-> Cx[k#E]. Where there exists a proof of E and F in T and #F and #E are the gödel numbers of E and F and kn is the number of numerals, as in 0, S0, SS0 and kn has n occurnces of S. B and C are formulas in T with one free variable each which is x.

This is an introductory class to mathematical logic but this one has me really stumped. I was thinking of showing that Godel numbering function is recursive and so it is representable. I wasnt really sure if/how I could construct that into an argument that would show |-E and |-F.

We are using the book Mathematical Logic by Shoenfield.

We are then supposed to use that to show incompleteness via the liars paradox but that's another story. I think just understanding the first part is a good place to start.

Any help is appreciated thanks.

Please be gentle, i'm not a mathematician. I'm a ordinary autistic person with attention disorder that wants to believe that the notion of "true statement" holds some intrinsic value.

If i understand correctly, an axiomatic theory has the following properties :

A/ It is always either incomplete or it is inconsistent.

B/ It is brittle, if it is inconsistent, every true statement is void of any value. It might be arbitrarily hard to prove that it is indeed inconsistent.

C/ It might be arbitrary. There is no particular way to distinguish a "good axiom" from a "bad axiom".

So given that ZFC is indeed axiomatic, and if those three above point holds, how exactly can it be considered a "foundation" ? Further more it seems that mathematics isn't dependent on axioms to build proofs and theorems. The incompleteness theorem, from what i could gather, doesn't seem to be based on any particular set of axioms, and indeed it seems much more powerful in nature. Yet it is a theorem. Hence mathematics doesn't need to be axiomatic to discuss what is or isn't true. And being axiomatic indeed prevents any definitive conclusion.

This all very confusing.

Hello,

First, sorry if this is not a purely math question (I tried to ask it in r/logic but it was not accepted). I separate it in two parts :

- I consider questions to be closed formulas (here in classical FOL) and answers to be corresponding proofs, because the proof can be checked by a decidable procedure. Is it the correct frame, or are there other ways to ask questions ? I come more from computer science where this viewpoint is IMO more standard, a question/type being a program specification and a proof/term being a terminating program that computes what we want.

- If we accept this viewpoint, there seems to be no way to ask formally how much is 1 + 2 : the closest formula we can ask is "∃x.(x = 1 + 2)", but then we cannot forbid proofs by contradiction that avoid mentioning 3. Contrast that with e.g. intuitionist FOL, where the formula above forces any proof of it to give us 3 (due to the existence property). Do I miss something ?

The closest I get would be applying a search procedure after proving the statement above is true, but then we wouldn't work purely in ZFC (I guess one way is to apply Herbrand Theorem to get a finite sequence of terms on any proof of the formula above, on which we can run a decidable procedure because the problem is simple enough). It also look like overkill and may not be working for more difficult questions ...

Or is it just a basic / obvious fact, that classical FOL can basically only answer yes/no questions (as opposed to constructive logics which can answer with algorithms) ?

Some small remarks :

- I'm not saying that we cannot ask "3 = 1 + 2", that's a legit formula.

- It's not a blame of ZFC and I understand that there, logic serves more often as a sanity check.

"okay class produce your homework of bringing in some random item from your houses for us to do magic on. Oh looks like a lot of people have brought metal cutlery, the people who have done that should come over here, we've got a scroll of an ancient text by a dude called faradey, you get no other information but you get points if your measurements line up with the results from the other class, we're seeing whose fork can get the most rusted when we plug them in to different batteries it's called "electrolysis" or some shit. Alternatively, here's a Bunsen burner, the only rule is you can't burn anyone else or their shit without their permission".

"Okay class it's PE: fight! Here's some boxing gloves and don't go for the head or we'll move your set down. Alternatively, you can come over here and learn HOW to fight like a boxer, that way your lot can do better in the punch up area. Useful for kids who get bullied, learn how to box and then fucking go for that kid who burned your aluminium coke can with a Bunsen burner. Alternatively, here's a ball you can kick about, and nerds who don't want to physically exert themselves here's a book on how to referee a football game."

"Religion studies, oh yeah! We're all gonna LARP as members of a particular chosen religion for this hour. It's like playing mum's and dad's except I'm here to explain what parts are accurate in your LARP of what the community structure of Tibetian sikh monks are like lol. We do atheism once a term too where we watch a film with Morgan Freeman in or something and chat about mental health or Camus' myth of sysiphus. Also if you're already in a religion and you don't want to do another one even as a pretend, come on the days we're studying your religion and help others live as your religion accurately, that's cool too."

"Foreign languages: for an hour we're just literally going to speak French to you, we're gonna say no English language at all whatsoever, nobody's allowed to do physical violence but if you don't start Google translating the shit I'm saying quickly you're probably gonna spend an hour being very fucking confused. You're allowed to converse with people in your class to try to figure out what they're saying, but if you understand the conversation I'm having in French with someone and successfully convince the class it's about something else you go to the top of the class. Also sometimes I'm gonna stop speaking French and just start speaking gibberish, the first person to call my

As I understand, the main argument of Godel's Incompleteness Theorem, once it's established that you can form an expressible string that basically says "this string is not a theorem in TNT" is as follows:

• If it is false, then it is a theorem in TNT. But all theorems in TNT are true, which leads to a contradiction.
• But if it is true, then it is not a theorem in TNT. But not all true statements in TNT are necessarily theorems in TNT, so this must be true.
• Therefore, there is a true statement in TNT that is not representable in TNT, making TNT incomplete.

I'm sure Douglas Hofstadter said enough in his book to explain what it means for something to be "true" in a formal system, but I guess I either forgot it, or didn't digest it the first time. It's easy to understand what it means for something to be a theorem in a formal system. A theorem in a formal system is any string that you can generate by starting from the axioms and applying the transition rules.

Here's why I'm confused. I always assumed that what's true about any arithmetic system depends entirely on the axioms and rules of the system. So a truth of mathematics is essentially a conditional truth, i.e. this theorem is true if the axioms you chose to use are true. So, for example, Euclid's theorem (infinite primes) is true if you assume that the Peano axioms of arithmetic are true. Otherwise, Euclid's theorem is just some nonsensical statement that needs more context (or could be sensible but "incorrect" for some other hypothetical set of axioms in which natural numbers, and primes are well defined, but in fact, there aren't infinite primes). But how can a set of axioms and transition rules imply that any statement is true, unless it's because you can generate that statement from the axioms and rules? That's what a theorem is. But, in what other sense can something in math be "true"?

Am I correct that any true statement in mathematics is a conditional truth, given the axioms? Or is there some notion of truth independent of the axioms of the formal system? And if truth is conditional on the axioms, then how is it distinct from a theorem? Could something be true about a formal system, given its axioms, yet not derivable in that system from the axioms?

When I look at the statement of Godel's first incompleteness theorem on Wiki, it says,

>Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there a

A mathematical theory in a modern axiomatic sense consists of three key components: primitive notions, deductive system and axioms. Speaking somewhat informally, the primitive notions serve as a foundation upon which the semantics of the theory are ultimately based; the deductive system determines the syntax of the theory, and the proper way in which conjectures can be posed and proven; and finally axioms are the primitive unproven postulates which serve as a basis of further proofs.

Note that not all bodies of mathematical knowledge commonly referred to as theories neccessarily fit these exact descriptions: for instance number theory arguably doesn't (I'm aware there is an axiomization of the number theory called Peano arithmetic, but it's far from exhaustive compared to the full scope of modern number theory).

The orthodox view of practicioner mathematicians seems to be that the primitive notions of a theory remain undefined and can only be understood intuitively if at all.

However, couldn't the entire theory be understood as a functionalist definition of its primitive notions from a certain point of view? This would seem to make sense especially since one can speak about certain mathematical structures as models of the theory if they follow the proper relations established by the axioms. So, for instance, if you say that a certain structure is a model of Peano arithmetic, you seem to be effectively saying that it contains some objects, operations or relations that meet the functionalist definitions of primitive notions of Peano arithmetic.

Does this viewpoint make any sense? What are some philosophers of mathematics who have written about it in a similar manner?

If not, is there a consistency proof for second-order arithmetic similar to Gentzen's consistency proof? Is such a proof even possible?