User:CircuitCraft
Update on where I've been
Recently, I've taken a break from writing proofs here to work on a more ambitious project. I'm redoing a lot of the work on provability, but in the Coq proof assistant.
So far, I've finished defining first-order logic and have proven basic results such as:
- the Deduction Theorem
Theorem thm_deduction {F P} : forall {a : formula -> Prop} {h : formula} t,
theorem (assume a h) t -> @theorem F P a (fimpl h t).
- the Universal Generalization Theorem
Theorem thm_univ_generalization {F P} : forall {a : formula -> Prop} x,
(forall f, a f -> var_bound_in_formula x f) ->
forall g, theorem a g -> @theorem F P a (funiv x g).
- the Soundness Theorem
Theorem soundness : forall (assump:formula -> Prop) val, (forall f, assump f -> formula_true val f) -> forall f, theorem assump f -> formula_true val f.
Second Update
I've just completed my proof of the $\Sigma_1$-completeness of Robinson arithmetic.
Theorem arith_sigma_1_complete : forall f, Sigma 1 f -> sentence f -> arith_formula_true (fun _ => 0) f -> robinson_theorem f.
I've gotten a little bit of a start on recursion theory so far, but there's a lot more to do before I can do anything useful with it.
In particular, I need to write a formula parsing function. For that reason, I'll probably use a Polish notation for my formula encoding. It should help make it slightly simpler to parse, and has the nice side effect of making the language prefix-free.
Once I have that, and the reduction to $\Sigma_1$ formulas as in Recursive Function is Arithmetically Definable, Kleene's Normal Form Theorem should be simple.
To clarify, instead of doing all of the stuff with URMs, I'll be using arithmetical formulae. While they're more complicated to work with, I'd have to do it all anyway for Gödel's First Incompleteness Theorem. Skipping URMs will save me work in the long-term.
Biography
I am a student with a strong (borderline obsessive) interest in mathematics of every kind.
My contributions will be sporadic and diverse, with little overall direction. There are still some specific theorems I would like to see on $\mathsf{Pr} \infty \mathsf{fWiki}$, and I will (probably) eventually add them.
I will often attempt to contribute to fields of which I am not very familiar, by extrapolating from existing pages on this website and checking out books from the Internet Archive to use as sources. If I make a mistake, please correct it; I can handle constructive criticism.
Current Projects
Computability theory
I have been working on building a more comprehensive theory of computation on $\mathsf{Pr} \infty \mathsf{fWiki}$. Equivalence from recursive relations to Turing machines is now complete. For completeness, I want to prove Symbol Reduction of Turing Machine. After that, I will use methods similar to Minsky to emulate a Turing machine with a URM, completing the equivalence.
I've also started working with provability. I will need to construct a recursive proof-finder, in the same manner as Gödel. From there, Godel's First Incompleteness Theorem should be in reach.
As a long-term goal, I want to formally construct a "practical" programming language, to help with algorithm design. It should be usable for computational complexity, so this will need to happen after we define Random Access Machines (which are crucial for fine-grained complexity). The paper that defines RAMs uses a language they call "RAM-ALGOL," a subset of ALGOL that immediately translates into a RAM. We could also use LISP, as the original version has a simple structure and a lot of discussion about the implementation.
Jordan Curve Theorem
This theorem is simple and intuitive to state, but famously difficult to prove. The following approaches are proposed:
- The Jordan Curve Theorem via the Brouwer Fixed Point Theorem, by Ryuji Maehara
- The Jordan-Schönflies Theorem and the Classification of Surfaces, by Carsten Thomassen
Eventually, we can of course include both of these approaches on $\mathsf{Pr} \infty \mathsf{fWiki}$, but each will require foundational work that we have yet to complete. The former requires Brouwer's Fixed Point Theorem, of course, while the latter requires Thomsen Graph is Non-Planar, of which a concise proof is in the source.
Perhaps, in the future, we could include an elementary proof, such as this adaptation of the original proof by Thomas C. Hales. This is, however, significantly longer, and most likely not worth the effort at the moment.
Non-Active Projects
- Von Neumann-Bernays-Gödel Set Theory is Conservative Extension of Zermelo-Fraenkel Set Theory