Is there a proof system for first order logic that does not use premisses and auxiliary variables?

Question

Before I have started to learn proof theory for first order logic I had the following simple (and maybe naive) expectations:

1. We can use formal language (first order logic) to formulate expressions (statements).
2. We formulate several statements that we accept without a proof (axioms).
3. We have a small set of "derivation rules". A derivation rule is something that can take one or two statements and generate one (or none or several) statements that follow from the input statement(s). One example might be a rule that is based on commutativity of "and (A and B = B and A). So, we can take an expression containing "and" and change places of two "inputs" of this binary function. A new statement should not be equivalent to the input statements. It just need to follow from input. For example: A and B -> B.

So, within this approach we can start from axioms and by applying different derivation rules we can generate new statements some of which might be useful theorems.

---

So far I have learned sequent calculus and Hilbert's system. Hilbert's system looks closer to what I expected / wanted but it is still not the same because of several reasons:

1. In a proof we start from axioms and premisses (assumptions). And I want any proof to use only axioms and statements that have been proved earlier (so, no assumptions).
2. In a proof we use "introductions" (universal and existential). As a result we get some "intermediate / auxiliary" formula that are not valid statements by themselves. You cannot take these statements and claim that they are some lemmas or theorems because they contain some "variables" (till the end of the proof we need to get rid of them).

---

So, my question is, if there is a proof system that I have naively imagined (without use of premisses and in which any statement generated in the proof is a "valid" statement that can be used as a theorem).

Answer 1

I think a typical Hilbert system is what you are looking for.

If you see premises being used, then there are probably two reasons for this:

1. The proof uses a premise that may have been derived as a Lemma in some earlier proof. As such, we can in fact substitute those earlier proofs and get rid of those premises, and obtain a premise-free proof.

2. The proof is about some domain, e.g. set theory or arithmetic or what have you. Since he theorems in those domains are not logical theorems, they have to rely on premises: axioms for those specific domains. So in that case you cannot get rid of the premises ... but that's only because you are trying to prove something beyond pure logic

Now, you also say that some proofs have lines/statements with free variables that, as such, aren't really claims by themselves. But actually, you can regard those statements as claims: any expression of the logic language requires some interpretation, and you can simply make the variable assignment part of the interpretation. As such, every line is a logically valid statement.

But if you really don't like the use of these variables, note that we can also use constants instead of the variables. The universal introduction rule can take a statement using constants and make it into a universal statement provided the use of that constant in the proof as a whole satisfies certain restrictions ... restrictions that of course make the constant really act like a variable and thus there is really no practical difference here .... but still, maybe you find this more palatable.