# Predicate logic: How do you self-check the logical structure of your own arguments?

In propositional logic, there are truth tables. So you can check if the logical structure of your argument is, not correct per se, but if it's what you intended it to be.

In predicate logic, I have seen no reference to truth tables, nor have I seen any use (literal use) of truth tables when searching for examples where truth tables are used in PL.

It would be nice to check the logical structure of my own arguments, as I will not always have someone to validate my own work. I plan on employing my skills in logic, but I want a sure fire way to ensure that my form is correct :)

• There are well-known rules of inference. Mar 3, 2016 at 19:03
• There are several proof verification software packages that are available free online. Mar 4, 2016 at 4:53
• Starting from a set of axioms, you can carry out your proof in some Hilbert style deduction system. In fact, "natural" proofs (those that we use on a daily basis) can be thought of as instructions to build a formal deduction in the Hilbert calculus... Mar 5, 2016 at 14:26

Truth tables are not enough to capture first-order logic (with quantifiers), so we use inference rules instead. Each inference rule is chosen to be sound, meaning that if you start with true statements and use the rule you will deduce only true statements. We say that these rules are truth-preserving. If you choose carefully enough, you can make it so that the rules are not just truth-preserving but also allow you to deduce every (well-formed) statement that is necessarily true (in all situations).

What you are probably looking for (namely a practical way to rigorously check the logical validity of your arguments) is natural deduction. There are many different styles, the most intuitive type being Fitch-style, which mark subcontexts using indentation or some related visual demarcation. The following system uses indentation and follows the intuition most closely in my opinion. $$\def\block#1{\begin{array}{ll}\ &{#1}\end{array}} \def\fitch#1#2{\begin{array}{|l}#1\\\hline#2\end{array}} \def\sub#1#2{\text{#1}:\\\block{#2}} \def\imp{\Rightarrow} \def\eq{\Leftrightarrow} \def\nn{\mathbb{N}} \def\none{\varnothing} \def\pow{\mathcal{P}}$$

## Contexts

Every line is either a header or a statement. We shall put a colon after each header and a full-stop after each statement. Each header specifies some subcontext (contained by the current context), and the lines governed by that header is indicated by the indentation. The full context of each line is specified by all the headers that govern it (i.e. all the nearest headers above it at each lower indentation level).

For example a nested case analysis might look like:

$$\sub{If A}{\sub{If B}{...} \\ \sub{If ¬B}{...}} \\ \sub{If \neg A}{...}$$

And reasoning about an arbitrary member of a collection $$S$$ would look like:

$$\sub{Given x{∈}S}{...}$$

Note that what is stated in some context may be invalid in other contexts. Once you understand the principle behind contexts and the indentation, the following rules are very natural. Also note that for first-order logic these two kinds of context headers (for conditional subcontexts and universal subcontexts respectively) are the only kinds needed.

## Syntax rules

A statement must be an atomic (indivisible) proposition or a compound statement formed in the usual way using boolean operations or quantifiers, with the restriction that every variable that is bound by a quantifier is not already used to refer to some object in the current context, and that there are no nested quantifiers that bind the same variable.

## Natural deduction rules

Each inference rule is of the form:

$$\fitch{\text{X}}{\text{Y}}$$

which means that if the last lines you have written match "X" then you can write "Y" immediately after that at the same level of indentation. Each application of an inference rule is also tied to the current context, namely the context of "X". We will not mention "current context" all the time.

## Boolean operations

Take any statements $$A,B,C$$ (in the current context).

restate: If we prove something we can affirm it again in the same context.

$$\fitch{A.\\ ...}{A.}$$

Note that "$$...$$" denote any number of lines that are at least at the depicted indentation level. In the above rule, this means that all the lines written since the earlier writing of "$$A.$$" must be in the same context (or some subcontext).

In practice we never actually write the same line twice. To indicate that we can omit a line in a proof, I'll mark it with square-brackets like this:

$$\fitch{A. \\ ...}{[A.]}$$

⇒sub       ⇒restate     (We can create a conditional subcontext where $$A$$ holds.)

$$\fitch{}{\sub{If A}{[A.]}}$$$$\fitch{B. \\ ... \\ \sub{If A}{...}}{\block{[B.]}}$$

⇒intro       ⇒elim

$$\fitch{\sub{If A}{... \\ B.}}{[A \imp B.]}$$$$\fitch{A \imp B. \\ A.}{B.}$$

∧intro     ∧elim

$$\fitch{A. \\ B.}{A \land B.}$$$$\fitch{A \land B.}{[A.] \\ [B.]}$$

∨intro     ∨elim

