Part Of: Computational Trinitarianism sequence
Content Summary: 700 words, 7 min read
Organizational Principles Of Logic
The ingredients of any system of logic are:
- A proposition is an atomic statement that can acquire a truth value. For example, “Socrates is a man”.
- A connective takes atomic propositions, and melds them into a more complex, composite proposition. For example, AND is a connective.
Propositions, in both atomic and composite form, represent containers for truth valuations. A judgment is a filled container: a proposition assigned a specific truth value (true or false).
But logical systems are not static entities. The heart of any logic is its dynamics: rules which permute its resident propositions.
The IPL System
Once upon a time, logicians tired of the tedious algebraic format of their logical systems. Natural deduction was invented as a graphical alternative to such systems.
In this post, I use the natural deduction format to present one particular system of logic, Intuitionistic Propositional Logic (IPL).
IPL permits the following connectives:
- ∧ (conjunction, “AND”)
- ⊃ (implication)
- ∨ (disjunction, “OR”)
- ⊤ (truth)
- ⊥ (falsity)
Rules can be categorized as follows:
- Introduction rules (constructors) specify how connectives are injected into the system.
- Elimination rules (destructors) describe how connectives are removed from the system.
IPL has ten rules total, five in each category.
Ready to take a look under the hood?
Conjunction (∧) Rules
The ∧ (AND) connective features three rules. In the following visuals, premises (knowledge before rule application) are on top, conclusions (knowledge after rule application) below.
Our first rule is AND-Introduction (∧I). It permits us to glue facts together.
In English: “Before we applied the ∧I rule, suppose we know two facts: A, and B. Afterwards, we know one additional fact: A∧B.”
Next, we have Left-AND-Elimination (∧EL) and Right-AND-Elimination (∧ER). Together, these rules “remove the glue”.
The left rule means: “If we use A∧B, we can use A by itself.”
Implication (⊃) Rules
IMPLICATION-Elimination (⊃E) proceeds fairly intuitively:
IMPLICATION-Introduction (⊃I) is where things get tricky. Consider the weaker version of this rule, on the left.
The ellipsis “..” means that other rules may be injected, the intermediate proof can be hundreds of lines long, if need be. So this weak rule seems intuitive:
If you know A, and from this information can eventually prove B, then you may conclude ‘A implies B’.
However, this version is too simplistic: it allows implications only to be introduced when the antecedent was already assumed. The real rule is more powerful:
If you assume A, and from this information can eventually prove B, then you may conclude ‘A implies B’.
Get the difference? Before, our assumptions were unchanged. But now we expand our assumption set, and denote the location of our assumption-expansion with a line, and name it (in this case, “a”.)
Disjunction (∨) Rules
OR statements only require only one of its terms to be true. If you have evidence for one statement, it doesn’t matter whether the others are true or false.
This intuition is cashed out in the Left-OR-Introduction (∨IL) and Right-OR-Introduction (∨IR) rules.
The left rule means: “If we use A, we can use A∨B.”
Of all the rules in Intuitionistic Propositional Logic, OR-Elimination (∨E) requires the most time to comprehend.
Notice that the last two inputs fit the criteria for implication, and could simplify to A⊃C and B⊃C.
Here is one way to interpret the above rule:
Suppose we know that A∨B.
If it is true that “A implies C” and “B implies C”, then we know C is true.
We know this because at least one component of A∨B must be true!
Truth (⊤) and Falsity (⊥) Rules
IPL includes two rules regarding Truth and Falsity.
The TRUTH-Introduction (⊤I) rule simply means that the system admits trivial truths. There is no TRUTH-Elimination rule.
The FALSITY-Elimination (⊥E) rule reflects the Principle Of Explosion: “from contradiction, anything follows.”
Notice that the IPL System connective for complement (¬). However, Falsity allows the system to express negation regardless: ¬A = A ⊃ ⊥.
In this post, we learned the ten rules which define Intuitionistic Propositional Logic (IPL):
Next time, we’ll use IPL to solve a real problem. 🙂