3 ms·

Unfortunately, the Gödel number of a proposition does not represent the order of the proposition. Consequently, the [Gödel 1931] proposition I'mUnprovable ca

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 5y 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 5y ago
  Orders on propositions are crucial for the consistency of foundations for reasons explained in the following article: "Epistemology Cyberattacks" https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
  - ganafagol 5y ago
    When appeling to authority, could you provide any sources that have not been written by yourself?
    - ProfHewitt 5y ago
      The link to the article is not an appeal to authority. Instead, the article is where you can learn more about the topic under discussion. There are many references in the article that provide additional background.
    - exdsq 5y ago
      In his defence, it isn't a case of the 'usual' HN appeal to authority fallacy https://en.wikipedia.org/wiki/Carl_Hewitt https://en.wikipedia.org/wiki/Carl_Hewitt
      - ProfHewitt 5y ago
        Thanks exdsq! The Wikipedia article on Carl Hewitt is way out date! And there is no way to fix it :-( Consequently, the Wikipedia article should be deleted in order not to mislead readers.
  - deleted 5y ago
    [deleted]
  - drdeca 5y ago
    Are you claiming that (e.g.) ZFC (which does not have orders for propositions) is not "foundations", or that it isn't consistent? Or by "foundations" are you referring to a particular system you are proposing as a foundational system, and which you have named "foundations"? You appear to justify the argument on the basis of the idea of a liar sentence. As exemplified in NFU , it is not necessary to give strict orders to things, as long as you put restrictions on how things are constructed. TST has linearly ordered types, but NFU has no need to introduce these types and orders, as just requiring that formulas be stratified is sufficient. There is no liar sentence in Peano Arithmetic. It isn't a well-formed-formula. Partitioning propositions into orders is not needed in order to prevent it being a well-formed-formula. Just, don't include anything in your rules for what counts as a wff which would let you define it. (you may object that, what if one just does the Godel numbering thing to do some quine-ing, and uses that to produce a liar sentence, but you can't express "The proposition [some number] encodes, is false" in PA (see Tarski's undefinability theorem) .) It isn't like UNK is defined in PA as "a statement UNK such that UNK iff not(provable('UNK'))". That wouldn't be a wff in PA. Rather, it is some long expression involving a bunch of quantifiers over natural numbers, and also a bunch of large numbers, and a bunch of arithmetical relations, and happens to be such that one can prove (in PA) that [UNK iff not(provable('UNK')] .

drdeca 5y 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 5y ago
Orders on propositions are crucial for the consistency of foundations for reasons explained in the following article: "Epistemology Cyberattacks" https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
- ganafagol 5y ago
  When appeling to authority, could you provide any sources that have not been written by yourself?
  - ProfHewitt 5y ago
    The link to the article is not an appeal to authority. Instead, the article is where you can learn more about the topic under discussion. There are many references in the article that provide additional background.
  - exdsq 5y ago
    In his defence, it isn't a case of the 'usual' HN appeal to authority fallacy https://en.wikipedia.org/wiki/Carl_Hewitt https://en.wikipedia.org/wiki/Carl_Hewitt
    - ProfHewitt 5y ago
      Thanks exdsq! The Wikipedia article on Carl Hewitt is way out date! And there is no way to fix it :-( Consequently, the Wikipedia article should be deleted in order not to mislead readers.
- deleted 5y ago
  [deleted]
- drdeca 5y ago
  Are you claiming that (e.g.) ZFC (which does not have orders for propositions) is not "foundations", or that it isn't consistent? Or by "foundations" are you referring to a particular system you are proposing as a foundational system, and which you have named "foundations"? You appear to justify the argument on the basis of the idea of a liar sentence. As exemplified in NFU , it is not necessary to give strict orders to things, as long as you put restrictions on how things are constructed. TST has linearly ordered types, but NFU has no need to introduce these types and orders, as just requiring that formulas be stratified is sufficient. There is no liar sentence in Peano Arithmetic. It isn't a well-formed-formula. Partitioning propositions into orders is not needed in order to prevent it being a well-formed-formula. Just, don't include anything in your rules for what counts as a wff which would let you define it. (you may object that, what if one just does the Godel numbering thing to do some quine-ing, and uses that to produce a liar sentence, but you can't express "The proposition [some number] encodes, is false" in PA (see Tarski's undefinability theorem) .) It isn't like UNK is defined in PA as "a statement UNK such that UNK iff not(provable('UNK'))". That wouldn't be a wff in PA. Rather, it is some long expression involving a bunch of quantifiers over natural numbers, and also a bunch of large numbers, and a bunch of arithmetical relations, and happens to be such that one can prove (in PA) that [UNK iff not(provable('UNK')] .