$$\fitch{A.}{[A \lor B.] \\ [B \lor A.]}$$$$\fitch{A \lor B. \\ A \imp C. \\ B \imp C.}{C.}$$

¬intro     ¬elim     ¬¬elim

$$\fitch{A \imp \bot.}{\neg A.}$$$$\fitch{A. \\ \neg A.}{\bot.}$$$$\fitch{\neg \neg A.}{A.}$$

Note that by using ¬intro and ¬¬elim we can get the following additional inference rule:

$$\fitch{\neg A \imp \bot.}{A.}$$

which corresponds to how one would attempt to prove $$A$$ by contradiction, namely to show that assuming $$\neg A$$ implies a falsehood.

⇔intro     ⇔elim

$$\fitch{A \imp B. \\ B \imp A.}{A \eq B.}$$$$\fitch{A \eq B.}{[A \imp B.] \\ [B \imp A.]}$$

## Quantifiers and equality

The rules here are for restricted quantifiers because usually we think in terms of them. First we need some definitions.

Used variable: A variable that is declared in the header of some containing ∀-context or declared in some previous ∃-elimination ("let") step in some containing context.

Unused variable: A variable that is not used.

Fresh variable: A variable that does not appear in any previous statement in any containing context.

Object expression: An expression that refers to an object (e.g. a used variable, or a function-symbol applied to object expressions).

Property with $$k$$ parameters: A string $$P$$ with some blanks where each blank has some label from $$1$$ to $$k$$, such that replacing each blank in $$P$$ by some object expression yields a statement. If $$k = 2$$, then $$P(E,F)$$ is the result of replacing each blank labelled $$1$$ by $$E$$ and replacing each blank labelled $$2$$ by $$F$$. Similarly for other $$k$$.

In this section, $$E,F$$ (if involved) can be any object expressions (in the current context).

We start with the following rules that provide a type of all objects.

universe: $$obj$$ is a type.

$$\fitch{}{[E{∈}obj.]}$$

Now take any type $$S$$ and a 1-parameter property $$P$$ and an unused variable $$x$$ that does not appear in $$S$$ or $$P$$.

∀sub           ∀restate         (We can create a ∀-subcontext in which $$x$$ is of type $$S$$.)

$$\fitch{}{\sub{Given x{∈}S}{[x{∈}S.]}}$$$$\fitch{A. \\ ... \\ \sub{Given x{∈}S}{...}}{\block{[A.]}}$$ ($$x$$ must not appear in $$A$$)

∀intro           ∀elim

$$\fitch{\sub{Given x{∈}S}{... \\ P(x).}}{\forall x{∈}S\ ( \ P(x) \ ).}$$$$\fitch{\forall x{∈}S\ ( \ P(x) \ ). \\ E{∈}S.}{P(E).}$$ ($$E$$ must not share any unused variables with $$P$$)

∃intro           ∃elim

$$\fitch{E{∈}S. \\ P(E).}{\exists x{∈}S\ ( \ P(x) \ ).}$$$$\fitch{\exists x{∈}S\ ( \ P(x) \ ).}{\text{Let y{∈}S such that P(y)}. \\ [y{∈}S.] \\ [P(y).]}$$ (where $$y$$ is a fresh variable)

=intro       =elim

$$\fitch{}{[E=E.]}$$$$\fitch{E=F. \\ P(E).}{P(F).}$$ ($$F$$ must not share any unused variable with $$P$$)

## Variable renaming

Finally, the following rules for variable renaming are redundant, but would shorten proofs.

∀rename         ∃rename

$$\fitch{\forall x{∈}S\ ( \ P(x) \ ).}{[\forall y{∈}S\ ( \ P(y) \ ).]}$$$$\fitch{\exists x{∈}S\ ( \ P(x) \ ).}{[\exists y{∈}S\ ( \ P(y) \ ).]}$$

(where $$y$$ is an unused variable that does not appear in $$P$$)

## Short-forms

For convenience we write "$$\forall x,y{∈}S\ ( \ P(x,y) \ )$$" as short-form for "$$\forall x{∈}S\ ( \ \forall y{∈}S\ ( \ P(x,y) \ ) \ )$$", and similarly for more variables and for "$$\exists$$". We shall also compress nested ∀-subcontext headers in the following form:

$$\sub{Given x{∈}S}{\sub{Given y{∈}S}{...}}$$

to:

$$\sub{Given x,y{∈}S}{...}$$

Additionally, "$$\exists! x{∈}S\ ( \ P(x) \ )$$" is short-form for "$$\exists x{∈}S\ ( \ P(x) \land \forall y{∈}S\ ( \ P(y) \imp x=y \ ) \ )$$".

