Dtyjlui

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 :)

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.
$
defblock#1{begin{array}{ll} &{#1}end{array}}
deffitch#1#2{begin{array}{|l}#1\hline#2end{array}}
defsub#1#2{text{#1}:\block{#2}}
defimp{Rightarrow}
defeq{Leftrightarrow}
defnn{mathbb{N}}
defnone{varnothing}
defpow{mathcal{P}}
$

Contexts

Every line is either a header or a statement. Only headers can have lines subsumed under it, as in a multi-level list. The context of each statement is specified by all the headers that are in effect.

For example a case analysis would look like:

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

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

  $sub{Given $x in 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 the above 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, which is defined to be 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, but to make the description of the rules easy we shall to consider it written anyway. I'll mark all such lines with square-brackets as follows:

  $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     ("$imp$" internally captures contextual statements.)

  $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

I show the rules for restricted quantifiers because usually we think in terms of them. First we need some definitions.

Unused variable: A variable that is not declared in the header of any containing ∀-subcontext or in any previous ∃-elimination ("let") step in the current context or any containing contexts.

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

Object expression: An expression that refers to an object. In classical first-order logic, the object expressions are simply the well-formed terms (whose free variables are each declared in the header of some containing ∀-subcontext). In the following rules $E,F$ (if involved) can be any object expressions.

And we need at least one type over which we can quantify, which is provided by the following rule.

universe: $obj$ is a type, which includes all objects.

  $fitch{}{[E in obj.]}$

Now take any type $S$ and a property $P$ and an unused variable $x$ that does not appear in $S$ or $P$. By $P$ being a property we mean that $P(x)$ is a statement about $x$.

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

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

∀intro         ∀elim

  $fitch{sub{Given $x in S$}{... \ P(x). \ ...} \ ...}{forall x in S ( P(x) ).}$
  $fitch{forall x in S ( P(x) ). \ ... \ E in S. \ ...}{P(E).}$ (unused variables appearing in $P$ must not appear in $E$)

∃intro           ∃elim

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

=intro       =elim

  $fitch{}{[E=E.]}$
  $fitch{E=F. \ P(E).}{P(F).}$ (unused variables appearing in $P$ must not appear in $F$)

Variable renaming

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

∀rename         ∃rename

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

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

Short-forms

For convenience we also write "$forall x,y in S ( P(x,y) )$" as short-form for "$forall x in S ( forall y in S ( P(x,y) ) )$", and similarly for more variables and for "$exists$".

Additionally, "$exists! x in S ( P(x) )$" is short-form for "$exists x in S ( P(x) land forall y in 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 in S ( forall y in T ( P(x,y) ) )$:   [⇒sub]

    $exists x in S ( forall y in T ( P(x,y) ) )$.   [⇒sub]

    Let $a in S$ such that $forall y in T ( P(a,y) )$.   [∃elim]

    $a in S$.   [∃elim]

    $forall y in T ( P(a,y) )$.   [∃elim]

    $forall z in T ( P(a,z) )$.   [∀rename]

    Given $y in T$:   [∀sub]

      $y in T$.   [∀sub]

      $forall z in T ( P(a,z) )$.   [∀restate]

      $y in T$.   [restate]

      $P(a,y)$.   [∀elim]

      $a in S$.   [∀restate]

      $exists x in S ( P(x,y) )$.   [∃intro]

    $forall y in T ( exists x in S ( P(x,y) ) )$.   [∀intro]

  $exists x in S ( forall y in T ( P(x,y) ) ) imp forall y in T ( exists x in S ( P(x,y) ) )$.   [⇒intro]

Finally with all lines in square-brackets removed:

  If $exists x in S ( forall y in T ( P(x,y) ) )$:   [⇒sub]

    Let $a in S$ such that $forall y in T ( P(a,y) )$.   [∃elim]

    Given $y in T$:   [∀sub]

      $P(a,y)$.   [∀elim]

      $exists x in S ( P(x,y) )$.   [∃intro]

    $forall y in T ( exists x in S ( P(x,y) ) )$.   [∀intro]

  $exists x in S ( forall y in T ( P(x,y) ) ) imp forall y in T ( exists x in S ( P(x,y) ) )$.   [⇒intro]

This final proof is much cleaner yet still easily computer-verifiable.

Notes

The above rules avoid the usual trouble that most 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) )$".

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 in nn ( x+y in nn )$.


