For the proof theoretical part of predicate logic we again just extend what we have developed for propositional logic. That is the natural deduction system. We extend it with a set of rules for the new operators.
This rule is quite central to any reasoning system. A given term is equal to itself. We state this as $$ \frac{}{t = t} = i $$ This is an axiom since it does not depend on any premises. Using semantic terminology the rule is a tautology. These appears in natural language as a figure of speech, like "a child is a child". You can't argue with that.
The rule can only be used on terms. As stated for propositional language equality between formulas is denoted with $\equiv$, and this operator is not part of the language - it is a meta operator.
The elimination rule for equality is given as $$ \frac{t_1 = t_2 \ \ \ \phi[t_1 / x]}{\phi[t_2 / x]} = e $$ Here $t_1,t_2$ have to be free for $x$ in $\phi$. We can use this rule to prove that the relation = is symmetric. We get:
t_1 == t_2 assumption; [l1] t_1 == t_1 by eq_i ; [l2] t_2 == t_1 by eq_e ([x] x == t_1) l2 l1 .We can also prove that the relation is transitive, we get
t_1 == t_2 assumption; [l1] t_2 == t_3 assumption; [l2] t_1 == t_3 by eq_e ([x] t_1 == x) l1 l2 .Note in both proofs that we substitute from left to right. That is the second assumption in the last proof allow us to substitute the term $t_2$ with the term $t_3$.
The elimination rule is given as follows $$ \frac{\forall x . \phi}{\phi[t / x]} \forall e $$ It states that you given $\forall x . \phi$, a term $t$ and that $t$ is free for $x$ in $\phi$, can do $\phi[t/x]$. That is you can substitute $x$ with $t$ in $\phi$, and $\forall x . \phi$ remains true. This is quite straight forward.
The introduction rule for forall is a bit more complicated. It is given as $$ \frac{x_0 \cdots \phi[x_0 / x]}{\forall x . \phi} \forall i $$ It involves a proof box as we have seen in propositional logic. However here the box is a scope for the variable/term $x_0$. The rule states that if we are given some arbitrary $x_0$ and can use this to prove $\phi$, then we conclude that every $x$ can be used to prove $\phi$. The idea is that since $x_0$ is picked arbitrary/random, any $x$ taken from the domain can take its place. Note that the instance $x_0$ cannot occur anywhere outside the scope box. This ensures that $x_0$ is not preconditioned, that is $x_0$ is truly arbitrarily picked.
We can use these forall-rules to prove that $$ \forall x . P(x) \rightarrow Q(x), \forall x . P(x) \vdash \forall x . Q(x) $$ We get
all ([x] P x => Q x) assumption; [l1] all ([x] P x) assumption; [l2] (var [x_0] P x_0 => Q x_0 by all_e x_0 l1 ; [l3] P x_0 by all_e x_0 l2 ; [l4] Q x_0 by imp_e l4 l3 ) ; [all1] all ([x] Q x) by all_i all1 .The introduction rule for the existential quantifier is given as $$ \frac{\phi[t / x]}{\exists x . \phi} \exists x i $$ It is pretty straight forward. It states that given $t$ is free for $x$ in $\phi$, and we can use this concrete $t$ to prove $\phi$, then we know that there exists some term that can prove $\phi$. Hence we travel from concrete to general. That is I have this $t$ that can be used as a instance for a proof, hence we know that there is some term that can be used in a proof.
The elimination involves a proof box (a scope). It is given as $$ \frac{\exists x . \phi \ \ \ (x_0) \phi[x_o / x] \cdots \chi}{\chi} \exists e $$ It states that given $\exists x. \phi$, if we assume some fresh $x_0$ that is fresh for $x$ in $\phi$, we do substitution and are able to prove $\chi$, then we end know $\chi$. The behind reasoning is kind of the same as for $\lor e$. Since we do not know which of all possible $x_0$ that is used to prove $\chi$, we need examine all of them. Since we can't exhaust cases (there might be infinite many), we instead pick $x_0$ arbitrarily. Hence $x_0$ cannot appear outside the proof box/scope.
We can combine these rules to prove that $$ \forall x . P(x) \rightarrow Q(x) , \exists x P(x) \vdash \exists x Q(x) $$ We get
all ([x] P x => Q x) assumption; [l1] exi ([x] P x) assumption; [l2] (var [x_0] P x_0 assumption; [l3] P x_0 => Q x_0 by all_e x_0 l1 ; [l4] Q x_0 by imp_e l3 l4 ; [l5] exi ([x] Q x) by exi_i x_0 l5 ) ; [exi1] exi ([x] Q x) by exi_e l2 exi1 .We can also use the rules to prove that $$ \forall x . P(x) \vdash \exists x . P(x) $$ Note that we have to restrict any model to be based on a non-empty set. Else the above is not generally true. That is let the domain be empty. Now $\forall x . P(x)$ is trivially true. But $\exists x . P(x)$ is never true. Anyway, we get
all ([x] P x) assumption; [l1] P x_0 by all_e x_0 l1 ; [l2] exi ([x] P x) by exi_i x_0 l2 ....