In my (philosophy) department (here in Brazil), undergrads are generally introduced to the basics of logic or formal reasoning, say through Priest's A Very Short Introduction or Steinhart's More Precisely. That is the only required logic course for philosophy undergrads. There are a couple more optional courses they can take, but these vary wildly in content. At the graduate student level, they are not required to take any logical course, though there is generally at least one such course every term, again on a wide variety of subjects. I myself (a grad student) have (unofficially) taught a course loosely based on the first part of Boolos, Jeffrey & Burgess's Computability and Logic, and last term we also had a course based on the first four chapters of Shoenfield's Mathematical Logic.

As for the math department (again, at my university, here in Brazil), they are not required to take logic courses, though there are optional classes on logic and set theory. The logic class generally goes through the completeness, compactness, and Löwenheim-Skolem theorems, some times also into incompleteness. The set theory classes generally go through the usual cardinal and ordinal stuff, some times going into a bit more detail on combinatorics, other times scratching the surface of the constructible universe, and one or two crazy professors go as far as forcing.

Doesn't Gödel's incompleteness theorem only state that there are sentences about F that are true but that can't be proved in F? That's not quite the same as saying that there are sentences about F that are true but that can't be proved.

An example would be the Paris–Harrington theorem which can't be proved in Peano arithmetic but can be proved in second-order arithmetic.

So prima facie there doesn't seem to be a problem with saying that a sentence is true iff it is provable – it's just that a second language is what proves the sentence. This would seem to fit with Tarski's claim that a metalanguage is required to make sense of an object language's truth.

So prima facie there doesn't seem to be a problem with saying that a sentence is true iff it is provable – it's just that a second language is what proves the sentence. This would seem to fit with Tarski's claim that a metalanguage is required to make sense of an object language's truth. — Michael

I think it gets a bit dicey; if you can assume anything that doesn't trivialise proof in a system as part of the system as an axiom, and a system proves all its axioms, this trivialises truth. I think such a statement "true iff provable" has to be thought of in terms of "P is true iff there exists system C which proves P", but so long as you can conjure a C which has P as an axiom, P is true since it is by assumption provable in C. Making a statement range over all formal systems and models of them is going to do weird things to any notion of truth by design.

I think it gets a bit dicey; if you can assume anything that doesn't trivialise proof in a system as part of the system as an axiom, and a system proves all its axioms, this trivialises truth. I think such a statement "true iff provable" has to be thought of in terms of "P is true iff there exists system C which proves P", but so long as you can conjure a C which has P as an axiom, P is true since it is by assumption provable in C. — fdrake

I understand what you mean, but is there an example of a statement that is true but isn't provable in any system? Surely it's impossible to know that a statement is true if it isn't provable?

It might be that "truth as provability" trivialises truth, but do we have any reason to believe that truth isn't trivial? Can we prove that it's something more?

Firstly, good spot about PA |-/- Prov S --> S

As you point out, that false derivational assumption which I took for granted and which led me to

PA |-- Prov('G') <--> ~Prov('G')

implies that PA is inconsistent due to LOM, something I overlooked as i don't think classically.

In fact, that 'Reductio ad absurdum' constitutes a weaker version of Lob's theorem, specifically applied to G.


But all of that said, from a constructivist position it doesn't seem surprising given that ~Prov already doesn't reflect non-derivability. Lob's theorem is just further ammunition for identifying truth directly with the derivable sentences, and for rejecting the interpretation of "prov" as meaning provability, and consequently for rejecting the semantic philosophical interpretation of incompleteness as implying 'arithmetically true but undecidable propositions'.

I think such a statement "true iff provable" has to be thought of in terms of "P is true iff there exists system C which proves P", but so long as you can conjure a C which has P as an axiom, P is true since it is by assumption provable in C. — fdrake

