Search Results
| Search type | Search syntax |
|---|---|
| Tags | [tag] |
| Exact | "words here" |
| Author |
user:1234 user:me (yours) |
| Score |
score:3 (3+) score:0 (none) |
| Answers |
answers:3 (3+) answers:0 (none) isaccepted:yes hasaccepted:no inquestion:1234 |
| Views | views:250 |
| Code | code:"if (foo != bar)" |
| Sections |
title:apples body:"apples oranges" |
| URL | url:"*.example.com" |
| Saves | in:saves |
| Status |
closed:yes duplicate:no migrated:no wiki:no |
| Types |
is:question is:answer |
| Exclude |
-[tag] -apples |
| For more details on advanced search visit our help page | |
Results tagged with lo.logic
Search options questions only
not deleted
user 2575
first-order and higher-order logic, model theory, set theory, proof theory, computability theory, formal languages, definability, interplay of syntax and semantics, constructive logic, intuitionism, philosophical logic, modal logic, completeness, Gödel incompleteness, decidability, undecidability, theories of truth, truth revision, consistency.
27
votes
3
answers
4k
views
Is deciding whether a Turing machine *provably* runs forever equivalent to the halting problem?
Assume for this question that ZF set theory is sound.
Now consider the language "PROVELOOP," which consists of all descriptions of Turing machines M, for which there exists a ZF proof that M runs for …
- 9,833
19
votes
0
answers
586
views
Can Gentzen-style proofs give omega-consistency and beyond?
In 1936, Gentzen famously showed that Primitive Recursive Arithmetic, plus the assumption that the ordinal $\epsilon_0$ is well-founded, is able to prove Con(PA). But of course, Con(PA) doesn't yet i …
- 9,833
77
votes
8
answers
12k
views
Succinctly naming big numbers: ZFC versus Busy-Beaver
Years ago, I wrote an essay called Who Can Name the Bigger Number?, which posed the following challenge:
You have fifteen seconds. Using standard math notation, English words, or both, name a single …
- 9,833
20
votes
3
answers
5k
views
Pi1-sentence independent of ZF, ZF+Con(ZF), ZF+Con(ZF)+Con(ZF+Con(ZF)), etc.?
Let
ZF1 = ZF,
ZFk+1 = ZF + the assumption that ZF1,...,ZFk are consistent,
ZFω = ZF + the assumption that ZFk is consistent for every positive integer k,
... and similarly define ZFα for every com …
- 9,833
40
votes
2
answers
4k
views
Is there a computable ordinal encoding the proof strength of ZF? Is it knowable?
In comments on Quora (see, for example, here, here, here), Ron Maimon has repeatedly expressed the strong opinion that Hilbert's program was not killed by Gödel's results in the way typically claimed. …
- 9,833
27
votes
1
answer
2k
views
Why isn't this a computable description of the ordinal of ZF?
In a previous MO question, I was told by several commenters that
(a) it's known that there exists a computable ordinal $\alpha_{ZF}$ that "encodes the strength of ZF set theory" (i.e., a least comput …
- 9,833
44
votes
3
answers
5k
views
"Simpler" statements equivalent to Con(PA) or Con(ZFC)?
Given any reasonable formal system F (e.g., Peano Arithmetic or ZFC), we all know that one can construct a Turing machine that runs forever iff F is consistent, by enumerating the theorems of F and ha …
- 9,833