3 ms·

A set of elements that lead to the concept of provability[1] are: 0, 1, addition, multiplication, quotient, remainder and inequality. Quotient and remainder ar

A set of elements that lead to the concept of provability[1] are: 0, 1, addition, multiplication, quotient, remainder and inequality. Quotient and remainder are definable implicitly in the language of number theory (the language of Peano Arithmetic). Sometimes inequality is explicitly defined, and sometimes it is implicitly defined using exists and addition. From these elements you can go on to define the Goedel beta function, which allows you to encode lists of numbers and extract the nth element from such an encoding. From there you can go on to define arbitrary primitive recursion (and even more). From there provability can be defined as a primitive recursive function. I'm not sure which element there you want to ban. Maybe you want to ban multiplication? [1]http://r6.ca/blog/20190223T161625Z.html http://r6.ca/blog/20190223T161625Z.html

scotty79 5y ago
You can ban the way how you combine the elements. When you reach the step where you define primitive recursion you could say that statements that involve recursion of depth of more than hundred are not true or false or undecided but just meaningless and excluded from mathematical consideration. I know it sounds silly but the statements that prevent infinite recursion in programming languages often do look silly. They look like a hackish stopgap that doesn't fit the pristine recursive algorithm. Yet they work and protect you at the cost of the recursion not to be able to correctly deal wit stuff that would need a deeper recursion.
- rssoconnor 5y ago
  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

You can ban the way how you combine the elements. When you reach the step where you define primitive recursion you could say that statements that involve recursion of depth of more than hundred are not true or false or undecided but just meaningless and excluded from mathematical consideration. I know it sounds silly but the statements that prevent infinite recursion in programming languages often do look silly. They look like a hackish stopgap that doesn't fit the pristine recursive algorithm. Yet they work and protect you at the cost of the recursion not to be able to correctly deal wit stuff that would need a deeper recursion.

rssoconnor 5y ago
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.