On a practical point, there's obviously a difference between developing second order arithmetic which can prove the Paris–Harrington theorem and developing a system that has the Paris–Harrington theorem as its only axiom. I don't know how to formalise that difference, but surely there is one (which is why second order arithmetic doesn't trivialise the theorem but this second system does).

It might be that "truth as provability" trivialises truth, but do we have any reason to believe that truth isn't trivial? — Michael

Ultimately? I dunno. Trivial truth makes 1+1=3. Trivial truth also makes "truth is trivial is false" true. You know, the usual stuff against trivialism.

I don't know very much at all about truth predicates in formal languages, I think you're better off consulting @Nagase.

(which is why second order arithmetic doesn't trivialise the theorem but this second system does). — Michael

It trivialises the proof of the statement, but not whether it is true. All truths are equal in terms of truth value. The only way I see to block that "there exists a system C that proves P => P is true" part of the if and only if trivialising truth (for anything which can be stated in a formal language) is to claim that a formal system can't prove its own axioms, and at that point I'm not even sure what a formal system means.

Trivial truth makes 1+1=3. — fdrake

I'm not sure what you mean by this. If we're doing Peano arithmetic then 1 + 1 = 2, whatever any other formal system says. If we're using a formal system where 1 + 1 = 3 then those symbols don't mean what they mean in Peano arithmetic.

If we had a formal system that used the Peano axioms to define the numbers and addition but also axioms that entailed that 1 + 1 = 3 then we'd have an inconsistent formal system, and so could dismiss it on those grounds.

Trivial truth also makes "truth is trivial is false" true.

I think if we're considering truth as provability and so therefore trivial then we just drop all talk about "true" and "false" and just talk about sentence P that is provable in F or sentence G_F that is provable in C. Does that lead to any sort of strangeness?

Also on this point a sentence like "truth is trivial is false" seems like it would belong in a natural language rather than a formal language like Peano arithmetic. Maybe truth in formal languages work differently to truth in natural languages.

If we had a formal system that used the Peano axioms to define the numbers and addition but also axioms that entailed that 1 + 1 = 3 then we'd have an inconsistent formal system, and so could dismiss it on those grounds. — Michael

It having no models in the usual way requires that truth and falsity work in the usual way, I think. If you wanna dismiss a formal system for being inconsistent (a provable contradiction) - ultimately the reason you'll do that is because it trivialises truth.

If you wanna dismiss a formal system for being inconsistent - ultimately the reason you'll do that is because it trivialises truth. — fdrake

I think I'd do it on practical grounds. If the rules allow me to derive both 2 and 3 from adding 1 to 1 then I don't know how I'd go about using it.

Imagine a game of chess with a rule that says that pawns can only move forward 1 square and a rule that says that pawns can only move forward 2 squares. I'd dismiss it as unplayable, not because I think that it "trivialises the truth" of the rules.

But two different games that have one or the other rule? Both are fine. And it's not that one game is "true" and the other game "false".

As another example, how about "there is a number greater than zero and smaller than every real number". Is it true or false? Does it even make sense to say that it's either true or false? Or is it more correct to say that it's provable if using the hyperreals and that its inverse is provable if not?

Isn't true but unprovable a contradiction? — TheMadFool

I'm feeling content right now. It's TRUE but not provable. In fact pretty much most of my internal experience is not provable but no less true (to me). I wouldn't say it's a contradiction except that empirical data collection and the application of scientific method depends on the equivalence of truth to proof.

Imagine a game of chess with a rule that says that pawns can only move forward 1 square and a rule that says that pawns can only move forward 2 squares. I'd dismiss it as unplayable, not because I think that it "trivialises the truth" of the rules. — Michael

Indeed, inconsistency trivialises the rules. If you've got 1+1=3 and 1+1=2, that gives you 0=1, and the whole thing loses the meaning it had. If there is a provable contradiction (and your logic is normal), then the rules no longer matter. The idea of there being a "contradiction" requires a notion of truth to evaluate it. If you lose that, you lose the idea of inconsistency. So what if the system proves 1+1=3 and 1+1=2 at the same time?

Wittgenstein makes a couple of remarks in this area; proving a contradiction can usefully be interpreted as a formal system "jamming" with regard to what it concerns. It ceases to be a useful model of any set of axioms - and that's reflected by the collection of models a formal system has, if there's a contradiction, there are no models which satisfy it. Proving a contradiction gives you a good model of this break down of purpose (with regard to abstract systems of reasoning, rather than providing a good description like a physical model).

The idea of there being a "contradiction" requires a notion of truth to evaluate it. — fdrake

I don't think it does. It just requires the axiom of non-contradiction, which some systems like dialetheism do away with (allowing "true" contradictions).

A true contradiction is one which is true and false. You're not gonna get the same notion of contradiction out if you jettison the relevance of truth entirely. AFAIK paraconsistent logics don't jettison truth, they modify how it behaves in a manner that limits explosion/trivialism.

A true contradiction is one which is true and false. You're not gonna get the same notion of contradiction out if you jettison truth. AFAIK paraconsistent logics don't jettison truth, they modify how it behaves in a manner that limits explosion/trivialism. — fdrake

Would you prefer it if I'd said "provable" contradiction? My point was only that I don't think we need a concept of truth to have as an axiom ¬(p ∧ ¬p), and that the reason I might dismiss a system that allows me to prove p ∧ ¬p or that has the single axiom p isn't "ultimately ... because it trivialises truth" but because it isn't usable. Whereas if I have one system that allows me to prove p ("there is a number greater than 0 and less than every real") and one system that allows me to prove ¬p then I can use one or the other as desired or appropriate, and I don't need to believe that p is either true or false irrespective of its provability in either system.

On a different note, has anyone come across this paper? I don't have a JSTOR account so can't read it, but it sounds interesting.

and one or two crazy professors go as far as forcing. — Nagase

:smile:

Thanks for your comments!

the reason I might dismiss a system that allows me to prove p ∧ ¬p or that has the single axiom p isn't "ultimately ... because it trivialises truth" but because it isn't usable. — Michael

I'm not going to pretend to be able to understand things like Godel, but this position sounds like the same conclusion Ramsey came to about deflating truth to something more like utility.

As another example, how about "there is a number greater than zero and smaller than every real number". Is it true or false? Does it even make sense to say that it's either true or false? Or is it more correct to say that it's provable if using the hyperreals and that its inverse is provable if not? — Michael

Unless we appeal non-constructively to the Axiom of Choice, we obtain a set of 'hyperreals' that is isomorphic to a subcountable set of natural numbers with their usual ordering relation. So in a superficial sense we can have infinitesimals in peano arithmetic by defining {1,1/2,1/3..} to be greater than {0,0,0...} even though we have only a subcountable number of such 'hyperrreals'.

Refer to my reply to ↪sime for a clearer sketch of why truth is not provability, and which has nothing to do with G or whatever. And, again, you're evading my point that, if you want to reduce A to B, the mere fact that B is sufficient to A is not enough: you must also show that B is necessary for A. But this is just what Gödel's theorems deny.

Your juridical reasoning may be convincing in the intuitive level, but, as Williamson has said, in these matters it is not enough to argue impressionistically. As counter-intuitive as it might be, it is demonstrable that truth (on most reasonable axiomatizations of the notion, anyway) is not redundant and is not the same as provability. — Nagase

You've made a good point. Godel's theorems depend on proof not being necessary for truth but the catch here is Godel, like all mathematicians and logicians I suppose, seems to have felt the need/necessity to prove his incompleteness theorems. Why didn't Godel simply state his theorems without proof? I reckon because he thought proof as necessary for the truth of his incompleteness theorems and then what does he prove? He proves some statements are true despite being unprovable. Isn't that a contradiction?

1. Proof is necessary for truth [Godel assumes and thus proves his incompleteness theorems]
2. The incompleteness theorems proves that proof is unnecessary for truth
3. Proof is unnecessary for truth (from 2)

1 and 3 contradict each other, no? This is a meta-cognitive statement regarding Godel's thought processes.

Despite my views I think it highly probable that I'm mistaken.

You've made a good point. Godel's theorems depend on proof not being necessary for truth but the catch here is Godel, like all mathematicians and logicians I suppose, seems to have felt the need/necessity to prove his incompleteness theorems. Why didn't Godel simply state his theorems without proof? — TheMadFool

Because he wanted to show it to be true. He wanted to convince us of it and not just ask us to accept it on faith.

1. Proof is necessary for truth [Godel assumes and thus proves his incompleteness theorems]
2. The incompleteness theorems proves that proof is unnecessary for truth
3. Proof is unnecessary for truth (from 2)

1 and 3 contradict each other, no? This is a meta-cognitive statement regarding Godel's thought processes. — TheMadFool

Yes, and your confusion is the fault of classical modal interpretations of logic that insist on misinterpreting PA's provability predicate as being meta-logical in character or representing knowledge, which it doesn't unless it is applied to theorems that are derivable without meta-logical reasoning.


The reason for all the persistent confusion that remains nearly 100 years after godels' proofs, is because Godel's theorems were baptised with their official philosophical interpretation as relating logic to a transcendental plane of mathematical reality, before the invention of the Turing Machine that collapsed the meta-logical distinction between logic and arithmetic by grounding them both in shared computational semantics; operations that also explicitly recognise the nondeterminism of provability due to the halting problem.


As an aside, the reason why the halting problem constitutes the quickest and easiest proof of Godel's incompleteness theorem is due the recognition that algorithms must halt to produce an answer.

For the logician, the predicate "A is provable" simply means that A is mechanically derivable by following the roles of the respective axiomatic system i.e.

"A is provable" := |--A

No other informal nomenclature about 'truth' is useful or necessary.

However, most philosophers describe logic using alternative nomenclature and then appeal to modal heuristics that only leads to confusion, misunderstanding and unnecessary arguments, for they define

"A is true" := |-- A

"A is provable" := |--- Prov('A')

Formally of course, Prov is equivalent to a prolog compiler written in the language of PA that translates theorems of PA into programs that when executed reveal the theorem of PA they they encode. Writing Prov as Comp, Lob's theorem no longer seems remotely surprising.

Recall that if we have PA |-- A , then we can also derive

PA |-- Comp('A') -> A

( i.e, a compiled program for a derivable theorem can be disassembled to reveal the theorem. )

Lob's theorem says

PA |-- ( Comp('A') --> A ) -> A

( i.e. if any compiled program is executed, then it's conclusion is the same as what the disassembler returns . )

So far, Lob's theorem isn't remotely surprising.

But in the case of Godel sentence G, if we assume that PA is consistent and hence that G isn't derivable, the following cannot be true by Lob's theorem:

PA |-- ( Comp('G') --> G )

i.e. if an undecidable statement is compiled, then it cannot be disassembled.

Bur recall that G is the statement saying

G <---> ~Comp'G')

This indicates that the only way to disassemble Comp('G') would be to substitute G into itself an infinite number of times. So it shouldn't be surprising that Comp('G') doesn't imply that it can be disassembled back into G (assuming consistency).

I suspect that those who find Lob's theorem surprising do so because they assume that compilation is always invertible.

I don't think Löb's theorem supports the constructivist position. That's because truth is generally taken, prima facie to obey the capture and release principles: if T('S'), then S (release), and, if S, then T('S') (capture). But what Löb's theorem shows is that proof does not obey the release principle. So there is at least something suspicious going on here.

Moreover, one can show that the addition of a minimally adequate truth-predicate to PA (one that respects the compositional nature of truth) is not conservative over PA. Call this theory CT (for compositional truth). Then $CT \vdash \forall x (\text{Sent}(x) \rightarrow (\text{Prov}(x) \rightarrow T(x)))$, where "T" is the truth predicate. As a corollary, CT proves the consistency of PA. So truth, unlike provability, is not conservative over PA.

Finally, you have yet to reply to my argument regarding the computability properties of the two predicates, namely that one does have an algorithm for listing all the theorems of PA, whereas one does not have an algorithm for listing all the truths of PA. So the two cannot be identical.

What you've written is above my pay grade BUT...

1. Godel felt a necessity to prove the truth of the incompleteness theorem

2. IF Godel felt a necessity to prove the truth of the incompleteness theorem THEN Godel thinks that proof is necessary to establish truth

Ergo...

3. Godel thinks that proof is necessary to establish truth

4. The incompleteness theorem states that a particular statement is true but unprovable

5. Godel believes the incompleteness theorem

5. IF the incompleteness theorem states that a particular statement is true but unprovable AND Godel believes the incompleteness theorem THEN Godel thinks proof is not necessary to establish truth

6. The incompleteness theorem states that a particular statement is true but unprovable AND Godel believes the incompleteness theorem (from 4 and 5)

Ergo

7. Godel thinks proof is not necessary to establish truth

8. Godel thinks proof is necessary to establish truth AND Godel thinks proof is not necessary to establish truth (contradiction from 3 and 7)

Do you see a problem in my simple argument?

(1) Gödel (well, Gödel, Church, Tarski, Rosser, etc.) showed a bit more than what you are implying. He showed that, for any consistent system containing enough arithmetic (i.e. extending Robinson's arithmetic), the set of theorems of that system is not identical to the set of truths of that system. So, if we just move one level up and claim that truth is provability in a higher system, this won't do, because the theorem will reapply at the higher level separating these sets again.

(2) As for why truth is not trivial, the surprising result here is that any minimally adequate theory of truth (i.e. one that respects the compositional nature of truth) is non-conservative over PA. That is, given a truth predicate, one is able to prove more things about the original system than one could before the introduction of such a predicate. In particular, one is able to prove the consistency of the original system. So adding a truth predicate is not a triviality. If you think about it, this is not that surprising, since the truth predicate can be used to express generalizations that wouldn't be possible without it except by the use of infinitary resources, such as infinite disjunctions or infinite conjunctions, i.e. "Jones always tells the truth".

(3) With regards to Fair's article, I've just read it and didn't find it much convincing. He basically argues that truth must be relative to a theory (instead of a model), introducing a family of operators "In T" (i.e. "In PA", "In the theory of algebraically closed fields of characteristic 0", "In ZFC", etc.) and argues that truth ascriptions are always prefixed by this operator, i.e. the hidden logic form of "2+2=4" is actually "In PA, 2+2=4". I personally think this is an instance of a bad (and unfortunately widespread) philosophical habit of postulating hidden linguistic forms without appealing to linguistic evidence (and thus being ad hoc), but let us leave that to the side. In order to deal with incompleteness, Fair is then lead to work with an analogy from fiction: just as the Sherlock Holmes stories don't settle how many hairs he has in his body, so PA doesn't settle G or other undecidable sentences.

In order to support this, he basically assimilates mathematics to fiction, saying that mathematical objects are mind-dependent, etc. In particular, he argues that mathematical objects "lack the 'open texture' we would expect of mind-independent physical objects" (p. 368), by which he means (presumably) that the properties of mathematical objects are fully determined by our beliefs about them (at least, that's what I gathered from the preceding discussion) and that we could not "failure to notice" some of their important properties. I think this is mistaken. Two historical examples: continuity and computability. In both cases, mathematicians had been working with objects that had those properties, but they didn't fully realize the nature of the properties themselves. It was only centuries after working informally with these objects that we began to understand their nature---and even today there are still disputes about them (e.g. is the continuum formed by points, such as Dedekind cuts, or is it formed by regions, like the intuitionists claim?). Moreover, greater clarity about these properties revealed surprising consequences (the existence of continuous functions that were nowhere differentiable or the fact that any local and atomistic process can be simulated by a Turing Machine).

So, at the end, I think there is a great disanology between mathematical truth and fiction. In the latter case, there is almost no friction, and our conceptions can be given free reign. With the former, however, our conceptions are tightly constrained. That is why truth in mathematics is not as problematic as truth in fiction, I gather.

You seem to be confusing knowledge with truth. Obviously, to establish a proposition as true, I need to, well, establish as such. And, in mathematics, to establish a proposition as truth---i.e. to know it---is precisely to prove it. But there can be true propositions that are unknowable, and hence that we cannot establish, and hence that we cannot prove. That there are such propositions is established by Gödel's theorems. Again, note that, in the form I have presented, the theorem does not rely on pointing to one such proposition and saying "This proposition is true, but we can't know it as true". Rather, it proceeds from general properties about truth and provability to show that these concepts must come apart.

You seem to be confusing knowledge with truth. Obviously, to establish a proposition as true, I need to, well, establish as such. And, in mathematics, to establish a proposition as truth---i.e. to know it---is precisely to prove it. But there can be true propositions that are unknowable, and hence that we cannot establish, and hence that we cannot prove. That there are such propositions is established by Gödel's theorems. Again, note that, in the form I have presented, the theorem does not rely on pointing to one such proposition and saying "This proposition is true, but we can't know it as true". Rather, it proceeds from general properties about truth and provability to show that these concepts must come apart. — Nagase

Well, Godel's incompleteness theorem must be part of mathematical knowledge but that's not what matters here. What matters is he's being inconsistent - metacognitively speaking. On one hand, by resorting to proof he endorses the necessity for proof and on the other hand, by accepting his incompleteness theorem, he rejects the necessity for proof.

There is no contradiction. One can hold that proof is necessary to establish truth, yet hold that it is not necessary for truth (cf. my point about unknowable truths). And, in the form I have presented, his theorem does not require him to establish the truth of any unknowable proposition.

There is no contradiction. One can hold that proof is necessary to establish truth, yet hold that it is not necessary for truth (cf. my point about unknowable truths). And, in the form I have presented, his theorem does not require him to establish the truth of any unknowable proposition. — Nagase

That's just word play.

Firstly, the incompleteness theorem has a proof, Godel's, with the express purpose of establishing the truth of the theorem.

Secondly, the incompleteness theorem itself speaks of a statement that's true but unprovably so i.e. the truth of that statement hasn't/can't be established and yet, Godel claims, it's true.

Secondly, the incompleteness theorem itself speaks of a statement that's true but unprovably so — TheMadFool

What are you about, Madfool? You're on notice - been told repeatedly - that the proof in question is a meta-mathematical proof, and that the unprovability is a consequence of the particular system. Failure to grasp this means you don't understand, and apparently don't want to understand, anything Godel.