[Math] What does it mean to axiomatize a logic

axiomslogicpredicate-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.

Best Answer

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.

Related Question