Method of 'Formal Logic'DiagramsLogical levels and criteriaContents1. Level I: Truth / Falsity of statements 2. Level II: Satisfiability / validity
2.1.
Truthvalues table for PPL  bivalid, for two variables.
2.2. Truthvalues table for PDL  bivalid, for two variables. 2.3. Truth / validity and logical power. 2.4. Formulas in standarized vorm. 2.5. Judging theories. (sets of propositions). 2.6. Contingency and Presupposition. 2.7. Basic Valid and Invalid derivations. 2.8. Validity, Satisfiability and Contingency. 2.9. Relations between logical criteria of level II. 4. Table with some Milestones in Metalogic 5. Criteria in formal logic Metatruth: logical criteria
Level I:Truth / Falsityof statements1.1. Truthvalues table for PPL for two variables.In a formal logical system all possible logical relations are completely defined by a chosen vocabulary by means of a Truth valuestable. The Truthvalues table for the most simple logical system, propositional logic (PPL), covers  for any chosen formalism or format  in any way all basic combinations that are involved in the most elementary beginning of any form of reasoning. Because of this, it really provides the very first, necessary foundings of accurate combinatory thinking. Truthvalues table PPL  for one variable.This Truthvalues table contains all possible orderings of values of two variables (propositions) in PPL, than can adopt two values. The basis consists of one variable by two values = two basic combinations. With this, two order s are possible of series of truth values: each of which reflects a unique logical relation. Thus the following table arises of the most simple nature, of two rows by two columns is four cells.
Level II:Satisfiability / validity2.1. Truthvalues table for PPL  bivalid.This truthvalues table contains all possible ordenings of values under the combination of two variables that each can adopt two values. Its base consists of 2 values to the power of 2 variables = 4 basic combinations or (possible) domain states. With this, 2 to the power of 4 = 16 orders are possible of series of truth values. Each of these reflects a unique logical relation, or (possible) domain statesrelation. Thus the following table arises of 4 rows by 16 columns is 64 cells; each containing one precise truth value.
2.2. Truthvalues table for PDL  bivalid.In predicate logic (PDL) attributes (or predicates) may be applied to various domain elements. Because of this, the combinatory possibilities again increase in hyperexponential ways. Next, in PDL socalled quantors may be applied to predications on objectvariables, to represent systematic relations between predications with identical predicate names, on identical variable names in a concise manner (conjunctive relations through universal quantors, disjunctive relations through existential quantor). However, before we succeed in finding these regularities, we still have tot deal with that combinatory explosion. Following here is a simple example: for a bivalid system, of a 'tiny' size: consisting of one predicate, of arity one, and a domain of only two elements. With this we end up again with 16 possible logical relations.
2.3. Truth value and logical power.Logical power is inversely proportional to truth value. Given a formula F  that is a each possible logical relation under formal system L! of set T^{*} (with size t=v^{**(v**d)}). The following applies:
(a) Logical power and contradiction.F is derivable from the maximum logical power in L!: i.e. contradiction (falsity under all conditions); or falsity; or truth value$0.
{ j ( (F_{[j]}
T^{*})
($0
F_{[j]}) )_{j}; (b)
j ($0
F_{[j]}) _{j};
($0 ( j F_{[j]}) ); ($0 ( j F_{[j]}) ); ($0 ( j F_{[j]}) ); ($0 ( T^{*})) }. Logical power and truth.F serves to derive the minimum logical power in L!: i.e. validity (truth under all conditions); or truth; or truth value$1.
{ j ( (F_{[j]}
T^{*})
(F_{[j]}
(c) $1) )_{j};
j (F_{[j]}
$1) _{j};(( j F_{[j]}) $1 );(( j F_{[j]}) $1 );((j F_{[j]}) $1 );(( T^{*}) $1 ) }.Contradiction, Logical power and truth.Combining (a) and (b).
{ j ( (F_{[j]}
T^{*}) ( ($0
F_{[j]})
(F_{[j]}
$1) ) )_{j};
j ( ($0
F_{[j]})
(F_{[j]}
$1 ) )_{j};( ($0 (j F_{[j]}) ) ( (j F_{[j]}) $1 ) );( ($0 (j F_{[j]}) ) ( (j F_{[j]}) $1 ) );( ($0 (j F_{[j]}) ) ( (j F_{[j]}) $1 ) );( ($0 (j F_{[j]}) ) ( (j F_{[j]}) $1 ) );( ($0 ( T^{*})) ( ( T^{*}) $1) );($0 $1) }.2.4. Formulas in standarized vorm.In formal logic a set of logical formulas is called a theory. The formulas in the set in general refer to statements or arguments (propositions). In formal logic a number of standarized forms exists by which formulas or sets of formulas can be represented in a clear, precise and compact manner, so that they can be processed and be judged efficiently, socalled normal forms. ]> A convenient form for formulas when we want to judge them is the Conjunctive Normal Form ( CNF). A formula inCNFconsists of a conjunction of disjunctions. In other words, on the mainline of argumentation a juxtaposition of one or more conjuncts exists, while each conjunct is a disjunction consisting of at least one simple formula (an atom or a literal).A CNFthus makes only use of the connectives {¬, , }.General structure of a 
Diagram Validity / Satisfiability / Contingentie 


