User ulrik buchholtz - MathOverflow

Answer by Ulrik Buchholtz for Arithmetic strength of Peano + the Howard ordinal

2012-12-08T18:55:17Z

The answer is yes, using the ordinal analysis of KP. See Pohlers' A Short Course in Ordinal Analysis for why the usual ordinal analyses are profound, 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 proper initial segments of the primitive recursive well-ordering $\prec$ that measures the proof-theoretic ordinal of the theory.

Answer by Ulrik Buchholtz for Why no morphisms from the contradictory proposition to the inconsistent context?

2012-02-14T00:36:08Z

I'm not sure what you mean by the individual propositional objects having models or not.

In any case, as you said, as morphism in $\mathbb P$ simply is 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.

Answer by Ulrik Buchholtz for Reduction rules for inductive types

2012-01-02T16:54:30Z

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:

Normalization by evaluation for typed lambda calculus with coproducts, by T. Altenkirch, P. Dybjer, M. Hofmann, and P. Scott

For a strongly normalizing reduction relation for commutative conversions, try:

Short Proofs of Normalization for the simply-typed lambda-calculus, permutative conversions and Gödel's T (1999) by Felix Joachimski , Ralph Matthes

(EDIT: Three more references. I haven't looked at these, but they sound helpful:)

Exceptional NbE for Sums by Freiric Barral

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.

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.

Answer by Ulrik Buchholtz for categorifying induction in homotopy type theory

2011-06-09T17:33:14Z

The first reason you give is sufficient to answer your question: any interpretation of nat (and any other type with decidable equality) must have contractible components. Let me try to unpack the proof:

The proof of isasetifdeceq goes as follows: Fixing $x:X$, we must show that $\text{Paths}(x,x)$ is contractible. We know that $\Sigma_{x':X}\text{Paths}(x,x')$ is contractible, so we just need the natural map $f:\text{Paths}(x,x)\to\Sigma_{x':X}\text{Paths}(x,x')$ to be a weak equivalence. This follows from the hypothesis using the theorem onefiber, 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.

Regarding (2). I think there's some confusion here: Let me try to unpack nat_rect in a more direct way: For any fibration $\Sigma_{\text{nat}} P\to\text{nat}$ over nat, given a point in $P_0$ and a section of $\Pi_{n:\text{nat}}\text{Map}(P_n,P_{n+1})\to\text{nat}$ , you get a section of $P$. That is the interpretation of primitive recursion/induction.

Answer by Ulrik Buchholtz for Mechanically instantiating abstract constructions

2010-04-10T06:55:15Z

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)$.

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$).

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.

Answer by Ulrik Buchholtz for Ackermann-related function

2010-03-29T15:38:28Z

Googling for "graph of the Ackermann function" gives this note by George Tourlakis, which proves both that the Ackermann function is not primitive recursive, and, at the end, that the graph is.

Answer by Ulrik Buchholtz for Reference request for type theory

2010-03-23T15:16:59Z

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:

Russell, Bertrand: Mathematical Logic as Based on the Theory of Types. Amer. J. Math. 30 (1908), no. 3, 222--262.

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:

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.

For the relation between set theory, type theory, and category theory, you might want to have a look at this preprint by Steve Awodey.

There's also an n-lab page, and the type theory page at Stanford Encyclopedia of Philosophy has a reference section.

Answer by Ulrik Buchholtz for Is there any proof assistant based on first-order logic?

2010-02-18T16:37:15Z

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 available online.

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.

Answer by Ulrik Buchholtz for Is any true sentence in the second-order Peano Axioms provable

2010-02-07T23:23:35Z

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.

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).

Answer by Ulrik Buchholtz for Theorems for nothing (and the proofs for free)

2009-11-22T05:02:41Z

Although not exactly what you're after, the question reminds me of Reynolds' parametricity theorem, or as Philip Wadler puts it: Theorems for Free!

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.

Comment by Ulrik Buchholtz

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.)

Comment by Ulrik Buchholtz

2012-09-22T16:52:45Z

Check out the topos approaches to quantum mechanics, as initiated by Isham/Butterfield and Döring/Isham (the contravariant approach, see review by Flori: arxiv.org/abs/1106.5660). There's also a covariant approach, developed by Heunen, Landsman and Spitters (see Wolters' comparison of the approaches: arxiv.org/abs/1010.2031). That should get you started.

Comment by Ulrik Buchholtz

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.

Comment by Ulrik Buchholtz

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.

Comment by Ulrik Buchholtz

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.

Comment by Ulrik Buchholtz

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 :-)

Comment by Ulrik Buchholtz

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 Type by a univalent universe, $U$, with corresponding fibration $\Sigma_{A:U} T(A)\to U$ (universe a la Tarski with decoding $T$). And then nat_rect is represented by a section of a certain fibration with base space $\text{Map}(\text{nat},U)$ . But it's frankly easier to understand in the type-theoretic notation, remembering to understand constructs constructively/continuously.

Comment by Ulrik Buchholtz

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, [homepages.inf.ed.ac.uk/jrl/Research/notions1.pdf] ?

Comment by Ulrik Buchholtz

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.

Comment by Ulrik Buchholtz

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 ("I want just those models I'll end up with!").

Comment by Ulrik Buchholtz

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 "higher-order type theory" 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.

Comment by Ulrik Buchholtz

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.

Comment by Ulrik Buchholtz

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.

Comment by Ulrik Buchholtz

2010-07-22T15:14:09Z

For an overview of the different provers, you might like Freek Wiedijk's "Comparing mathematical provers", cs.ru.nl/~freek/comparison/diffs.pdf John Harrison's book, "Handbook of Practical Logic and Automated Reasoning", contains the description of an interactive theorem prover in the LCF style. The code is available online: cl.cam.ac.uk/~jrh13/atp/index.html