I remember reading long ago that in a first-order theory, the only inference rule we need is modus ponens, because all of the instances of the other rules can be stated as implications and made into an axiom schema. For example, instead of the instance of universal quantifier elimination, "from $\forall x: x+1 \ne x$, conclude $0+1 \ne 0$", we have the axiom $(\forall x: x+1 \ne x) \rightarrow 0+1 \ne 0$. Then by applying modus ponens, we get the same effect as universal quantifier elimination, so we don't really need it. We can have any axioms we want as long as they are polynomial-time recognizable, and it doesn't matter whether we call them axiom schemas or inference rules because we have modus ponens.

Now I have realized this is not quite true. Introduce a new $0$-ary relation symbol $G$ to the language of a consistent theory, and also the inference rule "from $G$, conclude $0\ne0$". The new theory proves exactly the same formulas as the old one, and in particular it does not prove $G \rightarrow 0 \ne 0$. We can even add as an axiom that $G$ is equivalent to a Gödel sentence, or any other formula that is not decidable in the original theory, and the theory remains consistent, that formula remains undecidable, and $G$ remains undecidable; the new axiom simply acts as a definition naming the formula $G$, even in the presence of an inference rule saying that $G$ entails falsehood.

In the above example I could have kept the language the same and used as an inference rule "the Gödel sentence entails falsehood" with the same effect, but I wanted to address the potential objection that an inference rule should only use logical symbols, i.e. no arithmetic which would be needed to define a Gödel sentence. So to sidestep that distinction I invented a new symbol, declared it to be logical, and used it in an inference rule. Can I do that?

Overall, how should I understand the distinction between axiom schemas and inference rules, and how do we know when modus ponens is enough? If we have some inference rules aside from modus ponens, under what conditions can we prove the implicatory statements of those rules?

  • $\begingroup$ When you're adding non-logical inference rules instead of axioms, the result depends a lot of which proof system you're working with. For example in natural deduction adding $G\vdash 0\ne 0$ would allow you to prove $G\to 0\ne 0$. You seem to be tacitly assuming that your new inference rules are always interpreted relative to a Hilbert system, but that is not the only option. $\endgroup$ Apr 24 '17 at 22:03
  • 2
    $\begingroup$ @DanBrumleve What you are describing is a Hilbert-style deductive system. Certainly, the systems you describe with the only inference rule being modus ponens are representative of Hilbert-style systems. You are moving only a touch beyond that with your suggested addition. As the Wikipedia page linked above states, natural deduction tends to take the opposite extreme where most things are characterized by inference rules and there are relatively few axioms. $\endgroup$ Apr 25 '17 at 1:16
  • 1
    $\begingroup$ "If we have some inference rules aside from modus ponens, under what conditions can we prove the implicatory statements of those rules?" There are many different systems and they all are equivalent for many logical purposes, but your question is a little unclear. Are you just asking for an example of an axiom list that would be enough for logic (propositional calculus? predicate calculus?) with modus ponens as the only inference rule? $\endgroup$
    – Mark S.
    Apr 25 '17 at 2:01
  • 1
    $\begingroup$ @MauroALLEGRANZA: I think you're mischaracterizing what completeness of propositional logic means (and conflating it with what it means for a theory to be complete). How would you derive a contradiction from assuming $P$ as an axiom? $\endgroup$ Apr 25 '17 at 9:33
  • 1
    $\begingroup$ I can't answer the question directly -- I don't know of a clean criterion. But I can point out that this issue is closely related to the deduction theorem, as I explained at mathoverflow.net/a/132295/5442 $\endgroup$ Feb 3 '18 at 2:27

A proof does proof a formula. So I guess one requirement for this to happen is to identify inference rules with formulas. This is not possible in all logics directly. For example this inference rule:

     G |- A(y) 
 ------------------ y not in G
 G |- forall λx.A(x)

Has a side condition. So even if we would model it as the implication A(y) -> forall λx.A(x), we would have eradicated the side condition. The good news is that there are nevertheless ways to also model such side conditions. One way is to use dependent types and thus higher order logic:

λα.(λy.α(y) -> forall α)

If we instantiate α with λx.A(x) we get:

λy.(λx.A(x))(y) -> forall λx.A(x)

Which reduces to the following, using β-conversion:

λy.A(y) -> forall λx.A(x)

But to get λy.A(y) in the first place, we need to apply a deduction rule, which will remove the variable y from the context. Therefore establishing the side condition. Dependent types are therefore used for so called logic frameworks, where we can model inference rules as formulas.

See for example here:

Isabelle: The Next 700 Theorem Provers
Lawrence C. Paulson - 1990


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.