I am going to make this blogpost a bit different. I am going to make it a bit “fun”, and less proof/theorem.

Any propositional variables can be assigned a truth (\(T\)) or falsehood (\(F\)) value through a mapping \(f : \Phi \rightarrow \{T,F\}\). Where \(\Phi\) is a set of all propositional variables.  We can show that it’s more general than this, i.e. \(\Phi\) can be a set that contains all eff
—– HOW?—-
The values can be retrieved through \(f_x\), where we have

1. \(f_{x}p = f(p)\) for some propositional variable \(p\)
2. \(f_{x} \sim B = \sim f_{x} \sim B\) for some wff \(B\).
3. \(f_{x} [B \vee C] =  f_{x} B \vee f_{x} C\) for some wffs \(B, C\).

Facts

1. For some wff \(A\), we write \(\vDash A\) and say that \(A\) is a tautology if \(f_{x} A = T\) for any assignment (\(x\)) I make to the internal statements. That is to say that \(A\) evaluates to true probably because of its structure and not its content.
2. If a wff \(A\) always evaluates to F, then we say \(A\) is a contradiction.
3. \(A\) implies \(B\) iff \(\vDash A \Rightarrow B\)
4. \(A\) is equivalent to \(B\) iff \(A \equiv B\) is a tautology.

This is an episode in a series on mathematical logic approached with some rigour. Here, we will (still) be closely following the book by Peter B. Andrews: An Introduction To Mathematical Logic and Type Theory. We will look at the axiomatic structure of a logistic system we’ve been working on. The previous blogpost can be found here: (S1E01): The Rules.

An axiom is a statement that is taken to be true. The system we’ve been building from (S1E01) (called \(\mathcal{P}\)) consists of well-formed formulas having one of the following

(S1E02) (Sc0) axiomatic schemas:

1. \(A \lor A \Rightarrow A\)
2. \(A \Rightarrow B \lor A\)
3. \(A \Rightarrow B \Rightarrow (C \lor A) \Rightarrow (B \lor C)\)

We then also have just one primitive rule of inference:

1. Modus Ponens
   For some wff \(Q\), if it is accepted and is of the form \(A \Rightarrow B\), then we can infer \(B\), given \(A\) holds. \(A,\; and \;B\) are wffs.
   Example: Let \(Q =\) If it is an evergreen tree, then it doesn’t loose leaves in winter and its leaves are always green.

The Pilot. 

This is an episode in a series on mathematical logic approached with some rigour. Here, we will be closely following the book by Peter B. Andrews: An Introduction To Mathematical Logic and Type Theory. In this episode, we will:

Part 1

1. Learn about well-formed formulas.
2. Show the equivalence of the well-formed formula definition to that of a formation sequence on a formula.
3. Revisit the principle of mathematical induction and complete induction on the natural numbers.
4. Learn the principle of induction on the construction of a well-formed formula.

Part 2

1. Learn about substitutions in the context of propositional logic. And use this idea to derive one of De Morgan’s Laws.

The only knowledge this post will assume is a basic knowledge in set theory.

Part 1.

(The Prelude) Before we start with logic, let’s revise two ideas which may serve to be important later on. If one is familiar with the principle of mathematical induction and strong induction, one may skip this.…

Knowledge this posts assumes: What is a set, set cardinality, a function, an image of a function and an injective (one-to-one) function.

David Hilbert imagines a hotel with an infinite number of rooms. In this hotel, each room can only be occupied by one guest, and each room is indeed occupied by exactly one guest. What happens if more guests show up? Can they be accommodated for?

PAUSE: WHAT DO YOU THINK AND WHY?

Suppose we propose they cannot be accommodated for, since all the rooms are occupied. Hilbert then claims that he can define the functions \(f:A \mapsto B,\) and \(g:B \mapsto C,\) where \(A\) is a set containing all current guests, and \(f\) simply maps each guest to a room in the set \(B\), and \(g\) maps each room in \(B\) to a new one in \(C\). Notice that these functions must be injective, since if a room contains two different guests, those two different guests must be the same guest; recall \(f(a) = f(b) \rightarrow a = b\).…