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 orders 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 argument ation 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. 