This seems a lot like the great game Euclidea https://www.euclidea.xyz/ where you have to build target constructions in minimal steps. I highly recommend it for getting your proof fix on-the-go in your pocket when you may not have your favorite proof environment to hand. Happy proving!
In Euclidea, you don’t manipulate the proofs but unless you’re just brute-forcing the levels you have constructed a proof mentally. Similarly, if Euclidea is implemented correctly, it generates the proof internally and checks it (even if these stages are fused). I wouldn’t rely on a game for building large developments and indeed Euclidea lacks abstraction and modularity as far as I can tell but the same developer may have a freeform environment with these features. Euclidea is an activity that mentally scratches the same itch as proving and in the same or very similar theory to TFA.
No. A construction says what to draw; a proof says why you’ve drawn the right thing.
Say we want to find the midpoint M of AB. Construction:
“Draw the circle centered at A through B and the circle centered at B through A. Let the two circles meet at C, D. Let AB meet CD at M.”
Proof:
“Since AC = AB = BC, C lies on the perpendicular bisector of AB. Since AD = AB = BD, D lies on it as well. Hence CD is the perpendicular bisector of AB. That means AM = BM, so M is the midpoint of AB.”
In your example, let’s strip each statement of phrasing (“meet at” means the same as “intersect”, etc). Also, each requires external knowledge of the relationship between radii and right angles. These bits can presumably be reduced to the same clauses as well.
So. Is more information encoded in the proof than the construction?
Is one of two equivalent prolog programs just written upside down, while the other says “hence” a non-zero number of times??
My example was so simple that it would be taken as obvious for an experienced reader. With any nontrivial problem, the proof would have much more information than the construction. For example, the proof might require the construction of auxiliary objects not used in the main construction.
This is beautifully showcased by a 3Blue1Brown video about an extremely clever proof of the equivalence of three constructions of an ellipse: https://www.youtube.com/watch?v=pQa_tWZmlGs.
I’m not Godel, but my ad absurdum was meant to be slightly weirder than the objection that seems to have come across. I’ll try this way.
I had a flash of a question about whether the external information required in either case offsets the information provided by the objects in the proof (implicitly, explicitly, or artificially). I was thinking in terms of both formal logic and entropy, loosely.
The (usefully simple) construction here implies use of a compass or string. In a sense, the physical constraints of a compass encode the same information as the lemmas and theorems do abstractly.
“Brah, you should google metaphysics and Bertrand Russell,” is probably about right But, I’m sure there is a term that I just don’t know or can’t recall.
Perhaps an answer to one version of your question is that the Tarski–Seidenberg theorem implies that Euclidean geometry is decidable: there exists an algorithm that finds a proof for any theorem of Euclidean geometry. This algorithm, however, is too slow to be practical in general (double exponential time). The proofs it finds definitely don’t correspond one-to-one with the constructions in any reasonable sense.
The compass encodes a constant-radius constraint, and the string encodes a sum-of-distances constraint, but it’s not at all obvious why these two constraints turn out to be the same under a uniform stretching. There are plenty of similar-looking hypotheses that turn out to be false (for example, a curve of constant offset to an ellipse looks a lot like an ellipse but isn’t one).
These are but necessary early-generational craft, the descendants of which will be used to explore the upper atmosphere of the Jovian planets. And to mine them for helium and other gases, with which will then be used as fuel for airships on Earth, I guess.
OCaml exception constructors are just term constructors in the open sum type `exn`. In OCaml, to distinguish constructors from bound variables, constructors must begin with a capital letter. Thus `let Foo = 4;;` is an error.
And almost all of those, except maybe the router and phones if the users are technically sophisticated enough, will be locked down and refuse to obey the user. When Linux gets Tivoized, well-meaning devs have helped corporations abuse their users and customers.
It depends on the host firewall... many quality operating systems allow host firewalls to apply process-based policy which your upstream certainly can’t achieve.
I believe Germany reports deaths differently. Last I heard, they are not reporting covid deaths where the person had some underlying health condition and are instead only reporting those deaths where the cause was covid and only covid. I’m sorry I don’t have a link and don’t have the time to dig it up — check BBC or Guardian coverage of the European epidemic.
Federal law does not a priori supersede state law. The Tenth Amendment to the US Constitution reserves _all_ rights not explicitly granted to the federal government to the states and the people. The Civil War was fought, in part, over this contention between the power of the federal government to emancipate slaves and the power of the slaveholding states to continue to allow the practice of slavery. In more modern times, certain aspects of the constitution have been interpreted more and more broadly to allow e.g. the regulation of medical products under the auspices of regulating “interstate commerce” (even if said products are only ever sold in a single state — they can be transported across state lines).
From this system design, you can deduce that there _does_ exist a hierarchy in the theory of US government — the Constitution is the law of the land and all other actors and subsystems are subordinate to it. Modifying the Constitution requires significant effort at multiple levels of government usually including (by state law) extensive popular support and supermajorities of representatives.
They explicitly mention that the effect seems unrelated to wavelength of incident light — would love to see a test with a UV or IR laser source to demonstrate that the primary downside of the attack is mitigatable (of course with additional expense and increased safety risk).
