How did Tarski show that some propositions are neither true nor false?

Question

I'm not a logician, and I'm something of an amateur or beginner here, so please bear with me.

I was just reading Mike Nahas' tutorial on the Coq proof assistant, and I saw this paragraph, about an eighth of the way through the tutorial:

IT IS VITALLY IMPORTANT THAT YOU DO NOT THINK OF A Prop AS BEING EITHER "TRUE" OR "FALSE". A Prop either has a proof or it does not have a proof. Godel shattered mathematics by showing that some true propositions can never proven. Tarski went further and showed that some propositions cannot even said be to be true or false!!! Coq deals with these obstacles in modern mathematics by restricting Prop to being either proven or unproven, rather than true or false.

This, I think, is telling us that Coq uses a constructivist approach like Brouwer's. I more or less understand what Gödel did, at least at some level, but this is the first time I've heard of Tarski going further. Just what did Tarski do here, how did he do it, and what were its implications for mathematics and logic?

Answer 1

I can't really say what the author means here. Tarski accomplished an enormous amount in logic:

• Tarski developed the T-schema as part of his goal to understand what does it mean for a proposition to be true. The T-schema gives a kind of recursive definition of truth.

• Tarski's theorem on the undefinability of truth shows that it is impossible to define, in formal systems of arithmetic, what it means for a formula to be true.

But Tarski did not directly show that there are propositions that "cannot be said to be true or false". Indeed, throughout the history of mathematics most mathematicians have thought classically, writing and speaking as if each proposition is true or false, although we may not know which of these is the case or even know whether a given proposition is provable.

Now, to give the author some credit, it is almost certainly correct that, in order to work effectively in Coq, it is better to think constructively ("Is this propositional provable? Is it disprovable?") than to think classically ("Is this proposition true?"). I think this is really the point of the quoted paragraph, and it is an important one.

However, the entire logic of Coq can be interpreted into set theory (see this MathOverflow question and its answers for how much set theory is needed). Under that interpretation, each proposition $P$ in the language of Coq is just as true or false as the proposition of set theory that is used to represent $P$. Of course, there are many philosophical issues with set theoretic truth, but if someone accepts that each set theoretic proposition is true or false in some sense, they will see that the interpretation of each proposition of Coq is true or false in the same sense.