Stack Exchange
log in

Christopher King

 Discussion on question by Christopher…

Imported from a comment discussion on math.stackexchange.com/q...
Christopher King
Wed 12:35
@AlexKruckman oh, whoops. I'll edit it out then (unless someone else does).
Christopher King
Wed 12:35
@AsafKaragila They are represented by the same object in the meta theory, but are treated differently in the two models. For example, if $x \in_{M'} Y$, but $x$ is not an element of $M$, then obviously you can not have $x \in_M Y$, because $x$ is not even in the "domain" of $\in_M$, so to speak.
Christopher King
Wed 12:35
@AsafKaragila In particular, $M$ and $M'$ probably are not standard models. If they were, you'd be absolutely correct.
Christopher King
Wed 12:35
@AsafKaragila You have to remember that $M$ and $M'$ don't necessarily represent their elements using corresponding sets from the meta theory. For example, let's say that $M$ has an element $\{1,2,3\}$, which it proves to be $\mathbb N$. This is not a contradiction because the claim is made using $\in_M$, not $\in$. There would still exist infinitely many elements $x$ of $M$ such that $x \in_M \{1,2,3\}$, despite $x \notin \{1,2,3\}$. And there might be elements such that $x \notin_M \{1,2,3\}$ but $x \in_{M'} \{1,2,3\}$. The actual elements of $\{1,2,3\}$ don't matter at all.
Christopher King
Wed 12:35
@AsafKaragila it's the same object, but it has different elements in M and M' since they have different $\in$ relations.
Christopher King
Wed 12:35
@AsafKaragila in general, all three will different.
Christopher King
Wed 12:35
@AsafKaragila it may help if you label which sub set relation you are talking about: the meta one, the one in $M$, or the one in $M'$.
Christopher King
Wed 12:35
@AlexKruckman I think the source of the miscommunication is that even though the elements of $M$ are also in $M'$, $\in_M$ is not the same as $\in_{M'}$.
Christopher King
Wed 12:35
@AsafKaragila It is also impossible to prove that infinite elements of $M$ are subsets of $H$ in $M'$, since that would require invoking an infinite number of axioms (since each element of $H$ is given its own axiom).
Christopher King
Wed 12:35
@AsafKaragila The theory is definitely not inconsistent since it is modeled by a bunch of theories. Models can not model inconsistent theories. The reason that the infinite elements of $M$ will not be subsets of $H$ in $M'$ is that in $M'$ they will contain nonstandard elements. These nonstandard elements will not be in $H$.
Christopher King
Wed 12:35
@AsafKaragila Well, if $M$ says one of it elements are infinite, $M'$ will also say its infinite. Whether or not this is true outside the models, I do not know.
Christopher King
Wed 12:35
@AsafKaragila But the infinite elements of $M$ will also be bigger in the extension, I think. For example, if a set whose elements are $\mathbb N$ is in $M$, then in $M'$ that set will also contain nonstandard integers. Also, since it is an elementary extension, whether or not a given set is finite will have the same answer in both models.
Christopher King
Wed 12:35
@AlexKruckman looks good.
Christopher King
Wed 12:35
@AsafKaragila I don't think that's quite it. The elements of $M$ can still be infinite in the extension, but they will all be in $H$, a finite set. So $H$ will not be hereditary finite either.
 

 Discussion between Christopher King a…

Imported from a comment discussion on proofassistants.stackexc...
Christopher King
Feb 4, 2024 17:49
@AndrejBauer yeah I figured it was a bit extravagant (but perhaps there was a tiny proof-of-concept proof assistant that implemented it?). A use case I had in mind: if you have or are in the process of formalizing computability theory in the proof assistant, CR is a convenient way to prove a function of computable, so having it as a built-in tactic is convenient. The requirement that the proof assistant actually produces $e$ is just a preference for the proof assistant being able to compute things (just adding an axiom is obviously easy).
Christopher King
Feb 4, 2024 17:49
@AndrejBauer okay so my notation was perhaps a bit misleading. $\eta$ should actually be thought of as a relation, not a function. This formulation of CT is more specific about this (and also applies to CR).
Christopher King
Feb 4, 2024 17:49
@AndrejBauer $\eta$ could just be an interpreter for Turing machines. That doesn't run into any logical issues (although there are probably more convenient numberings that also avoid logical issues).
Christopher King
Feb 4, 2024 17:49
@AndrejBauer hmm, it's a very subtle issue but I think technically this approach would require $\eta$ to be an interpreter for $T$ terms, which I imagine is impossible to use for Gödelian/Tarskian reasons. $e$ is supposed to part of a discrete data structure, but $f$ is a function. The term underlying $f$ can be represented by a natural number, but turning it back into a function requires an interpreter.
Christopher King
Feb 4, 2024 17:49
(Like, the version with $\Sigma$ should probably be referred to as CR! (since the equivalent axiom is called CT!). But I'd also interested in implementations for CR!.)
Christopher King
Feb 4, 2024 17:49
@AndrejBauer yeah that's fine. In a system with both, CR using either $\exists$ or $\Sigma$ works.
Christopher King
Feb 4, 2024 17:49
@JasonRute by "implement" I mean an actual piece of software. I am very confident that CR is correct in Agda and Coq. CR is correct in IZF, for example. But I don't know of any software for performing it automatically. (It is always computable for recursively enumerable theories.)
Christopher King
Feb 4, 2024 17:49
@JasonRute there are no conditions of $\phi$ other than there being a proof of $\forall x.\exists y. \phi(x,y)$. The reason CR can exist is that in constructive proofs can be turned into programs. The program is found by analyzing the proof, not by analyzing the formula $\phi$.
Christopher King
Feb 4, 2024 17:49
@JasonRute if $T$ is classical, than the church rule can't hold because $T$ will be able to show the existence of uncomputable functions. For example, PA proves "for all x there is a y such that y is the xth busy beaver number", in which case $e$ won't exist.
 

 Discussion on question by thinkingman…

Imported from a comment discussion on philosophy.stackexchange...
PyRulez
Jul 30, 2023 20:50
An event matches the intuitive meaning of improbable if it's log probability is far higher than its kolmogorov complexity. For most sets of five people, the kolmogorov complexity of that set is similar to the log probability of them winning the lottery. The kolmogorov complexity of any single person is far lower than the log probability of them winning five times.
 

 Discussion on answer by apsillers: Do…

Imported from a comment discussion on opensource.stackexchange...
PyRulez
Dec 27, 2022 01:38
Remember that GPL doesn't authorize users to do illegal things, so if they break into your systems to victimize your users those users can sue for damages. So you just need to ensure that the compliant software doesn't authorize the things you don't want it to.
PyRulez
Dec 27, 2022 01:37
@dtech the pragmatic answer is that you need to write the software so that the clients that are compliant reject unauthorized network access. Regardless of licensing, the software is insecure if you do not do this.
 

 Discussion on answer by Dale: Is ther…

Imported from a comment discussion on physics.stackexchange.co...
PyRulez
Sep 27, 2022 18:00
@safesphere there are also no observations of black holes forming. What's your point?
 

 Discussion on answer by mishan: Can s…

Imported from a comment discussion on money.stackexchange.com/...
PyRulez
Jul 9, 2021 22:48
@user253751 lol, I'm just imagining a bunch of SE users emailing the New York Stock Exchange now.
 

 Discussion on answer by Nate Eldredge…

Imported from a comment discussion on law.stackexchange.com/qu...
PyRulez
Apr 7, 2021 14:44
To clarify, a government officer can regain viewpoint discrimination abilities if they resign, right?
 

 Discussion on question by YaDav: I'm …

Imported from a comment discussion on workplace.stackexchange....
PyRulez
Jan 3, 2021 19:53
I mean, 10 days is so short it seems like you could just wait 10 more days to apply, but then complain if you get an interview.
 

 Discussion on answer by Mark: What le…

Imported from a comment discussion on space.stackexchange.com/...
PyRulez
Dec 3, 2020 15:20
Couldn't you just have the axis of rotation be towards the sun, and stop the rotation when docking?
 

 Discussion on answer by mjoao: Why do…

Imported from a comment discussion on security.stackexchange.c...
PyRulez
Dec 1, 2020 12:32
So the security concern is that it's too secure?
 

 Discussion on answer by jmite: Assumi…

Imported from a comment discussion on cs.stackexchange.com/que...
PyRulez
Mar 15, 2020 19:46
@Arno there's a difference between "we have" and "there exists". There could exist an algorithm whose description has more symbols than the number of atoms in the universe, but it would be a stretch to say we "have" that algorithm.
 

 Discussion on answer by Kain0_0: Is i…

Imported from a comment discussion on worldbuilding.stackexcha...
PyRulez
Jan 14, 2020 03:33
It should be noted that you can use gyroscopes for most of the spinning.
 

 Discussion on question by anonymous1:…

Imported from a comment discussion on workplace.stackexchange....
PyRulez
Nov 9, 2019 08:35
Although I understand your legal worries, I don't get the ethical concern (other than if it is illegal or dishonest). Using the ideas in the new business doesn't stop the old one from using them.
 

 Discussion on question by user69899: …

Imported from a comment discussion on worldbuilding.stackexcha...
PyRulez
Oct 25, 2019 05:43
It seems like you're looking for a pocket dimension, not a black hole.
 

 Discussion on question by PyRulez: Wh…

Imported from a comment discussion on law.stackexchange.com/qu...
PyRulez
Sep 30, 2019 04:00
@Fiksdal is it illegal to cause weapons to exist on a plane?
PyRulez
Sep 30, 2019 04:00
@Fiksdal if it's really cold maybe.
PyRulez
Sep 30, 2019 04:00
@Fiksdal It's about the same melting point as ice.
PyRulez
Sep 30, 2019 04:00
@Fiksdal maybe they have a cooler and it accidentally gets in it. Or the crew set the climate controls wrong in the cargo area.
PyRulez
Sep 30, 2019 04:00
@Fiksdal I believe it just needs to be cold enough to freeze water. Liquid nitrogen would do it quickly.
 

 Discussion on answer by T.J. Crowder:…

Imported from a comment discussion on security.stackexchange.c...
PyRulez
Mar 1, 2019 21:24
@T.J.Crowder What if you are the VPN administrator?
 

 Rayo's Number

See comments on mathoverflow.net/q/291098/65915
PyRulez
Feb 9, 2019 08:59
In particular, I think you could construct a nonstandard model in which Rayo's number is quite low.
PyRulez
Feb 9, 2019 08:59
Well yeah, but maybe the maximum's value is decreased for some reason if you "toggle" CH, which would result in a new max potentially.
PyRulez
Feb 9, 2019 08:40
It is included in the length, but it could affect what value a given definition defines. For example the statement "x = 0 if CH and x = 1 if not CH" defines a number, but the number it defines depends on CH.
PyRulez
Feb 9, 2019 08:20
Well, there is a subtly there. Unlike me, KM can't talk about the semantics of second order set theory.
PyRulez
Feb 9, 2019 08:15
Anyways, my personal philosophy is that there is an intended model of first order arithmetic, but not of set theory (first or second order), so Rayo's number would not be well defined if you do not specify a model. However, KM disagrees with me, and happily asserts that Rayo's number is a specific number, despite not knowing what it is.
PyRulez
Feb 9, 2019 08:13
Rayo's number definitely could be affected by things like the continuum hypothesis.
PyRulez
Feb 9, 2019 08:13
Oh, and Scott Aaronson (the author of the second link) seems to require that a definition not depend on controversial statements about set theory for it to "work".
PyRulez
Feb 9, 2019 08:11
Actually wait no, it still works in NBG, it just can not prove many things about it.