6 ms·

Let ◻ be the modal operator "It is provable that", so ◻P means that P is provable. The first part of your argument in the second link says:[ Suppose that ther

by drdeca 6y ago

Let ◻ be the modal operator "It is provable that", so ◻P means that P is provable. The first part of your argument in the second link says:[ Suppose that there is a proposition UNP such that UNP ⇔ ¬◻UNP . Then, suppose that ¬UNP . It then follows that ¬¬◻UNP , i.e. that ◻UNP. Therefore, ◻◻UNP . Then, as UNP ⇔ ¬◻UNP, therefore ¬UNP ⇔ ◻UNP. Then, replace the ◻UNP in ◻◻UNP with ¬UNP, and therefore conclude ◻¬UNP . So, at this point, we have concluded that ◻¬UNP and also that ◻UNP. So, you can conclude that, __under these assumptions__, that ◻⊥ . So, under the assumption that there is a statement UNP such that UNP ⇔ ¬◻UNP , and the additional assumption that ¬UNP, you can conclude that ◻⊥. ] Indeed. If a system admits a statement UNP, (and the system is strong enough to do the appropriate reasoning) (and peano arithmetic and such does admit such a statement UNP), then within the system, you can show that ¬UNP implies ◻⊥. I.e. "if the statement that claims it cannot be proven, can be proven, then the system proves a contradiction". This is entirely normal, and does not overturn anything. However! While the assumption that ¬UNP allows us to derive ◻⊥, it does not allow us to derive ⊥. We have __not__ shown that ¬UNP → ⊥, we have only shown that ¬UNP → ◻⊥. Therefore, this is not justification in appealing to proof by contradiction, and concluding UNP (nor ◻UNP).

bloak 6y ago
I've not read ProfHewitt's argument, so I'm just looking at your summary. If ◻P means "P is a proposition that is formally provable within some implicit formal system" (perhaps there should be a subscripted letter to show which formal system because there are an infinite number of them), then I don't understand what ◻◻UNP means, because ◻UNP is not a proposition of the implicit formal system.
- chriswarbo 6y ago
  > If ◻P means "P is a proposition that is formally provable within some implicit formal system" (perhaps there should be a subscripted letter to show which formal system because there are an infinite number of them) It doesn't mean that. The formal system is explicit: it's the system we're using to write statements like `◻P` (it's a form of modal logic https://en.wikipedia.org/wiki/Modal_logic https://en.wikipedia.org/wiki/Modal_logic ).
  - ProfHewitt 6y ago
    Thanks Chris! It would be perfectly reasonable to be more explicit and use a subscript name for the theory after the ⊢. In fact, when more than one theory is being used, it is necessary to the use the subscript to avoid ambiguity. Unfortunately, many modal logics do not allow the subscript.
- ProfHewitt 6y ago
  Excellent question Bloak! The proof is for a foundation that can formalize its own provability. Consequently, ⊢⊢I’mUnprovable means that ⊢I’mUnprovable is provable in the foundation.
- drdeca 6y ago
  If we were doing this in Peano Arithmetic using Gödel numberings, then ◻P would be expression by taking the Gödel number encoding P and applying a predicate that expresses provability to that number. This might be written as like, Provable«P» with the quotes indicating taking the Gödel number of the proposition P, in order to encode it in a way that Peano arithmetic can talk about. (Usually one uses the right angle brackets on the upper corners for the quoting, but my phone doesn’t have that on the keyboard, which is why I’m using “«“ and “»”). Statements like this are statements in the same formal system as P. The modal logic known as “provability logic” is a nice abstracted system which captures how these things work, and allows for dealing with them in a general case. ◻◻P is perfectly sensible, and if the system is able to describe itself sufficiently well (which is not a high bar; Peano arithmetic satisfies this requirement.) then if you can derive P within the system (without additional assumptions), then, simply by including a proof that the proof of P is a proof of P, one can produce a proof in the system of ◻P, And so, if one can derive ◻P, so too can one derive ◻◻P . (ProfHewitt’s post also uses basically the same thing as ◻◻P , though he writes it using the turnstile symbol rather than the square symbol, and I prefer the square symbol for it, and the turnstile for something slightly different. Not saying the use of the turnstile for it is wrong though.)
  - ProfHewitt 6y ago
    Unfortunately, the Gödel number of a proposition does not represent the order of the proposition. Consequently, the [Gödel 1931] proposition I'mUnprovable cannot be constructed in foundations because the Diagonal Lemma used in [Gödel 1931] does not work for propositions with orders. Provability Logic is built on the existence of the proposition I'mUnprovable :-(
    - drdeca 6y ago
      You’re free to use a system that has orders of propositions, and I’m sure there are interesting things to be said about systems with such orders. (The set theory of NFU seems rather appealing, and stratified formulas seem somewhat analogous.) (And yes, if you restrict what a system can do, it is possible to produce a system which can, in a sense, prove its own consistency. Dan Willard produced one such system. It has subtraction and division as fundamental rather than addition and multiplication.) However, a theory is not required to have orders of propositions (Or, perhaps you might prefer saying this as “A theory can have all of its propositions be if the same order”?). Furthermore, in a formal system modeling the mathematical properties of a syntactical system (as in, a set of rules describing allowed transformations on some strings), this also does not require having multiple orders of propositions. And modeling what things are provable in a given formal system, is just that same kind of thing. So, when describing in a formal system which well-formed-formulas can be derived within that system, it is not necessary (in the sense of “you don’t have to do it.”) to use multiple orders of propositions. (Of course, in any formal proof of a wff which we interpret as having a meaning, there is perhaps a kind of gap between the string of characters which is provable within the system, and the thing which we interpret it to mean. However, if the system is sound with respect to our interpretation of it, then the things it proves will, under that interpretation of the system, correspond to a meaning which is true. As such, it is usually safe to elide the distinction between “the string corresponding to this proposition is derivable in this formal system” and “this system proves this proposition” (where “this proposition” is taken to refer to some meaning). When interpreting statements made in a system “about” that system, there are kind of two levels of interpretation, kinda-sorta. First, when we interpret a proof within the system that some statement(s) is(are) (not) provable in the system, we first have to interpret the string we have derived as corresponding to the meaning of a claim about the system, namely, a claim about what strings can be derived in the system. At that point, we also interpret what those strings that we interpret the first string as referring to, would mean. This can perhaps sometimes be a little confusing. Keeping this distinction in mind should make it clear why there is no need for orders of propositions when dealing with a system referring to what it can and can’t prove.)
ProfHewitt 6y ago
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 6y 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 6y 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

by drdeca 6y ago

bloak 6y ago

I've not read ProfHewitt's argument, so I'm just looking at your summary. If ◻P means "P is a proposition that is formally provable within some implicit formal system" (perhaps there should be a subscripted letter to show which formal system because there are an infinite number of them), then I don't understand what ◻◻UNP means, because ◻UNP is not a proposition of the implicit formal system.

chriswarbo 6y ago
> If ◻P means "P is a proposition that is formally provable within some implicit formal system" (perhaps there should be a subscripted letter to show which formal system because there are an infinite number of them) It doesn't mean that. The formal system is explicit: it's the system we're using to write statements like `◻P` (it's a form of modal logic https://en.wikipedia.org/wiki/Modal_logic https://en.wikipedia.org/wiki/Modal_logic ).
- ProfHewitt 6y ago
  Thanks Chris! It would be perfectly reasonable to be more explicit and use a subscript name for the theory after the ⊢. In fact, when more than one theory is being used, it is necessary to the use the subscript to avoid ambiguity. Unfortunately, many modal logics do not allow the subscript.
ProfHewitt 6y ago
Excellent question Bloak! The proof is for a foundation that can formalize its own provability. Consequently, ⊢⊢I’mUnprovable means that ⊢I’mUnprovable is provable in the foundation.
drdeca 6y ago
If we were doing this in Peano Arithmetic using Gödel numberings, then ◻P would be expression by taking the Gödel number encoding P and applying a predicate that expresses provability to that number. This might be written as like, Provable«P» with the quotes indicating taking the Gödel number of the proposition P, in order to encode it in a way that Peano arithmetic can talk about. (Usually one uses the right angle brackets on the upper corners for the quoting, but my phone doesn’t have that on the keyboard, which is why I’m using “«“ and “»”). Statements like this are statements in the same formal system as P. The modal logic known as “provability logic” is a nice abstracted system which captures how these things work, and allows for dealing with them in a general case. ◻◻P is perfectly sensible, and if the system is able to describe itself sufficiently well (which is not a high bar; Peano arithmetic satisfies this requirement.) then if you can derive P within the system (without additional assumptions), then, simply by including a proof that the proof of P is a proof of P, one can produce a proof in the system of ◻P, And so, if one can derive ◻P, so too can one derive ◻◻P . (ProfHewitt’s post also uses basically the same thing as ◻◻P , though he writes it using the turnstile symbol rather than the square symbol, and I prefer the square symbol for it, and the turnstile for something slightly different. Not saying the use of the turnstile for it is wrong though.)
- ProfHewitt 6y ago
  Unfortunately, the Gödel number of a proposition does not represent the order of the proposition. Consequently, the [Gödel 1931] proposition I'mUnprovable cannot be constructed in foundations because the Diagonal Lemma used in [Gödel 1931] does not work for propositions with orders. Provability Logic is built on the existence of the proposition I'mUnprovable :-(
  - drdeca 6y ago
    You’re free to use a system that has orders of propositions, and I’m sure there are interesting things to be said about systems with such orders. (The set theory of NFU seems rather appealing, and stratified formulas seem somewhat analogous.) (And yes, if you restrict what a system can do, it is possible to produce a system which can, in a sense, prove its own consistency. Dan Willard produced one such system. It has subtraction and division as fundamental rather than addition and multiplication.) However, a theory is not required to have orders of propositions (Or, perhaps you might prefer saying this as “A theory can have all of its propositions be if the same order”?). Furthermore, in a formal system modeling the mathematical properties of a syntactical system (as in, a set of rules describing allowed transformations on some strings), this also does not require having multiple orders of propositions. And modeling what things are provable in a given formal system, is just that same kind of thing. So, when describing in a formal system which well-formed-formulas can be derived within that system, it is not necessary (in the sense of “you don’t have to do it.”) to use multiple orders of propositions. (Of course, in any formal proof of a wff which we interpret as having a meaning, there is perhaps a kind of gap between the string of characters which is provable within the system, and the thing which we interpret it to mean. However, if the system is sound with respect to our interpretation of it, then the things it proves will, under that interpretation of the system, correspond to a meaning which is true. As such, it is usually safe to elide the distinction between “the string corresponding to this proposition is derivable in this formal system” and “this system proves this proposition” (where “this proposition” is taken to refer to some meaning). When interpreting statements made in a system “about” that system, there are kind of two levels of interpretation, kinda-sorta. First, when we interpret a proof within the system that some statement(s) is(are) (not) provable in the system, we first have to interpret the string we have derived as corresponding to the meaning of a claim about the system, namely, a claim about what strings can be derived in the system. At that point, we also interpret what those strings that we interpret the first string as referring to, would mean. This can perhaps sometimes be a little confusing. Keeping this distinction in mind should make it clear why there is no need for orders of propositions when dealing with a system referring to what it can and can’t prove.)

ProfHewitt 6y ago

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 6y 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 6y 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