Return to Answer

Let me triage my questions. I think Dr. David Roberts and me agree Mochizuki's definition is not rigorous. The point being disagreed with is how math papers having non-strict arguments should be treated. As far as I understand, I will try to explain about this in the following paragraph, and for people who would like to know this paper's situation from set theoretic foundationalism, in the next paragraph of it.

I thought mathematicians have their foundation of mathematics, and some is ZFC and others is dependent type theory, but practically this is not the case, even Grothendieck; the thing is, there are mathematicians not having any foundations. As Dr. Kevin Buzzard said in this blog post, Grothendieck sees $R[1/f]$ and $R[1/g]$ are the same when satisfying the condition that a prime ideal contains $f$ iff it contains $g$. Of course, although there is the unique $R$-algebra isomorphism, there is a non-small gap in proofs due to its set-theoretic non-equality.(For details, you can read it.) Although I understand how to think that any foundations are not essence, but mathematician's intuitions are, but in my opinion, non-rigorous arguments in math papers should be pointed out, such as Dick Gross's paper in 1990. Especially in recent rise of theorem provers like Lean (is based on dependent type theory not ZFC though, even so) mistakes from formalism can be more easily discovered. I think this is not troublesome; but also chance to improve mathematicians' paper quick. I think the reviewers would ought to comment about non-strictness, and it would be better that authors tackle formalization.

Let me change the subject. For those would like to know what in Mochizuki's definition doesn't go well from set theory more deeply, I'll try it. Normally, one starts from a meta theory and first-order logic it has. By using the logic, we can have the language $<\in>$ and the ZFC axioms, and using the axioms, develop mathematics, or proofs. However, in math, there are many symbols like $0$, not included in the language. This is justified by the extension by definition; concisely, $\emptyset$ which should be equal to $0$, is checked that it uniquely exists as sets. Then we can add $0$ to the language, and so it becomes $<\in, 0>$. On the other hand, if we have an object which is unique up to isomorphism, then can we define it? The answer is no, at least straightforward since 'isomorphic' doesn't necessarily mean 'equal' as sets, so it may be not unique. However, 'up to', as the link says, means the equivalence class is unique as sets, so we can define it as using the class without any stumbling blocks. Therefore, this uncovers that Mochizuki's definition have a problem: we don't know about 'up to poly-isomorphism' as I said in the edit, and we can't define ${}^{\circ} \mathcal{HT}^{\mathcal{D}\text{-}\Theta^{\pm \mathscr{ell}}}$.

People who have a different philosophical position as me, may think this is the problem of ZFC, not Mochizuki's definition, but this will be my answer to my question. If I have any mistakes, then I apologize for it.

Let me triage my questions. I think Dr. David Roberts and me agree Mochizuki's definition is not rigorous. The point being disagreed with is how math papers having non-strict arguments should be treated. As far as I understand, I will try to explain about this in the following paragraph, and for people who would like to know this paper's situation from set theoretic foundationalism, in the next paragraph of it.

I thought mathematicians have their foundation of mathematics, and some is ZFC and others is dependent type theory, but practically this is not the case, even Grothendieck; the thing is, there are mathematicians not having any foundations. As Dr. Kevin Buzzard said in this blog post or Chapter 6 of his recent paper on arXiv, Grothendieck's use of equality, Grothendieck sees $R[1/f]$ and $R[1/g]$ are the same when satisfying the condition that a prime ideal contains $f$ iff it contains $g$. Of course, although there is the unique $R$-algebra isomorphism, there is a non-small gap in proofs due to its set-theoretic non-equality.(For details, you can read it.) Although I understand how to think that any foundations are not essence, but mathematician's intuitions are, but in my opinion, non-rigorous arguments in math papers should be pointed out, such as Dick Gross's paper in 1990. Especially in recent rise of theorem provers like Lean (is based on dependent type theory not ZFC though, even so) mistakes from formalism can be more easily discovered. I think this is not troublesome; but also chance to improve mathematicians' paper quick. I think the reviewers would ought to comment about non-strictness, and it would be better that authors tackle formalization.

