most recent 30 from http://mathoverflow.net 2013-06-19T05:51:21Z http://mathoverflow.net/feeds/user/602 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/32923/how-do-proof-verifiers-work Noldorin 2010-07-22T09:26:07Z 2013-01-11T22:30:31Z

<p>I'm currently trying to understand the concepts and theory behind some of the common proof verifiers out there, but am not quite sure on the exact nature and construction of the sort of systems/proof calculi they use. Are they essentially based on higher-order logics that use Henkin semantics, or is there something more to it? As I understand, extending Henkin semantics to higher-order logic does not render the formal system any less sound, though I am not too clear on that.</p> <p>Though I'm mainly looking for a general answer with useful examples, here are a few specific questions:</p> <ul> <li>What exactly is the role of type theory in creating higher-order logics? Same goes with category theory/model theory, which I believe is an alternative.</li> <li>Is extending a) natural deduction, b) sequent calculus, or c) some other formal system the best way to go for creating higher order logics?</li> <li>Where does typed lambda calculus come into proof verification?</li> <li>Are there any other approaches than higher order logic to proof verification?</li> <li>What are the limitations/shortcomings of existing proof verification systems (see below)?</li> </ul> <p>The Wikipedia pages on proof verification programs such as <a href="http://en.wikipedia.org/wiki/HOL_Light" rel="nofollow">HOL Light</a> <a href="http://en.wikipedia.org/wiki/Calculus_of_constructions" rel="nofollow">Coq</a>, and <a href="http://us.metamath.org/" rel="nofollow">Metamath</a> give some idea, but these pages contain limited/unclear information, and there are rather few specific high-level resources elsewhere. There are so many variations on formal logics/systems used in proof theory that I'm not sure quite what the base ideas of these systems are - what is required or optimal and what is open to experimentation.</p> <p>Perhaps a good way of answering this, certainly one I would appreciate, would be a brief guide (albeit with some technical detail/specifics) on how one might go about generating a complete proof calculus (proof verification system) from scratch? Any other information in the form of explanations and examples would be great too, however.</p>

http://mathoverflow.net/questions/15951/propositional-logic-first-order-logic-and-higher-order-logics Noldorin 2010-02-21T01:01:37Z 2011-01-30T20:26:52Z

<p>I've been reading up a bit on the fundamentals of formal logic, and have accumulated a few questions along the way. I am pretty much a complete beginner to the field, so I would very much appreciate if anyone could clarify some of these points.</p> <ol> <li><p>A complete (and consitent) propositional logic can be defined in a number of ways, as I understand, which are all equivalent. I have heard it can be defined with one axiom and multiple rules of inferences or multiple axioms and a single rule of inference (e.g. Modus Ponens) - or somewhere inbetween. Are there any advantage/disvantages to either? Which is more conventional?</p></li> <li><p>Propositional (zeroth-order) logic is simply capable of making and verifying logical statements. First-order (and higher order) logics can represent proofs (or increasing hierarchial complexity) - true/false, and why?</p></li> <li><p>What exactly is the relationship between an nth-order logic and an (n+1)th-order logic, in general. An explanation mathematical notation would be desirable here, as long as it's not <em>too</em> advanced.</p></li> <li><p>Any formal logic above (or perhaps including?) first-order is sufficiently powerful to be rendered inconsistent or incomplete by Godel's Incompleteness Theorem - true/false? What are the advantages/disadvantages of using lower/higher-order formal logics? Is there a lower bound on the order of logic required to prove all known mathematics today, or would you in theory have to use an arbitrarily high-order logic?</p></li> <li><p>What is the role type theory plays in formal logic? Is it simply a way of describing nth-order logic in a consolidated theory (but orthogonal to formal logic itself), or is it some generalisation of formal logic that explains everything by itself?</p></li> </ol> <p>Hopefully I've phrased these questions in some vaguely meaningful/understandable way, but apologies if not! If anyone could provide me with some details on the various points without assuming too much prior knowledge of the fields, that would be great. (I am an undergraduate Physics student, with a background largely in mathematical methods and the fundamentals of mathematical analysis, if that helps.)</p>

http://mathoverflow.net/questions/36758/difference-between-a-calculus-and-an-algebra/36763#36763 Noldorin 2010-08-26T13:36:45Z 2010-08-26T13:36:45Z

<p><a href="http://www.merriam-webster.com/dictionary/calculus" rel="nofollow">Webster's</a> defines the primary definition of a <code>calculus</code> as follows:</p> <blockquote> <p>a method of computation or calculation in a special notation (as of logic or symbolic logic)</p> </blockquote> <p><a href="http://en.wiktionary.org/wiki/calculus" rel="nofollow">Wiktionary</a> gives a similar definition:</p> <blockquote> <p>Any formal system in which symbolic expressions are manipulated according to fixed rules.</p> </blockquote> <p>This agrees very much with the definitions I have encountered within mathematics. Free variables are not a requirement; indeed, even variables are not strictly required as objects within a calculus. (I am aware that there exist proof calculi that don't deal with the concept of variables; perhaps someone could give the name of such a one.)</p>

