20

We can define a sound proof system as a computable function $\Pi$ which maps strings (proofs) to strings (statements proved), with the following property: if $\Pi(\pi) = p$, then $p$ encodes a true statement. We think of $\pi$ as a proof of $p$. (If $\pi$ is not a valid proof, then $\Pi$ outputs some fixed true statement.) We consider sound proof systems ...


9

Your program P may halt if the proof system it is using is inconsistent, allowing it to prove a self-contradictory statement. The fact that no (sufficiently expressive) proof system can prove its own consistency is exactly what is shown by Gödel's second incompleteness theorem (which, not coincidentally, is in many ways analogous to Turing's halting theorem)....


6

Yes, with such a powerful oracle, the halting problem can be solved. To be clearer, given an arbitrary Turing machine, the oracle will tell the set of words accepted by that Turing machine is finite or not. Suppose we are given a Turing machine $M$ and an input $x$. Let us construct Turing machine $M'$ such that on all inputs, $M'$ will simulate $M$ running ...


6

Succinctly, your argument (that there is no such proof that P does not halt) is a proof but not in the same proof system that P is using to search for proofs! In fact, this very kind of computability-based argument can be used to great effect to prove the generalized incompleteness theorems, even the Rosser strengthening.


5

We can prove the following theorem: Theorem: A language $L$ is regular if and only if there exists a DFA or NFA for language $L$. Turing machines are more powerful than DFAs and NFAs. In particular, every finite state automaton can be simulated by some Turing machine. So, according to the above propositions, the answer to your question is yes: every regex ...


4

It's not about strength: the Baker-Gill-Solovay nonrelativization result relativizes (hehehe), in the sense that for every $A$ there is a $B\ge_p A$ such that $\mathsf{P}^B\not=\mathsf{NP}^B$, and for every $A$ there is a $B\ge_p A$ such that $\mathsf{P}^B=\mathsf{NP}^B$. What matters more - or at least, what matters more in a way we can understand - is ...


4

Not at all. The halting problem says it is impossible to decide whether an arbitrary turing machine with arbitrary input will halt. But there are many, many specific turing machines where we can prove that they halt for every input, or where we can look at the input and decide if the turing machine will halt or not. And since the people writing the download ...


4

The point of the halting program IMO is not to show that you can't check whether an arbitrary program can halt--that's not a very interesting fact on its own. The point of the halting program, is to use "reduction", to go on and prove that a (very large number of) procedures you might like to have a tool do are also impossible in general: Deciding ...


4

Let us say that $H$ is a partial Halting oracle if it takes as input a pair $(M,x)$ where $M$ is the description of a Turing machine and an input $x$, and: If $H$ terminates and outputs "yes" then $M(x)$ halts. If $H$ terminates and outputs "no" then $M(x)$ does not halt. In particular, $H$ is allowed to run forever and not give an ...


3

The problem of deciding whether, given a Turing machine $T$ and a word $w$, $T(w)$ halts is undecidable. If a Turing machine $T$ is fixed, the problem of deciding whether, given a word $w$, $T(w)$ halts might or might not be decidable (depending on the choice of $T$). As an example in which this problem is decidable consider the trivial Turing machine $T$ ...


3

You could totally do that, but there are some consequences it's worth being aware of. TM proofs only show difficulty of the halting problem for TMs, but here's a crucial thing that you might be overlooking: it is easy to implement a simulator of a TM in any language of one's choice. That can probably be done in a few dozen lines of code and it is ...


3

I think I understand what you are trying to ask. But you may have to work harder on the asking to get a non-trivial answer. As it stands, your question has a trivial answer. Take a language that always terminate, and add a command that never terminates and is syntactically constrained to be used first if at all in a program. To check termination, you only ...


3

The notion of automating mathematics is a vague one, and that's accounting for the discrepancy here. One interpretation would be: to automate mathematics would be to produce a machine $M$ which could tell whether or not a given sentence is true (or, more weakly, provable from some agreed-upon set of axioms like $\mathsf{ZFC}$). Even the weaker version is ...


3

