We have reached a turning point in our study of logic, as we now begin the review of Deductive Systems in Propositional Logic. This is where everything we’ve covered becomes operational and the true spirit of logic emerges, as we will study the essence of proofs. At this point, it is assumed that you have already learned how to write expressions and understand what propositional logic is about; if it’s not entirely clear, it’s recommended to review the previous classes.

From here, we will review how propositional logic expressions relate to one another to form a deduction. The mechanism through which these relationships are constructed is the formal deductive system.

What is a Formal Deductive System?

Formal deductive systems, or deductive calculus systems, have three basic components:

1. A Formal Language.
2. An Axiomatic Scheme.
3. Basic Inference Rules.

We have already reviewed formal languages. Now it’s time to introduce axiomatic schemes and basic inference rules.

To build the deductive system for propositional calculus, we will start by constructing the deductive system from the Axioms of Łukasiewicz, and use Modus Ponens as the basic inference rule.

Łukasiewicz’s Axioms for Propositional Logic

If \alpha, \beta and \gamma are propositional calculus expressions, then the following are axioms of propositional calculus:

Modus Ponens: The Deductive Engine of Propositional Calculus

If \alpha and \beta are valid propositional calculus expressions, then modus ponens states that from \alpha and (\alpha \rightarrow \beta), \beta is deduced. In reasoning form, this is written as follows:

Here, Modus Ponens is abbreviated between steps (1) and (2) using “MP(1,2)”, and the synthesis of all this is represented by the notation:

Therefore, \{\alpha, (\alpha \rightarrow \beta)\}\vdash \beta

We will soon see that all the deduction techniques of propositional calculus can be constructed from Łukasiewicz’s axioms and Modus Ponens, which synthesize the basic rules of usual reasoning and form the foundational basis of classical logic.

Reasoning, Theorems, and Premises

In the deductive systems of propositional logic, reasoning (or deductions) are performed, and these are any sequence of expressions where each is either a premise or an expression obtained from the premises using only Łukasiewicz’s axioms and modus ponens. A theorem is the result of a deduction without premises. A premise can be any expression that is neither an axiom nor derived from them. In general, when we have a set of premises \Gamma and an expression \alpha that is derived using some element of \Gamma, the axioms, and modus ponens, we write “\Gamma \vdash \alpha” and say

from \Gamma, \alpha is deduced

If \Gamma is an empty set, then instead of writing “\emptyset\vdash \alpha“, we write “ \vdash \alpha “. This reads “\alpha is a theorem”. This form of representing theorems can be extended to represent axioms such that if \alpha, \beta, and \gamma are expressions, then Łukasiewicz’s axioms can be written as follows:

Thus, axioms are said to be self-evident statements, or theorems are expressions inferred from nothing, meaning axioms and theorems are properties of propositional calculus.

How to Perform a Proof in Propositional Logic

At this point, we will move from theory to practice. And when it comes to performing a proof, many things can be said; however, no matter how brilliant the statements about deductive systems and propositional logic, understanding them does not necessarily imply the development of the necessary skills to perform a proof. For this reason, to teach how to make proofs, we will review the proof of a simple theorem.

Theorem

If \alpha is a propositional logic expression, then it follows that

\vdash (\alpha\rightarrow \alpha)

Proof

Therefore, \vdash (\alpha\rightarrow\alpha)

End of the proof.

As you can see, in deductive systems and propositional logic, proofs are far from trivial, but once built, they are easy to replicate.

Now, before diving into making deductions with these techniques, we will first develop some properties and definitions that will be extremely useful for this task, as reasoning only with this will lead to terrible problems.

The Concept of Proved Equivalence

If \alpha and \beta are any expressions, and it holds that both \{\alpha\}\vdash \beta and \{\beta\} \vdash \alpha, then \alpha and \beta are said to be proved equivalent, and this is written as \alpha \dashv \vdash \beta. This is symbolically summarized as:

\left(\{\alpha\}\vdash\beta \wedge \{\beta\}\vdash\alpha \right) \Leftrightarrow \left(\alpha\dashv\vdash\beta\right)

This is a meta-property of propositional logic.

The Deduction (Meta)Theorem

If \alpha and \beta are propositional calculus expressions and \Gamma is a set of premises, then it follows that if from \Gamma \cup \{\alpha\} \beta is deduced, then from \Gamma it is deduced (\alpha \rightarrow \beta). Symbolically, this is expressed as:

\left(\Gamma \cup \{\alpha\}\vdash \beta \right) \Rightarrow \left( \Gamma\vdash(\alpha\rightarrow\beta)\right)

Proof:

To satisfy \Gamma \cup \{\alpha\}\vdash \beta, it is necessary to have a deduction of the form:

Therefore, \Gamma\cup\{\alpha\} \vdash \beta

To achieve this, at least one of the expressions \gamma_1, \cdots \gamma_n,\overline{\gamma_1},\cdots,\overline{\gamma_m} must be of the form (\alpha\rightarrow \beta), but all these steps only involve elements of \Gamma and Łukasiewicz’s axioms in their deduction. Therefore, it must be that \Gamma\vdash (\alpha \rightarrow \beta), thus proving the theorem.

End of the proof.

The Reciprocal of the Deduction Theorem

Under the same conditions as the deduction theorem, it follows that:

\left(\Gamma\vdash(\alpha \rightarrow \beta)\right) \Rightarrow \left( \Gamma \cup \{\alpha\}\vdash \beta \right)

Proof:

If it is satisfied that \Gamma\vdash (\alpha\rightarrow \beta), then a deduction of the form is obtained:

Now, if we add \alpha as a premise to this reasoning, we will have the following steps:

Therefore, \Gamma \cup \{\alpha\} \vdash \beta

Which is what we wanted to prove.

End of the proof.

Deductions on Expressions and Deductions on Deductions

Proofs like the one we previously performed to obtain the result \vdash (\alpha\rightarrow \alpha) are cases of deductions based on expressions, where each step contains a specific expression. Similarly, deductions can be made based on other deductions, where each step is itself a deduction. In practice, both are done analogously, but the latter allows us to use the deduction theorem and its reciprocal, providing great flexibility to reasoning techniques. To see this, let’s prove again that \vdash (\alpha \rightarrow \alpha), but this time using deductions instead of expressions. An alternative approach is as follows:

Note that this reasoning is not shorter than the one we had done earlier, but it is much easier to perform; we only rely on the deduction theorem, its reciprocal, and the A1 axiom scheme to build the proof.

It may seem that in the reasoning we just performed, we used only one of Łukasiewicz’s axioms and ignored both the other axioms and modus ponens. Does this imply that by reasoning in this way, we forget the other axioms and modus ponens? The answer is both yes and no. On one hand, we can act as if we’ve forgotten some axioms and modus ponens simply because we are not explicitly using them; however, it must be remembered that both the deduction theorem and its reciprocal are direct consequences of Łukasiewicz’s axioms and modus ponens, which implies that by using them, as we did in the reasoning above, we are implicitly using those axioms and modus ponens.

Monotonicity Rule

If \tau is a theorem, then for any expression \beta, it holds that

\{\beta\}\vdash\tau

This is a very easy rule to prove since \tau being a theorem means that \vdash \tau. That is, there exists a reasoning that leads to the expression \tau without needing any additional premises, so adding another expression to the premises (empty) makes no difference.

Similarly, we can propose the following result: if from a set of premises \Gamma, \gamma is inferred, then it holds that:

\Gamma\cup\{\alpha\}\vdash\gamma

Where \alpha is any expression.

Synthesis and Reflections on Deductive Systems and Propositional Logic

When we provide the language of propositional logic with an inference rule and basic expressions: Modus Ponens and Łukasiewicz’s Axioms, we are doing something analogous to building a “deductive machine” and a “motor that powers it.” From here, all the basic deduction rules naturally emerge, and we will begin to review them in the lessons immediately following this one.

One more detail. The expressions of propositional logic are, in fact, meta-expressions of the two-symbol language we saw earlier. Remember, the beauty of these meta-expressions lies in their ability to substitute their meta-variables with any expression of the language to obtain a new one that satisfies that structure. When we endow propositional logic language with axiomatic schemes and inference rules, we construct the Deductive Systems of propositional logic, allowing for deductions that connect expressions. The result is a deductive framework capable of encompassing infinite deductions: all those that can be obtained by substituting meta-variables with any expressions we choose. The power of logic truly unleashes when we realize that beyond the two-symbol language expressions we initially used, we see what happens when we substitute them with expressions from our usual language.