• 
  $forall x,y in nn ( x·y in nn )$.


• 
  $forall x,y in nn ( x+y=y+x )$.


• 
  $forall x,y in nn ( x·y=y·x )$.


• 
  $forall x,y,z in nn ( x+(y+z)=(x+y)+z )$.


• 
  $forall x,y,z in nn ( x·(y·z)=(x·y)·z )$.


• 
  $forall x,y,z in nn ( x·(y+z)=x·z+y·z )$.


• 
  $forall x in nn ( x+0=x )$.


• 
  $forall x in nn ( x·1=x )$.


• 
  $forall x in nn ( neg x<x )$.


• 
  $forall x,y in nn ( x<y lor y<x lor x=y )$.


• 
  $forall x,y,z in nn ( x<y land y<z imp x<z )$.


• 
  $forall x,y,z in nn ( x<y imp x+z<y+z )$.


• 
  $forall x,y,z in nn ( x<y land 0<z imp x·z<y·z )$.


• 
  $forall x,y in nn ( x<y imp exists z in nn ( x+z=y ) )$.


• 
  $0<1$.


• 
  $forall x in nn ( 0=x lor 1=x lor 1<x )$.

Add the induction axioms, namely for each property $P$ involving only the symbols of PA and quantifiers over $nn$ add the following axiom:

• 
  $P(0) land forall k in nn ( P(k) imp P(k+1) ) imp forall k in 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 $×,FN$, 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 $FN(S,T) in set$ and $pow(S) in set$.


• If $S,T in set$ and $f in FN(S,T)$ and $x in S$, then $f(x) in T$.


• If $forall x in S ( x in set )$, then $bigcup(S) in set$.

Add the following axioms:

• 
  extensionality:   $forall S,T in set ( S=T eq forall x in obj ( x in S eq x in T ) ).$
  


• 
  empty-set:   $forall x in obj ( neg x in none ).$
  


• 
  power-set:   $forall S in set ( pow(S) = { T : T in set land forall x in T ( x in S ) } ).$
  


• 
  pair:   $forall x,y in obj ( {x,y} = { z : x=z lor x=y } ).$
  


• 
  ordered-pair:   $forall x,y in obj forall z,w in obj ( (x,y)=(z,w) eq x=z land y=w ).$
  


• 
  product-type:   $forall S,T in set ( S×T = { t : exists x in S exists y in T ( t=(x,y) ) } ).$
  


• 
  function-type:   $forall S,T in set ( FN(S,T) = \ { F : F in S×T land forall x in S exists! y in T ( (x,y) in F ) } ).$
  


• 
  function-application:   $forall S,T in set forall f in FN(S,T) forall x in S ( (x,f(x)) in f ).$
  


• 
  union:   $forall S in set ( bigcup(S) = { x : exists T in set ( x in T land T in S ) } ).$
  


• 
  choice:   $forall S,T in set forall R in S×T ( forall x in S exists y in T ( (x,y) in R ) \ imp exists f in FN(S,T) forall x in S ( (x,f(x)) in R ) ).$
  

Add the following rules:

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$)

collection

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

  $fitch{S in set. \ forall x in S exists y in obj ( P(x,y) ).}{{ y : exists x in 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 in nn ( P(k) imp P(k+1) ).}{forall k in 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 in S ( E(x) in T ). \ f = ( S x mapsto E(x) ).}{f in FN(S,T) land forall x in 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.)