Consistency of $\mathsf{PA}$ My reference book is A Course on Mathematical Logic by S.M. Srivastava.
Not so long ago, MO linked me to a video of a conference by Voevodsky wherein he considered the possibility of arithmetic being inconsistent. Apparantly, there is no (known) proof of consistency for $\mathsf{PA}$ or for $\mathsf{ZF}$.
Yet, example 2.3.3 on page on page $20$ of said book claims $\mathbb{N}=\lbrace 0,1,2,\dots\rbrace$ (with the usual interpretations of $0,S,+,\times, \lt $) is a model for Peano Arithmetic, and Theorem 4.4.8 (Completeness theorem, second form) on page $63$ says "a theory $T$ is consistent iff it has a model".

Why is this not proof of the consistency of $\mathsf{PA}$? What am I misunderstanding here?

Adding to my confusion, on page $74$, Theorem 5.3.10 states that $\mathsf{PA}$ is consistent iff $\mathsf{ZF}-\mathsf{Axiom~of~Infinity}$ is consistent.
If the root of the problem is set theory, the pending question of the consistency of $\mathsf{ZF}$, how can any theory $T$ be given a model, i.e. a set with a collection of interpretations for constants, functions and relations?
 A: 
Why is this not proof of the consistency of PA?

It is a proof of the consistency of PA. It is the same sort of proof that is used to show that the negation of the parallel postulate is consistent with the remainder of the axioms of Euclidean geometry, by constructing a model of non-Euclidean geometry. 

What am I misunderstanding here?

Perhaps you heard that it is not possible to prove the consistency of PA. That is simply false; for example you can prove it directly from the axiom "PA is consistent". What is true is just that there is no proof of the consistency of PA within PA itself. 

Apparantly, there is no (known) proof of consistency for PA or for ZF.

There are (at least) three proofs of the consistency of PA that are important: 


*

*The proof in ZFC, which proceeeds by just verifying that $\mathbb{N}$ is a model of PA. 

*The proof by Gentzen. Here consistency is proved in a much weaker theory than ZFC (but of course the theory is not included in PA). 

*The proof by Gödel using what is now called the Dialectica interpretation. This proof uses a completely different method than Gentzen's proof, but obtains the same result. It is also conducted in a weak system, but a different weak system than Gentzen's proof. 
A: I’m using the community wiki mode because this is not an answer. This is just a collection of links. (Some of them had already be given in the comments.) Please feel free to add others. 
Vladimir Voevodsky’s talk
MO questions


*

*What if current foundations of mathematics are inconsistent

*Question arising from Voevodskys talk on inconsistency

*Is PA consistent? Do we know it?

*Nelson’s program to show inconsistency of ZF
Ed Nelson’s webpage
FOM 


*

*May 2011

*June 2011

*Correspondence between Harvey Friedman and Vladimir Voevodsky
Excerpts (from the correspondence):
HF: Apparently, you think it worthwhile to spend some of your time to prove the inconsistency of PA. Un my opinion, that result would be the greatest result of all time in mathematics by orders of magnitude. And that doesn't touch on how it would compare with results in science and general human intellectual activity. 
HF: It would of course be useful if you would reassess or restate your position that "the consistency of PA is a legitimate open problem in mathematics" in light of our correspondence.
VV: So far I do not plan to reassess anything in my position.
A: The usual proofs of the Completeness Theorem are like proofs in any other branch of mathematics. They are rigorous, but not formal proofs in ZFC.  
However, the proofs can be made formal, and ZFC is strong enough to carry it out.  From a proof of consistency point of view, this is not particularly helpful, since it shifts the burden of consistency to ZFC, a stronger theory.  
A better candidate for a consistency proof for Peano Arithmetic is the long-ago work of Gentzen.  True, it involves transfinite induction up to $\varepsilon_0$, but it has a finitary character.  Unfortunately, "finitary character" is a matter of opinion, not rigorous definition.
