bio  website  science.marshall.edu/mummertc 

location  Marshall University  
age  36  
visits  member for  4 years, 7 months 
seen  21 hours ago  
stats  profile views  2,024 
I work in mathematical logic. My main areas of interest are arithmetic, reverse mathematics, computability, and proof theory.
16h

awarded  Nice Answer 
Oct 11 
comment 
Forcing is intuitionistic
Some modern accounts also incorporate classical logic into the definition of forcing by beginning with a limited set of connectives (e.g. including $\lnot$, $\land$, and $\forall$, but not $\exists$ and not $\lor$), and then assuming the other connectives are given by their classical definitions, which are not intuitionistically correct. 
Oct 11 
answered  Forcing is intuitionistic 
Sep 30 
awarded  Explainer 
Sep 25 
comment 
An interpretation of notCon(PA)
Of course, some of the steps may also be nonstandard instances of axiom schemes, such as nonstandard instances of the induction scheme or nonstandard tautologies. 
Sep 14 
comment 
Deduction theorem
+1. The solution of Negri and Hakli is elegant  they redefine the meaning of $\vdash$ so that what they have is not quite the standard Hilbert system (because they have changed the N rule to a weaker rule), but which does have a deduction theorem. Of course the original Hilbert system, with the full N rule, does not satisfy the deduction theorem, in that it admits $A \vdash \Box A$ as a derived rule but not $\vdash A \to \Box A$. Presumably one could apply a similar method to certain systems for first order logic as well. 
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 secondorder 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 omegamodels in second order arithmetic
I am not aware of any reverse math research in which the base theory includes true firstorder 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 omegamodels in second order arithmetic 
May 18 
revised 
Are there “nonconstructive” sets in secondorder arithmetic?
added 2880 characters in body 
May 17 
answered  Are there “nonconstructive” sets in secondorder 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 setexistence 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 nearmechanical?
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 