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

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.
    • CommentAuthorUrs
    • CommentTimeFeb 28th 2015
    • (edited Feb 28th 2015)

    Some years back, I seem to remember, a younger version of myself asked here some naive questions (or maybe rather: voiced some general confusion) about apparent circularity in the foundations of mathematics. In reaction to that (if I remember well, maybe at least in parts in reaction to that) Todd kindly wrote a text Notes on predicate logic with a section Are logical foundations circular?.

    I was very grateful back then for that, and still am.

    For some reasons I am thinking about this again every now and then, possibly in vain, but it so happens. I have one concrete question:

    Todd mentions the “paradox of the dictionary”. Is this some established term in the context of discussion not of dictionaries, but of the foundations of mathematics? Generally, what would be other respectable sources in print, if any, which would consider the points regarding circularity, or not, that Todd considers in that section? Are the any? I am not doubting anything that Todd is saying, not at all, nor do I think there is much to be added to what he writes, I am just trying to get a feeling for the “state of the literature” on the issue.

    Then I have a comment: that text by Todd eventually refers to physical reality as the justification of the standard foundations of mathematics in first-order logic:

    Our own view is that logical foundations avoids this paradox ultimately by being relentlessly concrete. We may put it this way: logic at the primary level consists of instructions for dealing with formal linguistic items, but the concrete actions for executing those instructions (electrons moving through logic gates, a person unconsciously making an inference in response to a situation) are not themselves linguistic items, not of the language. They are nevertheless as precise and exact as one could wish.

    I have no trouble with that, but I think it is a remarkable statement and am wondering if this is something that not only that younger version of myself would find remarkable to hear, but many other people who consider themselves mathematicians or physicists.

    What in closing I will now try to voice is something in between a comment and a question, probably just again a confusion of mine. Namely, wouldn’t it be hard to disagree with the statement that while that comment about “electrons moving though logic gates” does resolve the circularity issue on some level, that it doesn’t resolve it on a deeper level, a level which certainly one need not care about, but which it seems respectable to do care about?

    For instance suppose you were ambitious and wanted to not just find a physical “theory of everything” in the sense of the usual jargon of the field (for whatever that’s worth), but afterwards also wanted to give it a fully formal mathematical formulation. Irrespective of the fact that this ambition is by all accounts way out of reach and may always be, it is on the other hand one of the most obvious things that one should eventually want to do in the field of theoretical physics. So suppose you were after this. Then by the above argument on the circularity of mathematical foundations, you’d be left with the fact that you are trying to formalize a theory which, among many other things, is to describe from first principles how exactly electrons pass through logic gates (to pick that catch-phrase from any number of more satisfactory analogous statements we could add here), while at the same time the mathematical foundation which you use to perform that formalization is meant to justify itself (only!?) by the way how electrons pass through logic gates.

    See what I mean? I understand that one may well not care about this issue, since somehow “for all practical purposes” it is maybe not actually there. But it also seems clear to me that in some very obvious sense of intellectual pursuit (which one may or may not care about, but which seems to be respectable), this is an issue that is not to be dismissed lightly.

    What I am getting at, as you may or may not be guessing by now, is something like this: isn’t it true that if we don’t content ourselves with a “for all practical purposes” but go a bit deeper, that then the foundations are circular? That there is no way around this? That therefore one may want to say: even if this circularity seems nonsensical and even if we are inclined to bend over backwards to evade it, given that from a more, how should I say, ambitious perspective it is inevitable, then maybe instead of trying to evade it, the only reasonable move would be to try to make sense of it? Somehow.

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 28th 2015

    I sometimes struggle with this, too. And don’t expect me to say anything “profound”. But ultimately the type of circularity I was trying to suggest is not really an issue is one where we somehow feel a need for a completed infinity in order to speak of logical proof, or how to recognize a proof as valid.

    When we envisage the “space” of all proofs and try to talk about it, that refers to an infinite construct, part of a background meta-theory, sitting on the back of another turtle. To the extent that we want to go further and consider the space of all meta-theoretical proofs, etc., I see no way of breaking out of the evident circularity.

    This reminds me of an interesting interchange between Mike Shulman and “Walt” (Walt Pohl, aka “arsmath”) at the nn-Category Café. It’s hard to find exactly the right point of entry for what I’m referring to, but maybe start here where Mike quotes Walt and it goes from there. At some point down the thread, Mike says, “Agreed. For particular theorems with particular explicit proofs, we can give an absolute meaning to being a theorem of a formal system” followed a little later by “What I claim is that there’s no way to talk about the collection of all theorems in some formal system without a metatheory. There’s no metatheory-independent ’set of all explicit natural numbers’ “. So I think all I was trying to suggest was the first of those sentences, that the validity of any individual proof can be given an absolute meaning without getting us into an infinite regress. Coq can certify a proof without there being an infinite meta-theory residing somewhere in the software or hardware; it just deals with a tiny finite fragment at a time. And that’s all we ever ask or could ask, that humans and computers agree on each individual proof being valid or a construction being well-formed.

    (By the way, those Notes on Predicate Logic might be expanded soon. I’ve been thinking a bit about elementary model theory recently, especially the compactness theorem and the Löwenheim-Skolem theorems, and it’s given me glimmerings of how I’d like to proceed with the story I wanted to tell.)

    • CommentRowNumber3.
    • CommentAuthorNikolajK
    • CommentTimeFeb 28th 2015
    • (edited Feb 28th 2015)

    The book Moby-Dick has a message. But after all life in the world were forever gone (if nobody can receive anything anymore), if the world still exists, the physical book that remains on the shelf still has words printed on it but isn’t something which contains a message.

    The core of my perspective on this is that the physical theory is something which is only there when humans are around that interact with it. A theory of physics is something we use. Amongst other things, it generates the language for things (like “electron”) and plants an idea of the behavior of those things in our head. The conceptualization of those things, like a circuit, borrows from the theory, but our brain does not work with the infinity-topos formalization you write the theory down. And whatever the defined and described physical things are, they were there and did what they do from the day the baby physicists way born. A “justification” is something on the “message” level and it must use “message” language to count as “justification”.

    When discussing logical/type theoretical deduction rules, the reference to the electrons moving acts like the pointing out of at least one other concepts which behaves in a way that parallels the actions on your paper. I wouldn’t say that’s a necessary thing to do in the first place. But in any case, for describing either of those, you don’t need the formalized theory of everything, as engineering terms seemingly suffice. And indeed, that’s what the nLab page only does. It borrows the terms “electrons”, draws the parallel, and hopes the reader (maybe himself) accepts this as a “justification”. We get in Wittenstein territory here.

    Let me ask you this: Does your physical theory of “everything” permit a formalization of the notion of a “justification”? (Note that if the answer is yes, the justification of logic is something which sits inside the theory and is hence just a self-consistency requirement once you got the theory.)

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeMar 1st 2015

    One perspective on this issue is that it’s mistaken to expect foundations to be “prior to” mathematics. Foundations are about studying mathematics mathematically; but they are themselves mathematics, plus we already need to have mathematics before we can study it. I’m not sure whether or not that’s my view, but it’s one view.

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 1st 2015

    As well as the physical underpinning of the reasoning, there’s even the physicality of the writing. Talking of circularity, I remember being struck by Louis Kauffman’s thought:

    Notationally the Jordan curve theorem is a fact about the plane upon which we write. It is the fundamental underlying fact that makes the diagrammatics of knots and links correspond to their mathematics. This is a remarkable situation - a fundamental theorem of mathematics is the underpinning of a notation for that same mathematics.