Archive for the ‘Metatheory of First Order Logic’ Category

FOM Discussion on Consistency of Peano Arithmetic and Foundations of Mathematics

May 20, 2011

I’ve been folloiwing a discussion on the Foundations of Mathematics List (FOM) regarding these two videos (1, 2) on what noted Field’s Medalist Vladimir Voevodsky thinks regarding the consistency of Peano Arithmetic and the foundations of mathematics.  His comments have caused quite a stir on the list.  Below is a message to Voevodsky by Harvey Friedman and Voevodsky’s reply.

“Dear Professor Voevodsky,

I have become aware of your online videos at http://video.ias.edu/voevodsky-80th and http://video.ias.edu/univalent/voevodsky. I was particularly struck by your discussion of the “possible inconsistency of Peano Arithmetic”. This has created a lot of attention on the FOM email list. As a subscriber to that list, I would very much like you to send us an account of how you view the consistency of Peano Arithmetic. In particular, how you view the usual mathematical proof that Peano Arithmetic is consistent, and to what extent and in what sense is “the consistency of Peano Arithmetic” a genuine open problem in mathematics. It would also be of interest to hear your conception of what foundations of mathematics is, or should be, or could be, as it appears to be very different from traditional conceptions of the foundations of mathematics.

Respectfully yours,

Harvey M. Friedman
Ohio State University
Distinguished University Professor
Mathematics, Philosophy, Computer Science”

And Voevodsky’s reply:

“Dear Harvey,

such a comment will take some time to write …

“To put it very shortly I think that in-consistency of Peano arithmetic as well as in-consistency of ZFC are open and very interesting problems in mathematics. Consistency on the other hand is not an interesting problem since it has been shown by Goedel to be impossible to proof [sic].

Vladimir.”

I think that this reply still leaves a lot of room for interpretation. It could simply mean that Hilbert’s program is no longer interesting or it could be an call for finitism in foundations or it could indicate the possibility of fruitful mathematics by means of searching for an inconsistency proof of these well established systems.  “Curiouser and curiouser!” Cried Alice …

Posted in Godel's Incompleteness Theorems, Metatheory of First Order Logic, Peano Arithmetic | Leave a Comment »

Assumptions On Definability Over The Standard Model Ω, Part 2

September 11, 2010

So we set out the basic assumptions about definability over \Omega that factor into the proof of Tarski’s theorem.  Let’s go over each one to get clear on all the definitions.

(i) Every effectively computable function \textup{F}: \omega \rightarrow \omega is definable over \Omega.

A function \textup{F}: \textup{X} \rightarrow \textup{Z} is effectively computable if, and only if, there is an effective procedure such that, for any x \in \textup{X} the procedure calculates the value \textup{F}(x).  The claim is that every such function defined on the natural numbers is definable in the standard model.

(ii) Every decidable set \textup{X} \subseteq \omega is definable over \Omega.

A subset \textup{A} \subseteq \textup{X} is decidable if, and only if, the property \mathcal{P} defined as (\mathcal{P}(x): \Longleftrightarrow x \in \textup{A}) is decidable in \textup{X}.  And a property \mathcal{P} defined over a set \textup{X} is decidable in \textup{X} if, and only if, there is an effective (or decision) procedure for deciding, for any x \in \textup{X} whether or not \mathcal{P}(x) holds.  Here the claim is straightforward, every such set of natural numbers is definable in the standard model.

(iii) Every effectively countable set \textup{X} \subseteq \omega is definable over \Omega

Finally, a set \textup{X} is effectively countable if, and only if, \textup{X} is empty or there is an effectively computable function \textup{F}: \omega \rightarrow \textup{X} that counts \textup{X} (i.e., \textup{X} is the image of \textup{F}, \textup{X} = \mathsf{Im}(\textup{F}) := \{\textup{F}(n): n \in \omega\}). So, what’s being assumed here is that the effectively countable subsets of the natural numbers are definable in the standard model.

Just a few more definitions and we can get into Tarski’s theorem.  In the next update I’ll define the set of indices for the theorems of \Omega as well as a diagonalization function that will play a role in the proof.

Posted in Metatheory of First Order Logic, Models of Arithmetic, Undefinability of Truth | Leave a Comment »

Assumptions On Definability Over The Standard Model Ω, Part 1

September 10, 2010

In the late 30′s Tarski proved that arithmetical truth cannot be defined in arithmetic.  In the next few updates I’m going to be discussing Tarski’s Undefinability theorem and will follows chapter 4 of Hinman’s Fundamentals.  Check this earlier note if you want to get clear on the definability we’re talking about.

Below are some of the basic assumptions about definability and the standard model of arithmetic that will factor into the proof of Tarski’s theorem.

(i) Every effectively computable function \textup{F}: \omega \rightarrow \omega is definable over \Omega.

(ii) Every decidable set \textup{X} \subseteq \omega is definable over \Omega.

(iii) Every effectively countable set \textup{X} \subseteq \omega is definable over \Omega.

In the next update I’ll break down each of these assumptions and hopefully move into the theorem itself.  The point of all this is just to be able to get through Hellman’s example of determination without reduction using a corollary of the undefinability theorem.

Posted in Metatheory of First Order Logic, Models of Arithmetic, Undefinability of Truth | Leave a Comment »

Follow

Get every new post delivered to your Inbox.