Formal_logic_metalogic_criteria_logical_levels

**Method of 'Formal Logic'**

Diagrams

Logical levels and criteria

1. Level I: Truth / Falsity of statements
2. Level II: Satisfiability / validity

2.1. Truth-values table for PPL - bivalid, for two variables.
2.2. Truth-values 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.

3. Level III. Decidability of formal systems
4. Table with some Milestones in Meta-logic
5. Criteria in formal logic

Meta-truth: logical criteria

Logical quality

Level I:

Truth / Falsity

of statements

1.1. Truth-values 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 values-table.
The Truth-values 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.

Truth-values table PPL - for one variable.

This Truth-values 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.

1	2
1	0
0	1
T	F
A	¬A
¬B	B

Truth values
1	±	0
True , verum: Verification.	Unspecified , uninterpreted: Indefinite.	False , falsum: Falsification.
Truth value (value, valor):
$ (G) = 1.	(0 < $ (G) < 1).	$ (G) = 0.
Truth value assignment (valuation):
V!(G) :=1.	¬V!(G) {0,1}.	V!(G) :=0.
Truth value determination (evaluation), through a finite proof:
i E!_[i] G.	(¬i E!_[i] G) (¬j E!_[j] ¬G).	i E!_[i] ¬G.
Interpretation (denotation, assignment):
m M !_[m] G.	(¬m M !_[m] G) (¬n M !_[n] ¬G).	m M !_[m] ¬G.

Neither true nor false:

Definite-Contingency

,
Contingent-invalidity (invalid but consistent),
Contingent-satisfiability (invalid but satisfyable),
Insufficiently grounded.

D-CONTIN(G);

{SATBL(G)

¬TAUT(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

! _[n]

¬G) }.

Level II:

Satisfiability / validity

2.1. Truth-values table for PPL - bivalid.

This truth-values 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 states-relation.
Thus the following table arises of 4 columns by 16 rows is 64 cells; each containing one precise truth value.

