practal

11 ms·

151.
by practal 3y ago
Oh, it does give you special insight, but it doesn't make you infallible. It is easier to reach for something if you feel that it must be out there, and you just haven't got it right yet. That's how most mathematicians feel.
152.
by practal 3y ago
> I'm a little skeptical of the "something between 1st order logic and 2nd order logic" claim And rightfully so. I've discovered Abstraction Logic (AL) over the course of the last two years, and in the beginning I did
153.
by practal 3y ago
> That the solution could lie in something as simple as Zermelo’s separation axiom and the conception of the cumulative hierarchy of sets was seemingly not anticipated. It was a miracle. If you are a Platonist (I am), then it is not real
154.
by practal 3y ago
Interesting. This work was done at ITP (which is short for interactive theorem proving, but not here). The ITP has been founded by Red Burns, who has written a foreword (really a foreword interview) for John Maeda's "Creative Code
155.
by practal 3y ago
I love that quote too, used it for the last chapter of my PhD thesis 15 years ago.
156.
by practal 3y ago
Sorry, you are wrong here. We may never solve BB(6) exactly because of undecidability. We don't have an algorithm for computing BB(6). If we had one, BB(6) would be computable (= decidable). Of course, as soon as we know BB(6) = n, f
157.
by practal 3y ago
Yes, you are right, just saw this yesterday, too.
158.
by practal 3y ago
Great talk, thanks for sharing! I am looking for a way to finance building and maintaining the thing I want to build, and this talk was a nice reminder that donations actually CAN work. Otherwise, VCs are interested in an "Exit" e
159.
by practal 3y ago
Nice paper! The number is BB(748), by the way. Thinking in terms of concrete machines is great. The work on Abstraction Logic has made me a Platonist in a Goedel way as well. I insist that the mathematical universe is real: there are mathem
160.
by practal 3y ago
I think the important idea from math for programming, and pretty much everything else, is that of a function that operates on functions. You can build on that important idea in different general ways, for example category theory, or type th
161.
by practal 3y ago
I hear you. I picked up Isabelle relatively easily, but I had the good fortune to be at one of the places where Isabelle is developed, and actually became later part of that group for my PhD. Still, even for me, dealing with various issues
162.
by practal 3y ago
I think if the editor is a core piece of your app, you cannot really outsource it. After looking at lexical, ProseMirror, CodeMirror, etc., I am currently rolling my own. Your comments from last year ( https://news.ycombinator.com
163.
by practal 3y ago
Not sure where you are going with this. What is causality? Is there a non-mathematical way of making it precise? And if I have found some way to make it precise, does it matter if I write it down here in this HN comment, or on a piece of pa
164.
by practal 3y ago
You can say that a certain axiom system models a certain part of reality in an ideal way. But whatever is ideal, is also real, because otherwise there is nothing that could model anything. So your intersection of reality and ideality is jus
165.
by practal 3y ago
> math describes (fragments) of reality; This is only possible if math itself is real. Note that I am not saying that a particular axiom system like Euclidean geometry has some sort of "real physical manifestation". No, what I
166.
by practal 3y ago
I agree with you here, at least in the sense that the system is definitely not physical. You didn't answer my question, though. Is it real?
167.
by practal 3y ago
It does not really matter if the system is sound or not, right? Although of course a sound one is far more interesting. Anyway, any way of justifying this is mathematical (and so would be the definition of soundness, if it was relevant here
168.
by practal 3y ago
So would you say that your system of symbols and rules is real? Could it be that we both use the same system of symbols and rules, with the same assumptions, but derive different conclusions? If not, why not?
169.
by practal 3y ago
> I think mathematics is a human construction and doesn't have a real substance. Instead, mathematics is a system of assumptions and generative rules, and more generally a discipline around creating and operating such systems. But
170.
by practal 3y ago
Yes.
171.
by practal 3y ago
Fair enough. Although to encode a proposition as a type, only to then view it as a proposition again, would be two wrappers too many for my taste. I prefer to keep the notions of truth and types apart. In practice, this makes the logic both
172.
by practal 3y ago
Thanks for pointing out the Conal Elliott talk. Just watched it, very nice talk. I found myself nodding to pretty much everything he said, except of his fondness for dependent types. Each time he says "dependent types", I just rep
173.
by practal 3y ago
When working on an experimental VSCode plugin recently, I noticed that bracket colorization was at odds with some basic functionality. For example, in comments, I didn't want colorized brackets, I just wanted everything in the same col
174.
by practal 3y ago
Here is another example of an LR parser that reads the grammar on the fly and immediately parses the input (which is, among other things, also defining its own grammar) with it: https://marketplace.visualstudio.com/items?ite
175.
by practal 4y ago
I just skimmed the paper you linked (I read it before, but forgot its details). So Metamath Zero is still a logical framework, like Metamath, but has a few more tools to ensure soundness of the logics you formulate in it. Nevertheless, just
176.
by practal 4y ago
Metamath itself is a logical framework, and doesn't really have a semantics. You can encode rules of a logic with it, and then you have to convince yourself that this encoding is what you want. I believe most of Metamath's content
177.
by practal 4y ago
If your issue is that applied math doesn't need infinite sets, then you are just plain wrong. Applied math uses infinite sets, and real numbers, and measure theory, etc. all the time. Granted, what set theorists are interested in most
178.
by practal 4y ago
If we are talking about "most" mathematicians, then you should also admit that most mathematicians are not a member of the finitist church, and that most mathematicians appreciate the distinction between countable and uncountable.
179.
by practal 4y ago
Church tried to reduce logic to his invention, the untyped lambda calculus, but failed in a first attempt [1]. He then proceeded later on to invent the simple theory of types, [2], and type theory is pretty much a descendant of that. My arg
180.
by practal 4y ago
I like the way you are thinking about this. And yes, formal math is the future! If you want to check out how to deal with quantification properly, or more generally with operators, without a need to explicitly introduce types, check out ht

More ›