Splitting

In practice, such bijections from

A possibility, is to switch to a view over all variables as bound throughout the formula: from the concept of interpretation

We took unions over ℕ for the case we would need to see "all possible formulas" as terms interpreted in one same algebra.

**Theorem.** First-order logic has a proving system both sound and complete
in the following equivalent senses

- Any consistent
first-order theory
*T*with countable language has a countable model.

- Any formula true in all countable models of such a theory is deducible from its axioms.

Reduce *T* to a single-type theory *T*_{1} simulating the use of types
by relevant unary predicate symbols and axioms, but without requiring all objects to belong to some type.
Thus, the axiom (∃*x*, 1) can be added to *T*_{1} without harm (it still
allows types to be empty).

Then re-write axioms of *T*_{1} in prenex
form, that is chains of
quantifiers applied to quantifier-free formulas (using equivalences
from 2.5 and 2.6 simplified for a nonempty model).

Interpret the symbol = in axioms as an ordinary predicate
symbol, with the axioms of
equality [1.11].

(∀*x*,*x'*, ∃*y*, ∀*z*,
*A*(*x*,*x'*,*y*,*z*))
⇢ (∀*x*,*x'*,∀*z*,
*A*(*x*,*x'*,*K*(*x*,*x'*), *z*)).

Observe that

From all subterms occurring in used axioms of T_{2}, list without repetition all those
whose root is a symbol S which was added to the
language when converting some axiom
∀x,∃y,∀z,∃u,
A(x,y,z,u)
of T_{1}, into the axiom ∀x,z, A(x,K(x),z,
S(x,z)) in T_{2}. Successively replace them all by variables
in T_{1}: for terms
S(t_{0},t_{1})
and S(t_{0},t_{2})
(where t_{0}, t_{1}, t_{2}
∈ MT_{1} will say"Let y such that ∀z,∃u,
A(t_{0},y,z,u); let u_{1} such that
A(t_{0},y,t_{1},u_{1});let u_{2} such that
A(t_{0},y,t_{2},u_{2});"and use the contradiction in T_{2} where y replaces
K(t_{0}), u_{1} replaces
S(t_{0},t_{1}) and u_{2}
replaces S(t_{0},t_{2}). |

Then the quotient of

As this construction depends on an arbitrary order between formulas, different choices give different models, which may be non-isomorphic and even have different properties reflecting the undecidability of the theory's formulas.

T⊢A

⇔T∪ {¬A} is inconsistent

⇔T∪ {¬A} has no countable model

⇔Ais true in all countable models ofT. ∎

- A countable model
*U*interprets the powerset "℘(*E*)" of an infinite "set"*E*∈*U*as the "set"*P*of all objects in*U*which play the role of subsets of*E*(but may differ from these when*U*is non-standard); as*P*is meta-countable, it cannot exhaust the uncountable meta-powerset of "all" subsets of*E*. - As
*P*is meta-countable, it externally has a bijection with ℕ or*U*; but such bijections "do not exist" (have no representatives) as objects in*U*.

Set theory and foundations of mathematics

1. First foundations of mathematics

2. Set theory

3. Algebra 1

4.1.
Algebraic terms

4.2. Quotient systems

4.3. Term algebras

4.4. Integers and recursion

4.5. Presburger Arithmetic

4.6. Finiteness and countability (draft)

4.7.**The Completeness Theorem**

4.8. More recursion tools

4.9. Non-standard models of Arithmetic

4.10. Developing theories : definitions

4.11. Constructions

4.A. The Berry paradox

5. Second-order foundations 4.2. Quotient systems

4.3. Term algebras

4.4. Integers and recursion

4.5. Presburger Arithmetic

4.6. Finiteness and countability (draft)

4.7.

4.8. More recursion tools

4.9. Non-standard models of Arithmetic

4.10. Developing theories : definitions

4.11. Constructions

4.A. The Berry paradox

6. Foundations of Geometry