5 ms·

Prove I’mUnprovable using proof by contradictions as follows: In order to obtain a contradiction, hypothesize ¬I’mUnprovable. Therefore ⊢I’mUnprovab

Prove I’mUnprovable using proof by contradictions as follows: In order to obtain a contradiction, hypothesize ¬I’mUnprovable. Therefore ⊢I’mUnprovable (using I’mUnprovable⇔⊬I’mUnprovable). Consequently, ⊢⊢I’mUnprovable using ByProvabilityOfProofs {⊢∀[Ψ:Proposition<i>] (⊢Ψ)⇒⊢⊢Ψ}. However, ⊢¬I’mUnprovable (using I’mUnprovable ⇔⊬I’mUnprovable), which is the desired contradiction in foundations. Consequently, I’mUnprovable has been proved to be a theorem using proof by contradiction in which ¬I’mUnprovable is hypothesized and a contradiction derived. In your notation, the proof shows that following holds: ¬I’mUnprovable ⇒ ⊥ Why do you think that the proof is for the following? ¬I’mUnprovable ⇒ ⊢⊥

drdeca 5y ago
Because ◻P and ◻¬P together imply ◻⊥, not ⊥. Edit: if you had as an axiom, or could otherwise prove within the system, that ¬◻⊥, I.e. that the system is consistent, then you could conclude from ◻P and ◻¬P that ⊥, by first concluding ◻⊥, and then combining this with ¬◻⊥ . And in this case, you could indeed say that this is a contradiction, and therefore reject the assumption of ¬UNK, and then conclude UNK without assumptions. So, if one could show ¬◻⊥ (or if the system had it as an axiom), the reasoning would go through. (This is the thing that is missing.) Therefore, you could then prove ◻UNK, and therefore ¬UNK, and therefore (having already shown UNK) would have a contradiction, ⊥. So, this is a way of showing that, if you can show ¬◻⊥ (and if there is a statement UNK), then the system is inconsistent. Which is just one of Gödel’s theorems: a strong system can’t prove its own consistency without being inconsistent.
- ProfHewitt 5y ago
  But the proof shows the following: ¬I’mUnprovable ⇒ ⊥ By the way, because the proposition I'mUnprovable does not exist in foundations, it is OK for foundations to prove their own consistency as follows: Consistency of a theory can be formally defined as follows: Consistent⇔¬∃[Ψ] ⊢Ψ∧¬Ψ Contra [Gödel 1931], a foundational theory can prove its own consistency as shown in the following theorem: Classical theorem. ⊢Consistent Classical proof. In order to obtain a contraction, hypothesize ¬Consistent. Consequently, ¬¬∃[Ψ] ⊢Ψ∧¬Ψ, which classically implies ∃[Ψ]⊢Ψ∧¬Ψ by double negation elimination. Consequently, there is a proposition Ψ0 such that ⊢Ψ0∧¬Ψ0 (by eliminating the existential quantifier in ∃[Ψ]⊢Ψ∧¬Ψ). By the principle of ByTheoremUse {⊢∀[Φ] (⊢Φ)⇒Φ} with Ψ0 for Φ, Ψ0∧¬Ψ0, which is the desired contradiction. However, the proof does not carry conviction that a contradiction cannot be derived because the proof is valid even if the theory is inconsistent. Consistency of the mathematical theories Actors and Ordinals is established by proving each theory has a unique-up-to-isomorphism model with a unique isomorphism. See the following for more information: "Epistemology Cyberattacks" https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
  - drdeca 5y ago
    ByTheoremUse is not a valid principle, at least for any system that includes Peano Arithmetic. (It is essentially the assumption that the system is not only consistent, but sound. It is therefore no surprise that ByTheoremUse would imply Consistent.) By Löb’s theorem, ByTheoremUse would imply that for all propositions P, that P holds. I.e. it implies ⊥.
    - ProfHewitt 5y ago
      ByTheoremUse goes all the way back to Euclid. It says that "a theorem can used in a proof." It is part of many modern logic systems. Löb’s result depends on Gödel numbers, which are invalid in foundations because the Gödel number of proposition does not include the order of the proposition. ByTheoremUse works fine for Dedekind's axiomatisation of the natural numbers using unaccountably many axiom instances :-)
      - drdeca 5y ago
        Perhaps I misunderstood what you mean by ByTheoremUse . If you mean that, if in a context/environment with certain givens, one can derive a conclusion, then one can apply that in other cases, Or if you just mean modus ponens, or cut elimination, Then ok, that’s fine. That’s valid. (Though it doesn’t justify the step you cited it in.) But you can’t, within the system, go from ◻P to P. That isn’t a valid rule of inference. There’s a distinction between “therefore P” and “therefore ◻P”, and you cannot use the latter as the former. You seem to equivocate better “P is provable” and “therefore P” Like, suppose I was writing a computer program in a strongly typed language, and something required an argument of type A->B , and I tried to pass in a string which has the text of a function with that type. Obviously that wouldn’t type check.
        ProfHewitt 5y ago
        TheoremUse does indeed mean (⊢Φ)⇒Φ in powerful foundational theories. TheremUse is not a problem because the [Gödel 1931] proposition I'mUnprovable does not exist in foundations. Do you think that you can derive a contradiction in foundations by utilizing TheoremUse?

