Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 comma 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 finite 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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTobyBartels
    • CommentTimeSep 10th 2012

    Since the Idea section was so big, I put most of it in a Summary section instead. I also a few remarks about it along the way.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeSep 28th 2012

    I have added a lot to the “Summary” section at natural deduction, based on what I have learned recently from Dan Licata and other type theorists. I would kind of like to remove entirely the section “Examples of type formation/introduction/elemination/computation rules”, since I felt it necessary to incorporate a couple of examples already into the “Summary” description, and then having a long list of “examples” seems like unnecessary duplication of the pages product type, sum type, etc. But I thought I should ask first before deleting; thoughts?

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeSep 28th 2012
    • (edited Sep 28th 2012)

    Very nice. And, sure, I have removed the previous Examples-section.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeSep 28th 2012
    • (edited Sep 28th 2012)

    Can I just double-check if I am now following the ambient dependency tree; is the following a correct organization of the notions it mentions:

    1. At the beginning there is a logical framework.

    2. Given that, we may formulate a deductive system.

    ?

    I have put it this way now into deduction and induction - contents. But let me know what you think.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeSep 28th 2012

    Yes, I think that’s basically right, except that a deductive system doesn’t have to be formulated in the particular kind of metatheory that goes by the name ’logical framework’.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeSep 28th 2012
    • (edited Sep 28th 2012)

    Okay, thanks. This last point I would just like to understand a little bit better.

    What exactly is it that a “logical framework” achieves for a deductive system. It makes it “more formal”, is that what it is?

    I am hoping that it is possible to root these notions here in “reality” by saying what each of these means in terms of somebody setting up an actual computer implementation of a type theory.

    Can we maybe play through that? I think that would be worthwhile. I would like to have a dictionary where I hand you in the above order 1. a logical framework, 2. a deductive system, 3. a natural deduction systems, 4. an actual type theory, and you tell me what each of these steps means in terms of setting up a proof-checker for that type theory.

    So there will be a piece of software, and we build it in stages. At the lowest stage it has a parser that reads in strings of the form

    antecedent \vdash succedent

    and takes them apart into pairs of strings (antecedent,succedent)(antecedent, succedent). Then in the next stage we gradually add to the software a rule for how to turn such strings into other strings (or maybe rather a rule to check if a list of such strings is a valid list of symbol manipulations).

    In this kind of way of speaking, can one say what the piece of the software does that implements the “logical framework”, what the piece does that implements the “deductive system” and then the “natural deduction” specifically.

    Do you see what I am after here?

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeSep 28th 2012

    This is a great idea. I am planning to write more at logical framework which will partly answer this question, but first I need to finish asking my local type theorists about what “logical framework” means. (-:

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeOct 1st 2012

    Speaking of logical frameworks, is there a reason why Elf and Edinburgh Logical Framework are separate pages?

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeOct 1st 2012
    • (edited Oct 1st 2012)

    is there a reason

    Not a good one, at least.

    I have merged the pages.

    • CommentRowNumber10.
    • CommentAuthorThomas Holder
    • CommentTimeJan 28th 2015

    I’ve expanded the references at natural deduction mostly with some historical comments and done some cosmetics in the idea section.

  1. Thanks for adding these interesting historical references. I think it’s a bit strange, though, to say that Gentzen developed natural deduction, cut-elimination, and so on “for ‘h-propositions’ in propositional logic and untyped predicate logic”. Besides being anachronistic, one could argue that these are the very concepts that made it possible to have a non-trivial theory of identity of proofs (which is why Gentzen is credited with initiating the study of “structural” proof theory). How about replacing that phrase simply by “for propositional logic and untyped predicate logic”?

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJan 28th 2015
    • (edited Jan 28th 2015)
    I have turned into hyperlinks a few more of the keywords that were added.
    • CommentRowNumber13.
    • CommentAuthorThomas Holder
    • CommentTimeJan 28th 2015

    @NoamZeilberger: I agree. the quotes were actually added by me to a previous text which I bound with some additions to what in my view is an awkward phrase in need of improvement.

  2. Ah, I see. I went ahead and replaced the phrase simply by “for predicate logic” (since he didn’t give a separate system for propositional logic but just treated it as a fragment, and because at the time AFAIK there was no version of predicate logic to be “untyped” relative to), and slightly tweaked the ordering. Anyways, this was just a minor point – thanks to the people who have contributed to this article, which is pretty good overall.

    • CommentRowNumber15.
    • CommentAuthorThomas Holder
    • CommentTimeJan 29th 2015
    • (edited Jan 29th 2015)
    When I said 'awkward' I meant very much my own 'improvements' as well, as they made the sentence excessively long and praised cut-elimination before the proof system. Thanks for fixing this!

    Concerning the propositional logic, it might be worth mentioning that he gives (presumably the first) decision procedure for intuitionistic propositional logic.