http://mathoverflow.net/questions/33369/semantics-of-higher-order-logics Noldorin 2010-07-26T08:16:24Z 2010-07-26T13:02:47Z

<p>I've been trying to get to grips with the various semantics commonly discussed in formal logic. Specifically, the nature and role of interpretations of first and higher-order logics is slightly unclear.</p> <p>Here are a few of the specific questions that have occurred to me:</p> <ul> <li>Propositional logic only has one sensible interpretation, that is truth assignment. Correct?</li> <li>Predicate (first-order) logic has an interpretation that may be defined by the domain of discourse. For a given formal system (proof calculus), there is typically a single valid interpretation?</li> <li>Higher order logic has <a href="http://en.wikipedia.org/wiki/Interpretation_%28logic%29#Higher-order_predicate_logics" rel="nofollow">full semantics and Henkin semantics</a>. Are there any other valid/commonly-used interpretations?</li> <li>What exactly is the relation between many-sorted first-order logic and Henkin semantics? Many-sorted logic looks rather akin to type theory, what differences should I be aware of?</li> <li>What are the (common) valid interpretations for higher-order logic that permit a valid proof theory. Henkin semantics is certainly one, while full semantics seems not to be - are there any others? Do Henkin semantics pose any problems (soundness/completeness)?</li> <li>Generally, what aspects of a given proof calculus are orthogonal? i.e. type of logic (classical, intuitionistic, constructive), deduction system (natural, sequent, Hilbert), semantics (full, Henkin) - these three aspects should fully specify a proof caculus if I'm not mistaken.</li> </ul> <p>Explanations and clarifications regarding these questions and thoughts would be much appreciated.</p>

http://mathoverflow.net/questions/33096/reading-materials-for-mathematical-logic/33100#33100 Noldorin 2010-07-23T15:41:18Z 2010-07-23T15:41:18Z

<p>If you're a beginner to mathematical logic, as you seem to imply, I would strongly recommend you start off by getting acquainted with classical propositional and predicate logic. There is a very useful <a href="http://www.cs.odu.edu/~toida/nerzic/content/web_course.html" rel="nofollow">online set of aritlces</a> on the subject, with interactive exercises. The sections relevant to mathematical logic would be:</p> <ul> <li>Logic</li> <li>Predicate Logic</li> <li>Set Theory</li> <li>Recursion</li> </ul>

http://mathoverflow.net/questions/26231/how-do-researchers-carry-out-computational-experiments-in-graph-theory/28414#28414 Noldorin 2010-06-16T17:16:50Z 2010-06-16T17:16:50Z

<p>I wouldn't claim that it's complete, as I've only used parts of it, but <a href="http://quickgraph.codeplex.com/" rel="nofollow"><strong>QuickGraph</strong></a> is an excellent package for .NET/C#. Besides a wide range of mathematical/algorithmic tools, it also has layout algorithms and imports/exporters for various formats.</p>

http://mathoverflow.net/questions/28104/sieve-of-eratosthenes-eventual-independence-from-initial-values/28111#28111 Noldorin 2010-06-14T11:25:14Z 2010-06-14T11:25:14Z

<p>By missing out only the first prime (2), your statement is indeed correct, but it is a special case. This is because all even numbers > 4 are guaranteed to have a divisor > 2 (i.e. in the set of tested numbers). Likewise, all odd numbers that are not primes will have a divisor within your set, since you start with the lowest odd number > 1.</p> <p>You claim:</p> <blockquote> <p>We generally start with 2, but we could chose any finite set of integers >= 2, and it would still end up generating the same primes, after a "recalibrating" phase</p> </blockquote> <p>Yet if you consider the simple case of starting with 4 and 5 now, you immediately run into problems. Given your method, 6 and 7 would be resolved as primes, since there are no divisors within your set!</p> <p>I believe I've understood your statement correctly, and hopefully this should clarify why it actually fails in general. Let me know if you think I've missed any point, however.</p>

http://mathoverflow.net/questions/32923/how-do-proof-verifiers-work/118679#118679 Noldorin 2013-02-05T03:04:03Z 2013-02-05T03:04:03Z

Indeed, I did mean that. Thanks for the info about Mizar in particular; that's intriguing. Alas, I wrote this post when my knowledge was comparatively quite immature. Proof verifiers which are concerned with the entirety of proofs known to modern mathematics (and thus higher than simple FOL) are of particular interest here.

http://mathoverflow.net/questions/36758/difference-between-a-calculus-and-an-algebra/36763#36763 Noldorin 2011-04-30T22:19:07Z 2011-04-30T22:19:07Z

