Work on Cantor's 1883 Grundlagen article on how and when he found out that the set of all ordinals is not a set
edit
Ewald, p. 890:
Grundlagen (Cantor, 1883d):Towards a judgement on the question which is raised here, I give some of the most important references. One should see: Locke, Essay on Human Understanding , Bk. 11, Chs. XVI and XVII. [Followed by 3 other refs to Descartes, Spinoza, and Leibniz.] Even today, one cannot find stronger arguments than these against the introduction of infinite intergers; these arguments should be examined and compared with mine. ... Ewald, p. 1287:
Cantor 1886a: Cantor 1886b: Uber die verschiedenenverschiedenen Standpunkte in Bezug auf das aktuelle Unendliche. Zeitschrift fur Philosophie und philosophische Kritik, 88 , 224-33. (Reprinted in Cantor 1932, pp. 370-7). Cantor 1887-8: Mitteilungen zur Lehre vom Transfiniten I, II. Zeitschrift fur Philosophie und philosophische Kritik, 91 , 81-125; 92 , 250-65. (Reprinted in Cantor 1932, pp. 378-439). John Locke, An Essay Concerning Human Understanding. Read the following chapters carefully. I guessed what I had seen in them, but there may be more. [1] :
This further is observable in number, that it is that which the mind makes use of in measuring all things that by us are measurable, which principally are EXPANSION and DURATION; and our idea of infinity, even when applied to those, seems to be nothing but the infinity of number. For what else are our ideas of Eternity and Immensity, but the repeated additions of certain ideas of imagined parts of duration and expansion, with the infinity of number; in which we can come to no end of addition? For such an inexhaustible stock, number (of all other our ideas) most clearly furnishes us with, as is obvious to every one. For let a man collect into one sum as great a number as he pleases, this multitude how great soever, lessens not one jot the power of adding to it, or brings him any nearer the end of the inexhaustible stock of number; where still there remains as much to be added, as if none were taken out. And this ENDLESS ADDITION or ADDIBILITY (if any one like the word better) of numbers, so apparent to the mind, is that, I think, which gives us the clearest and most distinct idea of infinity: of which more in the following chapter.
CHAPTER XVII.—OF INFINITY.
13. No positive Idea of Infinity.
Though it be hard, I think, to find anyone so absurd as to say he has the POSITIVE idea of an actual infinite number;—the infinity whereof lies only in a power still of adding any combination of units to any former number, and that as long and as much as one will; the like also being in the infinity of space and duration, which power leaves always to the mind room for endless additions;—yet there be those who imagine they have positive ideas of infinite duration and space. It would, I think, be enough to destroy any such positive idea of infinite, to ask him that has it,—whether he could add to it or no; which would easily show the mistake of such a positive idea. We can, I think, have no positive idea of any space or duration which is not made up of, and commensurate to, repeated numbers of feet or yards, or days and years; which are the common measures, whereof we have the ideas in our minds, and whereby we judge of the greatness of this sort of quantities. And therefore, since an infinite idea of space or duration must needs be made up of infinite parts, it can have no other infinity than that of number CAPABLE still of further addition; but not an actual positive idea of a number infinite. For, I think it is evident, that the addition of finite things together (as are all lengths whereof we have the positive ideas) can never otherwise produce the idea of infinite than as number does; which consisting of additions of finite units one to another, suggests the idea of infinite, only by a power we find we have of still increasing the sum, and adding more of the same kind; without coming one jot nearer the end of such progression.
Question: Did Cantor use this argument in his article? OR does he have something that implies readers have read this argument or assumes that readers can develop this argument on their own?
Cantor Locke
edit
Counterexample (Herbrand, p. 193)
edit
A
p
:
∃
y
2
⋯
∃
y
p
+
1
[
R
(
y
2
,
y
3
)
∧
…
∧
R
(
y
p
−
1
,
y
p
)
∧
H
(
y
2
,
y
p
+
1
)
∧
∀
x
p
¬
H
(
y
p
,
x
p
)
]
P
p
:
A
p
∧
∀
x
1
∀
x
2
[
¬
R
(
x
1
,
x
2
)
∨
∀
x
¬
H
(
x
1
,
x
)
∨
∃
y
H
(
x
2
,
y
)
)
]
Q
p
:
A
p
∧
∀
x
1
∀
x
2
[
¬
R
(
x
1
,
x
2
)
∨
∀
x
{
¬
H
(
x
1
,
x
)
∨
∃
y
H
(
x
2
,
y
)
}
]
{\displaystyle {\begin{aligned}\\&A_{p}\!:\;\exists y_{2}\cdots \exists y_{p+1}[R(y_{2},y_{3})\land \ldots \land R(y_{p-1},y_{p})\land H(y_{2},y_{p+1})\land \forall x_{p}\neg H(y_{p},x_{p})]\\&P_{p}\!:\;A_{p}\land \forall x_{1}\forall x_{2}[\neg R(x_{1},x_{2})\lor \forall x\neg H(x_{1},x)\lor \exists yH(x_{2},y))]\\&Q_{p}\!:\;A_{p}\land \forall x_{1}\forall x_{2}[\neg R(x_{1},x_{2})\lor \forall x\{\neg H(x_{1},x)\lor \exists yH(x_{2},y)\}]\\\\\end{aligned}}}
E
(
A
p
)
:
R
(
a
2
,
a
3
)
∧
…
∧
R
(
a
p
−
1
,
a
p
)
∧
H
(
a
2
,
a
p
+
1
)
∧
¬
H
(
a
p
,
x
p
)
E
(
P
p
)
:
E
(
A
p
)
∧
[
¬
R
(
x
1
,
x
2
)
∨
¬
H
(
x
1
,
x
)
∨
H
(
x
2
,
f
(
x
1
,
x
2
)
)
]
E
(
Q
p
)
:
E
(
A
p
)
∧
[
¬
R
(
x
1
,
x
2
)
∨
¬
H
(
x
1
,
x
)
∨
H
(
x
2
,
f
(
x
1
,
x
2
,
x
)
)
]
{\displaystyle {\begin{aligned}&E(A_{p})\!:\;R(a_{2},a_{3})\land \ldots \land R(a_{p-1},a_{p})\land H(a_{2},a_{p+1})\land \neg H(a_{p},x_{p})\\&E(P_{p})\!:\;E(A_{p})\land [\neg R(x_{1},x_{2})\lor \neg H(x_{1},x)\lor H(x_{2},f(x_{1},x_{2}))]\\&E(Q_{p})\!:\;E(A_{p})\land [\neg R(x_{1},x_{2})\lor \neg H(x_{1},x)\lor H(x_{2},f(x_{1},x_{2},x))]\\\\\end{aligned}}}
Clauses
P
p
:
R
2
=
{
R
(
a
2
,
a
3
)
}
,
⋯
,
R
p
−
1
=
{
R
(
a
p
−
1
,
a
p
)
}
,
H
2
=
{
H
(
a
2
,
a
p
+
1
)
}
,
H
¬
p
=
{
¬
H
(
a
p
,
x
p
)
}
,
R
H
=
{
¬
R
(
x
1
,
x
2
)
,
¬
H
(
x
1
,
x
)
,
H
(
x
2
,
f
(
x
1
,
x
2
)
)
}
{\displaystyle {\begin{alignedat}{2}&{\text{Clauses }}P_{p}\!:\;\;&&R_{2}=\{R(a_{2},a_{3})\},\\&&&\cdots ,\\&&&R_{p-1}=\{R(a_{p-1},a_{p})\},\\&&&H_{2}=\{H(a_{2},a_{p+1})\},\\&&&H_{\neg p}=\{\neg H(a_{p},x_{p})\},\\&&&RH=\{\neg R(x_{1},x_{2}),\;\neg H(x_{1},x),\;H(x_{2},f(x_{1},x_{2}))\}\\\\\end{alignedat}}}
Resolvents:
P
5
R
2
,
R
H
[
a
2
/
x
1
,
a
3
/
x
2
]
=
{
R
(
a
2
,
a
3
)
}
,
{
¬
R
(
a
2
,
a
3
)
,
¬
H
(
a
2
,
x
)
,
H
(
a
3
,
f
(
a
2
,
a
3
)
)
}
H
¬
2
,
3
=
{
¬
H
(
a
2
,
x
)
,
H
(
a
3
,
f
(
a
2
,
a
3
)
)
}
H
2
,
H
¬
2
,
3
[
a
p
+
1
/
x
]
=
{
H
(
a
2
,
a
p
+
1
)
}
,
{
¬
H
(
a
2
,
a
p
+
1
)
,
H
(
a
3
,
f
(
a
2
,
a
3
)
)
}
H
3
=
{
H
(
a
3
,
f
(
a
2
,
a
3
)
)
}
R
3
,
R
H
[
a
3
/
x
1
,
a
4
/
x
2
]
=
{
R
(
a
3
,
a
4
)
}
,
{
¬
R
(
a
3
,
a
4
)
,
¬
H
(
a
3
,
x
)
,
H
(
a
4
,
f
(
a
3
,
a
4
)
)
}
H
¬
3
,
4
=
{
¬
H
(
a
3
,
x
)
,
H
(
a
4
,
f
(
a
3
,
a
4
)
)
}
H
3
,
H
¬
3
,
4
[
f
(
a
2
,
a
3
)
/
x
]
=
{
H
(
a
3
,
f
(
a
2
,
a
3
)
)
}
,
{
¬
H
(
a
3
,
f
(
a
2
,
a
3
)
)
,
H
(
a
4
,
f
(
a
3
,
a
4
)
)
}
H
4
=
{
H
(
a
4
,
f
(
a
3
,
a
4
)
)
}
R
4
,
R
H
[
a
4
/
x
1
,
a
5
/
x
2
]
=
{
R
(
a
4
,
a
5
)
}
,
{
¬
R
(
a
4
,
a
5
)
,
¬
H
(
a
4
,
x
)
,
H
(
a
5
,
f
(
a
4
,
a
5
)
)
}
H
¬
4
,
5
=
{
¬
H
(
a
4
,
x
)
,
H
(
a
5
,
f
(
a
4
,
a
5
)
)
}
H
4
,
H
¬
4
,
5
[
f
(
a
3
,
a
4
)
/
x
]
=
{
H
(
a
4
,
f
(
a
3
,
a
4
)
)
}
,
{
¬
H
(
a
4
,
f
(
a
3
,
a
4
)
)
,
H
(
a
5
,
f
(
a
4
,
a
5
)
)
}
H
5
=
{
H
(
a
5
,
f
(
a
4
,
a
5
)
)
}
H
¬
5
,
H
5
,
[
f
(
a
4
,
a
5
)
/
x
p
]
=
{
¬
H
(
a
5
,
f
(
a
4
,
a
5
)
)
}
,
{
H
(
a
5
,
f
(
a
4
,
a
5
)
)
}
R
e
s
u
l
t
=
{
}
{\displaystyle {\begin{alignedat}{2}&{\text{Resolvents: }}P_{5}\\&\qquad R_{2},RH\;[a_{2}/x_{1},a_{3}/x_{2}]\;=\;&&\{R(a_{2},a_{3})\},\;\{\neg R(a_{2},a_{3}),\;\neg H(a_{2},x),\;H(a_{3},f(a_{2},a_{3}))\}\\&\qquad H_{\neg 2,3}\;=&&\{\neg H(a_{2},x),\;H(a_{3},f(a_{2},a_{3}))\}\\&\qquad H_{2},H_{\neg 2,3}\;[a_{p+1}/x]\;=\;&&\{H(a_{2},a_{p+1})\},\{\neg H(a_{2},a_{p+1}),\;H(a_{3},f(a_{2},a_{3}))\}\\&\qquad H_{3}=&&\{H(a_{3},f(a_{2},a_{3}))\}\\\\&\qquad R_{3},RH\;[a_{3}/x_{1},a_{4}/x_{2}]\;=\;&&\{R(a_{3},a_{4})\},\;\{\neg R(a_{3},a_{4}),\;\neg H(a_{3},x),\;H(a_{4},f(a_{3},a_{4}))\}\\&\qquad H_{\neg 3,4}\;=&&\{\neg H(a_{3},x),\;H(a_{4},f(a_{3},a_{4}))\}\\&\qquad H_{3},H_{\neg 3,4}\;[f(a_{2},a_{3})/x]\;=\;&&\{H(a_{3},f(a_{2},a_{3}))\},\{\neg H(a_{3},f(a_{2},a_{3})),\;H(a_{4},f(a_{3},a_{4}))\}\\&\qquad H_{4}=&&\{H(a_{4},f(a_{3},a_{4}))\}\\\\&\qquad R_{4},RH\;[a_{4}/x_{1},a_{5}/x_{2}]\;=\;&&\{R(a_{4},a_{5})\},\;\{\neg R(a_{4},a_{5}),\;\neg H(a_{4},x),\;H(a_{5},f(a_{4},a_{5}))\}\\&\qquad H_{\neg 4,5}\;=&&\{\neg H(a_{4},x),\;H(a_{5},f(a_{4},a_{5}))\}\\&\qquad H_{4},H_{\neg 4,5}\;[f(a_{3},a_{4})/x]\;=\;&&\{H(a_{4},f(a_{3},a_{4}))\},\{\neg H(a_{4},f(a_{3},a_{4})),\;H(a_{5},f(a_{4},a_{5}))\}\\&\qquad H_{5}=&&\{H(a_{5},f(a_{4},a_{5}))\}\\\\&\qquad H_{\neg 5},H_{5},\,[f(a_{4},a_{5})/x_{p}]\,=&&\{\neg H(a_{5},f(a_{4},a_{5}))\},\{H(a_{5},f(a_{4},a_{5}))\}\\&\qquad Result=&&\{\;\}\\\end{alignedat}}}
A
p
:
∃
y
2
⋯
∃
y
p
+
1
[
R
(
y
2
,
y
3
)
∧
…
∧
R
(
y
p
−
1
,
y
p
)
∧
H
(
y
2
,
y
p
+
1
)
∧
∀
x
p
¬
H
(
y
p
,
x
p
)
]
P
p
:
A
p
∧
∀
x
1
∀
x
2
[
¬
R
(
x
1
,
x
2
)
∨
∀
x
¬
H
(
x
1
,
x
)
∨
∃
y
H
(
x
2
,
y
)
)
]
Q
p
:
A
p
∧
∀
x
1
∀
x
2
[
¬
R
(
x
1
,
x
2
)
∨
∀
x
{
¬
H
(
x
1
,
x
)
∨
∃
y
H
(
x
2
,
y
)
}
]
{\displaystyle {\begin{aligned}\\&A_{p}\!:\;\exists y_{2}\cdots \exists y_{p+1}[R(y_{2},y_{3})\land \ldots \land R(y_{p-1},y_{p})\land H(y_{2},y_{p+1})\land \forall x_{p}\neg H(y_{p},x_{p})]\\&P_{p}\!:\;A_{p}\land \forall x_{1}\forall x_{2}[\neg R(x_{1},x_{2})\lor \forall x\neg H(x_{1},x)\lor \exists yH(x_{2},y))]\\&Q_{p}\!:\;A_{p}\land \forall x_{1}\forall x_{2}[\neg R(x_{1},x_{2})\lor \forall x\{\neg H(x_{1},x)\lor \exists yH(x_{2},y)\}]\\\\\end{aligned}}}
E
(
A
p
)
:
R
(
a
2
,
a
3
)
∧
…
∧
R
(
a
p
−
1
,
a
p
)
∧
H
(
a
2
,
a
p
+
1
)
∧
¬
H
(
a
p
,
x
p
)
E
(
P
p
)
:
E
(
A
p
)
∧
[
¬
R
(
x
1
,
x
2
)
∨
¬
H
(
x
1
,
x
)
∨
H
(
x
2
,
f
(
x
1
,
x
2
)
)
]
E
(
Q
p
)
:
E
(
A
p
)
∧
[
¬
R
(
x
1
,
x
2
)
∨
¬
H
(
x
1
,
x
)
∨
H
(
x
2
,
f
(
x
1
,
x
2
,
x
)
)
]
{\displaystyle {\begin{aligned}&E(A_{p})\!:\;R(a_{2},a_{3})\land \ldots \land R(a_{p-1},a_{p})\land H(a_{2},a_{p+1})\land \neg H(a_{p},x_{p})\\&E(P_{p})\!:\;E(A_{p})\land [\neg R(x_{1},x_{2})\lor \neg H(x_{1},x)\lor H(x_{2},f(x_{1},x_{2}))]\\&E(Q_{p})\!:\;E(A_{p})\land [\neg R(x_{1},x_{2})\lor \neg H(x_{1},x)\lor H(x_{2},f(x_{1},x_{2},x))]\\\\\end{aligned}}}
Clauses
Q
p
:
R
2
=
{
R
(
a
2
,
a
3
)
}
,
⋯
,
R
p
−
1
=
{
R
(
a
p
−
1
,
a
p
)
}
,
H
2
=
{
H
(
a
2
,
a
p
+
1
)
}
,
H
¬
p
=
{
¬
H
(
a
p
,
x
p
)
}
,
R
H
=
{
¬
R
(
x
1
,
x
2
)
,
¬
H
(
x
1
,
x
)
,
H
(
x
2
,
f
(
x
1
,
x
2
,
x
)
)
}
{\displaystyle {\begin{alignedat}{2}&{\text{Clauses }}Q_{p}\!:\;\;&&R_{2}=\{R(a_{2},a_{3})\},\\&&&\cdots ,\\&&&R_{p-1}=\{R(a_{p-1},a_{p})\},\\&&&H_{2}=\{H(a_{2},a_{p+1})\},\\&&&H_{\neg p}=\{\neg H(a_{p},x_{p})\},\\&&&RH=\{\neg R(x_{1},x_{2}),\;\neg H(x_{1},x),\;H(x_{2},f(x_{1},x_{2},x))\}\\\\\end{alignedat}}}
Resolvents:
Q
5
R
2
,
R
H
[
a
2
/
x
1
,
a
3
/
x
2
]
=
{
R
(
a
2
,
a
3
)
}
,
{
¬
R
(
a
2
,
a
3
)
,
¬
H
(
a
2
,
x
)
,
H
(
a
3
,
f
(
a
2
,
a
3
,
x
)
)
}
H
¬
2
,
3
=
{
¬
H
(
a
2
,
x
)
,
H
(
a
3
,
f
(
a
2
,
a
3
,
x
)
)
}
H
2
,
H
¬
2
,
3
[
a
p
+
1
/
x
]
=
{
H
(
a
2
,
a
p
+
1
)
}
,
{
¬
H
(
a
2
,
a
p
+
1
)
,
H
(
a
3
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
}
H
3
=
{
H
(
a
3
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
}
R
3
,
R
H
[
a
3
/
x
1
,
a
4
/
x
2
]
=
{
R
(
a
3
,
a
4
)
}
,
{
¬
R
(
a
3
,
a
4
)
,
¬
H
(
a
3
,
x
)
,
H
(
a
4
,
f
(
a
3
,
a
4
,
x
)
)
}
H
¬
3
,
4
=
{
¬
H
(
a
3
,
x
)
,
H
(
a
4
,
f
(
a
3
,
a
4
,
x
)
)
}
H
3
,
H
¬
3
,
4
[
f
(
a
2
,
a
3
,
a
p
+
1
)
/
x
]
=
{
H
(
a
3
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
}
,
{
¬
H
(
a
3
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
,
H
(
a
4
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
)
}
H
4
=
H
(
a
4
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
R
4
,
R
H
[
a
4
/
x
1
,
a
5
/
x
2
]
=
{
R
(
a
4
,
a
5
)
}
,
{
¬
R
(
a
4
,
a
5
)
,
¬
H
(
a
4
,
x
)
,
H
(
a
5
,
f
(
a
4
,
a
5
,
x
)
)
}
H
¬
4
,
5
=
{
¬
H
(
a
4
,
x
)
,
H
(
a
5
,
f
(
a
4
,
a
5
,
x
)
)
}
H
4
,
H
¬
4
,
5
[
f
(
a
3
,
a
4
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
/
x
]
=
{
H
(
a
4
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
}
,
{
¬
H
(
a
4
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
,
H
(
a
5
,
f
(
a
4
,
a
5
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
)
}
H
5
=
H
(
a
5
,
f
(
a
4
,
a
5
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
)
}
H
5
,
H
¬
5
[
f
(
a
4
,
a
5
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
)
/
x
p
]
=
{
¬
H
(
a
5
,
f
(
a
4
,
a
5
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
)
}
,
{
H
(
a
5
,
f
(
a
4
,
a
5
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
)
)
}
R
e
s
u
l
t
=
{
}
{\displaystyle {\begin{alignedat}{2}&{\text{Resolvents: }}Q_{5}\\&\quad R_{2},RH\;[a_{2}/x_{1},a_{3}/x_{2}]\;=\;&&\{R(a_{2},a_{3})\},\;\{\neg R(a_{2},a_{3}),\;\neg H(a_{2},x),\;H(a_{3},f(a_{2},a_{3},x))\}\\&\quad H_{\neg 2,3}\;=&&\{\neg H(a_{2},x),\;H(a_{3},f(a_{2},a_{3},x))\}\\&\quad H_{2},H_{\neg 2,3}\;[a_{p+1}/x]\;=\;&&\{H(a_{2},a_{p+1})\},\{\neg H(a_{2},a_{p+1}),\;H(a_{3},f(a_{2},a_{3},a_{p+1}))\}\\&\quad H_{3}=&&\{H(a_{3},f(a_{2},a_{3},a_{p+1}))\}\\\\&\quad R_{3},RH\;[a_{3}/x_{1},a_{4}/x_{2}]\;=\;&&\{R(a_{3},a_{4})\},\;\{\neg R(a_{3},a_{4}),\;\neg H(a_{3},x),\;H(a_{4},f(a_{3},a_{4},x))\}\\&\quad H_{\neg 3,4}\;=&&\{\neg H(a_{3},x),\;H(a_{4},f(a_{3},a_{4},x))\}\\&\quad H_{3},H_{\neg 3,4}\;[f(a_{2},a_{3},a_{p+1})/x]\;=\;&&\{H(a_{3},f(a_{2},a_{3},a_{p+1}))\},\\&&&\quad \{\neg H(a_{3},f(a_{2},a_{3},a_{p+1})),H(a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))\}\\&\quad H_{4}=&&H(a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1}))\\\\&\quad R_{4},RH\;[a_{4}/x_{1},a_{5}/x_{2}]\;=\;&&\{R(a_{4},a_{5})\},\;\{\neg R(a_{4},a_{5}),\;\neg H(a_{4},x),H(a_{5},f(a_{4},a_{5},x))\}\\&\quad H_{\neg 4,5}\;=&&\{\neg H(a_{4},x),\;H(a_{5},f(a_{4},a_{5},x))\}\\&\quad H_{4},H_{\neg 4,5}\\&\qquad [f(a_{3},a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1}))/x]\;=\;&&\{H(a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})\},\\&&&\quad \{\neg H(a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})),\;H(a_{5},f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))\}\\&\quad H_{5}=H(a_{5},f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))\}\\\\&\quad H_{5},H_{\neg 5}\\&\qquad [f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))/x_{p}]\,=&&\{\neg H(a_{5},f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))\},\\&&&\qquad \{H(a_{5},f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1}))))\}\\&\quad Result=&&\{\;\}\\\end{alignedat}}}
Counterexample (Using implications)
edit
A
p
:
∃
y
2
⋯
∃
y
p
+
1
[
R
(
y
2
,
y
3
)
∧
…
∧
R
(
y
p
−
1
,
y
p
)
∧
H
(
y
2
,
y
p
+
1
)
∧
∀
x
p
¬
H
(
y
p
,
x
p
)
]
P
p
:
A
p
∧
∀
x
1
∀
x
2
[
¬
R
(
x
1
,
x
2
)
∨
∀
x
¬
H
(
x
1
,
x
)
∨
∃
y
H
(
x
2
,
y
)
)
]
Q
p
:
A
p
∧
∀
x
1
∀
x
2
[
¬
R
(
x
1
,
x
2
)
∨
∀
x
{
¬
H
(
x
1
,
x
)
∨
∃
y
H
(
x
2
,
y
)
}
]
{\displaystyle {\begin{aligned}\\&A_{p}\!:\;\exists y_{2}\cdots \exists y_{p+1}[R(y_{2},y_{3})\land \ldots \land R(y_{p-1},y_{p})\land H(y_{2},y_{p+1})\land \forall x_{p}\neg H(y_{p},x_{p})]\\&P_{p}\!:\;A_{p}\land \forall x_{1}\forall x_{2}[\neg R(x_{1},x_{2})\lor \forall x\neg H(x_{1},x)\lor \exists yH(x_{2},y))]\\&Q_{p}\!:\;A_{p}\land \forall x_{1}\forall x_{2}[\neg R(x_{1},x_{2})\lor \forall x\{\neg H(x_{1},x)\lor \exists yH(x_{2},y)\}]\\\\\end{aligned}}}
E
(
A
p
)
:
R
(
a
2
,
a
3
)
∧
…
∧
R
(
a
p
−
1
,
a
p
)
∧
H
(
a
2
,
a
p
+
1
)
∧
¬
H
(
a
p
,
x
p
)
E
(
P
p
)
:
E
(
A
p
)
∧
[
¬
R
(
x
1
,
x
2
)
∨
¬
H
(
x
1
,
x
)
∨
H
(
x
2
,
f
(
x
1
,
x
2
)
)
]
E
(
Q
p
)
:
E
(
A
p
)
∧
[
¬
R
(
x
1
,
x
2
)
∨
¬
H
(
x
1
,
x
)
∨
H
(
x
2
,
f
(
x
1
,
x
2
,
x
)
)
]
{\displaystyle {\begin{aligned}&E(A_{p})\!:\;R(a_{2},a_{3})\land \ldots \land R(a_{p-1},a_{p})\land H(a_{2},a_{p+1})\land \neg H(a_{p},x_{p})\\&E(P_{p})\!:\;E(A_{p})\land [\neg R(x_{1},x_{2})\lor \neg H(x_{1},x)\lor H(x_{2},f(x_{1},x_{2}))]\\&E(Q_{p})\!:\;E(A_{p})\land [\neg R(x_{1},x_{2})\lor \neg H(x_{1},x)\lor H(x_{2},f(x_{1},x_{2},x))]\\\\\end{aligned}}}
Axioms
P
p
:
R
2
:
R
(
a
2
,
a
3
)
,
⋯
,
R
p
−
1
:
R
(
a
p
−
1
,
a
p
)
H
2
:
H
(
a
2
,
a
p
+
1
)
H
¬
p
:
¬
H
(
a
p
,
x
p
)
R
H
:
R
(
x
1
,
x
2
)
⟹
[
H
(
x
1
,
x
)
⟹
H
(
x
2
,
f
(
x
1
,
x
2
)
)
]
{\displaystyle {\begin{alignedat}{2}&{\text{Axioms }}P_{p}\!:\;\;&&R_{2}\!:\;R(a_{2},a_{3}),\\&&&\cdots ,\\&&&R_{p-1}\!:\;R(a_{p-1},a_{p})\,\\&&&H_{2}\!:\;H(a_{2},a_{p+1})\,\\&&&H_{\neg p}\!:\;\neg H(a_{p},x_{p})\ \\&&&RH\!:\;R(x_{1},x_{2})\implies [H(x_{1},x)\implies H(x_{2},f(x_{1},x_{2}))]\\\\\end{alignedat}}}
Deduction:
P
5
R
2
;
R
H
[
a
2
/
x
1
,
a
3
/
x
2
]
:
R
(
a
2
,
a
3
)
;
R
(
a
2
,
a
3
)
⟹
[
H
(
a
2
,
x
)
⟹
H
(
a
3
,
f
(
a
2
,
a
3
)
)
]
H
2
⇒
3
:
H
(
a
2
,
x
)
⟹
H
(
a
3
,
f
(
a
2
,
a
3
)
)
H
2
;
H
2
⇒
3
[
a
p
+
1
/
x
]
:
H
(
a
2
,
a
p
+
1
)
;
H
(
a
2
,
a
p
+
1
)
⟹
H
(
a
3
,
f
(
a
2
,
a
3
)
)
H
3
:
H
(
a
3
,
f
(
a
2
,
a
3
)
)
R
3
;
R
H
[
a
3
/
x
1
,
a
4
/
x
2
]
:
R
(
a
3
,
a
4
)
;
R
(
a
3
,
a
4
)
⟹
[
H
(
a
3
,
x
)
⟹
H
(
a
4
,
f
(
a
3
,
a
4
)
)
]
H
3
⇒
4
:
H
(
a
3
,
x
)
⟹
H
(
a
4
,
f
(
a
3
,
a
4
)
)
H
3
;
H
3
⇒
4
[
f
(
a
3
,
a
4
)
)
/
x
]
:
H
(
a
3
,
f
(
a
3
,
a
4
)
)
;
H
(
a
3
,
f
(
a
3
,
a
4
)
)
⟹
H
(
a
4
,
f
(
a
3
,
a
4
)
)
H
4
:
H
(
a
4
,
f
(
a
3
,
a
4
)
)
R
4
;
R
H
[
a
4
/
x
1
,
a
5
/
x
2
]
:
R
(
a
4
,
a
5
)
;
R
(
a
4
,
a
5
)
⟹
[
H
(
a
4
,
x
)
⟹
H
(
a
5
,
f
(
a
4
,
a
5
)
)
]
H
4
⇒
5
:
H
(
a
4
,
x
)
⟹
H
(
a
5
,
f
(
a
4
,
a
5
)
)
H
4
;
H
4
⇒
5
[
f
(
a
4
,
a
5
)
)
/
x
]
:
H
(
a
4
,
f
(
a
4
,
a
5
)
)
;
H
(
a
4
,
f
(
a
4
,
a
5
)
)
⟹
H
(
a
5
,
f
(
a
4
,
a
5
)
)
H
5
:
H
(
a
5
,
f
(
a
4
,
a
5
)
)
H
¬
5
,
H
5
[
f
(
a
4
,
a
5
)
/
x
p
]
:
¬
H
(
a
5
,
f
(
a
4
,
a
5
)
)
;
H
(
a
5
,
f
(
a
4
,
a
5
)
)
R
e
s
u
l
t
:
F
A
L
S
E
{\displaystyle {\begin{alignedat}{2}&{\text{Deduction: }}P_{5}\\&\qquad R_{2};RH\;[a_{2}/x_{1},a_{3}/x_{2}]\!:\;&&R(a_{2},a_{3});\;\,R(a_{2},a_{3})\implies [H(a_{2},x)\implies H(a_{3},f(a_{2},a_{3}))]\\&\qquad H_{2\Rightarrow 3}\!:\;&&H(a_{2},x)\implies H(a_{3},f(a_{2},a_{3}))\\&\qquad H_{2};H_{2\Rightarrow 3}\;[a_{p+1}/x]\!:\;&&H(a_{2},a_{p+1});\;\,H(a_{2},a_{p+1})\implies H(a_{3},f(a_{2},a_{3}))\\&\qquad H_{3}\!:\;&&H(a_{3},f(a_{2},a_{3}))\\\\&\qquad R_{3};RH\;[a_{3}/x_{1},a_{4}/x_{2}]\!:\;&&R(a_{3},a_{4});\;\,R(a_{3},a_{4})\implies [H(a_{3},x)\implies H(a_{4},f(a_{3},a_{4}))]\\&\qquad H_{3\Rightarrow 4}\!:\;&&H(a_{3},x)\implies H(a_{4},f(a_{3},a_{4}))\\&\qquad H_{3};H_{3\Rightarrow 4}\;[f(a_{3},a_{4}))/x]\!:\;&&H(a_{3},f(a_{3},a_{4}));\;\,H(a_{3},f(a_{3},a_{4}))\implies H(a_{4},f(a_{3},a_{4}))\\&\qquad H_{4}\!:\;&&H(a_{4},f(a_{3},a_{4}))\\\\&\qquad R_{4};RH\;[a_{4}/x_{1},a_{5}/x_{2}]\!:\;&&R(a_{4},a_{5});\;\,R(a_{4},a_{5})\implies [H(a_{4},x)\implies H(a_{5},f(a_{4},a_{5}))]\\&\qquad H_{4\Rightarrow 5}\!:\;&&H(a_{4},x)\implies H(a_{5},f(a_{4},a_{5}))\\&\qquad H_{4};H_{4\Rightarrow 5}\;[f(a_{4},a_{5}))/x]\!:\;\;&&H(a_{4},f(a_{4},a_{5}));\;\,H(a_{4},f(a_{4},a_{5}))\implies H(a_{5},f(a_{4},a_{5}))\\&\qquad H_{5}\!:\;&&H(a_{5},f(a_{4},a_{5}))\\\\&\qquad H_{\neg 5},H_{5}\;[f(a_{4},a_{5})/x_{p}]\!:\;&&\neg H(a_{5},f(a_{4},a_{5}));\;H(a_{5},f(a_{4},a_{5}))\\&\qquad Result\!:\,&&FALSE\\\end{alignedat}}}
A
p
:
∃
y
2
⋯
∃
y
p
+
1
[
R
(
y
2
,
y
3
)
∧
…
∧
R
(
y
p
−
1
,
y
p
)
∧
H
(
y
2
,
y
p
+
1
)
∧
∀
x
p
¬
H
(
y
p
,
x
p
)
]
P
p
:
A
p
∧
∀
x
1
∀
x
2
[
¬
R
(
x
1
,
x
2
)
∨
∀
x
¬
H
(
x
1
,
x
)
∨
∃
y
H
(
x
2
,
y
)
)
]
Q
p
:
A
p
∧
∀
x
1
∀
x
2
[
¬
R
(
x
1
,
x
2
)
∨
∀
x
{
¬
H
(
x
1
,
x
)
∨
∃
y
H
(
x
2
,
y
)
}
]
{\displaystyle {\begin{aligned}\\&A_{p}\!:\;\exists y_{2}\cdots \exists y_{p+1}[R(y_{2},y_{3})\land \ldots \land R(y_{p-1},y_{p})\land H(y_{2},y_{p+1})\land \forall x_{p}\neg H(y_{p},x_{p})]\\&P_{p}\!:\;A_{p}\land \forall x_{1}\forall x_{2}[\neg R(x_{1},x_{2})\lor \forall x\neg H(x_{1},x)\lor \exists yH(x_{2},y))]\\&Q_{p}\!:\;A_{p}\land \forall x_{1}\forall x_{2}[\neg R(x_{1},x_{2})\lor \forall x\{\neg H(x_{1},x)\lor \exists yH(x_{2},y)\}]\\\\\end{aligned}}}
E
(
A
p
)
:
R
(
a
2
,
a
3
)
∧
…
∧
R
(
a
p
−
1
,
a
p
)
∧
H
(
a
2
,
a
p
+
1
)
∧
¬
H
(
a
p
,
x
p
)
E
(
P
p
)
:
E
(
A
p
)
∧
[
¬
R
(
x
1
,
x
2
)
∨
¬
H
(
x
1
,
x
)
∨
H
(
x
2
,
f
(
x
1
,
x
2
)
)
]
E
(
Q
p
)
:
E
(
A
p
)
∧
[
¬
R
(
x
1
,
x
2
)
∨
¬
H
(
x
1
,
x
)
∨
H
(
x
2
,
f
(
x
1
,
x
2
,
x
)
)
]
{\displaystyle {\begin{aligned}&E(A_{p})\!:\;R(a_{2},a_{3})\land \ldots \land R(a_{p-1},a_{p})\land H(a_{2},a_{p+1})\land \neg H(a_{p},x_{p})\\&E(P_{p})\!:\;E(A_{p})\land [\neg R(x_{1},x_{2})\lor \neg H(x_{1},x)\lor H(x_{2},f(x_{1},x_{2}))]\\&E(Q_{p})\!:\;E(A_{p})\land [\neg R(x_{1},x_{2})\lor \neg H(x_{1},x)\lor H(x_{2},f(x_{1},x_{2},x))]\\\\\end{aligned}}}
Clauses
Q
p
:
R
2
=
{
R
(
a
2
,
a
3
)
}
,
⋯
,
R
p
−
1
=
{
R
(
a
p
−
1
,
a
p
)
}
,
H
2
=
{
H
(
a
2
,
a
p
+
1
)
}
,
H
¬
p
=
{
¬
H
(
a
p
,
x
p
)
}
,
R
H
=
{
¬
R
(
x
1
,
x
2
)
,
¬
H
(
x
1
,
x
)
,
H
(
x
2
,
f
(
x
1
,
x
2
,
x
)
)
}
{\displaystyle {\begin{alignedat}{2}&{\text{Clauses }}Q_{p}\!:\;\;&&R_{2}=\{R(a_{2},a_{3})\},\\&&&\cdots ,\\&&&R_{p-1}=\{R(a_{p-1},a_{p})\},\\&&&H_{2}=\{H(a_{2},a_{p+1})\},\\&&&H_{\neg p}=\{\neg H(a_{p},x_{p})\},\\&&&RH=\{\neg R(x_{1},x_{2}),\;\neg H(x_{1},x),\;H(x_{2},f(x_{1},x_{2},x))\}\\\\\end{alignedat}}}
Resolvents:
Q
5
R
2
,
R
H
[
a
2
/
x
1
,
a
3
/
x
2
]
=
{
R
(
a
2
,
a
3
)
}
,
{
¬
R
(
a
2
,
a
3
)
,
¬
H
(
a
2
,
x
)
,
H
(
a
3
,
f
(
a
2
,
a
3
,
x
)
)
}
H
¬
2
,
3
=
{
¬
H
(
a
2
,
x
)
,
H
(
a
3
,
f
(
a
2
,
a
3
,
x
)
)
}
H
2
,
H
¬
2
,
3
[
a
p
+
1
/
x
]
=
{
H
(
a
2
,
a
p
+
1
)
}
,
{
¬
H
(
a
2
,
a
p
+
1
)
,
H
(
a
3
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
}
H
3
=
{
H
(
a
3
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
}
R
3
,
R
H
[
a
3
/
x
1
,
a
4
/
x
2
]
=
{
R
(
a
3
,
a
4
)
}
,
{
¬
R
(
a
3
,
a
4
)
,
¬
H
(
a
3
,
x
)
,
H
(
a
4
,
f
(
a
3
,
a
4
,
x
)
)
}
H
¬
3
,
4
=
{
¬
H
(
a
3
,
x
)
,
H
(
a
4
,
f
(
a
3
,
a
4
,
x
)
)
}
H
3
,
H
¬
3
,
4
[
f
(
a
2
,
a
3
,
a
p
+
1
)
/
x
]
=
{
H
(
a
3
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
}
,
{
¬
H
(
a
3
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
,
H
(
a
4
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
)
}
H
4
=
H
(
a
4
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
R
4
,
R
H
[
a
4
/
x
1
,
a
5
/
x
2
]
=
{
R
(
a
4
,
a
5
)
}
,
{
¬
R
(
a
4
,
a
5
)
,
¬
H
(
a
4
,
x
)
,
H
(
a
5
,
f
(
a
4
,
a
5
,
x
)
)
}
H
¬
4
,
5
=
{
¬
H
(
a
4
,
x
)
,
H
(
a
5
,
f
(
a
4
,
a
5
,
x
)
)
}
H
4
,
H
¬
4
,
5
[
f
(
a
3
,
a
4
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
/
x
]
=
{
H
(
a
4
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
}
,
{
¬
H
(
a
4
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
,
H
(
a
5
,
f
(
a
4
,
a
5
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
)
}
H
5
=
H
(
a
5
,
f
(
a
4
,
a
5
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
)
}
H
5
,
H
¬
5
[
f
(
a
4
,
a
5
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
)
/
x
p
]
=
{
¬
H
(
a
5
,
f
(
a
4
,
a
5
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
)
}
,
{
H
(
a
5
,
f
(
a
4
,
a
5
,
f
(
a
3
,
a
4
,
f
(
a
2
,
a
3
,
a
p
+
1
)
)
)
)
}
R
e
s
u
l
t
=
{
}
{\displaystyle {\begin{alignedat}{2}&{\text{Resolvents: }}Q_{5}\\&\quad R_{2},RH\;[a_{2}/x_{1},a_{3}/x_{2}]\;=\;&&\{R(a_{2},a_{3})\},\;\{\neg R(a_{2},a_{3}),\;\neg H(a_{2},x),\;H(a_{3},f(a_{2},a_{3},x))\}\\&\quad H_{\neg 2,3}\;=&&\{\neg H(a_{2},x),\;H(a_{3},f(a_{2},a_{3},x))\}\\&\quad H_{2},H_{\neg 2,3}\;[a_{p+1}/x]\;=\;&&\{H(a_{2},a_{p+1})\},\{\neg H(a_{2},a_{p+1}),\;H(a_{3},f(a_{2},a_{3},a_{p+1}))\}\\&\quad H_{3}=&&\{H(a_{3},f(a_{2},a_{3},a_{p+1}))\}\\\\&\quad R_{3},RH\;[a_{3}/x_{1},a_{4}/x_{2}]\;=\;&&\{R(a_{3},a_{4})\},\;\{\neg R(a_{3},a_{4}),\;\neg H(a_{3},x),\;H(a_{4},f(a_{3},a_{4},x))\}\\&\quad H_{\neg 3,4}\;=&&\{\neg H(a_{3},x),\;H(a_{4},f(a_{3},a_{4},x))\}\\&\quad H_{3},H_{\neg 3,4}\;[f(a_{2},a_{3},a_{p+1})/x]\;=\;&&\{H(a_{3},f(a_{2},a_{3},a_{p+1}))\},\\&&&\quad \{\neg H(a_{3},f(a_{2},a_{3},a_{p+1})),H(a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))\}\\&\quad H_{4}=&&H(a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1}))\\\\&\quad R_{4},RH\;[a_{4}/x_{1},a_{5}/x_{2}]\;=\;&&\{R(a_{4},a_{5})\},\;\{\neg R(a_{4},a_{5}),\;\neg H(a_{4},x),H(a_{5},f(a_{4},a_{5},x))\}\\&\quad H_{\neg 4,5}\;=&&\{\neg H(a_{4},x),\;H(a_{5},f(a_{4},a_{5},x))\}\\&\quad H_{4},H_{\neg 4,5}\\&\qquad [f(a_{3},a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1}))/x]\;=\;&&\{H(a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})\},\\&&&\quad \{\neg H(a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})),\;H(a_{5},f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))\}\\&\quad H_{5}=H(a_{5},f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))\}\\\\&\quad H_{5},H_{\neg 5}\\&\qquad [f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))/x_{p}]\,=&&\{\neg H(a_{5},f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))\},\\&&&\qquad \{H(a_{5},f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1}))))\}\\&\quad Result=&&\{\;\}\\\end{alignedat}}}
Definitions
edit
Herbrand's Theorem. (Example 1)
edit
(1) Validity Example:
∀
x
A
(
x
)
∨
∀
x
B
(
x
)
⟹
∀
x
[
A
(
x
)
∨
B
(
x
)
]
¬
[
∀
x
A
(
x
)
∨
∀
x
B
(
x
)
]
∨
∀
x
[
A
(
x
)
∨
B
(
x
)
]
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
∀
x
[
A
(
x
)
∨
B
(
x
)
]
[
∃
x
(
¬
A
(
x
)
)
∧
∃
y
(
¬
B
(
y
)
)
]
∨
∀
x
[
A
(
x
)
∨
B
(
x
)
]
[
¬
A
(
x
r
)
)
∧
¬
B
(
y
r
)
]
∨
[
A
(
x
g
)
∨
B
(
x
g
)
]
Validity Functional Form:
[
¬
A
(
f
x
)
∧
¬
B
(
f
y
)
]
∨
[
A
(
x
)
∨
B
(
x
)
]
Expansion:
[
¬
A
(
f
x
)
∧
¬
B
(
f
y
)
]
∨
[
A
(
f
x
)
∨
B
(
f
x
)
]
∨
[
¬
A
(
f
x
)
∧
¬
B
(
f
y
)
]
∨
[
A
(
f
y
)
∨
B
(
f
y
)
]
{\displaystyle {\begin{alignedat}{2}&\!\!\!\!{\text{(1) Validity Example:}}&&\\\;\;&\quad \forall x\,A(x)\lor \forall x\,B(x)\!\!\!&&\implies \forall x\,[A(x)\lor B(x)]\\&\neg \,[\forall x\,A(x)\lor \forall x\,B(x)]&&\lor \quad \forall x\,[A(x)\lor B(x)]\\&[\exists x\,(\neg A(x))\land \exists x\,(\neg B(x))]&&\lor \quad \forall x\,[A(x)\lor B(x)]\\&[\exists x\,(\neg A(x))\land \exists y\,(\neg B(y))]&&\lor \quad \forall x\,[A(x)\lor B(x)]\\&[\neg A(x_{r}))\land \neg B(y_{r})]&&\lor \quad [A(x_{g})\lor B(x_{g})]\\\\&\!\!\!\!{\text{Validity Functional Form:}}&&\\&[\neg A(f_{x})\land \neg B(f_{y})]&&\lor \quad [A(x)\lor B(x)]\\\\&\!\!\!\!{\text{Expansion:}}\\&[\neg A(f_{x})\land \neg B(f_{y})]&&\lor \quad [A(f_{x})\lor B(f_{x})]\quad \lor \\&[\neg A(f_{x})\land \neg B(f_{y})]&&\lor \quad [A(f_{y})\lor B(f_{y})]\\\end{alignedat}}}
Expansion is always true:
If expansion is false, then 2nd and 4th conjuncts imply
A
(
f
x
)
=
B
(
f
y
)
=
F
,
which implies first conjunct is
T
.
Therefore, expansion is always true.
{\displaystyle {\begin{aligned}&{\text{Expansion is always true: }}\,{\text{ If expansion is false, then 2nd and 4th conjuncts imply }}A(f_{x})=B(f_{y})=F,\\&{\text{which implies first conjunct is }}T.{\text{ Therefore, expansion is always true.}}\\\end{aligned}}}
Proof from expansion:
[
¬
A
(
f
A
)
∧
¬
B
(
f
B
)
]
∨
[
A
(
f
A
)
∨
B
(
f
A
)
]
∨
[
¬
A
(
f
A
)
∧
¬
B
(
f
B
)
]
∨
[
A
(
f
B
)
∨
B
(
f
B
)
]
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
[
A
(
f
A
)
∨
B
(
f
A
)
]
∨
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
[
A
(
f
B
)
∨
B
(
f
B
)
]
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
∀
x
[
A
(
x
)
∨
B
(
x
)
]
∨
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
[
A
(
f
B
)
∨
B
(
f
B
)
]
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
∀
x
[
A
(
x
)
∨
B
(
x
)
]
∨
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
∀
x
[
A
(
x
)
∨
B
(
x
)
]
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
∀
x
[
A
(
x
)
∨
B
(
x
)
]
{\displaystyle {\begin{aligned}&{\text{Proof from expansion: }}\\&[\neg A(f_{A})\land \neg B(f_{B})]\lor [A(f_{A})\lor B(f_{A})]\lor [\neg A(f_{A})\land \neg B(f_{B})]\lor [A(f_{B})\lor B(f_{B})]\\&[\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor [A(f_{A})\lor B(f_{A})]\lor [\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor [A(f_{B})\lor B(f_{B})]\\&[\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor \forall x[A(x)\lor B(x)]\lor [\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor [A(f_{B})\lor B(f_{B})]\\&[\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor \forall x[A(x)\lor B(x)]\lor [\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor \forall x[A(x)\lor B(x)]\\&[\exists x\,(\neg A(x))\land \exists x\,(\neg B(x))]\lor \forall x\,[A(x)\lor B(x)]\\\end{aligned}}}
(2) Satisfiability Example:
¬
{
∀
x
A
(
x
)
∨
∀
x
B
(
x
)
⟹
∀
x
[
A
(
x
)
∨
B
(
x
)
]
}
¬
{
¬
[
∀
x
A
(
x
)
∨
∀
x
B
(
x
)
]
∨
∀
x
[
A
(
x
)
∨
B
(
x
)
]
}
[
∀
x
A
(
x
)
∨
∀
x
B
(
x
)
]
∧
¬
∀
x
[
A
(
x
)
∨
B
(
x
)
]
[
∀
x
A
(
x
)
∨
∀
x
B
(
x
)
]
∧
∃
x
[
¬
A
(
x
)
∧
¬
B
(
x
)
]
[
∀
x
A
(
x
)
∨
∀
y
B
(
y
)
]
∧
∃
x
[
¬
A
(
x
)
∧
¬
B
(
x
)
]
[
A
(
x
g
)
∨
B
(
y
g
)
]
∧
[
¬
A
(
x
r
)
∧
¬
B
(
x
r
)
]
Satisfiability Functional F
orm:
[
A
(
x
)
∨
B
(
y
)
]
∧
[
¬
A
(
f
x
)
∧
¬
B
(
f
x
)
]
Expansion:
[
A
(
f
x
)
∨
B
(
f
x
)
]
∧
[
¬
A
(
f
x
)
∧
¬
B
(
f
x
)
]
{\displaystyle {\begin{alignedat}{2}&\!\!\!\!{\text{(2) Satisfiability Example:}}&&\\\;\;&\quad \neg \,\{\forall x\,A(x)\lor \forall x\,B(x)\;&&\implies \forall x\,[A(x)\lor B(x)]\}\\&\neg \,\{\neg \,[\forall x\,A(x)\lor \forall x\,B(x)]\;&&\lor \;\forall x\,[A(x)\lor B(x)]\}\\&\quad [\forall x\,A(x)\lor \forall x\,B(x)]\;&&\land \;\neg \,\forall x\,[A(x)\lor B(x)]\\&\quad [\forall x\,A(x)\lor \forall x\,B(x)]\;&&\land \;\exists x\,[\neg A(x)\land \neg B(x)]\\&\quad [\forall x\,A(x)\lor \forall y\,B(y)]\;&&\land \;\exists x\,[\neg A(x)\land \neg B(x)]\\&\quad [A(x_{g})\lor B(y_{g})]\;&&\land \;[\neg A(x_{r})\land \neg B(x_{r})]\\\\&{\text{Satisfiability Functional F}}&&{\text{orm:}}&&\\&\quad [A(x)\lor B(y)]&&\land \quad [\neg A(f_{x})\land \neg B(f_{x})]\\\\&{\text{Expansion:}}\\&\quad [A(f_{x})\lor B(f_{x})]\!\!\!&&\land \quad [\neg A(f_{x})\land \neg B(f_{x})]\\\end{alignedat}}}
Expansion is always false:
If expansion is true, then first conjunct implies
A
(
f
x
)
=
B
(
f
x
)
=
T
,
which implies 2nd conjunct is
F
.
Therefore, expansion is always false.
{\displaystyle {\begin{aligned}&{\text{Expansion is always false: }}\,{\text{ If expansion is true, then first conjunct implies }}A(f_{x})=B(f_{x})=T,\\&{\text{which implies 2nd conjunct is }}F.{\text{ Therefore, expansion is always false.}}\\\end{aligned}}}
Herbrand's Theorem. (Example 2)
edit
(1) Validity Example:
∃
x
∀
y
A
(
x
,
y
)
⟹
∀
y
∃
x
A
(
x
,
y
)
¬
∃
x
∀
y
A
(
x
,
y
)
∨
∀
y
∃
x
A
(
x
,
y
)
¬
∀
x
∃
y
A
(
x
,
y
)
∨
∀
y
∃
x
A
(
x
,
y
)
Validity Functional Form:
Expansion:
[
¬
A
(
f
x
)
∧
¬
B
(
f
y
)
]
∨
[
A
(
f
x
)
∨
B
(
f
x
)
]
∨
[
¬
A
(
f
x
)
∧
¬
B
(
f
y
)
]
∨
[
A
(
f
y
)
∨
B
(
f
y
)
]
{\displaystyle {\begin{alignedat}{2}&\!\!\!\!{\text{(1) Validity Example:}}&&\\\;\;&\quad \exists x\,\forall yA(x,y)\implies \forall y\,\exists x\,A(x,y)\\\;\;&\quad \neg \exists x\,\forall yA(x,y)\lor \forall y\,\exists x\,A(x,y)\\\;\;&\quad \neg \forall x\,\exists yA(x,y)\lor \forall y\,\exists x\,A(x,y)\\&\!\!\!\!{\text{Validity Functional Form:}}&&\\\\&\!\!\!\!{\text{Expansion:}}\\&[\neg A(f_{x})\land \neg B(f_{y})]&&\lor \quad [A(f_{x})\lor B(f_{x})]\quad \lor \\&[\neg A(f_{x})\land \neg B(f_{y})]&&\lor \quad [A(f_{y})\lor B(f_{y})]\\\end{alignedat}}}
Expansion is always true:
If expansion is false, then 2nd and 4th conjuncts imply
A
(
f
x
)
=
B
(
f
y
)
=
F
,
which implies first conjunct is
T
.
Therefore, expansion is always true.
{\displaystyle {\begin{aligned}&{\text{Expansion is always true: }}\,{\text{ If expansion is false, then 2nd and 4th conjuncts imply }}A(f_{x})=B(f_{y})=F,\\&{\text{which implies first conjunct is }}T.{\text{ Therefore, expansion is always true.}}\\\end{aligned}}}
Proof from expansion:
[
¬
A
(
f
A
)
∧
¬
B
(
f
B
)
]
∨
[
A
(
f
A
)
∨
B
(
f
A
)
]
∨
[
¬
A
(
f
A
)
∧
¬
B
(
f
B
)
]
∨
[
A
(
f
B
)
∨
B
(
f
B
)
]
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
[
A
(
f
A
)
∨
B
(
f
A
)
]
∨
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
[
A
(
f
B
)
∨
B
(
f
B
)
]
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
∀
x
[
A
(
x
)
∨
B
(
x
)
]
∨
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
[
A
(
f
B
)
∨
B
(
f
B
)
]
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
∀
x
[
A
(
x
)
∨
B
(
x
)
]
∨
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
∀
x
[
A
(
x
)
∨
B
(
x
)
]
[
∃
x
(
¬
A
(
x
)
)
∧
∃
x
(
¬
B
(
x
)
)
]
∨
∀
x
[
A
(
x
)
∨
B
(
x
)
]
{\displaystyle {\begin{aligned}&{\text{Proof from expansion: }}\\&[\neg A(f_{A})\land \neg B(f_{B})]\lor [A(f_{A})\lor B(f_{A})]\lor [\neg A(f_{A})\land \neg B(f_{B})]\lor [A(f_{B})\lor B(f_{B})]\\&[\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor [A(f_{A})\lor B(f_{A})]\lor [\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor [A(f_{B})\lor B(f_{B})]\\&[\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor \forall x[A(x)\lor B(x)]\lor [\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor [A(f_{B})\lor B(f_{B})]\\&[\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor \forall x[A(x)\lor B(x)]\lor [\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor \forall x[A(x)\lor B(x)]\\&[\exists x\,(\neg A(x))\land \exists x\,(\neg B(x))]\lor \forall x\,[A(x)\lor B(x)]\\\end{aligned}}}
(2) Satisfiability Example:
¬
{
∀
x
A
(
x
)
∨
∀
x
B
(
x
)
⟹
∀
x
[
A
(
x
)
∨
B
(
x
)
]
}
¬
{
¬
[
∀
x
A
(
x
)
∨
∀
x
B
(
x
)
]
∨
∀
x
[
A
(
x
)
∨
B
(
x
)
]
}
[
∀
x
A
(
x
)
∨
∀
x
B
(
x
)
]
∧
¬
∀
x
[
A
(
x
)
∨
B
(
x
)
]
[
∀
x
A
(
x
)
∨
∀
x
B
(
x
)
]
∧
∃
x
[
¬
A
(
x
)
∧
¬
B
(
x
)
]
[
∀
x
A
(
x
)
∨
∀
y
B
(
y
)
]
∧
∃
x
[
¬
A
(
x
)
∧
¬
B
(
x
)
]
[
A
(
x
g
)
∨
B
(
y
g
)
]
∧
[
¬
A
(
x
r
)
∧
¬
B
(
x
r
)
]
Satisfiability Functional F
orm:
[
A
(
x
)
∨
B
(
y
)
]
∧
[
¬
A
(
f
x
)
∧
¬
B
(
f
x
)
]
Expansion:
[
A
(
f
x
)
∨
B
(
f
x
)
]
∧
[
¬
A
(
f
x
)
∧
¬
B
(
f
x
)
]
{\displaystyle {\begin{alignedat}{2}&\!\!\!\!{\text{(2) Satisfiability Example:}}&&\\\;\;&\quad \neg \,\{\forall x\,A(x)\lor \forall x\,B(x)\;&&\implies \forall x\,[A(x)\lor B(x)]\}\\&\neg \,\{\neg \,[\forall x\,A(x)\lor \forall x\,B(x)]\;&&\lor \;\forall x\,[A(x)\lor B(x)]\}\\&\quad [\forall x\,A(x)\lor \forall x\,B(x)]\;&&\land \;\neg \,\forall x\,[A(x)\lor B(x)]\\&\quad [\forall x\,A(x)\lor \forall x\,B(x)]\;&&\land \;\exists x\,[\neg A(x)\land \neg B(x)]\\&\quad [\forall x\,A(x)\lor \forall y\,B(y)]\;&&\land \;\exists x\,[\neg A(x)\land \neg B(x)]\\&\quad [A(x_{g})\lor B(y_{g})]\;&&\land \;[\neg A(x_{r})\land \neg B(x_{r})]\\\\&{\text{Satisfiability Functional F}}&&{\text{orm:}}&&\\&\quad [A(x)\lor B(y)]&&\land \quad [\neg A(f_{x})\land \neg B(f_{x})]\\\\&{\text{Expansion:}}\\&\quad [A(f_{x})\lor B(f_{x})]\!\!\!&&\land \quad [\neg A(f_{x})\land \neg B(f_{x})]\\\end{alignedat}}}
Expansion is always false:
If expansion is true, then first conjunct implies
A
(
f
x
)
=
B
(
f
x
)
=
T
,
which implies 2nd conjunct is
F
.
Therefore, expansion is always false.
{\displaystyle {\begin{aligned}&{\text{Expansion is always false: }}\,{\text{ If expansion is true, then first conjunct implies }}A(f_{x})=B(f_{x})=T,\\&{\text{which implies 2nd conjunct is }}F.{\text{ Therefore, expansion is always false.}}\\\end{aligned}}}
![{\displaystyle {\begin{aligned}\\&A_{p}\!:\;\exists y_{2}\cdots \exists y_{p+1}[R(y_{2},y_{3})\land \ldots \land R(y_{p-1},y_{p})\land H(y_{2},y_{p+1})\land \forall x_{p}\neg H(y_{p},x_{p})]\\&P_{p}\!:\;A_{p}\land \forall x_{1}\forall x_{2}[\neg R(x_{1},x_{2})\lor \forall x\neg H(x_{1},x)\lor \exists yH(x_{2},y))]\\&Q_{p}\!:\;A_{p}\land \forall x_{1}\forall x_{2}[\neg R(x_{1},x_{2})\lor \forall x\{\neg H(x_{1},x)\lor \exists yH(x_{2},y)\}]\\\\\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9b326b7b93fc5ba7325462e0462202aa86883a72)
![{\displaystyle {\begin{aligned}&E(A_{p})\!:\;R(a_{2},a_{3})\land \ldots \land R(a_{p-1},a_{p})\land H(a_{2},a_{p+1})\land \neg H(a_{p},x_{p})\\&E(P_{p})\!:\;E(A_{p})\land [\neg R(x_{1},x_{2})\lor \neg H(x_{1},x)\lor H(x_{2},f(x_{1},x_{2}))]\\&E(Q_{p})\!:\;E(A_{p})\land [\neg R(x_{1},x_{2})\lor \neg H(x_{1},x)\lor H(x_{2},f(x_{1},x_{2},x))]\\\\\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b595aaff786ef907d8b0cc206075e0dcadb6e216)
![{\displaystyle {\begin{alignedat}{2}&{\text{Resolvents: }}P_{5}\\&\qquad R_{2},RH\;[a_{2}/x_{1},a_{3}/x_{2}]\;=\;&&\{R(a_{2},a_{3})\},\;\{\neg R(a_{2},a_{3}),\;\neg H(a_{2},x),\;H(a_{3},f(a_{2},a_{3}))\}\\&\qquad H_{\neg 2,3}\;=&&\{\neg H(a_{2},x),\;H(a_{3},f(a_{2},a_{3}))\}\\&\qquad H_{2},H_{\neg 2,3}\;[a_{p+1}/x]\;=\;&&\{H(a_{2},a_{p+1})\},\{\neg H(a_{2},a_{p+1}),\;H(a_{3},f(a_{2},a_{3}))\}\\&\qquad H_{3}=&&\{H(a_{3},f(a_{2},a_{3}))\}\\\\&\qquad R_{3},RH\;[a_{3}/x_{1},a_{4}/x_{2}]\;=\;&&\{R(a_{3},a_{4})\},\;\{\neg R(a_{3},a_{4}),\;\neg H(a_{3},x),\;H(a_{4},f(a_{3},a_{4}))\}\\&\qquad H_{\neg 3,4}\;=&&\{\neg H(a_{3},x),\;H(a_{4},f(a_{3},a_{4}))\}\\&\qquad H_{3},H_{\neg 3,4}\;[f(a_{2},a_{3})/x]\;=\;&&\{H(a_{3},f(a_{2},a_{3}))\},\{\neg H(a_{3},f(a_{2},a_{3})),\;H(a_{4},f(a_{3},a_{4}))\}\\&\qquad H_{4}=&&\{H(a_{4},f(a_{3},a_{4}))\}\\\\&\qquad R_{4},RH\;[a_{4}/x_{1},a_{5}/x_{2}]\;=\;&&\{R(a_{4},a_{5})\},\;\{\neg R(a_{4},a_{5}),\;\neg H(a_{4},x),\;H(a_{5},f(a_{4},a_{5}))\}\\&\qquad H_{\neg 4,5}\;=&&\{\neg H(a_{4},x),\;H(a_{5},f(a_{4},a_{5}))\}\\&\qquad H_{4},H_{\neg 4,5}\;[f(a_{3},a_{4})/x]\;=\;&&\{H(a_{4},f(a_{3},a_{4}))\},\{\neg H(a_{4},f(a_{3},a_{4})),\;H(a_{5},f(a_{4},a_{5}))\}\\&\qquad H_{5}=&&\{H(a_{5},f(a_{4},a_{5}))\}\\\\&\qquad H_{\neg 5},H_{5},\,[f(a_{4},a_{5})/x_{p}]\,=&&\{\neg H(a_{5},f(a_{4},a_{5}))\},\{H(a_{5},f(a_{4},a_{5}))\}\\&\qquad Result=&&\{\;\}\\\end{alignedat}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/df7f4e1bcd5018cdec0760d68f2b1ab65bd071cd)
![{\displaystyle {\begin{alignedat}{2}&{\text{Resolvents: }}Q_{5}\\&\quad R_{2},RH\;[a_{2}/x_{1},a_{3}/x_{2}]\;=\;&&\{R(a_{2},a_{3})\},\;\{\neg R(a_{2},a_{3}),\;\neg H(a_{2},x),\;H(a_{3},f(a_{2},a_{3},x))\}\\&\quad H_{\neg 2,3}\;=&&\{\neg H(a_{2},x),\;H(a_{3},f(a_{2},a_{3},x))\}\\&\quad H_{2},H_{\neg 2,3}\;[a_{p+1}/x]\;=\;&&\{H(a_{2},a_{p+1})\},\{\neg H(a_{2},a_{p+1}),\;H(a_{3},f(a_{2},a_{3},a_{p+1}))\}\\&\quad H_{3}=&&\{H(a_{3},f(a_{2},a_{3},a_{p+1}))\}\\\\&\quad R_{3},RH\;[a_{3}/x_{1},a_{4}/x_{2}]\;=\;&&\{R(a_{3},a_{4})\},\;\{\neg R(a_{3},a_{4}),\;\neg H(a_{3},x),\;H(a_{4},f(a_{3},a_{4},x))\}\\&\quad H_{\neg 3,4}\;=&&\{\neg H(a_{3},x),\;H(a_{4},f(a_{3},a_{4},x))\}\\&\quad H_{3},H_{\neg 3,4}\;[f(a_{2},a_{3},a_{p+1})/x]\;=\;&&\{H(a_{3},f(a_{2},a_{3},a_{p+1}))\},\\&&&\quad \{\neg H(a_{3},f(a_{2},a_{3},a_{p+1})),H(a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))\}\\&\quad H_{4}=&&H(a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1}))\\\\&\quad R_{4},RH\;[a_{4}/x_{1},a_{5}/x_{2}]\;=\;&&\{R(a_{4},a_{5})\},\;\{\neg R(a_{4},a_{5}),\;\neg H(a_{4},x),H(a_{5},f(a_{4},a_{5},x))\}\\&\quad H_{\neg 4,5}\;=&&\{\neg H(a_{4},x),\;H(a_{5},f(a_{4},a_{5},x))\}\\&\quad H_{4},H_{\neg 4,5}\\&\qquad [f(a_{3},a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1}))/x]\;=\;&&\{H(a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})\},\\&&&\quad \{\neg H(a_{4},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})),\;H(a_{5},f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))\}\\&\quad H_{5}=H(a_{5},f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))\}\\\\&\quad H_{5},H_{\neg 5}\\&\qquad [f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))/x_{p}]\,=&&\{\neg H(a_{5},f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1})))\},\\&&&\qquad \{H(a_{5},f(a_{4},a_{5},f(a_{3},a_{4},f(a_{2},a_{3},a_{p+1}))))\}\\&\quad Result=&&\{\;\}\\\end{alignedat}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6c91ae6788578aad5bb271bf47ac88b46aced0ba)
![{\displaystyle {\begin{alignedat}{2}&{\text{Axioms }}P_{p}\!:\;\;&&R_{2}\!:\;R(a_{2},a_{3}),\\&&&\cdots ,\\&&&R_{p-1}\!:\;R(a_{p-1},a_{p})\,\\&&&H_{2}\!:\;H(a_{2},a_{p+1})\,\\&&&H_{\neg p}\!:\;\neg H(a_{p},x_{p})\ \\&&&RH\!:\;R(x_{1},x_{2})\implies [H(x_{1},x)\implies H(x_{2},f(x_{1},x_{2}))]\\\\\end{alignedat}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a18be39a44bc04288ef7ea927617516ba6033964)
![{\displaystyle {\begin{alignedat}{2}&{\text{Deduction: }}P_{5}\\&\qquad R_{2};RH\;[a_{2}/x_{1},a_{3}/x_{2}]\!:\;&&R(a_{2},a_{3});\;\,R(a_{2},a_{3})\implies [H(a_{2},x)\implies H(a_{3},f(a_{2},a_{3}))]\\&\qquad H_{2\Rightarrow 3}\!:\;&&H(a_{2},x)\implies H(a_{3},f(a_{2},a_{3}))\\&\qquad H_{2};H_{2\Rightarrow 3}\;[a_{p+1}/x]\!:\;&&H(a_{2},a_{p+1});\;\,H(a_{2},a_{p+1})\implies H(a_{3},f(a_{2},a_{3}))\\&\qquad H_{3}\!:\;&&H(a_{3},f(a_{2},a_{3}))\\\\&\qquad R_{3};RH\;[a_{3}/x_{1},a_{4}/x_{2}]\!:\;&&R(a_{3},a_{4});\;\,R(a_{3},a_{4})\implies [H(a_{3},x)\implies H(a_{4},f(a_{3},a_{4}))]\\&\qquad H_{3\Rightarrow 4}\!:\;&&H(a_{3},x)\implies H(a_{4},f(a_{3},a_{4}))\\&\qquad H_{3};H_{3\Rightarrow 4}\;[f(a_{3},a_{4}))/x]\!:\;&&H(a_{3},f(a_{3},a_{4}));\;\,H(a_{3},f(a_{3},a_{4}))\implies H(a_{4},f(a_{3},a_{4}))\\&\qquad H_{4}\!:\;&&H(a_{4},f(a_{3},a_{4}))\\\\&\qquad R_{4};RH\;[a_{4}/x_{1},a_{5}/x_{2}]\!:\;&&R(a_{4},a_{5});\;\,R(a_{4},a_{5})\implies [H(a_{4},x)\implies H(a_{5},f(a_{4},a_{5}))]\\&\qquad H_{4\Rightarrow 5}\!:\;&&H(a_{4},x)\implies H(a_{5},f(a_{4},a_{5}))\\&\qquad H_{4};H_{4\Rightarrow 5}\;[f(a_{4},a_{5}))/x]\!:\;\;&&H(a_{4},f(a_{4},a_{5}));\;\,H(a_{4},f(a_{4},a_{5}))\implies H(a_{5},f(a_{4},a_{5}))\\&\qquad H_{5}\!:\;&&H(a_{5},f(a_{4},a_{5}))\\\\&\qquad H_{\neg 5},H_{5}\;[f(a_{4},a_{5})/x_{p}]\!:\;&&\neg H(a_{5},f(a_{4},a_{5}));\;H(a_{5},f(a_{4},a_{5}))\\&\qquad Result\!:\,&&FALSE\\\end{alignedat}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/04a9b9d7d072fe0de29b02e23c25fc0ae3c2358e)
![{\displaystyle {\begin{alignedat}{2}&\!\!\!\!{\text{(1) Validity Example:}}&&\\\;\;&\quad \forall x\,A(x)\lor \forall x\,B(x)\!\!\!&&\implies \forall x\,[A(x)\lor B(x)]\\&\neg \,[\forall x\,A(x)\lor \forall x\,B(x)]&&\lor \quad \forall x\,[A(x)\lor B(x)]\\&[\exists x\,(\neg A(x))\land \exists x\,(\neg B(x))]&&\lor \quad \forall x\,[A(x)\lor B(x)]\\&[\exists x\,(\neg A(x))\land \exists y\,(\neg B(y))]&&\lor \quad \forall x\,[A(x)\lor B(x)]\\&[\neg A(x_{r}))\land \neg B(y_{r})]&&\lor \quad [A(x_{g})\lor B(x_{g})]\\\\&\!\!\!\!{\text{Validity Functional Form:}}&&\\&[\neg A(f_{x})\land \neg B(f_{y})]&&\lor \quad [A(x)\lor B(x)]\\\\&\!\!\!\!{\text{Expansion:}}\\&[\neg A(f_{x})\land \neg B(f_{y})]&&\lor \quad [A(f_{x})\lor B(f_{x})]\quad \lor \\&[\neg A(f_{x})\land \neg B(f_{y})]&&\lor \quad [A(f_{y})\lor B(f_{y})]\\\end{alignedat}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/74774dfbb7e3851ef9699417cec79ecd5bd56a09)
![{\displaystyle {\begin{aligned}&{\text{Proof from expansion: }}\\&[\neg A(f_{A})\land \neg B(f_{B})]\lor [A(f_{A})\lor B(f_{A})]\lor [\neg A(f_{A})\land \neg B(f_{B})]\lor [A(f_{B})\lor B(f_{B})]\\&[\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor [A(f_{A})\lor B(f_{A})]\lor [\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor [A(f_{B})\lor B(f_{B})]\\&[\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor \forall x[A(x)\lor B(x)]\lor [\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor [A(f_{B})\lor B(f_{B})]\\&[\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor \forall x[A(x)\lor B(x)]\lor [\exists x(\neg A(x))\land \exists x(\neg B(x))]\lor \forall x[A(x)\lor B(x)]\\&[\exists x\,(\neg A(x))\land \exists x\,(\neg B(x))]\lor \forall x\,[A(x)\lor B(x)]\\\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/40d51d0f0f601a7020364dc84840a9b830ff866c)
![{\displaystyle {\begin{alignedat}{2}&\!\!\!\!{\text{(2) Satisfiability Example:}}&&\\\;\;&\quad \neg \,\{\forall x\,A(x)\lor \forall x\,B(x)\;&&\implies \forall x\,[A(x)\lor B(x)]\}\\&\neg \,\{\neg \,[\forall x\,A(x)\lor \forall x\,B(x)]\;&&\lor \;\forall x\,[A(x)\lor B(x)]\}\\&\quad [\forall x\,A(x)\lor \forall x\,B(x)]\;&&\land \;\neg \,\forall x\,[A(x)\lor B(x)]\\&\quad [\forall x\,A(x)\lor \forall x\,B(x)]\;&&\land \;\exists x\,[\neg A(x)\land \neg B(x)]\\&\quad [\forall x\,A(x)\lor \forall y\,B(y)]\;&&\land \;\exists x\,[\neg A(x)\land \neg B(x)]\\&\quad [A(x_{g})\lor B(y_{g})]\;&&\land \;[\neg A(x_{r})\land \neg B(x_{r})]\\\\&{\text{Satisfiability Functional F}}&&{\text{orm:}}&&\\&\quad [A(x)\lor B(y)]&&\land \quad [\neg A(f_{x})\land \neg B(f_{x})]\\\\&{\text{Expansion:}}\\&\quad [A(f_{x})\lor B(f_{x})]\!\!\!&&\land \quad [\neg A(f_{x})\land \neg B(f_{x})]\\\end{alignedat}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/97364d7bba506ed476c8972fc658deedef1afb6e)
![{\displaystyle {\begin{alignedat}{2}&\!\!\!\!{\text{(1) Validity Example:}}&&\\\;\;&\quad \exists x\,\forall yA(x,y)\implies \forall y\,\exists x\,A(x,y)\\\;\;&\quad \neg \exists x\,\forall yA(x,y)\lor \forall y\,\exists x\,A(x,y)\\\;\;&\quad \neg \forall x\,\exists yA(x,y)\lor \forall y\,\exists x\,A(x,y)\\&\!\!\!\!{\text{Validity Functional Form:}}&&\\\\&\!\!\!\!{\text{Expansion:}}\\&[\neg A(f_{x})\land \neg B(f_{y})]&&\lor \quad [A(f_{x})\lor B(f_{x})]\quad \lor \\&[\neg A(f_{x})\land \neg B(f_{y})]&&\lor \quad [A(f_{y})\lor B(f_{y})]\\\end{alignedat}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/48bf34894928874e2790c66c6b8bfc264454a652)