drdeca 5y ago

Because ◻P and ◻¬P together imply ◻⊥, not ⊥. Edit: if you had as an axiom, or could otherwise prove within the system, that ¬◻⊥, I.e. that the system is consistent, then you could conclude from ◻P and ◻¬P that ⊥, by first concluding ◻⊥, and then combining this with ¬◻⊥ . And in this case, you could indeed say that this is a contradiction, and therefore reject the assumption of ¬UNK, and then conclude UNK without assumptions. So, if one could show ¬◻⊥ (or if the system had it as an axiom), the reasoning would go through. (This is the thing that is missing.) Therefore, you could then prove ◻UNK, and therefore ¬UNK, and therefore (having already shown UNK) would have a contradiction, ⊥. So, this is a way of showing that, if you can show ¬◻⊥ (and if there is a statement UNK), then the system is inconsistent. Which is just one of Gödel’s theorems: a strong system can’t prove its own consistency without being inconsistent.

ProfHewitt 5y ago
But the proof shows the following: ¬I’mUnprovable ⇒ ⊥ By the way, because the proposition I'mUnprovable does not exist in foundations, it is OK for foundations to prove their own consistency as follows: Consistency of a theory can be formally defined as follows: Consistent⇔¬∃[Ψ] ⊢Ψ∧¬Ψ Contra [Gödel 1931], a foundational theory can prove its own consistency as shown in the following theorem: Classical theorem. ⊢Consistent Classical proof. In order to obtain a contraction, hypothesize ¬Consistent. Consequently, ¬¬∃[Ψ] ⊢Ψ∧¬Ψ, which classically implies ∃[Ψ]⊢Ψ∧¬Ψ by double negation elimination. Consequently, there is a proposition Ψ0 such that ⊢Ψ0∧¬Ψ0 (by eliminating the existential quantifier in ∃[Ψ]⊢Ψ∧¬Ψ). By the principle of ByTheoremUse {⊢∀[Φ] (⊢Φ)⇒Φ} with Ψ0 for Φ, Ψ0∧¬Ψ0, which is the desired contradiction. However, the proof does not carry conviction that a contradiction cannot be derived because the proof is valid even if the theory is inconsistent. Consistency of the mathematical theories Actors and Ordinals is established by proving each theory has a unique-up-to-isomorphism model with a unique isomorphism. See the following for more information: "Epistemology Cyberattacks" https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
- drdeca 5y ago
  ByTheoremUse is not a valid principle, at least for any system that includes Peano Arithmetic. (It is essentially the assumption that the system is not only consistent, but sound. It is therefore no surprise that ByTheoremUse would imply Consistent.) By Löb’s theorem, ByTheoremUse would imply that for all propositions P, that P holds. I.e. it implies ⊥.
  - ProfHewitt 5y ago
    ByTheoremUse goes all the way back to Euclid. It says that "a theorem can used in a proof." It is part of many modern logic systems. Löb’s result depends on Gödel numbers, which are invalid in foundations because the Gödel number of proposition does not include the order of the proposition. ByTheoremUse works fine for Dedekind's axiomatisation of the natural numbers using unaccountably many axiom instances :-)
    - drdeca 5y ago
      Perhaps I misunderstood what you mean by ByTheoremUse . If you mean that, if in a context/environment with certain givens, one can derive a conclusion, then one can apply that in other cases, Or if you just mean modus ponens, or cut elimination, Then ok, that’s fine. That’s valid. (Though it doesn’t justify the step you cited it in.) But you can’t, within the system, go from ◻P to P. That isn’t a valid rule of inference. There’s a distinction between “therefore P” and “therefore ◻P”, and you cannot use the latter as the former. You seem to equivocate better “P is provable” and “therefore P” Like, suppose I was writing a computer program in a strongly typed language, and something required an argument of type A->B , and I tried to pass in a string which has the text of a function with that type. Obviously that wouldn’t type check.
      - ProfHewitt 5y ago
        TheoremUse does indeed mean (⊢Φ)⇒Φ in powerful foundational theories. TheremUse is not a problem because the [Gödel 1931] proposition I'mUnprovable does not exist in foundations. Do you think that you can derive a contradiction in foundations by utilizing TheoremUse?