2

Propositional systems have axioms and inference rules. They bifurcate into two types, Hilbert-style where the number of inference rules are minimised; and Natural Deduction where the number of axioms are minimsed.

In fact it is possible to have Natural Deduction systems that have no axioms, I'm not sure if this is in fact the usual ones looked at.

In general Hilbert-Style systems usually have just one inference rule: modus ponens.

Obviously it is possible to have a Hilbert-style formal system with no inference rules, the question is whether they are useful in anyway?

(Perhaps if we consider the category of all Hilbert-style formal systems they need to be included to get good formal properties for the category?)

Improve this question

1 Answer 1

Reset to default
3

Yes, usually natural deduction systems that you would get in intro textbooks have no axioms. A logical theory could be just a set of theorems, and so have no inference rules. I think the use of such theories is that sometimes you want to put an emphasis on what the theory says and not how it delivers those results.

For instance, in ontology you'll often want to apply a criterion for ontological commitment (like Quine's "to be is to be the value of a variable") to a theory. Since the criterion will (often) just read off commitments from quantified statements, you don't really need the inference rules. To make sure you get all of a theory's commitments, you'll often see authors taking the closure of a theory under logical entailment.

So, if by a "propositional logic without inference rules" you just mean a set of theorems, then yes I think they are sometimes useful. I think the general rule of thumb might be that such formulations are preferable when only the content of the theory matters for your purposes.

Improve this answer
2
  • aren't most of theorems just based on inference? "if conditions are satisfied, then effect is true".
    – SF.
    Mar 6, 2013 at 14:24
  • @SF. It sounds like you're identifying conditional propositions with inferences. I don't think that is, generally, a safe identification. Systems that satisfy the deduction theorem will let you move from statements about, say, A being provable from B to the conditional B->A, but this is a substantive metatheoretic result. The difference here is just the object language/metalanguage distinction. Inferences are metalanguage statements written with the single turnstile. Conditionals are statements in the object language.
    – Dennis
    Mar 6, 2013 at 15:02

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .