Splitting

In practice, such bijections from

Binding all variables modifies the view on the above concept of interpretation of a term

Op_{E} = ⋃_{n∈ℕ} Op_{E}^{(n)}
and Rel_{E } = ⋃_{n∈ℕ} ℘(*E ^{n}*).

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

Any good formal proof system needs of course to be sane, which means never
proving anything wrong (so that the provability of a formula ensures its truth in every model).
More remarkable is the converse property, that is *completeness*.
Without trying to completely formalize the concept of proof, the below will
implicitly suggest its possibility for first-order logic.

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

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

Sketch of proof of the first statement (not using the axiom of choice, anyway out of topic here):

- Rewrite through equivalences in 2.1 and 2.3 (simplified by assuming a nonempty model) each axiom into a chain of quantifiers applied to a quantifier-free formula (prenex form).
- Replace each occurrence of ∃ in an axiom by a new
operator symbol
*K*added to the language of the theory, in the natural way where for example

(∀*x*,*x'*, ∃*y*, ∀*z*,*A*(*x*,*x'*,*y*,*z*)) ⇢ (∀*x*,*x'*,∀*z*,*A*(*x*,*x'*,*K*(*x*,*x'*),*z*)). - Replace the predicate = in axioms, by an ordinary predicate symbol to play the role of equality, together with the axioms of equality [1.6].
- Let
*M*be the ground term algebra over the language of operator symbols enriched as described in 2. Reinterpreting each ∀ in axioms into axiom schemas replacing their variables with all possible tuples of elements of*M*, gives a propositional theory*T*' (its axioms are composed of logical connectives over Boolean variables), whose set of Boolean variables is*P*⋆*M*where*P*is the set of predicate symbols in the theory plus the equality symbol. - Observe that
*T*' is still consistent, as any contradiction in*T*' (= finite set of axioms not satisfied by any tuple of Boolean values of their variables) can be converted into a contradiction in the initial theory*T*, as follows:

List without repetition all (ground) terms occurring as a subterm of some used axiom of *T*', and whose root is some symbol*S*that was added by converting some axiom of*T*such as "∀*x*,∃*y*,∀*z*,∃*u,**A*(*x*,*y*,*z,u*)" into the axiom "∀*x,z,**A*(*x,K*(*x*),*z*,*S*(*x,z*))" in*T*'. For example if we have terms*S*(*t*_{0},t_{1}) and*S*(*t*_{0},t_{2}) (where*t*_{0},*t*_{1},*t*_{2}∈*M*), the reasoning in*T*can start by

"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 continue using the contradiction in*T*' where*y*replaces*K*(),*t*_{0}*u*_{1}replaces*S*(*t*_{0},t_{1}) and*u*_{2}replaces*S*(*t*_{0},t_{2}).

- Recursively by a chosen enumeration of
*P*⋆*M*as a countable set, add one by one to the axioms, each of these Boolean variables if it is consistent with previously accepted axioms, so that all get values without contradiction. - Then the quotient
of
*M*by the equivalence relation of "equality", forms a model (with the "true equality"). ∎

In other words, taking the Galois connection as in the fundamental exampleT⊢A

⇔T∪ {¬A} is inconsistent

⇔T∪ {¬A} has no model

⇔Ais true in all models ofT. ∎

*X*is the set of ground formulas using some language*L**Y*is the class of systems interpreting*L*, well enough represented by the set of the countable ones (those using a subset of ℕ as its set of objects),*R*is the truth relation between them

However, this still does not make everything clear about provability and existence of models, as announced in the section on truth in mathematics, and will be established by the incompleteness theorem:

- If a proof exists, nothing says how to find it; it might be too big to be found at all.
- We just know that both properties of a theory are equivalent : consistency and existence of a model. This does not decide whether these are both true or both false, but only ensures that, in case this was undecidable (a case which may be itself undecidable), both properties would be true together in some universes and false together in the rest of universes.
- Models built this way depend on an arbitrary choice of order between formulas; other choices may generate other non-isomorphic models, which may have different properties reflecting the undecidability of the theory's formulas.
- For any specific choice, this construction of the model is still not really effective, in the sense that it is not algorithmic: it requires an infinity of steps, each of which involves an infinite knowledge (knowing if a formula remains consistent with previously accepted ones, which is the answer to a halting problem of search for contradiction). Actually, most foundational theories such as set theories, do not have any algorithmically definable model.

Finally, as the powerset axiom implicity takes the actual form of a relation between ℘(

First comes Skolem's paradox:

*If set theory is consistent then it has countable models, despite Cantor's theorem by which
some sets there, such as *℘(ℕ)*, are uncountable.*

- A countable model
*U*does not interpret ℘(ℕ) as the uncountable "true" set of "all" subsets of ℕ but only as the countable set*P*of those which belong to*U*. (The value of "℘(ℕ)" in*U*represents*P*but may technically differ from*P*as*U*is non-standard). - As
*P*is countable, there exist bijections between*P*and ℕ; but such bijections "do not exist" (have no representatives) as objects inside*U*.

Set theory and foundations of mathematics

1. First foundations of mathematics

2. Set theory (continued)

3. Algebra 1

4.1. Finiteness and countability

4.2.The Completeness Theorem

4.3. Infinity and the axiom of choice

4.4. Non-standard models of Arithmetic

4.5. How theories develop

4.6. The Incompleteness Theorem