bio | website | noldorin.com |
---|---|---|
location | London, United Kingdom | |
age | 23 | |
visits | member for | 4 years, 6 months |
seen | Apr 8 at 1:22 | |
stats | profile views | 215 |
entrepreneur; graduate in mathematics / theoretical computer science / theoretical physics; polymath-in-training
based in London, United Kingdom
Sep 30 |
awarded | Caucus |
Jul 8 |
awarded | Famous Question |
Apr 28 |
awarded | Critic |
Feb 5 |
comment |
How do proof verifiers work?
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. |
May 15 |
awarded | Popular Question |
Apr 30 |
comment |
Difference between a 'calculus' and an 'algebra'
@Todd: Absolutely. And thank you for reminding me, I believe I was thinking of Tarski and Givant's formulation. |
Feb 10 |
awarded | Notable Question |
Jan 31 |
comment |
How do proof verifiers work?
@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 "strength"? I wonder if there exists an "ideal" proof theory under which all mathematics can be proven, minus of course the limitations of Godel's Incompleteness Theorems. |
Jan 31 |
comment |
Propositional Logic, First-Order Logic, and Higher-Order Logics
@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. |
Jan 28 |
awarded | Nice Question |
Jan 9 |
awarded | Nice Question |
Oct 23 |
comment |
Newton equations, second order equation and (im)possible motions
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)! |
Oct 18 |
awarded | Yearling |
Oct 12 |
comment |
Quantum Error Correction
Since there is no physics/quantum information SE site, you may want to try cstheory.stackexchange.com. This question concerns a lot more than just mathematics. |
Oct 9 |
comment |
How do I explain the number e to a ten year old?
J. M.: I'm pretty sure it's a hypothetical question! |
Sep 14 |
comment |
Difference between a 'calculus' and an 'algebra'
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. |
Aug 26 |
answered | Difference between a 'calculus' and an 'algebra' |
Aug 13 |
awarded | Popular Question |
Aug 11 |
comment |
Semantics of Higher-Order Logics
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. |
Aug 5 |
comment |
Semantics of Higher-Order Logics
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. |