Can we deduce anything from the empty set of axioms?

Question

If the set of logical axioms is empty and so is the set of non-logical axioms, then it seems we can't make any deduction.As the first formula in the deduction must belong to either sets or it it's deduced from previous formulas by means of a rule of inference (no such previous formulas even exists!)

In Friendly introduction to logic, it's stated that,

Actually, after we set up our rules of inference, there will be some deductioms from the empty set of axioms, but that comes later.

Is that even possible? my answer is yes since I can think of the possibility when we have a rule of the inference of the form: $(\emptyset,\phi)$ for some tautlology $\phi$. So we can start the deduction using this particular $\phi$, Is that right?

But, If we don't have even any rule of inference at hand, Can we still have some deductions? It seems to be impossible for this to happen, right?

Answer 1

See Definition 2.4.5. [page 61] :

If $\Gamma$ is a finite set of $\mathcal L$-formulas, $\phi$ is an $\mathcal L$-formula, and $\phi$ is a propositional consequence of $\Gamma$, then $\langle \Gamma, \phi \rangle$ is a rule of inference of type (PC).

[...] notice that if $\phi$ is a formula such that $\phi_p$ is a tautology, rule (PC) allows us to assert $\phi$ in any deduction, using $\Gamma = \emptyset$.

Thus, we can start a deduction simply "writing down" a tautology.

See Ch.2.3 The Logical Axioms : the logical axioms are :

• the three equality axioms [see page 56]

• two quantifiers axioms [page 57].

You can compare with the very similar deductive calculus of Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 112 : the logical axioms are the axioms for equality, three axioms for the (universal) quantifier plus all the tautologies.

Enderton's choice and Leary's one are quite similar; in both cases, at each step in a derivation we may "introduce" a tautology.

Answer 2

Your reasoning is correct. However, t's difficult to find any technical or even philosophical motivations for the conception of such logic system you are describing. Such system would be as useful as a trivial one, i.e. an inconsistent system. For practical purposes, we are interested in systems we can derive something from something.

Answer 3

There are many, many, many ways of defining the proof system for first-order logic. Some authors may consider the logical axioms to be "axioms"; some may consider them to be "rules of inference". In general, I would read the quote in the question to mean there will be deductions without non-logical axioms, because this is almost certainly what the author intended.

In other deduction systems, such as the tableau method, it is possible to prove all logically valid formulas with no axioms at all - there are no "logical axioms" in these systems. I mention the tableau system in particular because it is so different from the Hilbert-style system that you refer to. A tableau-style deduction is a tree with the negation of the desired formula at its root, and other formulas labeling the other nodes of the tree.

Similarly, the proof systems that are known as "natural deduction" have a very different structure than Hilbert-style systems. A deduction in a natural deduction system is a different sort of tree, not just a list of formulas.