1 
± 
0 
Not necessarily untrue:Satisfiable,'Logically possible'. (Is not yet equivalent to 'possibly true').
SATBL(G);
(TAUT(G) CONTIN(G); ¬ ¬G; (( G ) (¬ ( ¬G ) ) );
{ k ( (G$ = c_{[k]})
(c_{[k]}
>$0) )_{k} };
{ j F_{[j]}
G };
{ m
M!_{[m]} G }.
{ j ((F_{[j]}
¬F_{[j]}) G) };

Impossibly true:Unsatisfiable,Logically excluded. 'Excluded grounds'.
¬SATBL(G);
¬G;
{ k ( (G$ = c_{[k]})
(c_{[k]} =
$0) )_{k} };
{¬j ((¬ ¬F_{[j]})
(F_{[j]}
G)) };
{¬m
M!_{[m]} G }.
{ j ((F_{[j]}
¬F_{[j]}) G) };


Consistency,Widerspruchsfreiheit. Set K^{*} is consistent: From K^{*} no contradiction is derivable.
CONSIS(K^{*});
{ ¬( (K^{*} G) (K^{*} ¬G) ) }; { ¬(K^{*} ) }; { j ( ¬( (K^{*} F_{[j]}) (K^{*} ¬F_{[j]}) )_{j} }; { j ( ¬( {K^{*} F_{[j]}} ) ¬( {K^{*} ¬F_{[j]}} ) )_{j} };
{ ¬j ( (
F_{[j]}
K^{*}
)
( ¬F_{[j]} K^{*} ) )_{j} }. 
Inconsistency,Inconsistentinvalidity. Set K^{*} is inconsistent. From K^{*} a contradiction can be derived.
INCNS(K^{*});
¬CONSIS(K^{*}); { (K^{*} G) (K^{*} ¬G) }; { K^{*} }; { j ( (K^{*} F_{[j]}) (K^{*} ¬F_{[j]})_{j} }; { j ( ( {K^{*} F_{[j]}} ) ( {K^{*} ¬F_{[j]}} ) )_{j} };
{ j ( (
F_{[j]}
K^{*}
)
( ¬F_{[j]} K^{*} ) )_{j} }. 

Consistency theorem,Fundamental theorem (Modelexistence theorem): 'Consistency implies Satisfiability'. (Every subset : (Consistent Satisfiable)).
{CONSIS(K^{*})
SATBL(K^{*})};
{¬(K^{*} ) ¬(K^{*} )}. 

Necessarily / always true:Valid,Tautology, Validsatisfiability.
TAUT(G);
G;
{ k ( (G$ = c_{[k]})
(c_{[k]} =
$1) )_{k} };
{¬j ((¬ ¬F_{[j]})
(F_{[j]}
¬G)) };
{¬m
M!_{[m]} ¬G }.
{¬j (F_{[j]}
¬F_{[j]}
G) };

Undecided:Contingency,Contingentinvalidity, Contingentsatisfiability. Insufficiently grounded, Indefinite.
CONTIN(G);
{SATBL(G) ¬TAUT(G)}; {(¬ G) (¬ ¬G)};
{ k ( (G$ = c_{[k]})
($0 <c_{[k]}<$1) )_{k} };
{ j ((¬ ¬F_{[j]})
(F_{[j]}
G)) }
{ k ((¬ ¬F_{[k]}) (F_{[k]} ¬G)) };
{ (m
M!_{[m]} G)(n M!_{[n]} ¬G) }. 

Not necessarilytrue:Invalid,non sequitur [nonseq]:
NONSEQ(G);
¬TAUT(G); (CONTIN(G) ¬SATBL(G); ¬ G;
{ k ( (G$ = c_{[k]})
(c_{[k]}
<$1) )_{k} };
{ j ((¬ ¬F_{[j]})
(F_{[j]}
¬G)) };
{ m
M!_{[m]} ¬G }. 

Correctness(Soundness informelezin): 'Derivable implies logical consequence'. Set K^{*} is correct. (Every subset : (Derivable Logical consequence).
CORRECT(K^{*});
{DRVBL(K^{*},G) SEQUIT(K^{*},G)}; { (K^{*} G) (K^{*} G) }; { j ( (K^{*} F_{[j]}) (K^{*} F_{[j]}) ) }. 

Completeness(Vollständigkeit). 'Validity implies Derivability'. Set K^{*} is complete: (Every subset : (Logical consequence Derivable)).
COMPLET(K^{*});
{SEQUIT(K^{*},G) DRVBL(K^{*},G)}; { (K^{*} G) (K^{*} G) }; { j ( (K^{*} F_{[i]}) (K^{*} F_{[j]}) ) }. 

Maximal consistency:Set K^{*} is maximally consistent: (Every subset : (Logical consequence Derivable)).
MAXCONS(K^{*});
{ CONSIS(K^{*}) COMPLET(K^{*}) }; { (K^{*} G) (K^{*} G) }; { j ( (K^{*} F_{[j]}) (K^{*} F_{[j]}) )_{j} }; { j ( CONSIS(K^{*} \ {F_{[j]}}) ¬CONSIS(K^{*} {F_{[j]}}) )_{j} }; { j ( ( (F_{[j]} K^{*}) ( {K^{*} ¬F_{[j]}} ) ) ( ¬(F_{[j]} K^{*}) ¬( {K^{*} F_{[j]}} ) ) )_{j} }; Implications:
{ j (
(F_{[j]}
K^{*})
(¬F_{[j]} K^{*}) )_{j} }; 


(·) Completeness of PPL: proof by Emil L. Post (1920, Introduction to a general theory of elementary propositions). (·) Completeness of PDLI: proof by Kurt F. Gödel (1929/1930, Über die Vollständigkeit des Logikkalküls). 
(·) Incompleteness of elementary arithmetic (firstorder theory of natural numbers
according to the logicistic
research program, that was based on classic logic in the Organon of Aristotelis,
and had been further developed in the Grundgesetze der Arithmetik
of F.L. Gottlob Frege (1893, 1903) and the Principia Mathematica
of Bertrand Russell and Alfred North Whitehead, parts IIII (1910, 1912, 1913): proved by Kurt Gödel (1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme 1). 
Diagram Decidability and Recursivity 


1 
± 

Decidable:The question whether an expression G has a definite (truth) value, can always be answered: The (truth) value of G is always derivable through a finite proof. 
UnDecidable:The question whether an expression G has a definite (truth) value, can not always be answered: The (truth) value of G is not always derivable through a finite proof. 

G is Truthvalue Decidable:
DECIDBL(G);
{( ( G $1) )( ( G$0) ) };{( ( G ) ) ( ( ¬G ) ) };Implications:
{
( (
G
)
( ¬G ) ) }.
{
(
( G
¬G ) ) };
{
( G
¬G ) };
{ G
¬G } (always logical value).$1 (truth). 
G is Not truthvalue deDecidable:
¬DECIDBL(G);
{ (¬ ( G $1) ) (¬ ( G$0) ) };{ (¬ ( G ) ) (¬ ( ¬G ) ) }; Implications:
{ ¬
( (
G
)
( ¬G ) ) };
{ ¬
(
( G
¬G ) ) };
{ ¬
( G
¬G ) };
{ } (no logical value);
$0 (no truth). 

G is Validity Decidable:
{ (
(
G) )
( (¬ G) ) };Implications:
{
( (
G
)
( ¬ G ) ) };
{ (
G
)
( ¬ G ) }.
{ TAUT(G)
¬SATBL(G) } (always validity value).$1 (truth).G is determinate. 
G is Not validity Decidable:
{ (¬
(
G) )
(¬
(¬
G) ) };
Implications:
{ ¬
( (
G
)
( ¬ G ) ) }.
{ ¬(
G
)
¬(
¬G
) }.
{ CONTIN(G) } (no validity value).
$0 (no truth).G is indeterminate. 

Recursive:For all input, the system will be 'halting' (terminating in finite time). 
Nonrecursive:For some input the system will be infinitely 'looping'. 

RC(G);
{ RE(G) CORE(G) }; { ( ( G) ) ( (¬ G) ) };Implications:
{
( (
G)
(¬ G) ) }. 
¬RC(G);
{ ¬RE(G) ¬CORE(G) }. { (¬ ( G) ) (¬ (¬ G) ) }; Implications:
{ ¬
( (
G)
(¬ G) ) }. 

Recursively

Corecursively



Set K^{*} is Recursively enumerable: If K^{*} has a result, then that will always be provable.
RE(K^{*});
{ k ( (Ks^{*}_{[k]} K^{*}) j ( (Ks^{*}_{[k]} F_{[j]}) (Ks^{*}_{[k]} F_{[j]}) )_{j} )_{k} }. 
Complement of K^{*} is Recursively enumerable: If K^{*} has no result, then that will always be provable.
CORE(K^{*});
{ k ( (Ks^{*}_{[k]} K^{*}) j ( ¬(Ks^{*}_{[k]} F_{[j]}) ¬(Ks^{*}_{[k]} F_{[j]}) )_{j} )_{k} }. 
Set K^{*} is not Recursively enumerable: If K^{*} has a result, then that will not always be provable.
¬RE(K^{*});
{ k ( (Ks^{*}_{[k]} K^{*}) j ( (Ks^{*}_{[k]} F_{[j]}) ¬ (Ks^{*}_{[k]} F_{[j]}) )_{j} )_{k} }. 
Complement of K^{*} is not Recursively enumerable: If K^{*} has no result, then that will not always be provable.
¬CORE(K^{*});
{ k ( (Ks^{*}_{[k]} K^{*}) j ( ¬(Ks^{*}_{[k]} F_{[j]}) ¬ ¬(Ks^{*}_{[k]} F_{[j]}) )_{j} )_{k} }. 
Set K^{*} is Recursively enumerable (through Turing Machine procedure): If K^{*} has a result, then that will always be computable.
RE(K^{*})_{TM};
{ k ( (Ks^{*}_{[k]} K^{*}) j h ( (TM_{[h]}(Ks^{*}_{[k]}) F_{[j]}) m (TM_{[m]}(K^{*}) (TM_{[h]}(Ks^{*}_{[k]}) F_{[j]}) )_{m} )_{h} ,_{j} )_{k} }. 
Complement of K^{*} is Recursively enumerable (through Turing Machine procedure): If K^{*} has no result, then that will always be computable.
CORE(K^{*})_{TM};
{ k ( (Ks^{*}_{[k]} K^{*}) j h ( ¬(TM_{[h]}(Ks^{*}_{[k]}) F_{[j]}) m ( (TM_{[m]}(K^{*}) ¬(TM_{[h]}(Ks^{*}_{[k]}) F_{[j]}) )_{m} )_{h} ,_{j} )_{k} }. 
Set K^{*} is not Recursively enumerable (through Turing Machine procedure): If K^{*} has a result, then that will not always be computable.
¬RE(K^{*})_{TM};
{ k ( (Ks^{*}_{[k]} K^{*}) j h ( (TM_{[h]}(Ks^{*}_{[k]}) F_{[j]}) ¬m (TM_{[m]}(K^{*}) (TM_{[h]}(Ks^{*}_{[k]}) F_{[j]}) )_{m} )_{h} ,_{j} )_{k} }. 
Complement of K^{*} is not Recursively enumerable (through Turing Machine procedure): If K^{*} has no result, then that will not always be computable.
¬CORE(K^{*})_{TM};
{ k ( (Ks^{*}_{[k]} K^{*}) j h ( ¬(TM_{[h]}(Ks^{*}_{[k]}) F_{[j]}) ¬m (TM_{[m]}(K^{*}) ¬(TM_{[h]}(Ks^{*}_{[k]}) F_{[j]}) )_{m} )_{h} ,_{j} )_{k} }. 
(·) 'Effective procedure' (Hilbert, 1900, 1928). (·) 'Recursive function' (Gödel, 1930, 1931). (·) 'Lambda definable function' (Church, 1935, 1936). (·) 'Turing Machine computable function' (Turing, 1936, 1937). 
(·) UnDecidability/ nonrecursivity of elementary calculus of natural numbers (elementary number theory): proof by Alonzo Church, (1935/1936, An Unsolvable Problem of Elementary Number Theory). (·) UnDecidability/ nonrecursivity of entire elementary arithmetic (first order arithmetic): proof by Alan M. Turing (1936/1937, On computable numbers, with an application to the Entscheidungsproblem). 
Author  Year  Formalism  Domain  Criterion  

Hilbert  1900,1928  Effective procedure (hypothetical)  Mathematics, Logic 
Decidability; Entscheidbarheit; Entscheidungsdefinitheit; 

Post  1920 
Truth table method 
PPL 
Completeness; Vollständigkeit. 

Gödel  1929/1930  Deduction  PDLI 
Completeness; Vollständigkeit. Recursively enumerable 

Gödel  1931  Gödelnumbering 
PDLI, Arithmetic of Natural numbers Firstorder theory of natural numbers (Principia Mathematica) 
Einige formal unentscheidbare Satze: Incompleteness; Unvollständigkeit. Not recursively enumerable. 

Church  1935/1936 
Lambdacalculus (Lambdadefinable): Recursive functions of positive integers 
PDLI, Arithmetic of Natural numbers: Elementary number theory 
Unsolvable problem: UnDecidability; Unentscheidbarheit. 

Turing  1936/1937 
(Universal) Turing machine (Turing machine computability) 
PDLI, Arithmetic: First order arithmetic 
UnDecidability; Unentscheidbarheit. 