Let me change the subject. For those would like to know what in Mochizuki's definition doesn't go well from set theory more deeply, I'll try it. Normally, one starts from a meta theory and first-order logic it has. By using the logic, we can have the language $<\in>$ and the ZFC axioms, and using the axioms, develop mathematics, or proofs. However, in math, there are many symbols like $0$, not included in the language. This is justified by the extension by definition; concisely, $\emptyset$ which should be equal to $0$, is checked that it uniquely exists as sets. Then we can add $0$ to the language, and so it becomes $<\in, 0>$. On the other hand, if we have an object which is unique up to isomorphism, then can we define it? The answer is no, at least straightforward since 'isomorphic' doesn't necessarily mean 'equal' as sets, so it may be not unique. However, 'up to', as the link says, means the equivalence class is unique as sets, so we can define it as using the class without any stumbling blocks. Therefore, this uncovers that Mochizuki's definition have a problem: we don't know about 'up to poly-isomorphism' as I said in the edit, and we can't define ${}^{\circ} \mathcal{HT}^{\mathcal{D}\text{-}\Theta^{\pm \mathscr{ell}}}$.

People who have a different philosophical position as me, may think this is the problem of ZFC, not Mochizuki's definition, but this will be my answer to my question. If I have any mistakes, then I apologize for it.

Let me triage my questions. I think Dr. David Roberts and me agree Mochizuki's definition is not rigorous. The point being disagreed with is how math papers having non-strict arguments should be treated. As far as I understand, I will try to explain about this in the following paragraph, and for people who would like to know this paper's situation from set theoretic foundationalism, in the next paragraph of it.

I thought mathematicians have their foundation of mathematics, and some is ZFC and others is dependent type theory, but practically this is not the case, even Grothendieck; the thing is, there are mathematicians not having any foundations. As Dr. Kevin buzzard said in this blog post, Grothendieck sees $R[1/f]$ and $R[1/g]$ are the same when satisfying the condition that a prime ideal contains $f$ iff it contains $g$. Of course, although there is the unique $R$-algebra isomorphism, there is a non-small gap in proofs due to its set-theoretic non-equality.(For details, you can read it.) Although I understand how to think that any foundations are not essence, but mathematician's intuitions are, but in my opinion, non-rigorous arguments in math papers should be pointed out, such as Dick Gross's paper in 1990. Especially in recent rise of theorem provers like Lean (is based on dependent type theory not ZFC though, even so) mistakes from formalism can be more easily discovered. I think this is not troublesome; but also chance to improve mathematicians' paper quick. I think the reviewers would ought to comment about non-strictness, and it would be better that authors tackle formalization.

Let me change the subject. For those would like to know what in Mochizuki's definition doesn't go well from set theory more deeply, I'll try it. Normally, one starts from a meta theory and first-order logic it has. By using the logic, we can have the language $<\in>$ and the ZFC axioms, and using the axioms, develop mathematics, or proofs. However, in math, there are many symbols like $0$, not included in the language. This is justified by the extension by definition; concisely, $\emptyset$ which should be equal to $0$, is checked that it uniquely exists as sets. Then we can add $0$ to the language, and so it becomes $<\in, 0>$. On the other hand, if we have an object up to isomorphism, then can we define it? The answer is no, at least straightforward since 'isomorphic' doesn't necessarily mean 'equal' as sets, so it may be not unique. However, 'up to', as the link says, means the equivalence class is unique as sets, so we can define it as using the class without any stumbling blocks. Therefore, this uncovers that Mochizuki's definition have a problem: we don't know about 'up to poly-isomorphism' as I said in the edit, and we can't define ${}^{\circ} \mathcal{HT}^{\mathcal{D}\text{-}\Theta^{\pm \mathscr{ell}}}$.

People who have a different philosophical position as me, may think this is the problem of ZFC, not Mochizuki's definition, but this will be my answer to my question. If I have any mistakes, then I apologize for it.

