Using PL to Describe Properties of Systems
View
This is a book resource with multiple pages. Navigate between the pages using the buttons.
Example 1. Simple axiom system
Let , where , , , are defined as follows:
- The functionally complete set of logical operators (logical connectives and negation) is as follows. Of the three connectives for conjunction, disjunction, and implication (, and →), one can be taken as primitive and the other two can be defined in terms of it and negation (¬). Alternatively, all of the logical operators may be defined in terms of a sole sufficient operator, such as the Sheffer stroke (nand). The biconditional () can of course be defined in terms of conjunction and implication as .
Adopting negation and implication as the two primitive operations of a propositional calculus is tantamount to having the omega set partition as follows:
Then is defined as , and is defined as .
- The set (the set of initial points of logical deduction, i.e., logical axioms) is the axiom system proposed by Jan Łukasiewicz, and used as the propositional-calculus part of a Hilbert system. The axioms are all substitution instances of:
- The set of transformation rules (rules of inference) is the sole rule modus ponens (i.e., from any formulas of the form and , infer ).
This system is used in Metamath set.mm formal proof database.