axiom system for propositional logic
The language of (classical) propositional logic PL consists of a set of propositional letters or variables, the symbol (for falsity), together with two symbols for logical connectives and . The well-formed formulas (wff’s) of PL are inductively defined as follows:
-
•
each propositional letter is a wff
-
•
is a wff
-
•
if and are wff’s, then is a wff
We also use parentheses and to remove ambiguities. The other familiar logical connectives may be defined in terms of : is , is the abbreviation for , is the abbreviation for , and is the abbreviation for .
The axiom system for PL consists of sets of wffs called axiom schemas together with a rule of inference. The axiom schemas are:
-
1.
,
-
2.
,
-
3.
,
and the rule of inference is modus ponens (MP): from and , we may infer .
A deduction is a finite sequence of wff’s such that each is either an instance of one of the axiom schemas above, or as a result of applying rule MP to earlier wff’s in the sequence. In other words, there are such that is the wff . The last wff in the deduction is called a theorem of PL. When is a theorem of PL, we write
For example, , whose deduction is
-
1.
by Axiom II,
-
2.
by Axiom I,
-
3.
by modus ponens on to ,
-
4.
by Axiom I,
-
5.
by modus ponens on to .
More generally, given a set of wff’s, we write
if there is a finite sequence of wff’s such that each wff is either an axiom, a member of , or as a result of applying MP to earlier wff’s in the sequence. An important (meta-)theorem called the deduction theorem, states: if , then . The deduction theorem holds for PL (proof here (http://planetmath.org/deductiontheoremholdsforclassicalpropositionallogic))
Remark. The axiom system above was first introduced by Polish logician Jan Łukasiewicz. Two axiom systems are said to be deductively equivalent if every theorem in one system is also a theorem in the other system. There are many axiom systems for PL that are deductively equivalent to Łukasiewicz’s system. One such system consists of the first two axiom schemas above, but the third axiom schema is , with MP its sole inference rule.
Title | axiom system for propositional logic |
---|---|
Canonical name | AxiomSystemForPropositionalLogic |
Date of creation | 2013-03-22 19:31:50 |
Last modified on | 2013-03-22 19:31:50 |
Owner | CWoo (3771) |
Last modified by | CWoo (3771) |
Numerical id | 13 |
Author | CWoo (3771) |
Entry type | Definition |
Classification | msc 03B05 |
Synonym | axiom system for classical propositional logic |
Related topic | DeductionTheoremHoldsForClassicalPropositionalLogic |
Related topic | SubstitutionTheoremForPropositionalLogic |