## Example

Here is an example, where $$S,T$$ are any types and $$P$$ is any property with two parameters.

First with all lines shown:

If $$\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ )$$:   [⇒sub]
$$\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ )$$.   [⇒sub]
Let $$a{∈}S$$ such that $$\forall y{∈}T\ ( \ P(a,y) \ )$$.   [∃elim]
$$a{∈}S$$.   [∃elim]
$$\forall y{∈}T\ ( \ P(a,y) \ )$$.   [∃elim]
$$\forall z{∈}T\ ( \ P(a,z) \ )$$.   [∀rename]
Given $$y{∈}T$$:   [∀sub]
$$y{∈}T$$.   [∀sub]
$$\forall z{∈}T\ ( \ P(a,z) \ )$$.   [∀restate]
$$y{∈}T$$.   [restate]
$$P(a,y)$$.   [∀elim]
$$a{∈}S$$.   [∀restate]
$$\exists x{∈}S\ ( \ P(x,y) \ )$$.   [∃intro]
$$\forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$$.   [∀intro]
$$\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ ) \imp \forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$$.   [⇒intro]

Finally with all lines in square-brackets removed:

If $$\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ )$$:   [⇒sub]
Let $$a{∈}S$$ such that $$\forall y{∈}T\ ( \ P(a,y) \ )$$.   [∃elim]
Given $$y{∈}T$$:   [∀sub]
$$P(a,y)$$.   [∀elim]
$$\exists x{∈}S\ ( \ P(x,y) \ )$$.   [∃intro]
$$\forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$$.   [∀intro]
$$\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ ) \imp \forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$$.   [⇒intro]

This final proof is clean yet still easily computer-verifiable.

## Definitorial expansion

To facilitate definitions, which can significantly shorten proofs, we also have the following definitorial expansion rules.

For each $$k$$-parameter property $$P$$ and fresh predicate-symbol $$Q$$:

$$\fitch{}{\text{Let Q(x_1,...x_k) ≡ P(x_1,...x_k) for each x_1{∈}S_1 and ... and x_k{∈}S_k.} \\ [∀x_1{∈}S_1\ \cdots ∀x_k{∈}S_k\ ( \ Q(x_1,...x_k) ⇔ P(x_1,...x_k) \ ).]}$$

For each $$(k+1)$$-parameter property $$R$$ and fresh function-symbol $$f$$:

$$\fitch{∀x_1{∈}S_1 \cdots ∀x_k{∈}S_k\ ∃!y{∈}T ( \ R(x_1,...x_k,y) \ ) } {\text{Let f : S_1{×}{\cdots}{×}S_k{→}T such that R(x_1,...x_k,f(x_1,...x_k)) for each x_1{∈}S_1 and ... and x_k{∈}S_k.} \\ [∀x_1{∈}S_1\ \cdots ∀x_k{∈}S_k\ ( \ f(x_1,...x_k)∈T ∧ R(x_1,...x_k,f(x_1,...x_k)) \ ).]}$$

These rules are redundant in the sense that any statement you can prove that does not use any of the new symbols can be proven without using definitorial expansion.

## Notes

The above rules avoid the usual trouble that many other systems have, where variables used for witnesses of existential statements must be distinguished from variables used for arbitrary objects. The reason is that every variable here is either specified by a ∀-subcontext or by a "let"-statement; in other words there are no free variables. The fact that every variable is bound is strongly related to the fact that this system allows an empty universe, if there are no other axioms.

Also, every variable is specified by a unique header or "let"-statement in the current context; in other words there is no variable shadowing. This is by design, and in actual mathematical practice we also abide by this, though most other formal systems do not. As a consequence, sentences such as "$$\exists x\ \forall x\ ( x=x )$$." simply cannot be written down in this system. If you wish to permit such kind of terrible sentences, you would have to modify the rules appropriately, but it will most probably cause a headache.

Finally, there were some subtle technical decisions. For the quantifier rules, the reason I required that $$x$$ does not appear in $$S,P$$ is that, if we later on include rules for specifying types, we would usually have variable names in its syntax, which would cause problems. For example, if we have written in the current context "$$x∈\{y:y∈S∧y∈T\}$$" and "$$x∈U$$", it will not be sensible to allow writing "$$∃y∈U\ ( y∈\{y:y∈S∧y∈T\} )$$". Similarly, if we have written "$$x=\{y:P(y)\}$$" and "$$∃y∈U\ ( Q(x,y) )$$", we do not want to allow writing "$$∃y∈U\ ( Q(\{y:P(y)\},y) )$$".