The problem is decidable. You can enumerate the (finitely many) programs that use at most $b$ bytes. For each such candidate program $P$, you can check whether $P$ is valid program (for any reasonable representation) and execute it for up to $t$ time steps. Eventually you either find a program that prints $s$ (and accept) or you run out of programs (and ...


2

There is past and current research on this. Such problem is called Termination Analysis, and a quick look on Google (Scholar) provides several old as well as new publications on this: 2005, Termination Analysis of Higher-Order Functional Programs; 2006, Automated Termination Analysis for Haskell; 2008, Termination Analysis of Logic Programs based on ...


2

The problem is PSPACE-complete. The problem is in PSPACE. You can test whether such a machine halts in polynomial space, by running the Turing machine for $2^n |Q| n + 1$ steps, where $|Q|$ is the size of the finite control, and checking whether it halts. Why? Each configuration of the Turing machine is determined by the values on the tape, the state of ...


2

The main issue, I think, is that you have reduced your unknown problem (file download times) to a hard problem (the Halting Problem), showing that if you had some efficient algorithm for solving the hard problem, then the unknown problem would also be efficiently solvable. To prove hardness of the unknown problem, you need a reduction that goes the other way,...


2

There is a finite number of different states (the set of values of the variables and the program counter). Your "limited goto programs" are just a (messy) way to describe a deterministic finite automaton. Or just reason that the program states being finite, it is certainly possible to map out all possible non-looping computations (by something like ...


2

You are conflating two possible meanings of the phrase "mathematics can be automated": "any theorem can be proved true or false by an algorithm" "the practical activity of proving theorems, as presently performed by humans, can instead be performed by computers in an economically-viable fashion" Due to the halting problem, it is impossible for any ...


2

Solving the "download time problem" is just impossible. Nothing says if your machine (or the network, or the origin, or...) will (or won't) crash, or get overloaded (perhaps everybody in India wakes up with the urge to get the same file, and crash the server) or slow to a crawl, or just speed up to a breeze, halfway through. The problem here is ...


2

Yes. Given a machine $M$ and input $I$, one of the two things happens: $M(I)$ halts. $M(I)$ does not halt. We may not be able to predict or compute which of these happens, but one and only one happens simply by rules of classical logic. Now to show that $H_{M,I}$ exists we consider two cases: If $M(I)$ halts then $H_{M,I}$ exists because we can take it to ...


2

The goal we really want is a total impossibility result: There is no reasonable model of computation which can solve its own halting problem. Church's thesis says that all the usual models (Turing machines, $\mu$-recursion, Python, etc.) are appropriately equivalent and so a proof in any one system should be convincing. However, initially at least we might ...


2

The author is here referring to the Halting problem, and possibly also Rice's theorem (without putting words into their mouths). It says indeed that it's not possible to decide in advance whether a Turing machine will halt on any given input or not, thus it makes it impossible to decide in advance what the actual output of the machine will be. This is the ...


2

Your logic is somewhat correct. I will start by discussing the new definition you tried to give for the halting problem, and then move on to explain the finite set of TMs. Halting problem, with size less than the TM that solves it This idea is certainly interesting, but it has some inherent problems with it. First is a syntax problem. What language is here? ...


1

is EVEN undecidable? How can you prove its undecidability? It depends entirely on the enumeration that you use. E.g. one could make an enumeration that maps all Turing machines that halt with 1000 steps to an even index and all others to odd indices. Then EVEN is still an infinite set but decidable. However a simple way to prove EVEN undecidable (assuming ...


1

You actually have a missing detail on how the machine $TM_2$ is defined (and a bit of confusion between $TM_1$ and $TM_0$). Let's clear this up. You start by the assumption that there is a machine $TM_0$ that operates as follows. On input $x = <TM_1, w>$, the machine $TM_0$ answers "yes" whenever $TM_1$ halts on its input $w$, and $TM_0$ ...


1

Yes, you can prove Rice's theorem by reduction from the Halting problem. See https://en.wikipedia.org/wiki/Rice%27s_theorem#Proof_by_reduction_from_the_halting_problem. The reverse direction is also provable and is trivial. In some sense all statements that true and provable are equivalent, in the sense that you can prove any by starting from any other, but ...


1

The proof you wrote in the question is faulty, because it uses the wrong definition of the Halting oracle. You tried to fix the proof by inserting the assumption $X(X) = X$, but that is not the way to do it. Here is the correct proof. Definition: A halting oracle is a machine $H$ which takes as input a pair $(M,I)$ where $M$ is the (description of) a ...


1

For any reasonable public key cryptosystem that I can think of, no, this is not possible. You cannot base a practical public key cryptosystem on any complexity class larger than EXPTIME. If the private key is linear in the size of the public key (i.e. if the public key is $b$ bits in size, then the private key is no larger than $\alpha b + \beta$ bits for ...


1

You don't define $H_0$. Presumably it's an undecidable set. First, $f : \mathbb{N} \to H_0$ only means that all the values of $f(x)$ are in $H_0$, i.e. the image of $f$ is a subset of $H_0$: $f(\mathbb{N}) \subseteq H_0$. The proof of the counterexample involves a stronger property: it constructs a function $f$ whose image is exactly $H_0$, that is, $f(\...


Only top voted, non community-wiki answers of a minimum length are eligible