Let me triage my questions. I think Dr. David Roberts and me agree Mochizuki's definition is not rigorous. The point being disagreed with is how math papers having non-strict arguments should be treated. As far as I understand, I will try to explain about this in the following paragraph, and for people who would like to know this paper's situation from set theoretic foundationalism, in the next paragraph of it.

I thought mathematicians have their foundation of mathematics, and some is ZFC and others is dependent type theory, but practically this is not the case, even Grothendieck; the thing is, there are mathematicians not having any foundations. As Dr. Kevin Buzzard said in this blog post, Grothendieck sees $R[1/f]$ and $R[1/g]$ are the same when satisfying the condition that a prime ideal contains $f$ iff it contains $g$. Of course, although there is the unique $R$-algebra isomorphism, there is a non-small gap in proofs due to its set-theoretic non-equality.(For details, you can read it.) Although I understand how to think that any foundations are not essence, but mathematician's intuitions are, but in my opinion, non-rigorous arguments in math papers should be pointed out, such as Dick Gross's paper in 1990. Especially in recent rise of theorem provers like Lean (is based on dependent type theory not ZFC though, even so) mistakes from formalism can be more easily discovered. I think this is not troublesome; but also chance to improve mathematicians' paper quick. I think the reviewers would ought to comment about non-strictness, and it would be better that authors tackle formalization.

Let me change the subject. For those would like to know what in Mochizuki's definition doesn't go well from set theory more deeply, I'll try it. Normally, one starts from a meta theory and first-order logic it has. By using the logic, we can have the language $<\in>$ and the ZFC axioms, and using the axioms, develop mathematics, or proofs. However, in math, there are many symbols like $0$, not included in the language. This is justified by the extension by definition; concisely, $\emptyset$ which should be equal to $0$, is checked that it uniquely exists as sets. Then we can add $0$ to the language, and so it becomes $<\in, 0>$. On the other hand, if we have an object which is unique up to isomorphism, then can we define it? The answer is no, at least straightforward since 'isomorphic' doesn't necessarily mean 'equal' as sets, so it may be not unique. However, 'up to', as the link says, means the equivalence class is unique as sets, so we can define it as using the class without any stumbling blocks. Therefore, this uncovers that Mochizuki's definition have a problem: we don't know about 'up to poly-isomorphism' as I said in the edit, and we can't define ${}^{\circ} \mathcal{HT}^{\mathcal{D}\text{-}\Theta^{\pm \mathscr{ell}}}$.

People who have a different philosophical position as me, may think this is the problem of ZFC, not Mochizuki's definition, but this will be my answer to my question. If I have any mistakes, then I apologize for it.

Let me triage my questions. I think Dr. David Roberts and me agree Mochizuki's definition is not rigorous. The point being disagreed with is how math papers having non-strict arguments should be treated. As far as I understand, I will try to explain about this in the following paragraph, and for people who would like to know this paper's situation from set theoretic foundationalism, in the next paragraph of it.

I thought mathematicians have their foundation of mathematics, and some is ZFC and others is dependent type theory, but practically this is not the case, even Grothendieck; the thing is, there are mathematicians not having any foundations. As Dr. Kevin buzzard said in this blog post, Grothendieck sees $R[1/f]$ and $R[1/g]$ are the same when satisfying the condition that a prime ideal contains $f$ iff it contains $g$. Of course, although there is the unique $R$-algebra isomorphism, there is a non-small gap in proofs due to its set-theoretic non-equality.(For details, you can read it.) Although I understand how to think that any foundations are not essence, but mathematician's intuitions are, but in my opinion, non-rigorous arguments in math papers should be pointed out, such as Dick Gross's paper in 1990. Especially in recent rise of theorem provers like Lean (is based on dependent type theory not ZFC though, even so) mistakes from formalism can be more easily discovered. I think this is not troublesome; but also chance to improve mathematicians' paper quick. I think the reviewers would ought to comment about non-strictness, and authors would tackle formalization.

