# What is the accurate definition of inference rule?

Take the inference rule "$$P\land Q \Rightarrow P$$" for example, what is its accurate definition?

1. "For any string $$P\land Q$$, if P and Q are w.f.f, then we can derive P"
2. "For any string $$P\land Q$$, we can derive P"

I prefer the second definition because it is simpler and not much meta-knowledge is involved. If we use the second definition to derive, and P and Q happen to be w.f.f., then the inference has the property of truth preservation defined by meta-logic.

An inference rule is an instruction how to produce from given formulas (premises) a new formula (conclusion).

The general form is: "from (premises) $$\varphi_1, \ldots, \varphi_n$$ derive (conclusion) $$\psi$$".

We may schematically write them in different ways: $$\dfrac {\varphi_1, \ldots \varphi_n}{\psi}$$, but also with: $$\langle \{ \varphi_1, \ldots , \varphi_n \}, \psi \rangle$$.

A deduction is a pair $$\langle \Gamma, \phi \rangle$$, where $$\Gamma$$ is a set of sentences, the premises, and $$\phi$$ is the conclusion and each step in the deduction is obtained applying a rule to the already available formulas.

Note (to avoid possible misunderstanding): we may formalize a "calculus" also for other expressions than formulas; see e.g. Hebbinghaus's Mathematical Logic, page 19, for a "calculus of terms": in this case the rules are rules of formation that applies to expressions that are terms.

• My concern is: as an inference rule, does it really consider if the premises/conclusion are formulas or not. Actually, when we are doing the derivation, we never examine carefully that the current string is a formula or not. Apr 15 at 16:13
• @William - yes, the rule must be applied to formulas. See the verbose form as well as the symbolic one. Apr 15 at 16:15

The idea of an inference rule is to capture some elementary piece of valid deductive reasoning.

But, when we formalize it, all we care is syntax. That is, an inference rule effectively says: "If you have a string of characters that looks like [this], then you can write down a new string of characters that looks like [that]"

In some formal derivation systems, these character strings are sentences: formulas that do not contain any free variables. In other systems, they can be formulas with free variables. but in the end we don't care. We simply depict your inference rule as:

$$\begin{array}{} P \land Q\\ \hline P \end{array}$$

and we can leave it at that.

• But according to Mauro ALLEGRANZA's answer, the rule requires you to check if the strings are formulas, i.e., "If you have a string of characters that looks like [this], then you must check the strings are w.f.f, if they are, then you can write down a new string of characters that looks like [that], and the new string is definitely a w.f.f., no need to further check". Apr 18 at 3:19
• @William True … although if the premises are well formed formulas, the nature of most inference rules will be such that the inferred expressions are w.f.f’s as well. The only exceptions are rules like disjunction introduction where you go from $P$ to $P \lor Q$, contradiction elimination where you derive $P$ from $\bot$, and anytime you start a subproof to make an additional assumption Apr 18 at 11:26
• Yes, there are some rules that produce more formulas so they also need to be checked. The point is I think a rule is just a rule, we should keep it as simple as possible unless something makes it impossible to execute a rule. The other things such as formula verification would be better done by other modules. Apr 18 at 12:06
• Or,we can define the rule as "If you have a string of characters that looks like $P\land Q$, suppose P,Q are w.f.f's, then you can write down a new string of characters that looks like P". In this way, we can transfer the task of verifying P,Q are w.f.f's to other parts outside the rule itself. Apr 18 at 12:42