I have just finished something like logic (first try, should be very
raw). Hope
this can help in dealing with several logical puzzle (e.g. Russell's
paradox), at least, in the moment.
Mostly, I would like to gather response form you to improve what
is typed, thank you.

In my opinion, many C++ programs written are actually from
'intuition', not even close to C++'s original idea
(class, concept,..,so called RAII). The is an higher level thinking
about using C++, e.g. how to translate/solve problems in C++, or
'modeling problems' and solve in C++.
----------------------------------------------------

Description::= Description is composed of a series of terms which are
composed
of discrete symbols. The form of description is indefinite, it can
be like
computer programs, mathematical expression,..,or the sentense in
this file.
Description associates to the object being described, called its
semantics.

Axiom0: Description and its semantics object are physical entities,
both occupy
different position in spacetime domain.

Axiom1: Description exists via manufraturing.

Ex: "A tree falls in a forest": This description must be made in
someone's
head. If no one is there, this description (and its object) is
a made up
in latter time (Thus, most of our knowledge are
archaeological).
Ex: "This sentence is false": Ans: Undecidable (borrow from Halting
Prolem
Theorem). Self-referential descriptions like this, including
"This
sentence is true", suffer from circular reasoning. Although the
latter
seems not to cause paradox.

Normalized Description::= A description of concated terms like
"P(a,b,..)" or
(P,a,b,..). Normalized description is like a natural sentence, but
all the
ingredient must be defined. Thus, the form is mostly regular.
The object of normalized description can be another description but
cannot
be the description itself (would cause circular reasoning). Thus,
from this
definition, we will have the chain "description ->
object(description) ->
... -> object(description) -> object". The last one is called a
terminal
description. Thus, for simplicity reasons, the description that has
no
object is also called a terminal description.

Substitute::= The term in a description that functions as a placeholder
for
another description or a parameter of the description. Thus,
substitute may
also be called as argument, parameter, or variable. In any
condition,
description that contain substitute are not terminal description.
(In
reality, terminal description may also has its object except such
object
is inexpressible).

Partial Solution::= Part of a whole solution.

Theorem: If a (whole) solution is built procedurally by accululating
parts, a
partial solution will appear in the process of creating the
solution.

+-------------+
| Proposition |
+-------------+
Proposition::= Any description that can be classified as true or false
(note
that true/false are arbitrary. This article is only concerned with
the
manipulation of symbols, not the attribution of true or false).
Proposition
can be any form of description as long as it can be classified as
true (T)
or false (F). Since we are more concerned with normalized
propositon, in the
formal presentation, some token should be added to indicate the
notion of
proposition, e.g. Prop(x,y,..).

Sometimes, descriptive proposition may be called as 'abstract
proposition'.
In contrast, the object of that description can be called the
object
proposition. If a descriptive proposition does not contain
substitute, it
can be called a terminal or atomic proposition.

+-------------------------+
| Creation of Proposition |
+-------------------------+
From Axiom1, proposition also exists via manufraturing (inversely,
proposition does not exist before manufratured).

From the observation of the descriptions we used, our knowledge can
all be
be called partial description. Such observation indicates that we
should
add procedure into 'description'. If so, the most suitable choice
of the
language for procedure should be C++, because it has the concept of
'object' and 'construction'(manufacture). Therefore, the following
article,
pseudo-C++ will be used in the sense of computation theory.

+-----+
| Set |
+-----+
Substitute in normalized description is often the substitute of the
element
of a set, e.g. the n in Prop(n∈ℕ).
Set is often expressed by using proposition, and is often defined
in way of
procedural description like the example in Peano Axioms.

+------------------------+
| Procedural Proposition |
+------------------------+
Procedural Proposition::= Proposition whose semantics is a program,
e.g.
decision function.

Postulate: Precedure is the only way to express infinite instances.