@Todd: Absolutely. And thank you for reminding me, I believe I was thinking of Tarski and Givant's formulation.

http://mathoverflow.net/questions/32923/how-do-proof-verifiers-work/51492#51492 Noldorin 2011-01-31T17:23:48Z 2011-01-31T17:23:48Z

@Mark: You're certainly not too late; I'm always willing to learn more. :) Thanks for pointing out HOL Zero, it looks like a very useful way to learn things. It's also interesting to hear how there is no standard/accepted way of designing a proof theory (and thus verification system). I suppose none of them are truly capable of representing all mathematics, but they vary in their &quot;strength&quot;? I wonder if there exists an &quot;ideal&quot; proof theory under which all mathematics can be proven, minus of course the limitations of Godel's Incompleteness Theorems.

http://mathoverflow.net/questions/15951/propositional-logic-first-order-logic-and-higher-order-logics/53699#53699 Noldorin 2011-01-31T17:19:17Z 2011-01-31T17:19:17Z

@Mark: Thanks for your response. This is a great answer; it answers many of my questions without being needlessly technical. Just a couple of little clarifications really: a) how exactly do nth-order logic and higher-order logic differ? (I always understood them to be the same thing.) does higher-order logic imply the use of type theory/category theory? b) How does a formal logic with a type theory relate to its semantics? They seem closely related, but I can't say much more.

http://mathoverflow.net/questions/15951/propositional-logic-first-order-logic-and-higher-order-logics/53618#53618 Noldorin 2011-01-31T17:13:02Z 2011-01-31T17:13:02Z

These &quot;general semantics&quot; sound very much like &quot;Henkin semantics&quot;. Could you elaborate on the difference please? As far as I know, Henkin semantics have nice model-theoretic properties, but proof theorists care less about them. (Full semantics allow for a greater range of proofs?)

http://mathoverflow.net/questions/43292/newton-equations-second-order-equation-and-impossible-motions/43296#43296 Noldorin 2010-10-23T15:19:11Z 2010-10-23T15:19:11Z

Huh? The expression you give for quantum mechanical mass is rubbish (or I'm misunderstanding it very much). It simply equates to one (for a normalised wavefunction)!

http://mathoverflow.net/questions/41943/quantum-error-correction Noldorin 2010-10-12T20:36:08Z 2010-10-12T20:36:08Z

Since there is no physics/quantum information SE site, you <i>may</i> want to try <a href="http://cstheory.stackexchange.com/" rel="nofollow">cstheory.stackexchange.com</a>. This question concerns a lot more than just mathematics.

http://mathoverflow.net/questions/41577/how-do-i-explain-the-number-e-to-a-ten-year-old Noldorin 2010-10-09T20:08:15Z 2010-10-09T20:08:15Z

J. M.: I'm pretty sure it's a hypothetical question!

http://mathoverflow.net/questions/36758/difference-between-a-calculus-and-an-algebra/36805#36805 Noldorin 2010-09-14T21:37:22Z 2010-09-14T21:37:22Z

This answers the question and yet somehow misses the point entirely. The term 'calculus' was coined when Latin was the language of all academics in Europe and was used in a very general sense.

http://mathoverflow.net/questions/33369/semantics-of-higher-order-logics Noldorin 2010-08-11T09:53:15Z 2010-08-11T09:53:15Z

I will set a bounty on this question if there are no more updates in a few days... my reputation points are pretty meager at the moment, but we'll see.

http://mathoverflow.net/questions/33369/semantics-of-higher-order-logics Noldorin 2010-08-05T07:46:51Z 2010-08-05T07:46:51Z

I've had some good answers to some of the questions so far, but am still looking for further clarification on the others/additions to the existing answers. Thanks.

http://mathoverflow.net/questions/12684/switching-research-fields Noldorin 2010-08-04T14:05:45Z 2010-08-04T14:05:45Z

Doing quantum computation with &quot;very little background&quot; in physics is not likely to have much success, methinks.

http://mathoverflow.net/questions/34226/35-alcohol-mixed-with-60-alcohol Noldorin 2010-08-02T08:29:00Z 2010-08-02T08:29:00Z

<a href="http://math.stackexchange.com/" rel="nofollow">math.stackexchange.com</a>

http://mathoverflow.net/questions/34226/35-alcohol-mixed-with-60-alcohol Noldorin 2010-08-02T08:28:29Z 2010-08-02T08:28:29Z

Might be more appropiate for Math.SE. And yes, this question is complete.

http://mathoverflow.net/questions/33911/why-linear-algebra-is-funor/33914#33914 Noldorin 2010-07-30T15:00:52Z 2010-07-30T15:00:52Z

I'm not sure how much that article simplifies things, but last time I checked PageRank was based off algoriths involving (spectral) graph theory. This does of course relate to linear algebra, but is a bit more involved.