Before I have started to learn proof theory for first order logic I had the following simple (and maybe naive) expectations:
- We can use formal language (first order logic) to formulate expressions (statements).
- We formulate several statements that we accept without a proof (axioms).
- 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:
- 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).
- 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).