5 ms·

These statements are not phrased in terms of recursion. Once you inline all the definitions then they are phrased in terms of arithmetic. That's the whole poin

These statements are not phrased in terms of recursion. Once you inline all the definitions then they are phrased in terms of arithmetic. That's the whole point of all this! Have a look at http://tachyos.org/godel/Godel_statement.html http://tachyos.org/godel/Godel_statement.html and tell me exactly why that formula is banned? Is the formula too long? To many uses of multiplication? Give me a decision procedure.

scotty79 5y ago
Yes. To avoid paradoxes you need to limit nesting, inlined or not. This statement reeks of uncontrolled infinities with all the quantifiers and I don't even know what some symbols mean like 0''' Because of my ignorance I can't point the exact problem here but I don't think it is the multiplication. Alternatively you might just redefine the concept of something being true such that you only provable things are true and unprovable ones are either false, undecidable or nonsensical. And nonsensical thing is defined as a statement thats unprovable but seemingly true. I think there many ways to fix this just by restricting yourself with how you define things. And it's not about restricting arithmetc because that's not the core of the issue, that's just the (simplest?) example.
- rssoconnor 5y ago
  So your problem is with the use of unbounded quantifiers that range over all natural numbers? So for example you would consider "∀x. ∀y. x + y = y + x" a nonsense statement because we are quantifying over all natural numbers, and there are an infinite number of natural numbers, so we cannot quantify over them? (For the record the ' in 0' or x1' is a post-fix notation for the successor operation. See http://tachyos.org/godel/proof.html http://tachyos.org/godel/proof.html for details).
  - scotty79 5y ago
    I don't know what the problem with that particular long statement is. You might just say that a thing is nonsensical if it's not provable but is not false either. This might be sensible 'stack overflow' exception if we really are unable to provide reasonable limits on self reference reference and reasoning relying on infinities.
    - rssoconnor 5y ago
      Nonsensical if it's not provable with respect to what theory exactly? Elementary function Arithemetic? Primitive Recursive Arithemetic? Peano Arithemtic? Martin-Löf type theory? ZF set theory? ZFC+"there exist an infinite number of Woodin cardinals"? "The set of true statements of number theory"? Each of these logical theories are each able to prove an increasing number of arithmetic propositions. What is or is not provable is relative the deduction system or selection of axioms. For example, that big expression that I linked to is designed so that isn't provable in Peano Arithmetic, but it will be provable Martin-Löf type theory, ZF set theory, etc.
      - scotty79 5y ago
        If it's not provable and not false in F it's nonsensical in F. Might become sensible with more axioms. I'd like to ask you a question... Can you take the expression you linked to and add its negation as the additional axiom to Peano arithmetic? Or would it lead to some contradictions?
ProfHewitt 5y ago
The [Gödel 1931] proposition I'mUnprovable does not exist because the fixed-point on which it is based does not exist since it violates restrictions on orders of propositions.
- rssoconnor 5y ago
  The statement clearly that I linked to clearly exists. It's right there in front of your eyes.
  - ProfHewitt 5y ago
    If proposition I'mUnprovable exists in foundations, then the foundations are inconsistent, which was proved in the article linked elsewhere in this discussion.
    - rssoconnor 5y ago
      Does the proposition I linked to exist? Can you see it? Is it not a well-formed proposition in the language of number theory? How about this proposition: "∀x. ∀y. x + y = y + x". Does it exist? Is it not a well-formed proposition in the language of number theory?
      - ProfHewitt 5y ago
        Did you not get the point? If [Gödel 1931] proposition I'mUnprovable exists in foundations, then foundations are inconsistent. See https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
        rssoconnor 5y ago
        I'm sorry that no I don't get the point. You keep talking about [Gödel 1931] proposition I'mUnprovable, but today is 2021 not 1931, and I'm talking about a specific proposition that I've linked to which is, what appears to me to be a clearly well defined first-order logical proposition involving classical logic, zero, successor, plus and times. I want to know if you object to the existence of that formula that you can see on your screen with your own eyes, and if you do object to it why you do. Because I contend that that formula is of exactly the same character as Goedel's statement, with the difference being that with a computer, and modern encoding functions, we can actually strip away all the definitions and compute the fixed point and literally print it out onto your screen. It is right there in front of your eyes. Look at it! Yet you keep on insisting that fixpoints don't exist despite the fact that I have pointed you directly to a formula that has been specifically computed to satisfy a logical fixed point equation. It's like saying that there cannot be a fixed point of the function f(x) := 3x-10 by waiving your hands and claiming functions don't have fixed point because numbers need to be ordered. But that is daft. All you have to do is compute f(5) = 3*5-10 = 5 to see that 5 is a fixed point of f. Take a look at this. The proposition 0=0 is a fixed point of phi(X) = ¬(¬X). Just do the logical deduction to see 0=0 ⇔ ¬(¬ 0=0) is a true arithmetic statement. See even fixed points for propositions sometimes exist!

scotty79 5y ago

Yes. To avoid paradoxes you need to limit nesting, inlined or not. This statement reeks of uncontrolled infinities with all the quantifiers and I don't even know what some symbols mean like 0''' Because of my ignorance I can't point the exact problem here but I don't think it is the multiplication. Alternatively you might just redefine the concept of something being true such that you only provable things are true and unprovable ones are either false, undecidable or nonsensical. And nonsensical thing is defined as a statement thats unprovable but seemingly true. I think there many ways to fix this just by restricting yourself with how you define things. And it's not about restricting arithmetc because that's not the core of the issue, that's just the (simplest?) example.

rssoconnor 5y ago
So your problem is with the use of unbounded quantifiers that range over all natural numbers? So for example you would consider "∀x. ∀y. x + y = y + x" a nonsense statement because we are quantifying over all natural numbers, and there are an infinite number of natural numbers, so we cannot quantify over them? (For the record the ' in 0' or x1' is a post-fix notation for the successor operation. See http://tachyos.org/godel/proof.html http://tachyos.org/godel/proof.html for details).
- scotty79 5y ago
  I don't know what the problem with that particular long statement is. You might just say that a thing is nonsensical if it's not provable but is not false either. This might be sensible 'stack overflow' exception if we really are unable to provide reasonable limits on self reference reference and reasoning relying on infinities.
  - rssoconnor 5y ago
    Nonsensical if it's not provable with respect to what theory exactly? Elementary function Arithemetic? Primitive Recursive Arithemetic? Peano Arithemtic? Martin-Löf type theory? ZF set theory? ZFC+"there exist an infinite number of Woodin cardinals"? "The set of true statements of number theory"? Each of these logical theories are each able to prove an increasing number of arithmetic propositions. What is or is not provable is relative the deduction system or selection of axioms. For example, that big expression that I linked to is designed so that isn't provable in Peano Arithmetic, but it will be provable Martin-Löf type theory, ZF set theory, etc.
    - scotty79 5y ago
      If it's not provable and not false in F it's nonsensical in F. Might become sensible with more axioms. I'd like to ask you a question... Can you take the expression you linked to and add its negation as the additional axiom to Peano arithmetic? Or would it lead to some contradictions?

ProfHewitt 5y ago

The [Gödel 1931] proposition I'mUnprovable does not exist because the fixed-point on which it is based does not exist since it violates restrictions on orders of propositions.

rssoconnor 5y ago
The statement clearly that I linked to clearly exists. It's right there in front of your eyes.
- ProfHewitt 5y ago
  If proposition I'mUnprovable exists in foundations, then the foundations are inconsistent, which was proved in the article linked elsewhere in this discussion.
  - rssoconnor 5y ago
    Does the proposition I linked to exist? Can you see it? Is it not a well-formed proposition in the language of number theory? How about this proposition: "∀x. ∀y. x + y = y + x". Does it exist? Is it not a well-formed proposition in the language of number theory?
    - ProfHewitt 5y ago
      Did you not get the point? If [Gödel 1931] proposition I'mUnprovable exists in foundations, then foundations are inconsistent. See https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
      - rssoconnor 5y ago
        I'm sorry that no I don't get the point. You keep talking about [Gödel 1931] proposition I'mUnprovable, but today is 2021 not 1931, and I'm talking about a specific proposition that I've linked to which is, what appears to me to be a clearly well defined first-order logical proposition involving classical logic, zero, successor, plus and times. I want to know if you object to the existence of that formula that you can see on your screen with your own eyes, and if you do object to it why you do. Because I contend that that formula is of exactly the same character as Goedel's statement, with the difference being that with a computer, and modern encoding functions, we can actually strip away all the definitions and compute the fixed point and literally print it out onto your screen. It is right there in front of your eyes. Look at it! Yet you keep on insisting that fixpoints don't exist despite the fact that I have pointed you directly to a formula that has been specifically computed to satisfy a logical fixed point equation. It's like saying that there cannot be a fixed point of the function f(x) := 3x-10 by waiving your hands and claiming functions don't have fixed point because numbers need to be ordered. But that is daft. All you have to do is compute f(5) = 3*5-10 = 5 to see that 5 is a fixed point of f. Take a look at this. The proposition 0=0 is a fixed point of phi(X) = ¬(¬X). Just do the logical deduction to see 0=0 ⇔ ¬(¬ 0=0) is a true arithmetic statement. See even fixed points for propositions sometimes exist!