some valid schemas of first order logic
In this entry, we record some valid schemas of first order logic FO(Σ) based on the signature Σ:
-
1.
∀xA→∀yA[y/x] if y does not occur free, but free for x, in A
-
2.
∀yA[y/x]→∀xA if y does not occur in A
-
3.
∀xA↔A if x is not free in A
-
4.
∃xA↔A if x is not free in A
-
5.
∀x∀yA→∀y∀xA
-
6.
∃x∃yA→∃y∃xA
-
7.
∀x(A→B)→(∀xA→∀xB)
-
8.
(∀xA→∀xB)→∀x(A→B)
-
9.
∀x(A∧B)↔∀xA∧∀xB
-
10.
∃x(A∨B)↔∃xA∨∃xB
-
11.
∀x(A∨B)↔(∀xA)∨B if x is not free in B
-
12.
∃x(A∧B)↔(∃xA)∧B if x is not free in B
where A,B are well-formed formulas (wff’s) of FO(Σ).
Title | some valid schemas of first order logic |
---|---|
Canonical name | SomeValidSchemasOfFirstOrderLogic |
Date of creation | 2013-03-22 19:32:28 |
Last modified on | 2013-03-22 19:32:28 |
Owner | CWoo (3771) |
Last modified by | CWoo (3771) |
Numerical id | 11 |
Author | CWoo (3771) |
Entry type | Definition |
Classification | msc 03B10 |