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

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

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

Any good formal proof system (a proof theory, expressible by a verification algorithm)
needs of course to be sound, which means only
"proving" what is always true (the provability of a formula implies its truth in every model).
More remarkable is the converse property, that is *completeness*.
The completeness of first-order logic was originally Gödel's
thesis. Once proven for a specific formal
proving system, it gives a perfect meaning to the concept of provability in first-order logic
(independent of the choice of formalism with the same quality),
eliminating any disagreement between realism
and formalism for first-order theories.

- 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.

- Rewrite each axiom into a chain of quantifiers applied to a quantifier-free formula (prenex form) using equivalences in 2.1 and 2.3 (simplified by assuming a nonempty model).
- Replace the predicate = in axioms, by an ordinary predicate symbol to play the role of equality, together with the axioms of equality [1.6].
- 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*)). - Let
*M*be the ground term algebra over the language of operator symbols enriched as just described. Reinterpreting all ∀ in axioms as the use of axiom schemas (one axiom for each replacement of variables by a tuple 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) would provide a contradiction in*T*, as follows:

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 ), the reasoning in*t*_{0},*t*_{1},*t*_{2}∈*M**T*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}).

- 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"). ∎

Deduction of the second statement from the first :

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. Infinity and the axiom of choice

4.5. How theories develop

4.6. Second-order logic

4.7. The Incompleteness Theorem