Gödel: What could it mean for a statement to be “true but not provable”? Is this just because there are some statements such that neither P nor not-P can be proven, yet one of them must be true? If so, I would (stubbornly) contest that perhaps P and not-P really are both non-true.
“P and not-P really are both non-true” is classically false, and Gödel holds in classical mathematics, so Sunny’s response isn’t available in that case.
Sunny’s sense that “perhaps P and not-P really are both non-true” might be a reason for him to endorse intuitionism as “more correct” than classical math in some sense.
All provable statements follow from the axioms, including “P or not P” for any particular P. It’s the same sense as any other statement can be provable.
Yes, in any formal system, all provable statements follow from the axioms. However, there are many formal systems. Two of the most commonly used ones are Classical Logic and the Calculus of Inductive Constructions.
In Classical Logic, “forall P, P or not P” is an axiom. So, it’s technically provable, but it would be misleading to say that you can prove it without further comment.
In the Calculus of Inductive Constructions (which is an extension of Intuitionistic Logic, if I understand correctly), “forall P, P or not P” is not provable.
So if there’s a non-trival proof of “forall P, P or not P”, it isn’t in either of these formal systems. If you do have one in mind, what formal system (logic) is it in, and what does the proof look like?
Note that you can prove “P or not P”.
In what sense? In Classical Logic it’s an axiom, and in the Calculus of Indutive Constructions it’s unprovable.
(Interestingly, you can prove in Coq that the negation of “forall P, P or not P” is unprovable. So it’s safe to assume it: https://stackoverflow.com/questions/32812834/how-to-prove-excluded-middle-is-irrefutable-in-coq )
Ike is responding to this:
“P and not-P really are both non-true” is classically false, and Gödel holds in classical mathematics, so Sunny’s response isn’t available in that case.
Sunny’s sense that “perhaps P and not-P really are both non-true” might be a reason for him to endorse intuitionism as “more correct” than classical math in some sense.
All provable statements follow from the axioms, including “P or not P” for any particular P. It’s the same sense as any other statement can be provable.
Yes, in any formal system, all provable statements follow from the axioms. However, there are many formal systems. Two of the most commonly used ones are Classical Logic and the Calculus of Inductive Constructions.
In Classical Logic, “forall P, P or not P” is an axiom. So, it’s technically provable, but it would be misleading to say that you can prove it without further comment.
In the Calculus of Inductive Constructions (which is an extension of Intuitionistic Logic, if I understand correctly), “forall P, P or not P” is not provable.
So if there’s a non-trival proof of “forall P, P or not P”, it isn’t in either of these formal systems. If you do have one in mind, what formal system (logic) is it in, and what does the proof look like?
There’s a non-trivial proof of “P or not P” for a specific P.