+---------------+
| Some examples |
+---------------+
Prop(∀x,P(x))::= P(x1)∧P(x2)∧..∧P(xn) (x∈{x1,x2,..})
Equ. to "∀xP(x)" in many books. If defined in Pseudo-C, then:
bool f() {
for(int x=1; x<=S.size(); ++x) {
if(P(x)==false) {
return false;
}
}
return true;
};
Universal quantifier itself is also a proposition, therefore, from
definition, its negation exists:
~Prop(∀x,P(x))= ~(P(x1)∧P(x2)∧..∧P(xn)= ~P(x1)∨~P(x2)∨..∨~P(xn)∨
= Prop(∃x,~P(x))

Prop(∃x,P(x))::= P(x1)∨P(x2)∨..∨P(xn) (x∈{x1,x2,..})
Equ. to "∃xP(x)" in many books. If defined in Pseudo-C, then:
bool f() {
for(int x=1; x<=SetX.size(); ++x) {
if(P(x)==true) {
return true;
}
}
return false;
};
Existential quantifier itself is also a proposition, therefore,
from
definition, its negation exists:
~Prop(∃x,P(x))= ~(P(x1)∨P(x2)∨..∨P(xn))= ~P(x1)∧~P(x2)∧..∧~P(xn)
= Prop(∀x,~P(x))

Prop(∃x,∀y,P(x,y))::= Prop(∀x,Prop(∃y,P(x,y))) // Concatenation:
∃x∀y:P(x,y)
= (P(x1,y1)∧P(x1,y2)∧..∧P(x1,yn))∨
(P(x2,y1)∧P(x2,y2)∧..∧P(x2,yn))∨
...
(P(xn,y1)∧P(xn,y2)∧..∧P(xn,yn))

From procedual definition:
　　bool f() {
for(int x=1; x<=SetX.size(); ++x) {
for(int y=1; y<=SetY.size(); ++y) {
if(P(x,y)==false) {
break;
}
}
if(y>=SetY.size()) {
return true;
}
}
return false;
}

"∃x∀y:P(x,y)" itself is also a proposition, therefore, from
definition, its
negation exists: ~(∃x∀y:P(x,y))
= (~P(x1,y1)∨~P(x1,y2)∨..∨~P∨(x1,yn))∧
(~P(x2,y1)∨~P(x2,y2)∨..∨~P∨(x2,yn))∧
...
(~P(xn,y1)∨~P(xn,y2)∨..∨~P∨(xn,yn))
= Prop(∃y,~P(x1,y))∧
Prop(∃y,~P(x2,y))∧
...
Prop(∃y,~P(xn,y))∧
= Prop(∀x,Prop(∃y,~P(x,y))) = (∀x,∃y,~P(x,y))

Prop(∀x,∃y,P(x,y))::= Prop(∀x,Prop(∃y,P(x,y))) // Concatenation:
∀x∃y:P(x,y)
= (P(x1,y1)∨P(x1,y2)∨..∨P(x1,yn))∧
(P(x2,y1)∨P(x2,y2)∨..∨P(x2,yn))∧
...
(P(xn,y1)∨P(xn,y2)∨..∨P(xn,yn))

From procedual definition:
　　bool f() {
for(int x=1; x<=SetX.size(); ++x) {
for(int y=1; y<=SetY.size(); ++y) {
if(P(x,y)==true) {
break;
}
}
if(y>=SetY.size()) {
return false;
}
}
return true;
}

"∀x∃y:P(x,y)" itself is also a proposition, therefore, from
definition, its
negation exists: ~(∀x∃y:P(x,y))
= (~P(x1,y1)∧~P(x1,y2)∧..∧~P(x1,yn))∨
(~P(x2,y1)∧~P(x2,y2)∧..∧~P(x2,yn))∨
...
(~P(xn,y1)∧~P(xn,y2)∧..∧P~(xn,yn))
= (∃x,∀y,~P(x,y))
-----------------------------------------------------------------------
------