# some valid schemas of first order logic

In this entry, we record some valid schemas of first order logic FO$(\Sigma)$ based on the signature $\Sigma$:

1. 1.

$\forall xA\to\forall yA[y/x]$ if $y$ does not occur free, but free for $x$, in $A$

2. 2.

$\forall yA[y/x]\to\forall xA$ if $y$ does not occur in $A$

3. 3.

$\forall xA\leftrightarrow A$ if $x$ is not free in $A$

4. 4.

$\exists xA\leftrightarrow A$ if $x$ is not free in $A$

5. 5.

$\forall x\forall yA\to\forall y\forall xA$

6. 6.

$\exists x\exists yA\to\exists y\exists xA$

7. 7.

$\forall x(A\to B)\to(\forall xA\to\forall xB)$

8. 8.

$(\forall xA\to\forall xB)\to\forall x(A\to B)$

9. 9.

$\forall x(A\land B)\leftrightarrow\forall xA\land\forall xB$

10. 10.

$\exists x(A\lor B)\leftrightarrow\exists xA\lor\exists xB$

11. 11.

$\forall x(A\lor B)\leftrightarrow(\forall xA)\lor B$ if $x$ is not free in $B$

12. 12.

$\exists x(A\land B)\leftrightarrow(\exists xA)\land B$ if $x$ is not free in $B$

where $A,B$ are well-formed formulas (wff’s) of FO$(\Sigma)$.

Title some valid schemas of first order logic SomeValidSchemasOfFirstOrderLogic 2013-03-22 19:32:28 2013-03-22 19:32:28 CWoo (3771) CWoo (3771) 11 CWoo (3771) Definition msc 03B10