where $P$ , $Q$ , and $R$ are well-formed formulas in the language $\mathscr$ . The above axioms are obvious to me. I can see that they are ubiquitous in everyday mathematics.
The first order logic has, in addition, the following extra axiom schemes:
- If $x$ does not occur free in $P$ , then ( $\forall x$ ) $P\rightarrow P$ ,
- If $P(x)$ is a well-formed formula and $t$ is free for $x$ in $P(x)$ , then $(\forall x)P(x)\rightarrow P(t)$ ,
- If $P$ contains no free occurrence of $x$ , then $(\forall x)(P\rightarrow Q)\rightarrow(P\rightarrow(\forall x)Q)$ .
In addition, in mathematics, one also need the following axioms for equality:
- For each variable $x$ , $x=x$ .
- $(t_=x)\rightarrow(f_^(t_,\cdots,t_,\cdots,t_)=f_^(t_,\cdots,x,\cdots,t_))$ , where $t_,\cdots$ , $t_$ , and $x$ are any terms, and $f_^$ is any $n$ -ary function letter of the language $\mathscr$ .
- $(t_=x)\rightarrow(A_^(t_,\cdots,t_,\cdots,t_)\rightarrow A_^(t_,\cdots,x,\cdots,t_))$ , where $t_,\cdots$ , $t_$ , and $x$ are any terms, and $A_^$ is any predicate symbol in $\mathscr$ .
The axioms $4$ , $5$ , $6$ , $7$ , $8$ , and $9$ look trivially true to me, but I have no impression that I have ever used these axioms in mathematics. If ZFC set theory is expressed in the language of first order logic, then I believe it is necessary to use these axioms in giving ZFC axioms.
Can anyone give me examples of how these axioms are used in expressing ZFC axioms?
- set-theory
- first-order-logic
- predicate-logic
