Richard Zach on Nostr: Relatedly, why go to all this trouble to get an example of a mathematical claim where ...
Relatedly, why go to all this trouble to get an example of a mathematical claim where \(A \lor \lnot A\) fails (\(A\) is undecided) but \(\lnot\lnot A \to A\) holds? Isn't this true for every \(A=\forall x P(x)\) where \(A\) is an unsolved question but \(P(n)\) is decidable for each particular \(n\), i.e., we also have \(\forall x(A(x) \lor \lnot P(x))\) (say, Goldbach)?
Published at
2024-07-18 22:01:31Event JSON
{
"id": "3927bfa8943563173458ae303150f8bec0ccd7ceec499febdaf1e3a6eb8db68c",
"pubkey": "580ba9c3849e80d58cbcd2c76728f33468f41c54396d73656137b224781f45d2",
"created_at": 1721340091,
"kind": 1,
"tags": [
[
"e",
"2770f9232189d16dd0da7313ff6c137f40993477e78a5cd4313399cf7b21811b",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/rrrichardzach/statuses/112809744236469085",
"activitypub"
]
],
"content": "Relatedly, why go to all this trouble to get an example of a mathematical claim where \\(A \\lor \\lnot A\\) fails (\\(A\\) is undecided) but \\(\\lnot\\lnot A \\to A\\) holds? Isn't this true for every \\(A=\\forall x P(x)\\) where \\(A\\) is an unsolved question but \\(P(n)\\) is decidable for each particular \\(n\\), i.e., we also have \\(\\forall x(A(x) \\lor \\lnot P(x))\\) (say, Goldbach)?",
"sig": "cc64cf89fd6c3a604cd142843e73f7f2f87f6ad6593488c63759d7438c059e006dd0f42d7c1f1d230ec362c8f63f585604869badf7ff9e93e1c522f4807454f7"
}