User:Physis/Logical axiom

The article Axiom may be a better treatment of the topic.

The distinction between logical axioms versus non-logical ones is based on an idea of separating

• factors responsible for a “general” underlying “apparatus”
• from the “specific”, “professional” ones responsible for the peculiarities of the particular theory (being the object of the investigation).

An analogous idea is seen at the distinction of non-logical symbols from logical ones, but here at axioms the idea is manifested in a more sophisticated form.

Variations

There are more ways to formalize the notion of deduction in mathematical logic.

Axioms and inference rules

The “apparatus” (chosen to achieve a formalization of the notion “deduction”) may share the work between

• axioms
• rules of inference

The proportion of these two may vary, e.g.

• at some frameworks, all work may be done by rules of inference;
• while at others, the set of inference rule is chosen to be very limited (modus ponens and a suitable rule for quantifiers), and more work is undertaken by axioms (thus they are more in number).

Axioms burnt in the definition of deduction

Other variations may be caused by the fact that

• at some formalization frameworks, more axioms are built in the apparatus of deduction itself;
• while at other ones, the apparatus of deduction does less work, thus more things must be stated explicitly at the start of each deduction.

E.g. the “own”, “professional” axioms of the theory being under consideration (which are responsible for its all peculiarities which makes it the object of investigation) may be required to be a part of each set from which we make deduction, because the deduction machinery itself may be ignorant of them. But the so-called logical axioms (and also the equality axioms) are more likely to be worth of being built into the very definition of the apparatus for deduction.

Metaphor of modularity, reusability

At some frameworks for formalization it may be useful to think of a kind of “modularity” by making a distinction between

• axioms which establish the specific peculiarities of the theory being investigated or axiomatized
• axioms which establish an underlying “background” which can be “reusable”, capable of underlying in the formalization of more other particular theories. They may be thought of as “plugins” or “extensions” to the former group of axioms.

This “plugin”, “separation” should be thought of at a higher level of abstraction, because “physically”, a clear separation may not be provided:

• The logical axioms may be generated using axiom schema on the set of all formulas — thus, not being “independent” of the specific theory (at any rate at this level of abstraction), on the contrary, being built “physically” directly on top of the set of its formulas.
• Also the equality axioms may rely on the signature of the specific theory under consideration (while, “at least”, not being built directly on top of the set of formulas of the specific theory, thus they depend only on the signature, not on the whole set of formulas).

Thus, the idea that we have seen at the distinction of non-logical symbols from logical ones, is manifested also here, but in a more sophisticated form with more precautions.

See also

• First-order logic: Defining first-order logic
• Deductive reasoning: Axiomatization
• Non-logical symbol
• Axiom: Non-logical axioms
• Axiom: Logical axioms
• Hilbert-style deduction system

External links

Modularity, reusability, importance of abstraction:

• John Hughes: Why functional programming matters
• John Hughes: Generalising Monads to Arrows. (See section 3.1 “On Category Theory”, introductory text, pp. 10–11)