I recall that GEB gives an informal proof that systems that can formalize arithmetic are incomplete. But a standard textbook would certainly give a terser and more rigorous proof.
I think the statement may be corrected by replacing the “and” with “or”. Does it work to say that “Every sufficiently powerful formal system is incomplete or has a contradiction.”?
I wonder if these findings may partially explain the often derided theory that childhood vaccines can cause autism. The article directly mentions that an autism misdiagnosis can result from psychiatric symptoms resulting from an autoimmune response after certain infections.
I think usually the sovereignty must be handed down through an unbroken chain. This is how monarchy and dynasty worked. Once the chain was broken, then you have a new sovereign entity. I think this is how citizenship works in most countries.
In modernity we have different notions of justice where it becomes meaningful to claim that a chain of sovereignty was unjustly broken from one group of people and handed to another. If this were the case, you might have claims in Europe in some people’s eyes.
Whether this is the actual case or not, parental lineage is a major force that justifies claims of sovereignty in the American legal system and elsewhere.
Yes there are other routes to sovereignty over US soil other than familial inheritance, including being born on the land or becoming a naturalized citizen.
Still, the predominant route is via a claim to the correct ancestral lineage. Here I mean that one’s ancestors form an unbroken chain of people who also had sovereignty over the land. This route is also the predominant one taken by citizens of most other countries.
Isn't this how most nations work? If one's parents are American, they inherit all the rights due to Americans, including the ability to run for political office. This gives the descendants of Americans sovereignty over a chunk of land in North America known as the United States.
With respect to your first point, we should all make sure the products we buy are ethically produced. But this has no bearing on the question of whether it's rational to assign higher prices to naturally produced diamonds. There are many other things that are unethically produced, that people pay high prices for, and where those prices are viewed as sensible (eg. oil, smart phones, opioids).
As for your second point, there is a large marketing component for most things that are bought and sold, including art and memorabilia. You say that for diamonds, the value is fabricated. But I believe the fabrication of value creates real consequences. It's not trivial to coordinate the action and common knowledge of an entire population. If you do it right, it creates a new Nash equilibrium. If someone then gifts you a "natural" diamond, it is irrational to sell it at the "synthetic" price. Your buyer might even be a diamond dealer who also believes the natural-synthetic thing is a marketing scam. The whole population can even know the whole situation is fabricated. But unless they can all coordinate and change the market price in unison, it doesn't make sense to deviate from the equilibrium.
I take it to mean that there is an effective generally accepted solution or methodology for problems in the field. Bridge building has been largely solved by methods of mathematical and computational structural analysis, manufacturing, and government regulation. We know how to build a bridge. Before the solution was known, designers would just go by intuition and we wouldn’t have any actual assurance that the bridge would hold. We can probably never solve larger domains like physics, programming, or architecture.
I just looked up this paper from "other places". The author evolves an FPGA to discriminate between 1Khz and 10Khz square waves. I don't know that much about FPGAs, but it seems like such a task should not be possible without an external clock signal, since otherwise the output wave-form the 10Khz signal should simply be the 1Khz signal sped up 10x. Somehow, evolution learned to make use of electrical and thermal effects to accomplish the task. There were even units that were electrically separated from the rest of the device which were crucial to its functioning. Pretty amazing.
This is a great point. In a computer proof system, you produce judgements like "the term x has type is T", where the type "T" encodes the statement of a theorem and "x" is the proof. We must be certain that whenever the type checker verifies that "x has type T", it means that the theorem "T" is actually true. Such a meta-proof must be done on pen and paper, before any code is written at all. Any bug in this meta-proof would destroy our ability to rely on the computer proof system.
Agreed. I think the interviewee is a little pessimistic when he says "I’m just not sure it’s any more secure than most things done by humans." about computer assistance. If the ABC conjecture were to be proven in Lean, I'm pretty sure it would be accepted as true by an overwhelming majority of the mathematical community.
I think the quote is about the fallibility of the humans who convert theorems into statements of type theory. You could end up with a valid theorem, but not the theorem you meant to prove. This would be a bug in the statement of the theorem, not the proof.
For example, you might want to prove that a certain sorting algorithm is correct. You formalize the specification as "for every two integers i, j, output[i] <= output[j]" and prove that outputs of the algorithm satisfy this spec. However, this is not a correct characterization of sorting, since the algorithm might return the empty list.
Yet still professional mathematicians have an underlying notion of truth outside of any axiom systems. I forgot who said it but if we were to find a contradiction using Peano’s axioms, we would say that the axioms were wrong, rather than arithmetic itself.
Even your comment references “perfect rules which totally correspond to reality” which seems to be another way to say “absolute truth”.
I realize that calling any type of mansion affordable seems out of touch. I was commenting on the relative expense of some of these design components. The prefix “Mc” evokes McDonald’s. The post pokes fun at a statue of a maid, because the owners could not afford to hire true maids. From the site, I assume that a McMansion is like a mansion, but made with cheaper components and without the taste and class that comes with an elite upbringing.
I’m not sure there is anything objectively bad about these designs. Does it affect the utility of the house? Or is there some inherent ugliness that comes with affordable and popular things?
The author’s second example is extremely unconvincing for me. Why would I want to be forced to use a SELECT expression to calculate a mean? Relational algebra is a great abstraction. SQL, however, seems to be poorly thought out and ad hoc. It’s just the first implementation of a relational algebra language that worked. But why should we be stuck with it forever?
I thought ray tracing was very branchy type code which is not suited for GPU. If I have a bundle of rays strike an object, they could all scatter different directions and end up following very different paths in the scene. Is it hard to make all rays execute the same code at the same time?
By assign(a,b) I meant to denote the copying of the matrix b into the matrix a. The ability to use arithmetic symbols `+` and `-` as function identifiers definitely aids in readability but I don't think this is possible in Zig.
I am not familiar with Emmy but I'm guessing that the usual work flow will involve an interactive shell with many calls to `render` to display expressions in infix notation so that you can better check if the expression you typed is actually what you meant to type.
The infix notation, although arbitrary and not as logically simple as other notations, is almost universal in the math-speaking world. Most mathematicians and engineers have have years of experience staring at infix expressions on blackboards, and disseminate new knowledge using this notation, and do new calculations in this notation.
In reading your reply, I think that maybe some tooling that could auto-insert corresponding infix-like comments above an AST-like syntax could be a solution for writing such code in Zig.
In robotics, numerical linear algebra expressions comprise a large part of the code base. If not by line count, then definitely by the amount of time spent writing, reading, and debugging such code. This makes Zig unusable for these applications, at least not without additional tooling. You can get a feel for how unergonomic this is by avoiding the use of all arithmetic operators in your code and instead forcing yourself to use user defined plus(a,b), minus(a,b), assign(a,b), etc, or programming directly with the C blas api.
I used to use ROS 1 for work. It is incredibly over-engineered. Somewhere in the code base there is a three level hierarchy wrapping a shared pointer to double. The actual address is configured using an xml file. The purpose? To “abstract” the commanded torque ultimately sent to a motor.
I had a bunch of matrices dumped by a Matlab script that I needed to paste into a Python script. I asked ChatGTP to write a sed script to reformat the matrices into numpy arrays.
I was quite taken by these ideas but now I’ve come to a more balanced viewpoint. Just look around and see how much of the modern world is built using interpretable physical and mathematical models. No one would suggest that we build skyscrapers by training a neural net to empirically predict the probability of collapse. But this is hindsight bias, because we already solved skyscrapers through centuries of accumulated foundational knowledge. Looking to the future, it’s unclear what class of problems are tractable engineering challenges and which ones need the hammer of deep learning — including AGI.
Another commenter has mentioned nonstandard analysis but I find that most people (commonly physicists, engineers) who are manipulating dy and dx are not actually using the framework of nonstandard analysis.
What usually is going on is you mentally replace dx and dy with Delta x and Delta y = y(x + Delta x) - y(x), where Delta x is some small nonzero quantity. After doing your manipulations, you take the limit as Delta x -> 0. Then you have rigorous statements like Delta y / Delta x -> f'(x) (this is the definition of derivative), and Delta x/Delta x = 1, and (Delta x)^2/Delta x -> 0 (ability to neglect second order terms), etc.
You do this type of thing so many times and it becomes rote and annoying to explicitly mention the limits and the reader is trusted to formalize it themselves as an exercise.
The stuff that you are "allowed" to do is taught in a first course in real analysis. After taking such a course, you will be able to justify for yourself which manipulations are valid.