From: Nam Nguyen on
Nam Nguyen wrote:
>
> ***
>
> Assuming you've accepted the original UT I'll technical present steps to
> accept the counterpart (FOL) UT regarding to the naturals.
>
> First let's assume the following languages:
>
> - L1 = L2(0,S,+)
> - L2 = L1(0,<,*)
> - L = L(0,S,+,*,<)
>
> Now the steps:
> [...]
>
> Step3: Demonstrate that, as alluded in Step2, if there's an an arithmetic
> truth value that would be impossible to know as true, if being
> "true", there are infinite arithmetic truth values whose truth
> values can't be assigned! These are effectively truth-unassigned-
> able formulas, reflecting concepts independent of the concept of
> the natural numbers.

The ultimate aim here is to demonstrate the _existences_ of infinitely
many truth-unassigned-able formulas, _without necessarily knowing_ their
exact spellings. The demonstration would be done using a particular binary
tree called, say, G2Tree (Godel-Goldbach Tree).

The Tree Anatomy:
=================

The infinite binary tree has the following structure:

Prp1 - A node of the tree is an unordered pair of formulas (f1, f2),
where T = {f1, f2} is an inconsistent formal system.

Prp2 - A path in between 2 nodes (of adjacent levels), the parent node
and the child node, is just a formula (say, cF) but which has
the following characteristics:

- given the parent node of (pF1, pF2), then {cF} |- f, where f is
either pF1 or pF2 but not both;
- if {cF} |- pF1, then for its sibling path-formula cF' [from the
same parent (pF1, pF2)] we'd have {cF'} |- pF2, and vice versa.

Prp3 - From a particular node, is a sub-tree containing only formulas
of the form stipulated in UT2.


The Tree Construction:
======================

The tree would begin with the root node (f1,f2):

f1 <-> GC
f2 <-> "There are infinitely many counter examples of GC".

Now, suppose we're at a particular node Nd = (nF1, nF2), we'll construct
the following paths and nodes:

- The 2 child paths (2 formulas): cNdPath1, cNdPath2
- the 2 pairs of formulas: one is the child node of cNdPath1, and the
other of cNdPath1.


[To be continued....]