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.

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

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

This quality of perfection, established for a certain formal proving system for first-order logic, ensures that any other formal proving system with the same quality will be necessarily equivalent : any formal proof according to one is automatically convertible into a proof according to any other.

Express axioms in prenex form, that is chains of quantifiers applied to quantifier-free formulas (using equivalences from 2.1 and 2.3 simplified for a nonempty model).

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

Replace each occurrence of ∃ in an axiom by the use of an additional operator symbol

(∀*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', 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, into the axiom ∀x,z, A(x,K(x),z,
S(x,z)) in T'. Successively replace them all by variables
in T: for terms
S(t_{0},t_{1})
and S(t_{0},t_{2})
(where t_{0}, t_{1}, t_{2}
∈ MT 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' 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.

So, the provability function giving the set of theorems from each set of axioms, is the closure of the Galois connection defined by the truth relationT⊢A

⇔T∪ {¬A} is inconsistent

⇔T∪ {¬A} has no model

⇔Ais true in all models ofT. ∎

- the set
*X*of ground formulas using some language*L* - the
set
*Y*of*L*-structures on ℕ or a subset of it (sufficient representatives of the class of all*L*-systems).

- The proven equivalence between consistency and existence of a model, does not inform
whether these are both true, or both false:
- Provability, if true, can stay
*practically*unknowable: if a proof exists, nothing says how to find it; it may be too big to be ever given. - The consistency of a theory may be true but unprovable: completeness only ensures that, in this case (and it may be undecidable whether it is the case or not), there also exists universes in which, equivalently, this theory is inconsistent and it has no models.

- Provability, if true, can stay
- Such constructions of models as provided by the above proof, are not really effective, as they are not algorithmic: they require 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.

- 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 (continued)

3. Algebra 1

4.1. Finiteness and countability

4.2.The Completeness Theorem

4.3. Non-standard models of Arithmetic

4.4. Development of theories : definitions

4.5. Constructions

4.6. Second-order logic

4.7. Well-foundedness

4.8. Ordinals and cardinals

4.9. Undecidability of the axiom of choice

4.10. Second-order arithmetic

4.11. The Incompleteness Theorem