bio | website | science.marshall.edu/mummertc |
---|---|---|
location | Marshall University | |
age | 36 | |
visits | member for | 4 years, 4 months |
seen | 6 hours ago | |
stats | profile views | 1,982 |
I work in mathematical logic. My main areas of interest are arithmetic, reverse mathematics, computability, and proof theory.
Aug 24 |
awarded | Nice Answer |
Aug 24 |
comment |
Deduction theorem
@bellpeace: the original system is sound for a particular class of models, namely those in which $A \to B$ holds. Whenever we add new rules of inference, we have to restrict the set of models to those for which the new rules are sound. Of course the system I described, with the additional inference rule, is not complete, and no example that answers the question can be complete in that sense. |
Jul 12 |
awarded | Enlightened |
Jul 12 |
awarded | Nice Answer |
Jul 9 |
revised |
Infinite decreasing sequence by the Turing jump
added 826 characters in body |
Jul 9 |
answered | Infinite decreasing sequence by the Turing jump |
Jun 5 |
comment |
Is the Invariant Subspace Problem arithmetic?
Here "equivalent" means "provably equivalent in a sufficiently weak system", which is more or less what the question is asking. Of course every true statement is uninerestingly equivalent to $0=0$. |
Jun 5 |
comment |
Is the Invariant Subspace Problem arithmetic?
Do we know that the statement in question is true in the setting of computable analysis? If it is not, then that immediately prevents it from being equivalent to any arithmetical formula, because every true arithmetical formula is satisfied by the model of second-order arithmetic with the standard natural numbers and only computable sets. Actually, every true $\Pi^1_1$ formula is true in that model. This is a standard method for showing that particular theorems are not expressible by excessively simple formulas. |
May 18 |
comment |
Necessity of omega-models in second order arithmetic
I am not aware of any reverse math research in which the base theory includes true first-order arithmetic. But there is another point: the induction schemes in reverse mathematics all include set parameters. This is the case even for schemes like B$\Sigma^0_2$. Formulas of true first order arithmetic don't include set parameters. |
May 18 |
answered | Necessity of omega-models in second order arithmetic |
May 18 |
revised |
Are there “non-constructive” sets in second-order arithmetic?
added 2880 characters in body |
May 17 |
answered | Are there “non-constructive” sets in second-order arithmetic? |
May 17 |
comment |
Proof complexity of two directions of equivalency?
This sort of question comes up very naturally, but it is often hard to find precisely the notion we want to capture. The length of a formal proof is not a very interesting metric, because we don't normally look at formal proofs anyway (so the length is meaningless for practice) and because the length depends as much on the proof system as on the theorem being proved. Reverse Mathematics can capture the set-existence axioms required for each direction. But trying to capture how "easy" or "natural" each direction is to prove is a challenge that has not been solved. |
May 15 |
comment |
Does formalizing math require search and creativity, or is it near-mechanical?
In his paper about the formalization of the prime number theorem, Avigad reported that once he was up to speed it took about a day to formalize a page of mathematics in Isabelle. I recommend that paper for its discussion of the formalization process. repository.cmu.edu/philosophy/31 |
May 5 |
comment |
What new primitive recursive functions are needed to reconcile Turing time complexity with Gödel time complexity?
@Joel: Yes, exactly. Some other models have a different, unchangeable tape symbol to mark the left edge of the tape. |
May 5 |
comment |
What new primitive recursive functions are needed to reconcile Turing time complexity with Gödel time complexity?
@Joel: By the way, there is a technical reason to start the machine on the first input symbol, which is to accommodate machines that have a one-sided (i.e. semi-infinite) input tape, which are common in the computational complexity literature. These need to know where the left end of the tape is, because in the usual framework they have no way to find it otherwise. |
May 5 |
revised |
What new primitive recursive functions are needed to reconcile Turing time complexity with Gödel time complexity?
added 512 characters in body |
May 5 |
comment |
What new primitive recursive functions are needed to reconcile Turing time complexity with Gödel time complexity?
@Joel: Silly Turing machines - everyone has their own idea how they work! In my mind they need to start on the first symbol of input. This is also (likely) why the author said that $h(x) = x-1$ takes $O(|x|)$ steps; it would also take only one step if the machine started on the last digit. I'll edit the answer, however. |
May 5 |
comment |
What new primitive recursive functions are needed to reconcile Turing time complexity with Gödel time complexity?
@Dan Turetsky: as I point out in my answer, the question is somewhat trivially unsolvable in that context. |
May 5 |
answered | What new primitive recursive functions are needed to reconcile Turing time complexity with Gödel time complexity? |