# Exercises #3 – Quantified Theories

These were pulled from Exercises for [latex]\S[/latex]3 and Exercises for [latex]\S[/latex]4 of Chapter I in Bourbaki’s set theory book.

Let [latex]A[/latex] be a relation in logical theory [latex]\mathfrak{T}[/latex]. If [latex]A\iff (\mbox{not } A)[/latex] is a theorem in [latex]\mathfrak{T}[/latex], show that [latex]\mathfrak{T}[/latex] is contradictory.

The negation of [latex]A\iff (\mbox{not } A)[/latex] is itself, so its negation must also be a theorem by hypothesis, implying [latex]\mathfrak{T}[/latex] is contradictory.

Let [latex]A[/latex] and [latex]B[/latex] be relations in [latex]\mathfrak{T}[/latex], and let [latex]x[/latex] be a letter, distinct from the constants of [latex]\mathfrak{T}[/latex], which does not appear in [latex]A[/latex]. If [latex]B\implies A[/latex] is a theorem in [latex]\mathfrak{T}[/latex], then [latex]((\exists x)B)\implies A[/latex] and [latex]((\forall x)B)\implies A[/latex] is a theorem in [latex]\mathfrak{T}[/latex].

If [latex]B\implies A[/latex] is a theorem in [latex]\mathfrak{T}[/latex], then by [latex]C31[/latex],

(\exists x) B\implies (\exists x) A

[/latex]

is also a theorem in [latex]\mathfrak{T}[/latex]. But [latex](\exists x) A[/latex] is equivalent to [latex](\tau_X(A)|x)A[/latex] and since [latex]x[/latex] does not appear in [latex]A[/latex], the latter is simply [latex]A[/latex], hence [latex](\exists x) A[/latex] is equivalent to [latex]A[/latex]. It follows that

(\exists x) B\implies A

[/latex]

Replacing [latex]\exists[/latex] with [latex]\forall[/latex] in the argument will give the proof of [latex]((\forall x)B)\implies A[/latex].

Let [latex]A[/latex] and [latex]R[/latex] be relations in [latex]\mathfrak{T}[/latex], and let [latex]x[/latex] be a letter distinct from the constants of [latex]\mathfrak{T}[/latex]. If [latex]R\implies A[/latex] is a theorem in [latex]\mathfrak T[/latex], then

(\exists x) R\iff (\exists_Ax)R

[/latex]

is a theorem in [latex]\mathfrak T[/latex]. If [latex](\mbox{not }R\implies A[/latex] is a theorem in [latex]\mathfrak T[/latex], then

(\forall x) R\iff (\forall_Ax)R

[/latex]

is a theorem in [latex]\mathfrak T[/latex]. If [latex]A[/latex] is a theorem in [latex]\mathfrak T[/latex], then

(\exists x) R\iff (\exists_Ax)R[/latex] and [latex](\forall x) R\iff (\forall_Ax)

[/latex]

are theorem in [latex]\mathfrak T[/latex].

By I.C21, [latex](A\mbox{ and }R)\implies R[/latex] is a theorem in [latex]\mathfrak{T}[/latex], so by I.C31, [latex](\exists x) (A\mbox{ and }R)\implies (\exists x) R[/latex] is a theorem in [latex]\mathfrak{T}[/latex], so by definition of [latex]\exists_A[/latex], [latex](\exists_A x)R\implies (\exists x)R[/latex]. Conversely, since [latex]R\implies A[/latex] is a theorem in [latex]\mathfrak{T}[/latex], then [latex]R\implies (A\mbox{ and }R)[/latex] is a theorem in [latex]\mathfrak{T}[/latex] since [latex]R\implies R[/latex] by I.C8, so by I.C31, [latex](\exists x) R\implies (\exists x) (A\mbox{ and }R)[/latex] is a theorem in [latex]\mathfrak{T}[/latex]. Thus by definition of [latex]\exists_A[/latex], [latex](\exists x)R\implies (\exists_A x)R[/latex] is a theorem in [latex]\mathfrak{T}[/latex]. It follows that [latex](\exists x)R\iff (\exists_A x)R[/latex] is a theorem in [latex]\mathfrak{T}[/latex].

If [latex](\mbox{not } R)\implies A[/latex], then [latex](\exists x)(\mbox{not } R)\iff (\exists_A x)(\mbox{not } R)[/latex] is a theorem in [latex]\mathfrak{T}[/latex] by what was just shown. The negation [latex]\mbox{not } (\exists_A x)(\mbox{not } R)\iff \mbox{not } (\exists x)(\mbox{not } R)[/latex] is also a theorem in [latex]\mathfrak{T}[/latex] by I.C23, and by definition of [latex]\forall_A[/latex], this is precisely [latex](\forall x) R\iff (\forall_Ax)R[/latex] (By I.C22).

Now if [latex]A[/latex] is a theorem in [latex]\mathfrak{T}[/latex], then [latex]R\implies A[/latex] and [latex]\mbox{not } R\implies A[/latex] are theorems in [latex]\mathfrak{T}[/latex] by I.C9. A priori, this implies

(\exists x) R\iff (\exists_Ax)R[/latex] and [latex](\forall x) R\iff (\forall_Ax)

[/latex]