# What does it mean to axiomatize a logic?

I'm sorry if this question is not clearly formulated: An axiomatization, or an axiomatic system, usually means a set of axioms (i.e. a theory). A formal theory is such a set of formulas in some formal language (e.g. Peano axioms, in the language of first order arithmetic).

My question is, what does it mean to axiomatize a logic (e.g predicate logic)? It does not seem to mean the same thing because, for example, the Hilbert style of axiomatization of predicate logic includes rules of inference and those are not formulas in a formal language. And what is supposed to be the formal language here in the axiomatization of predicate logic? Is there such a language as "predicate logic"? What is its signature, does it include an infinite number of arbitrary constants, functions and relations?

I understand the difference between a schema and a formula. But I don't see how that difference answers my question.

• In any formulation of logic we need inference rules; Natural Deduction is a "presentation style" of logic with only rules. The so-called Hilbet-style presents logic with axioms and inference rules (at least one : usually modus ponens). In the Hilbert-style approach all valid formulae are generated starting from a little number of "preferred" ones (called logical axioms) through the rules of inference. – Mauro ALLEGRANZA Mar 23 '15 at 21:29
• I know, but still this does not solve my question. My question is about the notion of axiomatizing a logic. For example it is said that some axiomatization of predicate logic (or propositional logic or what ever) is complete (with respect to some semantics). I know what that means, it means that if some sentence (in some interpreted language) is valid, it is provable (in predicate logic). But still I don't know exactly what does it mean to axiomatize a logic, at least I have not seen an exact definition of it. – Johannes Mar 23 '15 at 21:42
• At some point, you have to get down to simple, typographical rules, i.e. rules having to do with nothing more than mechanically manipulating strings of characters without any regard for interpretations. You have simple typographical rules for constructing syntactically correct statements. And you have simple typographical rules for constructing valid proofs consisting of ordered lists of statements. – Dan Christensen Mar 23 '15 at 21:43
• Yes, ok. But that is an informal definition. It is not the same definition that is usually given to a formal theory, which is a set of sentences in some formal language (with a signature). I mean "predicate logic" is not even a language in this sense. – Johannes Mar 23 '15 at 21:48
• Yes, it is informal. Nevertheless, there should be no ambiguity. We are given some initial strings of characters and rules for using them to create others. We are also given rules for constructing ordered lists of them, all without regard to any interpretation. – Dan Christensen Mar 23 '15 at 21:59

Once you have a syntax for your formal logic, you know what the rules are for putting together symbols in your language, so you know what the valid strings are.

Next we need to know what

1. what the strings mean and

2. what we can do with these strings.

The first one is given by the satisfaction relation $\models$, which tells you when a string is satisfied, or in other words, when a string is "true".

The second one is given by the rules of inference of the system, also called the axioms, deduction rules, or proof calculus. These describe the relation $\vdash$, and tell you what are the valid rules for proving new statements in the logic. This is the axiomatization of the logic.

So on the one hand we have a notion of truth and on the other hand we have a notion of provability, and of course we would like these two to correspond to each other, i.e. we want the system to be sound (meaning that if something can be proven, then it is true) and complete (meaning that if something is true, then it can be proven).

So to axiomatize a logic means to start with a formal language for your logic and a satisfaction relation that tells you what those strings mean, and from this create a set of axioms or deduction rules such that the logic is at the least sound, and hopefully also complete.