Propositions

We start with the basic building blocks of first-order logic: propositions. The collection of propositions is simply a collection of symbols. Common ones are based on the Roman or Greek alphabets, e.g. $$A, B, C ,\ldots \\ \alpha, \beta, \gamma, \ldots$$ But we could just as easily using emoji for our symbols

Right now, they have no meaning attached.

Given a set of propositions, we next need rules to combine them into expressions.

Deduction

The operations we use to combine expressions will reflect oft-occuring structures in human reason. But, we also need to model the common steps in deduction. Here there are two separate roles: assumptions we are given and goals we want to establish (if we can).

In the written (or natural) language, you might see.

Example. If $n$ and $m$ are even integers, then so is $n-m$.

Recall here that the integers are $$\mathbb{Z} = \lbrace \ldots, -2,-1,0,1,2, \ldots \rbrace$$

This could also be written as

Example. Let $n$ and $m$ be even integers. The integer $n-m$ is also an even integer.

While the latter example is not written an explicit if-then the content is the same. Our set of assumptions is $n$ and $m$ are even integers while our goal is $n-m$ is an even integer.

Let’s write down a proof of these statements. We can represent as a table.

Mathematics is well-known for compact (and difficult) notation. In a proof, it is often valuable to unfold the definitions into the statement they represent. We perform this operation on the assumptions.

We also rewrite the goal in the same way.

To achieve our goal, we want to exhibit the desired $e$ using the assumptions at hand. To make progress, we import another “known fact” into the assumptions context: distribution of multiplication over subtraction.

Now we can an apply distribution with $u = 2, v = c, w = d$ to gain another statement and finish.

While we modeled this proof as a table, it is notationally simpler to represent deduction from assumption $A$ to goal $B$ (with some intermediate steps) vertically.

And we write $A \vdash B$ to indicate that we can prove the goal(s) $B$ given the assumption(s) $A$.