Let me change the subject. For those would like to know what in Mochizuki's definition doesn't go well from set theory more deeply, I'll try it. Normally, one starts from a meta theory and first-order logic it has. By using the logic, we can have the language $<\in>$ and the ZFC axioms, and using the axioms, develop mathematics, or proofs. However, in math, there are many symbols like $0$, not included in the language. This is justified by the extension by definition; concisely, $\emptyset$ which should be equal to $0$, is checked that it uniquely exists as sets. Then we can add $0$ to the language, and so it becomes $<\in, 0>$. On the other hand, if we have an object up to isomorphism, then can we define it? The answer is no, at least straightforward since 'isomorphic' doesn't necessarily mean 'equal' as sets, so it may be not unique. However, 'up to', as the link says, means the equivalence class is unique as sets, so we can define it as using the class without any stumbling blocks. Therefore, This uncovers that Mochizuki's definition have a problem: we don't know about 'up to poly-isomorphism' as I said in the edit, and we can't define ${}^{\circ} \mathcal{HT}^{\mathcal{D}\text{-}\Theta^{\pm \mathscr{ell}}}$.

People who have a different philosophical position as me, may think this is the problem of ZFC, not Mochizuki's definition, but this will be my answer to my question. If I have any mistakes, then I apologize for it.

Let me triage my questions. I think Dr. David Roberts and me agree Mochizuki's definition is not rigorous. The point being disagreed with is how math papers having non-strict arguments should be treated. As far as I understand, I will try to explain about this in the following paragraph, and for people who would like to know this paper's situation from set theoretic foundationalism, in the next paragraph of it.

I thought mathematicians have their foundation of mathematics, and some is ZFC and others is dependent type theory, but practically this is not the case, even Grothendieck; the thing is, there are mathematicians not having any foundations. As Dr. Kevin buzzard said in this blog post, Grothendieck sees $R[1/f]$ and $R[1/g]$ are the same when satisfying the condition that a prime ideal contains $f$ iff it contains $g$. Of course, although there is the unique $R$-algebra isomorphism, there is a non-small gap in proofs due to its set-theoretic non-equality.(For details, you can read it.) Although I understand how to think that any foundations are not essence, but mathematician's intuitions are, but in my opinion, non-rigorous arguments in math papers should be pointed out, such as Dick Gross's paper in 1990. Especially in recent rise of theorem provers like Lean (is based on dependent type theory not ZFC though, even so) mistakes from formalism can be more easily discovered. I think this is not troublesome; but also chance to improve mathematicians' paper quick. I think the reviewers would ought to comment about non-strictness, and it would be better that authors tackle formalization.

Let me change the subject. For those would like to know what in Mochizuki's definition doesn't go well from set theory more deeply, I'll try it. Normally, one starts from a meta theory and first-order logic it has. By using the logic, we can have the language $<\in>$ and the ZFC axioms, and using the axioms, develop mathematics, or proofs. However, in math, there are many symbols like $0$, not included in the language. This is justified by the extension by definition; concisely, $\emptyset$ which should be equal to $0$, is checked that it uniquely exists as sets. Then we can add $0$ to the language, and so it becomes $<\in, 0>$. On the other hand, if we have an object up to isomorphism, then can we define it? The answer is no, at least straightforward since 'isomorphic' doesn't necessarily mean 'equal' as sets, so it may be not unique. However, 'up to', as the link says, means the equivalence class is unique as sets, so we can define it as using the class without any stumbling blocks. Therefore, this uncovers that Mochizuki's definition have a problem: we don't know about 'up to poly-isomorphism' as I said in the edit, and we can't define ${}^{\circ} \mathcal{HT}^{\mathcal{D}\text{-}\Theta^{\pm \mathscr{ell}}}$.

People who have a different philosophical position as me, may think this is the problem of ZFC, not Mochizuki's definition, but this will be my answer to my question. If I have any mistakes, then I apologize for it.