Also, to allow a variable to become fresh again after leaving the subcontext in which it was declared, I required that the ⇒intro and ∀intro rules can be applied only immediately after the corresponding ⇒-subcontext or ∀-subcontext. It would be simpler to simply define a fresh variable as one that does not appear in any previous line, but then we can easily run out of fresh variable names in a long proof.

~ ~ ~ ~ ~ ~ ~

To illustrate the flexibility of this system, I will express both Peano Arithmetic and Set Theory as extra rules that can be simply added to the system.

## Peano Arithmetic

Add the type $$\nn$$ and the symbols of PA, namely the constant-symbols $$0,1$$ and the $$2$$-input function-symbols $$+,·$$ and the $$2$$-input predicate-symbol $$<$$.

Add the axioms of PA$$^-$$, adapted from here:

• $$\forall x,y{∈}\nn\ ( \ x+y ∈ \nn \ )$$.
• $$\forall x,y{∈}\nn\ ( \ x·y ∈ \nn \ )$$.
• $$\forall x,y{∈}\nn\ ( \ x+y=y+x \ )$$.
• $$\forall x,y{∈}\nn\ ( \ x·y=y·x \ )$$.
• $$\forall x,y,z{∈}\nn\ ( \ x+(y+z)=(x+y)+z \ )$$.
• $$\forall x,y,z{∈}\nn\ ( \ x·(y·z)=(x·y)·z \ )$$.
• $$\forall x,y,z{∈}\nn\ ( \ x·(y+z)=x·y+x·z \ )$$.
• $$\forall x{∈}\nn\ ( \ x+0=x \ )$$.
• $$\forall x{∈}\nn\ ( \ x·1=x \ )$$.
• $$\forall x{∈}\nn\ ( \ \neg x.
• $$\forall x,y{∈}\nn\ ( \ x.
• $$\forall x,y,z{∈}\nn\ ( \ x.
• $$\forall x,y,z{∈}\nn\ ( \ x.
• $$\forall x,y,z{∈}\nn\ ( \ x.
• $$\forall x,y{∈}\nn\ ( \ x.
• $$0<1$$.
• $$\forall x{∈}\nn\ ( \ 0=x \lor 1=x \lor 1.

Add the induction axioms, namely for each property $$P$$ involving only the symbols of PA and quantifiers over $$\nn$$ add the following axiom (where $$k$$ does not appear in $$P$$):

• $$P(0) \land \forall k{∈}\nn\ ( \ P(k) \imp P(k+1) \ ) \imp \forall k{∈}\nn\ ( \ P(k) \ )$$.

## Set Theory

Add the type $$set$$ and the rule that every member of $$set$$ is also a type.

Add the unary function-symbols $$\pow,\bigcup$$, the binary function-symbols $$×,→$$, and the constant-symbol $$\none$$. We reuse the binary predicate-symbol $$\in$$, as there will be no ambiguity. Also add the following rules (in every context) for the other notation:

• If $$E,F \in obj$$, then $$(E,F) \in obj$$ and $$\{E,F\} \in set$$.
• If $$S,T \in set$$, then $$S×T \in set$$ and $$(S{→}T) \in set$$ and $$\pow(S) \in set$$.
• If $$S,T \in set$$ and $$f \in (S{→}T)$$ and $$x \in S$$, then $$f(x) \in T$$.
• If $$S \in set$$ and $$\forall x{∈}S\ ( \ x \in set \ )$$, then $$\bigcup(S) \in set$$.

• extensionality:   $$\forall S,T{∈}set\ ( \ S=T \eq \forall x{∈}obj\ ( \ x \in S \eq x \in T \ ) \ ).$$
• empty-set:   $$\forall x{∈}obj\ ( \ \neg x \in \none \ ).$$
• naturals:   $$\nn{∈}set$$.
• power-set:   $$\forall S{∈}set\ ( \ \pow(S) = \{ T : T \in set \land \forall x{∈}T\ ( \ x \in S \ ) \} ).$$
• pair:   $$\forall x,y{∈}obj\ ( \ \{x,y\} = \{ z : x=z \lor x=y \} ).$$
• ordered-pair:   $$\forall x,y{∈}obj\ \forall z,w{∈}obj\ ( \ (x,y)=(z,w) \eq x=z \land y=w \ ).$$
• product-type:   $$\forall S,T{∈}set\ ( \ S×T = \{ t : \exists x{∈}S\ \exists y{∈}T\ ( \ t=(x,y) \ ) \} \ ).$$
• function-type:   $$\forall S,T{∈}set\ ( \ (S→T) = \\ \{ F : F \in \pow(S×T) \land \forall x{∈}S\ \exists! y{∈}T\ ( \ (x,y) \in F \ ) \} \ ).$$
• function-application:   $$\forall S,T{∈}set\ \forall f{∈}(S{→}T)\ \forall x{∈}S\ ( \ (x,f(x)) \in f \ ).$$
• union:   $$\forall S{∈}set\ ( \ \bigcup(S) = \{ x : \exists T{∈}set\ ( \ x \in T \land T \in S \ ) \} \ ).$$
• choice:   $$\forall S,T{∈}set\ \forall R{∈}\pow(S×T)\ ( \ \forall x{∈}S\ \exists y{∈}T\ ( \ (x,y) \in R \ ) \\ \imp \exists f{∈}(S{→}T)\ \forall x{∈}S\ ( \ (x,f(x)) \in R \ ) \ ).$$

type-notation

Take (in the current context) any property $$P$$ and object expression $$E$$ and unused variable $$x$$.

Then $$\{ x : P(x) \}$$ is a type and its membership is governed by:

$$\fitch{}{E \in \{ x : P(x) \} \eq P(E).}$$. ($$x$$ must not appear in $$E$$ or $$P$$)

comprehension

Take any property $$P$$ and unused variable $$x$$.

$$\fitch{S \in set.}{\{ x : x \in S \land P(x) \} \in set.}$$. ($$x$$ must not appear in $$S$$ or $$P$$)

replacement

Take any $$2$$-parameter property $$P$$ and unused variables $$x,y$$.

$$\fitch{S \in set. \\ \forall x{∈}S\ \exists! y{∈}obj\ ( \ P(x,y) \ ).}{\{ y : \exists x{∈}S\ ( \ P(x,y) \ ) \} \in set.}$$ ($$x,y$$ must not appear in $$S$$ or $$P$$)

induction

Take any property $$P$$ with $$1$$ parameter from $$\nn$$.

$$\fitch{P(0). \\ \forall k{∈}\nn\ ( \ P(k) \imp P(k+1) \ ).}{\forall k{∈}\nn\ ( \ P(k) \ ).}$$ ($$k$$ must not appear in $$P$$)

The induction rule subsumes the induction axioms for PA, and essentially the only difference is that the property $$P$$ can involve set operations and quantification over sets.

function-notation

This rule is theoretically unnecessary but pragmatically very convenient (also known as lambda expressions in computer science).

Take any set $$S$$ and any object expression $$E$$ with $$1$$ parameter from $$S$$, and unused variable $$x$$.

Then $$( S\ x \mapsto E(x) )$$ is an object and its behaviour is governed by:

$$\fitch{\forall x{∈}S\ ( \ E(x) \in T \ ). \\ f = ( S\ x \mapsto E(x) ).}{f \in (S→T) \land \forall x{∈}S ( \ f(x) = E(x) \ ).}$$

## Foundational system

Combining the above Peano Arithmetic plus Set Theory yields a foundational system that is essentially as strong as ZFC but much more user-friendly. It is also agnostic to the existence of objects that are not sets, and does not even assume that the members of $$\nn$$ are sets. It also treats cartesian products and ordered pairs as inbuilt abstract notions. This is how we use them in actual mathematics. (More precisely, the above system directly interprets ZFC minus regularity.)

• @user108262: You're welcome and I hope it helps you as much as it has helped me! When I devised these rules I was strongly influenced by programming where the context of every statement is explicit. That really is the key, because it is then simple to construct the inference rules based on intuition. Like in programming, there can be multiple statements within the same context, and this minimizes the amount of writing needed, in stark contrast to Hilbert-style systems. I presented it here in Fitch-style but we can just as well use braces or indentation like in C or Python. Mar 10, 2016 at 0:57
• I decided to update my post with all the rules, and I changed to Python style. The underlying idea is certainly correct, as I've used it for years. But it is a long post and there may be bugs, so if anyone has any question feel free to ask me at chat.stackexchange.com/rooms/44058/logic. Dec 31, 2016 at 17:04
• @Buraian: "fithch" ≠ "Fitch", and my post explicitly links to the wikipedia article describing Fitch-style. A style is not a system, just like the executable file format is not an application software. In any case, the purpose of this post is to present a complete user-friendly foundational system for mathematics, and for that it is actually unimportant to know what style it uses. After you learn to use it, it will become trivially obvious why Fitch-style is better than other styles, but such an understanding only comes after learning it and seeing how unusable alternative systems are. Jan 14 at 9:32
• (I cite Fitch purely for the sake of attribution of credit, not for pedagogy.) Jan 14 at 9:35
• @Buraian: If you want to learn to use this system, you can ask me about it in the Basic Math chat-room. Jan 14 at 9:53