User ulrik buchholtz - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-25T21:26:57Z http://mathoverflow.net/feeds/user/2004 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/115809/arithmetic-strength-of-peano-the-howard-ordinal/115826#115826 Answer by Ulrik Buchholtz for Arithmetic strength of Peano + the Howard ordinal Ulrik Buchholtz 2012-12-08T18:55:17Z 2012-12-08T18:55:17Z <p>The answer is <em>yes</em>, using the ordinal analysis of KP. See Pohlers' <em>A Short Course in Ordinal Analysis</em> for why the usual ordinal analyses are <em>profound</em>, that is, they imply conservativity of the analyzed theory over PA + TI($\prec_i$) for arithmetical sentences. Here TI($\prec_i$) is the scheme of transfinite induction along all <em>proper</em> initial segments of the primitive recursive well-ordering $\prec$ that measures the proof-theoretic ordinal of the theory.</p> http://mathoverflow.net/questions/88380/why-no-morphisms-from-the-contradictory-proposition-to-the-inconsistent-context/88391#88391 Answer by Ulrik Buchholtz for Why no morphisms from the contradictory proposition to the inconsistent context? Ulrik Buchholtz 2012-02-14T00:36:08Z 2012-02-14T00:36:08Z <p>I'm not sure what you mean by the individual propositional objects having models or not.</p> <p>In any case, as you said, as morphism in $\mathbb P$ simply <em>is</em> a context morphism compatible with the preordering. So $A$ and $B$ are definitely not isomorphic in $\mathbb P$. In a model, $A$ is the initial subobject of the terminal object, while $B$ is the terminal subobject of the initial object (taking models in subobject fibrations for simplicity), and an isomorphism of these subobjects would restrict to an isomorphism of the initial object with the terminal object.</p> http://mathoverflow.net/questions/84745/reduction-rules-for-inductive-types/84753#84753 Answer by Ulrik Buchholtz for Reduction rules for inductive types Ulrik Buchholtz 2012-01-02T16:54:30Z 2012-01-03T19:03:40Z <p>Your second reduction is called a commutative conversion. You can read about it in Girard, Taylor and Lafont, Proofs and Types, p. 80, for example. The congruence relation with commutative conversions for coproducts is has normal forms, see for instance:</p> <p>Normalization by evaluation for typed lambda calculus with coproducts, by T. Altenkirch, P. Dybjer, M. Hofmann, and P. Scott</p> <p>For a strongly normalizing reduction relation for commutative conversions, try:</p> <p>Short Proofs of Normalization for the simply-typed lambda-calculus, permutative conversions and Gödel's T (1999) by Felix Joachimski , Ralph Matthes</p> <p>(EDIT: Three more references. I haven't looked at these, but they sound helpful:)</p> <p>Exceptional NbE for Sums by Freiric Barral</p> <p>P. de Groote. Strong normalization of classical natural deduction with disjunction. In S. Abramsky, editor, Typed Lambda Calculi and Applications, volume 2044 of Lecture Notes in Computer Science, pages 182-196. Springer, 2001.</p> <p>K. Nour and R. David. A short proof of the strong normalization of classical natural deduction with disjunction. The Journal of Symbolic Logic, 68(4):1277-1288, December 2003.</p> http://mathoverflow.net/questions/67329/categorifying-induction-in-homotopy-type-theory/67361#67361 Answer by Ulrik Buchholtz for categorifying induction in homotopy type theory Ulrik Buchholtz 2011-06-09T17:33:14Z 2011-06-09T17:33:14Z <p>The first reason you give is sufficient to answer your question: any interpretation of <code>nat</code> (and any other type with decidable equality) must have contractible components. Let me try to unpack the proof:</p> <p>The proof of <code>isasetifdeceq</code> goes as follows: Fixing $x:X$, we must show that <code>$\text{Paths}(x,x)$</code> is contractible. We know that <code>$\Sigma_{x':X}\text{Paths}(x,x')$</code> is contractible, so we just need the natural map <code>$f:\text{Paths}(x,x)\to\Sigma_{x':X}\text{Paths}(x,x')$</code> to be a weak equivalence. This follows from the hypothesis using the theorem <code>onefiber</code>, which establishes that for a fibration which is empty over all but one path-component of the base, the total space is equivalent to a fiber over the remaining component.</p> <p>Regarding (2). I think there's some confusion here: Let me try to unpack <code>nat_rect</code> in a more direct way: For any fibration <code>$\Sigma_{\text{nat}} P\to\text{nat}$</code> over <code>nat</code>, given a point in <code>$P_0$</code> and a section of <code>$\Pi_{n:\text{nat}}\text{Map}(P_n,P_{n+1})\to\text{nat}$</code>, you get a section of $P$. That is the interpretation of primitive recursion/induction.</p> http://mathoverflow.net/questions/20779/mechanically-instantiating-abstract-constructions/20900#20900 Answer by Ulrik Buchholtz for Mechanically instantiating abstract constructions Ulrik Buchholtz 2010-04-10T06:55:15Z 2010-04-10T06:55:15Z <p>I don't know if this answers your question, but here's how I would think about it. Work in a dependent type theory, and suppose we've defined a type of categories, $\mathrm{Cat}$. Suppose we've proved some theorem about categories, $\mathit{Thm}$, with proof term $p\colon\forall C\colon\mathrm{Cat},\mathit{Thm}(C)$. An example of the phenomenon in question would then be to specialize this theorem to a specific category, or to a specialized class of categories. Say we want to specialize to monoids. Then we might have a type of monoids, $\mathrm{Mon}$, and a function $\alpha\colon\mathrm{Mon}\to\mathrm{Cat}$ constructing for every monoid the corresponding one-object category. Then we can specialize $\mathit{Thm}$ to get a new theorem, $\forall M\colon\mathrm{Mon},\mathit{Thm}(\alpha M)$, with proof term $\lambda M\colon\mathrm{Mon}, p(\alpha M)$.</p> <p>Another way to look at this, it that having a theorem in some context $\Gamma$ corresponds to a display map in the context category, $(\Gamma, p\colon T)\to\Gamma$. Specializing to another context, $\Delta$, is given by a morphism of contexts $\alpha\colon\Delta\to\Gamma$. Pulling back along $\alpha$ gives you a display map over $\Delta$ with your specialized theorem (obtained by substituting according to $\alpha$).</p> <p>In any case, the specialization procedure is mechanical, given by some sort of substitution, but then the question arises as to how to best simplify and present the result. Say you've specialized the proposition that every split epimorphism in a category is, in fact, an epimorphism. Specializing to monoids states this result in the language of monoids, but maybe you want afterwards to search for definitions and restate the proposition to be that every monoid element with a right inverse is right cancellable. This was just a simple example, but in general there may of course be many possible simplifications of the specialized terms. You could normalize, but the normalization is rarely the most simple form, especially if everything takes place in a non-empty background context.</p> http://mathoverflow.net/questions/19732/ackermann-related-function/19736#19736 Answer by Ulrik Buchholtz for Ackermann-related function Ulrik Buchholtz 2010-03-29T15:38:28Z 2010-03-29T15:38:28Z <p>Googling for "graph of the Ackermann function" gives <a href="http://www.cse.yorku.ca/~gt/papers/Ackermann-function.pdf" rel="nofollow">this note</a> by George Tourlakis, which proves both that the Ackermann function is not primitive recursive, and, at the end, that the graph is.</p> http://mathoverflow.net/questions/19070/reference-request-for-type-theory/19114#19114 Answer by Ulrik Buchholtz for Reference request for type theory Ulrik Buchholtz 2010-03-23T15:16:59Z 2010-03-23T15:16:59Z <p>The kind of type theory you're asking about, Russell's simple theory of types, is from about the early 1900's. Here's a reference:</p> <ul> <li>Russell, Bertrand: Mathematical Logic as Based on the Theory of Types. Amer. J. Math. 30 (1908), no. 3, 222--262.</li> </ul> <p>Recent work in type theory is somewhat different, continuing the tradition of Per Martin-Löf. In addition to his work (referenced by Andrej), I would also recommend the following book by Luo:</p> <ul> <li>Luo, Zhaohui: Computation and reasoning. A type theory for computer science. International Series of Monographs on Computer Science, 11. The Clarendon Press, Oxford University Press, New York, 1994. xii+228 pp. ISBN: 0-19-853835-9.</li> </ul> <p>For the relation between set theory, type theory, and category theory, you might want to have a look at <a href="http://www.andrew.cmu.edu/user/awodey/preprints/stcsFinal.pdf" rel="nofollow">this preprint</a> by Steve Awodey.</p> <p>There's also an <a href="http://ncatlab.org/nlab/show/type+theory" rel="nofollow">n-lab page</a>, and the <a href="http://plato.stanford.edu/entries/type-theory/" rel="nofollow">type theory page</a> at Stanford Encyclopedia of Philosophy has a reference section.</p> http://mathoverflow.net/questions/15689/is-there-any-proof-assistant-based-on-first-order-logic/15724#15724 Answer by Ulrik Buchholtz for Is there any proof assistant based on first-order logic? Ulrik Buchholtz 2010-02-18T16:37:15Z 2010-02-18T16:37:15Z <p>You might want to search out John Harrison's book: Handbook of Practical Logic and Automated Reasoning. In the book he (among other things) develops an interactive theorem prover for first-order logic in OCaml. The code is <a href="http://www.cl.cam.ac.uk/~jrh13/atp/index.html" rel="nofollow">available online</a>.</p> <p>EDIT: The system in the book is based on a Hilbert-style calculus, but due to the LCF-style of the interaction, it can be made to feel a lot like natural deduction.</p> http://mathoverflow.net/questions/14499/is-any-true-sentence-in-the-second-order-peano-axioms-provable/14570#14570 Answer by Ulrik Buchholtz for Is any true sentence in the second-order Peano Axioms provable Ulrik Buchholtz 2010-02-07T23:23:35Z 2010-02-07T23:23:35Z <p>Note that there are two different types of models of second-order logic: standard models, where second-order quantified variables range over all subsets of the domain; and Henkin models, where second-order quantified variables are allowed to range over a proper subset of the full power-set.</p> <p>Henkin proved the completeness theorem for second-order logic for Henkin models, so if a sentence is true in all Henkin models, it is derivable. For completeness to hold, it is not enough to consider only standard models, so even though second-order PA is categorical for standard models, it is not complete (as we would expect, this being a corollary Gödel's theorem).</p> http://mathoverflow.net/questions/5357/theorems-for-nothing-and-the-proofs-for-free/6431#6431 Answer by Ulrik Buchholtz for Theorems for nothing (and the proofs for free) Ulrik Buchholtz 2009-11-22T05:02:41Z 2009-11-22T05:02:41Z <p>Although not exactly what you're after, the question reminds me of Reynolds' parametricity theorem, or as Philip Wadler puts it: <a href="http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html" rel="nofollow">Theorems for Free!</a></p> <p>The basic idea is that a polymorphic construction (in a polymorphic lambda calculus) must behave uniformly, and so must preserve relations. For example, any term of type $\Pi X. X\to X$ must be the identity function, and every term of type $\Pi X Y. X\times Y\to X$ must be the first projection.</p> http://mathoverflow.net/questions/118857/forcing-in-homotopy-type-theory Comment by Ulrik Buchholtz Ulrik Buchholtz 2013-01-14T16:40:43Z 2013-01-14T16:40:43Z Can you add the tag lo.logic ? Thanks! (Later on, there will perhaps be a need for a HoTT tag, but in the meantime I think adding logic as a tag to questions like this will help, as the people interested in HoTT aren't necessarily interested in set theory, nor abstract homotopy or infinity-topos theory outside of the type-theoretic context.) http://mathoverflow.net/questions/107846/is-there-any-connection-between-the-consistent-histories-interpretation-of-quantu Comment by Ulrik Buchholtz Ulrik Buchholtz 2012-09-22T16:52:45Z 2012-09-22T16:52:45Z Check out the topos approaches to quantum mechanics, as initiated by Isham/Butterfield and D&#246;ring/Isham (the contravariant approach, see review by Flori: <a href="http://arxiv.org/abs/1106.5660" rel="nofollow">arxiv.org/abs/1106.5660</a>). There's also a covariant approach, developed by Heunen, Landsman and Spitters (see Wolters' comparison of the approaches: <a href="http://arxiv.org/abs/1010.2031" rel="nofollow">arxiv.org/abs/1010.2031</a>). That should get you started. http://mathoverflow.net/questions/93631/nno-first-order-pa/93739#93739 Comment by Ulrik Buchholtz Ulrik Buchholtz 2012-04-21T16:48:35Z 2012-04-21T16:48:35Z @Andrej: yes, you make sense, and I guess my objection is more terminological: I would take first-order PA to satisfy an induction schema for first-order formulas only, whereas the version here (in Lambek and Scott) is schematic in all (ambiently definable) predicates on N. If you have a PA object N in a topos that only satisfies induction for first-order formulas, then it could be non-standard, but in the topos logic you could then separate out the standard part and make a NNO. http://mathoverflow.net/questions/93631/nno-first-order-pa/93739#93739 Comment by Ulrik Buchholtz Ulrik Buchholtz 2012-04-18T19:34:57Z 2012-04-18T19:34:57Z Andrej, aren't these results about higher-order type theories with power types and full comprehension? They say that a topos with NNO is equivalent to a model of higher-order type theory with full comprehension, in the sense that you can go back and forth (using internal language and syntactic category). Since full comprehension is always assumed, this says little about first-order PA. http://mathoverflow.net/questions/84745/reduction-rules-for-inductive-types/84753#84753 Comment by Ulrik Buchholtz Ulrik Buchholtz 2012-01-03T18:38:37Z 2012-01-03T18:38:37Z Of course you're right that normalization by evaluation only produces normal forms for a congruence relation. For these eta-like rules you have to be careful I you want to extract a normalizing reduction relation, which is why normalization by evaluation seems preferable in this case. I've edited my answer to reflect this, and added another reference you might find helpful. http://mathoverflow.net/questions/67329/categorifying-induction-in-homotopy-type-theory/67361#67361 Comment by Ulrik Buchholtz Ulrik Buchholtz 2011-06-10T06:09:25Z 2011-06-10T06:09:25Z As for (2): The argument you refer to doesn't make much sense to me, since $\sigma$ is not interpreted as a fibration, so why does the question arise as to whether it has a section? That's why I suggested there might be some confusion going on – although I'm probably also confused :-) http://mathoverflow.net/questions/67329/categorifying-induction-in-homotopy-type-theory/67361#67361 Comment by Ulrik Buchholtz Ulrik Buchholtz 2011-06-10T06:05:01Z 2011-06-10T06:05:01Z I agree it's an incredible kind of reasoning - that's part of the fun! And you're right that to give a full unpacking we have to interpret <code>Type</code> by a univalent universe, $U$, with corresponding fibration <code>$\Sigma&#95;{A:U} T(A)\to U$</code> (universe a la Tarski with decoding $T$). And then <code>nat&#95;rect</code> is represented by a section of a certain fibration with base space <code>$\text{Map}(\text{nat},U)$</code>. But it's frankly easier to understand in the type-theoretic notation, remembering to understand constructs constructively/continuously. http://mathoverflow.net/questions/64856/defining-computability-for-functionals-of-partial-oracles Comment by Ulrik Buchholtz Ulrik Buchholtz 2011-05-13T04:00:00Z 2011-05-13T04:00:00Z A thorough answer to this question will be quite long. In the meantime, may suggest section 4 of John R. Longley's survey, Notions of Computability at Higher Types I, [<a href="http://homepages.inf.ed.ac.uk/jrl/Research/notions1.pdf]" rel="nofollow">homepages.inf.ed.ac.uk/jrl/Research/notions1.pdf]</a> ? http://mathoverflow.net/questions/34629/what-is-the-completion-at-a-family-of-ideals Comment by Ulrik Buchholtz Ulrik Buchholtz 2010-08-05T18:12:30Z 2010-08-05T18:12:30Z Just for reference: In other contexts, completion with respect to a family of ideals does occur, where one takes the directed system of finite (possibly repeated) products of ideals in the family, and then takes the limit of the resulting diagram. This nicely generalizes the completion wrt a single ideal. http://mathoverflow.net/questions/32923/how-do-proof-verifiers-work/33019#33019 Comment by Ulrik Buchholtz Ulrik Buchholtz 2010-07-23T19:22:18Z 2010-07-23T19:22:18Z @Noldorin: When developing a proof system, you might have an intended model in mind, but you don't necessarily have to say anything about semantics. You might even want to allow for several intended models (e.g., a full set theoretical one and a computable one). For systems with a minimum of strength there will always be non-standard models (incompleteness). Henkin semantics is just a way to get completeness by allowing all possible models. Therefore, it is circular to have Henkin semantics in mind during the design of a system (&quot;I want just those models I'll end up with!&quot;). http://mathoverflow.net/questions/32923/how-do-proof-verifiers-work Comment by Ulrik Buchholtz Ulrik Buchholtz 2010-07-23T16:56:29Z 2010-07-23T16:56:29Z @Noldorin: I think you're right that those table rows are a bit misleading. Perhaps the meaning is that a logic is a &quot;higher-order type theory&quot; if there is a type for propositions, so that the logic embeds in the types. Otherwise, the logic is built on top of the type theory. But if so, then Agda and others should have been included in that category. A more interesting comparison would be according to the features of the type theory: predicative/impredicative, extensional?, polymorphic?, dependent?, and so on. http://mathoverflow.net/questions/32923/how-do-proof-verifiers-work Comment by Ulrik Buchholtz Ulrik Buchholtz 2010-07-22T17:52:19Z 2010-07-22T17:52:19Z @Noldorin: I don't know of short summary, but with a constructive system you can in principle extract witnesses to existential statements and computable functions for $\forall\exists$-statements and so on. However, constructive and classical logic can be interpreted in each other, so in that sense they're equivalent. And for instance both Coq and Isabelle/HOL allow program extraction from constructive proofs. http://mathoverflow.net/questions/32923/how-do-proof-verifiers-work Comment by Ulrik Buchholtz Ulrik Buchholtz 2010-07-22T15:24:35Z 2010-07-22T15:24:35Z @Noldorin: Concerning constructive/classical logic: both are used, with for example Coq being popular for constructive reasoning (though also supporting classical logic), while the various HOL systems are popular for classical reasoning. http://mathoverflow.net/questions/32923/how-do-proof-verifiers-work Comment by Ulrik Buchholtz Ulrik Buchholtz 2010-07-22T15:14:09Z 2010-07-22T15:14:09Z For an overview of the different provers, you might like Freek Wiedijk's &quot;Comparing mathematical provers&quot;, <a href="http://www.cs.ru.nl/~freek/comparison/diffs.pdf" rel="nofollow">cs.ru.nl/~freek/comparison/diffs.pdf</a> John Harrison's book, &quot;Handbook of Practical Logic and Automated Reasoning&quot;, contains the description of an interactive theorem prover in the LCF style. The code is available online: <a href="http://www.cl.cam.ac.uk/~jrh13/atp/index.html" rel="nofollow">cl.cam.ac.uk/~jrh13/atp/index.html</a>