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<x \ )$.
- $\forall x,y{∈}\nn\ ( \ x<y \lor y<x \lor x=y \ )$.
- $\forall x,y,z{∈}\nn\ ( \ x<y \land y<z \imp x<z \ )$.
- $\forall x,y,z{∈}\nn\ ( \ x<y \imp x+z<y+z \ )$.
- $\forall x,y,z{∈}\nn\ ( \ x<y \land 0<z \imp x·z<y·z \ )$.
- $\forall x,y{∈}\nn\ ( \ x<y \imp \exists z{∈}\nn\ ( \ x+z=y \ ) \ )$.
- $0<1$.
- $\forall x{∈}\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 (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$.
Add the following axioms:
- 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 \ ) \ ).$
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$)
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.)
Best Answer
Correct!
The 'logical equivalence' between implication and contrapositive is this: For any statements $\phi$ and $\psi$: $\phi$ logically implies $\psi$ if and only if $\neg \psi$ logically implies $\neg \phi$
Please note that this 'if and only if' is not your 'typical' logical equivalence, which is usually between two specific statements. Rather, this 'if and only if' is between two logical relationships; between two statements that already express some relationship between two statements. As such, this 'logical equivalence' between a logical implication and its contrapositive is more of a 'meta-logical' equivalence. The point is: you're not using both logical equivalence and logical implication ... but rather use a meta-logical equivalence to show a logical implication.
I am not sure in what sense you feel that the issue is being exacerbated in predicate logic ... could you maybe elaborate on this? Still, I can already say this: Two statements are logically equivalent if and only if they logically entail each other. This is true for any logic, whether propositional, predicate, or what have you. We could call this "reciprocal logical entailment" ... but logical equivalence is the very same idea.