Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorDavidRoberts
   • CommentTimeMay 18th 2012
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexIN the paper <http://www.tac.mta.ca/tac/volumes/16/19/16-19abs.html> Freyd states >12. Theorem. There is a “rewrite” rule that converts any sentence in the logic of topoi with NNO (sometimes called intuitionistic type theory with the axiom of infinity) to an equally provable sentence in the logic of topoi (no axiom of infinity). This seems quite extraordinary on face value. I can't grok this straight up, does anyone have a conceptual explanation?

   IN the paper http://www.tac.mta.ca/tac/volumes/16/19/16-19abs.html Freyd states

   1. Theorem. There is a “rewrite” rule that converts any sentence in the logic of topoi with NNO (sometimes called intuitionistic type theory with the axiom of infinity) to an equally provable sentence in the logic of topoi (no axiom of infinity).

   This seems quite extraordinary on face value. I can’t grok this straight up, does anyone have a conceptual explanation?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeMay 18th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI find the paper very obscure, but I *think* his argument is the following. If we suppose a particular sort of axiom of infinity "$\neg R_\Omega$", then there exists an NNO. And using an NNO, we can construct the free topos-with-NNO. Now the "rewrite rule" takes a statement $\phi$ to the statement "if $\neg R_\Omega$, then $\phi$ holds in the free topos-with-NNO"; call this statement $\phi'$. If $\phi'$ is provable in the logic of toposes, then since $\neg R_\Omega$ holds in sets, $\phi$ holds in the actual free topos-with-NNO, hence is provable in the logic of toposes-with-NNO. Conversely, if $\phi$ is provable in the logic of toposes-with-NNO, then it holds in the actual free topos-with-NNO. But Freyd constructs, internally to the free topos (without NNO), the "free topos with NNO assuming $\neg R_\Omega$" and shows that its global sections are the actual free topos-with-NNO. Hence $\phi$ must also hold for this internal topos-object in the free topos, and therefore $\phi'$ is provable in the logic of toposes. But don't ask me to justify any of those intermediate steps, please. (-:

   I find the paper very obscure, but I think his argument is the following. If we suppose a particular sort of axiom of infinity “$\neg R_\Omega$”, then there exists an NNO. And using an NNO, we can construct the free topos-with-NNO. Now the “rewrite rule” takes a statement $\phi$ to the statement “if $\neg R_\Omega$, then $\phi$ holds in the free topos-with-NNO”; call this statement $\phi'$.

   If $\phi'$ is provable in the logic of toposes, then since $\neg R_\Omega$ holds in sets, $\phi$ holds in the actual free topos-with-NNO, hence is provable in the logic of toposes-with-NNO. Conversely, if $\phi$ is provable in the logic of toposes-with-NNO, then it holds in the actual free topos-with-NNO. But Freyd constructs, internally to the free topos (without NNO), the “free topos with NNO assuming $\neg R_\Omega$” and shows that its global sections are the actual free topos-with-NNO. Hence $\phi$ must also hold for this internal topos-object in the free topos, and therefore $\phi'$ is provable in the logic of toposes.

   But don’t ask me to justify any of those intermediate steps, please. (-:

3. • CommentRowNumber3.
   • CommentAuthorTobyBartels
   • CommentTimeMay 20th 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexAre there any nice properties of this rewrite? Something to ensure that it's not too trivial? (I could rewrite every sentence to $\top$, but that wouldn't be interesting.) This talk of "If the axiom of infinity holds, then $\phi$ holds." reminds me of Fred Richman's deliberately uninteresting method of making any result in classical mathematics constructively valid: rewrite $P$ as $AC \Rightarrow P$. (But apparently Freyd's version is more sophisticated than that.)

   Are there any nice properties of this rewrite? Something to ensure that it’s not too trivial? (I could rewrite every sentence to $\top$, but that wouldn’t be interesting.)

   This talk of “If the axiom of infinity holds, then $\phi$ holds.” reminds me of Fred Richman’s deliberately uninteresting method of making any result in classical mathematics constructively valid: rewrite $P$ as $AC \Rightarrow P$. (But apparently Freyd’s version is more sophisticated than that.)

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeMay 20th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> I could rewrite every sentence to ⊤, but that wouldn't be interesting. It also wouldn't be "equally provable".

   I could rewrite every sentence to ⊤, but that wouldn’t be interesting.

   It also wouldn’t be “equally provable”.

5. • CommentRowNumber5.
   • CommentAuthorTobyBartels
   • CommentTimeMay 20th 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexSomehow I got an extra "provable" when I read Theorem 1, and that nothing was claimed about unprovable statements. So that is one good property: every statement is rewritten, and the implication goes both ways. This still allows Richman's $AC \Rightarrow P$, however. It also allows us to rewrite statements as $\top$ or $\bot$ accordingly as they are provable or not (assuming EM in the metalogic). This can be ruled out if the rewrite rule is computable.

   Somehow I got an extra “provable” when I read Theorem 1, and that nothing was claimed about unprovable statements. So that is one good property: every statement is rewritten, and the implication goes both ways. This still allows Richman’s $AC \Rightarrow P$, however.

   It also allows us to rewrite statements as $\top$ or $\bot$ accordingly as they are provable or not (assuming EM in the metalogic). This can be ruled out if the rewrite rule is computable.

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeMay 20th 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexOne possibility: If the original statement is already expressible and provable in the language without infinity, then how is it rewritten?

   One possibility: If the original statement is already expressible and provable in the language without infinity, then how is it rewritten?

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeMay 21st 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI told you already in #2 everything I was able to gather about what the rewrite rule is. If I was right, it looks computable to me.

   I told you already in #2 everything I was able to gather about what the rewrite rule is. If I was right, it looks computable to me.

8. • CommentRowNumber8.
   • CommentAuthorDavidRoberts
   • CommentTimeMay 21st 2012
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexThanks. It still seems terribly mysterious, and the looseness of the style of the paper does not help.

   Thanks. It still seems terribly mysterious, and the looseness of the style of the paper does not help.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeMay 21st 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexAgreed.

   Agreed.