Table bivalid value combinations - with two variables, interpreted for PPL
No.	Value pattern				Logical relation in PPL			Logical power
1	1	1	1	1	T	¬ F	X ¬ X	0
2	0	0	0	0	F	¬ T	X ¬ X	1
3	1	1	0	0	A	¬¬ A		0.50
4	1	0	1	0	B	¬¬ B		0.50
5	0	0	1	1	¬ A	¬ A		0.50
6	0	1	0	1	¬ B	¬ B		0.50
7	1	0	0	0	A B	¬(¬ A ¬ B )		0.75
8	0	1	0	0	A ¬ B	¬(¬ A B )		0.75
9	0	0	1	0	¬ A B	¬( A ¬ B )		0.75
10	0	0	0	1	¬ A ¬ B	¬( A B )	A \ B	0.75
11	1	1	1	0	A B	¬(¬ A ¬ B )		0.25
12	1	1	0	1	A ¬ B	¬(¬ A B )	A B	0.25
13	1	0	1	1	¬ A B	¬( A ¬ B )	A B	0.25
14	0	1	1	1	¬ A ¬ B	¬( A B )	A \| B	0.25
15	1	0	0	1	A B	¬( A # B )		0.50
16	0	1	1	0	A # B	¬( A B )		0.50
{Naar: Benjamin Peirce (1809-1880), Friedrich Wilheml Karl Ernst Schröder (1841-1902), e.a..}
{Zie: Bewijsmethode voor Propositielogica: de Waarheidswaarden- tabelmethode.}

2.2. Truth-values 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 hyper-exponential ways.
Next, in PDL so-called quantors may be applied to predications on object-variables, 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.

Table bivalid value combinations - with two variables, interpreted for PDL and PPL
No.	Value pattern				Logical relation in PPL			Logical relation in PDL		Logical relation in Sk	Logical power
1	1	1	1	1	T	¬ F	X ¬ X				0
2	0	0	0	0	F	¬ T	X ¬ X				1
3	1	1	0	0	A ₁	¬¬ A ₁					0.50
4	1	0	1	0	A ₂	¬¬ A ₂					0.50
5	0	0	1	1	¬ A ₁	¬ A ₁					0.50
6	0	1	0	1	¬ A ₂	¬ A ₂					0.50
7	1	0	0	0	A ₁ A ₂	¬(¬ A ₁ ¬ A ₂)		x A _[x]	¬x ¬ A _[x]	A [x]	0.75
8	0	1	0	0	A ₁ ¬ A ₂	¬(¬ A ₁ A ₂)					0.75
9	0	0	1	0	¬ A ₁ A ₂	¬( A ₁ ¬ A ₂)					0.75
10	0	0	0	1	¬ A ₁ ¬ A ₂	¬( A ₁ A ₂)	A ₁ \ A ₂	¬x A _[x]	x ¬ A _[x]	¬ A [x]	0.75
11	1	1	1	0	A ₁ A ₂	¬(¬ A ₁ ¬ A ₂)		x A _[x]	¬x ¬ A _[x]	A [ c _s]	0.25
12	1	1	0	1	A ₁ ¬ A ₂	¬(¬ A ₁ A ₂)	A ₁ A ₂				0.25
13	1	0	1	1	¬ A ₁ A ₂	¬( A ₁ ¬ A ₂)	A ₁ A ₂				0.25
14	0	1	1	1	¬ A ₁ ¬ A ₂	¬( A ₁ A ₂)	A ₁ \| A ₂	¬x A _[x]	x ¬ A _[x]	¬ A [ c _s]	0.25
15	1	0	0	1	A ₁ A ₂	¬( A ₁ # A ₂)					0.50
16	0	1	1	0	A ₁ # A ₂	¬( A ₁ A ₂)					0.50

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

$

{

j ( (F_[j]

T^*)

($0

F_[j]) )_j;

j ($0

F_[j]) _j;

($0

(

F_[j]) );

($0

(

j F _[j]) );

($0

(

F_[j]) );

($0

(

T^*)) }.

(b)

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

$

{

j ( (F_[j]

T^*)

(F_[j]

1 ) }.

(c)

Contradiction, Logical power and truth.

Combining (a) and (b).

{

j ( (F_[j]

T^*)

( ($0

F_[j])

(

k ( (K^*_[k]

CNF

^*(T^*))

(K^*_[k]

=

{ [ F _[1]

[ F_[2]

.. ] ] F _[n[k]] } )

(n[k]

=

|

K^*_[k]

|

)

(K^*_[k]

=

{

_{(j[k]=1,..n[k])} F_[j[k]] } )

( (

j ( (F_[j]

K^*_[k])

F_[j]

=

{ [ G_{[j
,1]}

[ G_[j,2]

.. G _[m[j[k]]] ] ] } )

(m[j[k]]

=

|

F_[j]

|

( (F_[j]

=

{

_{(h[j[k]]=1,..h[n[k]])} G_[h[j[k]]]) } )

( (0

>

j[k]

≥

n[k] )

>

h[j[k]]

≥

m[j[k]]) ) ) )_j )_k ) }.

2.5. Judging theories (sets of propositions).

How can we judge the logical 'status', or semantical value, of such a set? This is dependent of the formal system, or the logical language in which the set has been formulated.

We can only mention some preconditions that in general apply to judge a set of formulas.

General requirements for judging a theory :

(a)

The set is valid (is a tautology).

{

k ( (K^*_[k]

CNF

^*(T^*))

( (

j ( (F_[j]

K^*_[k])

( (F_[j]

$

=

( (

|

F_[j]

|

>

(

h ( (G_{[h[j[k
]]]}

F_[j])

(G_[h[j[k]]]

$

=

1) )_h ) ) ) )_j )

)

(K^*_[k]

$

=

1) )_k }.

(b)

The set is inconsistent (contains contradiction).

{

k ( (K^*_[k]

CNF

^*(T^*))

( (

j ( (F_[j]

K^*_[k])

( (F_[j]

$

=

( (

|

F_[j]

|

>

(

h ( (G_{[h[j[k
]]]}

F_[j])

(G_[h[j[k]]]

$

=

0) )_h ) ) ) )_j )

)

(K^*_[k]

$

=

0) )_k }.

(c)

The set is contingent (is undecided).

Neither (a) nor (b).

**2.6. Contingency and Presupposition.**

Contingency.

In its most general sense, 'contingent' means indefinite, which meaning can in turn have various shades: not defined, not yet established, conditional, thus yet to be determined; also: not necessarily (the case), not inherent, not essential; sometimes also: accidental, 'by chance' or subject to chance, coincidence and the like.
In formal logic we can distinguish two meanings of the term contingency which can be defined in a perfectly precise and exact way.

(1)

Indefinitely-contingent.

Contingent in the sense of sub-specific indefinite, or indefinitely. Which means: (entirely) undecided as for the truth value.
(Not to be confused with indefinite in mathematic, algebraic sense).
The truth value can therefore in principle still vary 'freely' over the entire value scale, that is in a binary system from 0[00..] (false, contradiction) to 1[11..] (true, valid, tautology), i.e. both these extremes included.

{

j (I-CONTIN(F_{[
j]} )

((0[00..) ≤

$

(F_[j] ) ≤ (1[11..]) );

(

$

(F_[j])

[

0[00..] .. 1[11..]

]

) }.

A statement or reasoning which is indefinitely-contingent, is thus not (yet) valuated. Therefore, it does not necessarily need to be (finitely-)provable.
It doesn't even have to be decidable.
So it has not been validated, So it doesn't have to be valid too.
It certainly doesn't have to consistent.
(2)

Definite-contingent, or Contingent-invalid.

Contingent in the sense of specifically indefinite, or definite, which means (entirely) decided as for the truth value.
The truth value however, is here between the extreme values of the value scale, that is in a binary system as it were 'locked in' between 0[00..] (false, contradiction) to 1[11..] (true, valid, tautology ), i.e. both these extremes excluded.

{

j (D-CONTIN(F_{[
j]} )

((0[00..) <

$

(F_[j] ) < (1[11..]) );

(

$

(F_[j])

<

0[00..] .. 1[11..]

>

) }.

A statement or reasoning which is definitely-contingent, has therefore been shown to be - in terms of truth/validity - not (finitely-)provable.
As such, she has thus been shown to be decidable.
She is indeed thereby proven to be invalid, and in addition, she has proven to be consistent, and, moreover, according to the Consistency Theorem (see 2.8) to be satisfyable.

Unless otherwise stated, 'contingent' will be used here in the sense of 'definitely-contingent' or ' contingent-invalid'.

Presupposition.

To be distinguished:

(1) Logical presupposition is what completes the grounds of an invalid inference pattern thus making the latter valid.
She is only bounded to universal abstract patterns following laws and principles of a system of (formal, or combinatory) logic.
(2) Linguistic presupposition is different: namely, what is implied by a language expression or sign-giving regardless of any truth value of the latter in her references (is as it where a consequens in termines).
She is bounded to specific language symbols and structures following conventional rules of syntax and lexicon of a (human) language system.
Both are therefore not directly physically-bound (i.e. not to time, space, energy, matter).
(3) A prejudice is an internal, mental or psychological content, in particular of cognitive nature.
Thus she is bounded to a person or group (performative, author, source). Because of this, she is at least in part, and at least first - through neuro-physiology - physically-bound. Thus she is essentially incidental of nature (although possibly of relative long duration). She precedes in time actual conclusions, decisions, utterances, behavior, etc..

Some mutual relations.

(·) Any given language expression may imply a linguistic presupposition.
(·) A linguistic presupposition may originate from the presence of a psychological (cognitive) content - or, not too rarely, absence of such.
(·) A psychological (cognitive) content may entirely or partly be construed on basis of the presence of prejudice.
(·) A prejudice may come from an invalid inference.
(·) An invalid inference necessarily and simultaneously implies a logical presupposition: i.e. contradiction or definite-contingency.

Notice how only the latter relation is necessarily always valid, and may also be derivable in a explicit, complete, precise and secure way .. (although dependent of finitely-provability and decidability).

Definite-contingency, in formal terms.

A formula F_[j] is definitely-contingent:

• F_[j] is satisfyable, but invalid;
• F_[j] is neither true, nor false;
• The truth-value pattern c_[t] of F_[j] lies between

$

0[00..] and

$

1[11..];

(·) There exists a formula X_[i]) that is logically equivalent to F _[j], and that is syntactically identical to the maximal semantical reduct of F_[j], i.e. F_{[j]·equiv-rdc};

Thus: Assuming X_[i] satisfies F_[j]) ;
In other words: F_[j] presupposes X_[i]) .

(·) There exists an interpretation i.e. model

M

!_[m] that is or contains X_[i], and (therefore) under which F_[j] is valid.

{

j ( D-CONTIN(F_[j] );

•

{SATBL(F_[j] )

¬TAUT(F_[j] ) };
•

( ((¬

F_[j])

(¬

¬F_[j]));
•

(

t ( (F_[j]$ = c _[t])

(

$

<

c_[t]

<

$

1) )_t;

(·)

(

i ( ( (F _[j]

X_[i])

(F_{[j]·equiv-rdc}

=

_(syn
) X_[i])

((¬

X_[i])

(¬

¬X_[i])) );

(X_[i]

F_[j]);

(X_[i]

(

F_[j]));

(·)

(

m (

M

!_[m]

X_[i] )

(

M

!_[m]

F_[j] ) )_m ) )_i ) )_j }.

2.7. Basic Valid and Invalid derivations.

(a)

Equivalent-validity.

(Semantical equivalent-reduction; Paraphrase).

E.g.: {

j ( (¬F _[h]

G_[j])

(F _[h]

G_[j]) )_j ,_h }.

(b)

Degressive-validity.

(Semantical degressive-reduction; Subsumption).

E.g.: {

j ( (F_[h]

G_[j])

_{(
degres
)} (

l ( (F_[h]

C_[k])

(G_[j]

D_[l]) )_l ,_k ) )_j ,_h }.

(c)

Contingent-invalidity.

E.g.: {

j ( (F_[h]

G_[j])

_{(
nonseq
)} ( (

k ( (F_[h]

D_[k])

G_[j] )_k )

(

l ( F_[h]

(G_[j]

C_[l]) ) _l ) ) )_j ,_h }.

(d)

Inconsistent-invalidity.

(Contradiction; Reductio ad absurdum).

E.g.: {

j ( (F_[h]

G_[j])

_{(
contrad
)} (F_[h]

¬G_[j]) )_j ,_h }.

Inference in Logic - Basic valid and invalid derivations

2.8. Validity, Satisfiability and Contingency.

Diagram Validity / Satisfiability / Contingentie
1	±	0
Not necessarily untrue : Satisfiable , 'Logically possible'. (Is not yet equivalent to 'possibly true'). SATBL(G); (TAUT(G) D-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 , Inconsistent-invalidity. 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 (Model-existence theorem): 'Consistency implies Satisfiability'. (Every subset : (Consistent Satisfiable)). {CONSIS(K^) SATBL(K^)}; {¬(K^* ) ¬(K^* )}.
Necessarily / always true : Valid , Tautology, Valid-satisfiability. 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) };	Neither true nor false: Definite-Contingency , Contingent-invalidity (invalid but consistent), Contingent-satisfiability (invalid but satisfyable), Insufficiently grounded. D-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 necessarily-true : Invalid , non sequitur [nonseq]: NONSEQ(G); ¬TAUT(G); (D-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 in-formele-zin): '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 PDL-I: proof by Kurt F. Gödel (1929/1930, Über die Vollständigkeit des Logikkalküls).	(·) Incompleteness of elementary arithmetic (first-order 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 I-III (1910, 1912, 1913): proved by Kurt Gödel (1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme 1 ).

2.9. Relations between logical criteria of level II.

(1)

Valid statement or inference.

(By assumption or (re)presentation).
'From strong to weak'.

( Valid

Satisfiable /Consistent ).

( Definitely-Contingent

Satisfiable / Consistent ).

( Definitely-Contingent

Invalid ).

( Unsatisfiable /Inconsistent /Contradiction

Invalid ).

( Onvervulbaar /Inconsistent /Contradictie

#

Satisfiable /Consistent ).

( Valid

#

Invalid ).

Level III.

Decidability and Recursivity of formal systems

*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 Truth-value 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 truth-value 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 ) }. { D-CONTIN(G) } (no validity value). $ 0 (no truth). G is indeterminate.
Recursive: For all input, the system will be 'halting' (terminating in finite time).		Non-recursive: For some input the system will be infinitely 'looping'.
RC(G); { RE(G) CO-RE(G) }; { ( ( G) ) \|\| ( (¬ G) ) }; Implications: { ( ( G) \|\| (¬ G) ) }.		¬RC(G); { ¬RE(G) ¬CO-RE(G) }. { (¬ ( G) ) (¬ (¬ G) ) }; Implications: { ¬ ( ( G) \|\| (¬ G) ) }.
Recursively enumerable: Formula G is Recursively enumerable: If G has a result, then that will always be provable. RE(G); { j ( (G F_[j]) (G F_[j]) )_j }.	Co-recursively enumerable: Complement of G is Recursively enumerable: If G has no result, then that will always be provable. CO-RE(G); { j ( ¬(G F_[j]) ¬(G F_[j]) )_j }.	Not recursively enumerable: Formula G is not Recursively enumerable: If G has a result, then that will not always be provable. ¬RE(G); { j ( (G F_[j]) ¬(G F_[j]) )_j }.	Not co-recursively enumerable: Complement of G is not Recursively enumerable: If G has not a result, then that will not always be provable. ¬CO-RE(G); { j ( ¬(G F_[j]) ¬¬(G F_[j]) )_j }.
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. CO-RE(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. ¬CO-RE(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. CO-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 }.	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. ¬CO-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 }.
(·) '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/ non-recursivity of elementary calculus of natural numbers (elementary number theory): proof by Alonzo Church, (1935/1936, An Unsolvable Problem of Elementary Number Theory). (·) UnDecidability/ non-recursivity of entire elementary arithmetic (first order arithmetic): proof by Alan M. Turing (1936/1937, On computable numbers, with an application to the Entscheidungsproblem).

Table with Some Milestones in Meta-logic

Author	Year	Formalism	Domain	Criterion
Hilbert	1900,1928	Effective procedure (hypothetical)	Mathematics, Logic	Decidability; Entscheidbarheit; Entscheidungs-definitheit;
Post	1920	Truth table method	PPL	Completeness; Vollständigkeit.
Gödel	1929/1930	Deduction	PDL-I	Completeness; Vollständigkeit. Recursively enumerable
Gödel	1931	Gödel-numbering	PDL-I, Arithmetic of Natural numbers First-order theory of natural numbers (Principia Mathematica)	Einige formal unentscheidbare Satze: Incompleteness; Unvollständigkeit. Not recursively enumerable.
Church	1935/1936	Lambda-calculus (Lambda-definable): Recursive functions of positive integers	PDL-I, Arithmetic of Natural numbers: Elementary number theory	Unsolvable problem: UnDecidability; Unentscheidbarheit.
Turing	1936/1937	(Universal) Turing machine (Turing machine computability)	PDL-I, Arithmetic: First order arithmetic	UnDecidability; Unentscheidbarheit.

Criteria in formal logic

In the overview ' Criteria in Formal Logic' the most important criteria in formal logic are being discussed.
These criteria may be applied to formulas, sentences, sets, theories and (language) systems in logic.
They are meant to represent entirely accurate the most essential characteristics of certain data: quality, scope, possibilities but also limitations.

Criteria in Formal Logic

(1)

Semantic criteria

Criteria for decisions about content aspects of language expressions.
A.o. satisfiability, validity, (definitely-)contingency, finite-satisfiability, compactness, etc..

(1a) Satisfiability: (Logical possibility): Truth under at least one possible interpretation.

((Well-formed

not-Refuted)

Satisfiable).

(1b) Validity (tautology):) Truth under any possible interpretation.

((Well-formed

always-True)

Valid).

(1c) Definitely-contingency: Satisfiable, but not valid.
(Truth under at least one possible interpretation, maar not all).

((Well-formed

(Satisfiable

not-Valid))

Definitely-contingent).

(1d) Finite-satisfiability: A (sub)set of formulas is finite and satisfiable.

(((Sub)set

(Well-formed

(Finite

Satisfiable)))

Finite-satisfiable).

(1e) Compactness: If every finite subset of a - possibly infinite - set is satisfiable, that the entire set is satisfiable.

(((Every subset: (Well-formed

Finitely satisfiable))

Satisfiable)

Compact).

(2)

Syntactical criteria.

Criteria for decisions about aspects of form and structure of statements.
Correctness: A.o. derivability, provability, consistency.

(2a) Derivability: Derivable through syntactical production rules.

((Well-formed

result of accurate formal operations)

Derivable).

(2b) Provability (finite-derivability): Syntactical derivable through a finite derivation chain.

(((Well-formed

result of finite series of purely formal operations)

Finite-derivable)

Provable).

(2c) Consistency: Derivable guarantees non-contradiction.

(For any subset: ((Derivable

Non-contradiction)

Consistent)).

(2d) Maximal consistency: Consistency guarantees inconsistency with every possible semantic/i> (ie. nonredundant, conjunctive) expansion.

((Consistent (adding of any other formula inconsistent)) Maximally consistent).

(2e) Negation-completeness: A set K^* contains for every well-formed formula in the language either the confirmation, or the negation.

((Every subset: (Well-formed (Truth decision (either True, or False)))) Negation-complete).

(3)

Semantical criteria, in relation to syntax:

Ie. projections from semantics to syntax.
A.o. completeness.

(3a) Syntactical - Adequacy.
Satisfiability guarantees Consistency.

((Every subset: (Satisfiable

Consistent))

Adequate).

(3b) Syntactical - Completeness (proof potential, Vollständigkeit): Truth/ validity guarantees Derivability.

((Every subset: (True/ valid

Derivable))

Complete).

(4)

Syntactical criteria, in relation to semantics:

Ie. projections from syntax to semantics.
A.o. consistency theorem, correctness, Decidability.

(4a) Fundamental theorem, consistency theorem: Consistency guarantees satisfiability.

((Every subset: (Consistent

Satisfiable))

Fundamental theorem).

(4b) Logical correctness of formal systems ('soundness', in weak sense, deductive power): Derivability guarantees Validity.

((Every subset: (Derivable

True/ Valide))

Correct)).

(4c) Logical 'soundness' of formal systems (in strong sense): Derivability guarantees Logical Consequence.

((Every subset: (Derivable

Logical consequent))

Sound).

(4d) Reductio ad absurdum: Logical validity guarantees Non-contradiction.

In other words, from provability of contradiction derived from the opposite, follows logica l validity.
Principle of proof by 'refutation of the opposite'.

((Well-formedness

(Opposite/Negation

(Some conjunct subset: (Contradiction derivable: inconsistent ))))

True/ Valid).

(4e) Decidability (decision capacity) of formal systems: Syntactical well-formedness guarantees validity decision.

(Well-formedness

(Validity decision:

(either Valid, or Invalid)))

Validity Decidable).

Method of 'Formal Logic'

Diagrams

Logical levels and criteria

Contents

Meta-truth: logical criteria

Logical quality

Level I:

Truth / Falsity

of statements

1.1. Truth-values table for PPL for two variables.

Truth-values table PPL - for one variable.

Truth values

1

±

0

True

Unspecified

False

Truth value

$

=

<

$

<

$

=

Truth value assignment

Truth value determination

Interpretation

M

M

M

M

Neither true nor false:

Definite-Contingency

<

<

$

M

M

Level II:

Satisfiability / validity

2.1. Truth-values table for PPL - bivalid.

Table bivalid value combinations - with two variables, interpreted for PPL

PPL

T

F

X

X

F

T

X

X

A

A

B

B

A

A

B

B

A

B

A

B

A

B

A

B

A

B

A

B

A

B

A

B

A

B

A

**Method of 'Formal Logic'**

Table bivalid value combinations
- with two variables, interpreted for PPL

Table bivalid value combinations
- with two variables, interpreted for PDL and PPL