2.3 Propositional Calculus: \(P_2\)

The formal system that we are going to be using for Propositional Logic was built by Jan Łukasiewicz and is called \(P_2\). \(P_2\) is actually an improvement over another system proposed by Frege: not only did he remove a redundant axiom schema that could be proved by the others, but he also managed to replace 3 other axiom schemas by a single one.

Behold \(P_2\)'s axiom schemas:

• \(A_1\): \(\varphi\rightarrow(\psi\rightarrow\varphi)\)
• \(A_2\): \([\varphi\rightarrow(\psi\rightarrow\eta)]\rightarrow[(\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\eta)]\) \(\qquad\longrightarrow\) you may call this implication distributivity
• \(A_3\): \((\neg\varphi\rightarrow\neg\psi)\rightarrow(\psi\rightarrow\varphi)\) \(\qquad\qquad\qquad\qquad\ \ \longrightarrow\) you may call this contraposition

\(P_2\) has a single inference rule called Modus Ponens (abbreviated as MP): \(\vdash\varphi\) and \(\vdash\varphi\rightarrow\psi\) \(\Rightarrow\) \(\vdash\psi\)

Remarks:

• This isn't the original version of \(P_2\), but another that is believed to be due to John von Neumann (according to Raymond M. Smullyan's A Beginner's Guide to Mathematical Logic). The original \(P_2\) system uses axioms instead of axiom schemas. The difference is that in the axioms, the symbols that aren't logical connectives stand for statement letters, whereas in the axiom schemas, they stand for metavariables. Since metavariables stand for any wff of your choice, an axiom schema stands for an infinite amount of axioms. The reason that an axiom schema is preferrable to an axiom is simply that if we were to use axioms, we would require an additional inference rule which would allow us to replace any statement letter by a wff. In the following chapters, we'll always be working with metavariables
• You may realize that the only logical connectives that appear in the axiom schemas are \(\neg\) and \(\rightarrow\). It's then impossible to create any statement containing any other connective. Indeed, when using \(P_2\), we restrict our list of logical connectives to only these two and treat the others as abbreviations in the metalanguage:
• \(A \land B\) stands for \(\neg(A \rightarrow\neg B)\)
• \(A \lor B\) stands for \(\neg A \rightarrow B\)
• \(A \oplus B\) stands for \((\neg A \land B) \lor (A \land\neg B) \lor (\neg A \land\neg B)\)
• \(A \leftarrow B\) stands for \(B \rightarrow A\)
• \(A \leftrightarrow B\) stands for \((A \rightarrow B) \land (A \leftarrow B)\)
• \(A \uparrow B\) stands for \(A \rightarrow \neg B\)
• \(A \downarrow B\) stands for \(\neg(\neg A \rightarrow B)\)
• \(A \not\rightarrow B\) stands for \(\neg(A \rightarrow B)\)
• \(A \not\leftarrow B\) stands for \(\neg(A \leftarrow B)\)
• \(A \not\leftrightarrow B\) stands for \(\neg(A \leftrightarrow B)\)

These abbreviations do make sense from the semantics standpoint, as if you compare their truth tables, they are equivalent.

• These axiom schemas are called logical axiom schemas, because they are purely logical. After the chapter on Propositional Logic, we are going to work with more axioms along with the logical ones to study other mathematical subjects, like set theory, number theory or group theory. Such additional axioms are called non-logical axioms

At this point, we don't know much about the properties of this formal system. By the way, you may be wondering why I'm even bothering with a formal system in the first place. Besides the intent to model our reasoning and mathematically study it, the reason is that I want a way to prove whether any given wff is a tautology, i.e. a wff that always evaluates to true regardless of the truth value of any of its most basic subformulas. Sure, we could simply check that with truth tables, but the problem with that brute-force approach is that the number of the table's rows exponentially increases with the number of most basic subformulas. It would then be useful to devise a faster way to check for tautologies, and that's where formal systems come in. Another reason for using formal systems, is that after the chapter about Propositional Logic, we'll eventually tackle the chapter on First-Order Logic, in which truth tables will be virtually useless.

The Modus Ponens rule is pretty intuitive, but the choice of axiom schemas may seem obscure. The main reason why the choice of considering \(\neg\) and \(\rightarrow\) as the only connectives of our language has been made is that they work really well in systems possessing Modus Ponens as an inference rule. In the following chapters, we'll justify \(P_2\)'s design by proving that it does satisfy some desirable properties, namely

• Soundness: the system is by definition sound if it can only prove true theorems
• Consistency: the system is by definition consistent if it cannot prove both \(A\) and \(\neg A\)
• Completeness: the system is by definition complete if any true theorem is provable
• Decidability: the system is by definition decidable if there is an algorithm to determine whether arbitrary wffs are theorems of the system
• Independence: the list of axioms/axiom schemas is by definition independent if no axiom/axiom schema can be proved from another

Just be aware that the soundness, consistency, completeness, decidability and independence theorems are metatheorems and are then going to be informally, though rigorously proven.

Before ending this chapter, I just want to warn you one last time not to mix syntax and semantics. For example, a mistake that I was tempted to make when I started learning about formal proofs was that whenever I had an wff with two negation symbols, say \(\neg\neg\varphi\), I sometimes would for example want to write

Even if I had previously shown that \(\neg\neg\varphi \vdash \varphi\), this wouldn't justify replacing \(\neg\neg\varphi\) by \(\varphi\) in the middle of a wff. The reason why I made that mistake is that semantically, \(\neg\neg\varphi\) and \(\varphi\) have the same truth value. However, our system doesn't have a rule of inference that allows us to do that. Maybe such a rule could be proven as a metatheorem, but until then, it's illegal to use it!

Sources:

• Hilbert systemWikipedia
• Introduction to Mathematical LogicEliott Mendelson