I will add the induction scheme tonight, but if above description doesn't ring a bell, then I have my answer.

That would require a few pages. I am busy with making a web-based theorem checking tool and then I want to show that you can prove that there are infinite number of primes. I think the description above should be enough to ring a bell, if it already exists. A comparison with PRA is inevitable (although I didn't start with that). Basically, it is just comparing two programs, where the programs can be non-deterministic (no oracles). A non-deterministic loop in computer science, is a transitive reflexive closure in math.

@Christoph, there is indeed no precise description of "simple". For that mathematics and logic are an art as it has ever been. However, adding an additional axiom saying that ZFC is consistent, sounds simple in English, but formally it isn't. You have to formalize ZFC completely in the finitary system. The axiom will be a huge axiom. That can not be considered simple.

One way to prove that they are not necessary is to show that ZFC can prove the absolute consistency of such simplified system. Has such proof been given? I am not convinced that further simplifications are not possible.

Those are the more obvious ones. But can you also drop unnecessary nesting of quantifyers?

I think with the introductions of computers. Then they started to talk about grammer (for instance BNF), and then you have to be more precise.

If you enumerate the values of x (for instance when they are natural numbers), you don't need an extension of the language, to my opinion.

I am not sure, but since we don't have equations, it looks like a provable correct calculator. You might look at: prover.cs.ru.nl/calc.html. "The ProofWeb interface has been used and extended in various projects. The main ones are a prototype by Cezary Kaliszyk and Pierre Corbineau of a system that combines ProofWeb with a mathematical encyclopedia in the style of Wikipedia, and PC-Extra, an arbitrary precision calculator by Cezary Kaliszyk, based on the PhD work of Russell O'Connor. "

Garabed, I suggest that you look at NPC problems. Problems that are finite, but still very hard to solve, are often NPC problems. I am quite confident, that your halting problem is a NPC problem.

Note, that you can see formulas as graphs. The variables are needed to describe that the nodes with same variable name are connected. The fact that we need variables is just our preference to write everything sequential.

I think it is rather arbitrary to limit the number variables, while you do not limit the formula. You can invent an FOL without variables at all, but then you have a kind of environment, from which you select your variable. But this is just window dressing.

I have been thinking how exactly the second order proof goes. One should prove that if the exponents follow a well ordered relation, then the newly created relation is also well ordered. Which such proof, you can then do induction on the height of the exponent tower. Because, we are quantifying over all well ordered relations, this is a second order proof. In case of meta-logic (using Constructive omega rule), the quantification is on syntactical level.