User:Wvbailey/Consistency

This is a trial location for improvements to the article consistency

Requirements for a demonstration of consistency

Notion of "theory"

• Finitary methods without making use of an interpretation of the system (Kleene 1967:69)
• List formal symbols
• Axioms

The theory has a logical basis

The theory must contain the symbol ¬(logical negation, NOT)

¬, ⊢, ∀, 0

Kleene 1967:124 --

"The proposition calculus (and generally, any formal system having the symbol ¬ for negation is said to be (simply) consistent , if for no formula A are both A and ¬A provable in the system; and to be (simply) inconsistent in the contrary case that for some formula A, both ⊢A and ⊢¬A.

"This is a striclty metamathematical definition [i.e. the symbol ¬ has no meaning, just behaviors in the system]. It refers only to the formal symbol ¬, and to the defintions of formula and provable formula. It thus becomes an exact mathematical problem, which we can consider in the metamathematics, to prove the consistency of a given formal system.

"... (and generally, for any formal system which as &-elimination and weak ¬-elimination sa postulated or derived rules), the above definition is equivalent to the following. The system is (simply) consistent, if there is some unprovable formula; (simply) inconsistent, if every formula is provable. For if both ⊢A and ⊢¬A, then by use of weak ¬A-elimination, ⊢B for every formula B. In the case of consistency, A & ¬A is an example of an unprovable formula, since otherwise by &-elmination both ⊢A and ⊢¬A.

• informally (A & ¬A), A, ¬A

("If we have an adjunctive implication [p → q] with a false implicans [ p ], the first line of the schema [i.e. the modus ponens p --> q, p] will be true; but, since the implicans [ p ] cannot be asserted, the second line is not true and the conclusion cannot be derived:

IF snow is black THEN sugar is sweat

Snow is black

-------------

X failure of modus ponens

If we have an adjunctive implication [p → q] with a true implicate [ q ], the first line will also be true; if in addition the implicans is true, as in

IF snow is white THEN sugar is sweat

Snow is white

-------------

sugar is sweat

the concluision can be derived; but then it is true, and the inference thus furnishes a true conclusion. . . .

[However in the case of adjunctive implication[ the knowledge of the truth of the implicate is a necessary condition for the case that an inference based on a merely adjunctive implication can be made; therefore the inference is of no use. It is only in its application to connective implicaitons that the inference has practical value. The truth of the implication is then established by means other than an examination of the truth of the implicate . . . the connective implications to be used may be either of the tautological kind or of the synthetic [not-tautological but also not wholly contradictory] kind (cf §9 and chapter VIII).

cf this comes up I think also in Post 1930. Thus the theory must have the symbol ¬ (logical negation, NOT) if simple consistency is to be demonstrated (Kleene 1952:124)

• If "discharge of double negation" is not allowed in the theory, then ¬A → (A → B), given that → is logical implication defined as ¬A V B (i.e. so-called weak ¬A-elimination (cf Kleene 1967:101)

As Franzen notes: "The [Goedel] incompleteness theorm applies to many other kinds of formal systems than first-order theories, but we will assume that the language of a formal system at least includes a negation operator, so that every sentence A in the language has a negation not-A. ... This allows us to define what it means for S to be consistent (there is no A such that both A and not-A are theorems) and for a sentence to be undecidable in S (neither A nor not-A is a theorem of S). A system is complete (sometimes called "negation complete" if no sentence in the lanugage of S is undecidable in S, [sic] and otherwise incomplete."

The theory contains a notion of "truth", and from "truth" derives "falsehood"

"It is the truth of derivable formulas that we have raised . . . To say, for instance, that 'a' V 'b' is true has a meaning only when the symbols a and b are interpreeded as propostions and the hook is interpreted as the operation 'or' . The reason is that truth is a sematntical concept and applies to signs only when they are coordinated to objects, i.e. when they are given a meaning. Within the formal system, the notion of truth is represented mearly by the letter 'T' used in the truth tables, a symbol to which this sytem gives no meaning . . .. The formal system provides us merely with rules for the transfer of the T-symbol; i.e., it tells us which formulas will be of the T-character if certain other formulas are of this character. Both these results are achieved by the rules of derivation and the rules for the establishment of tautologies. " (Reichenbach 1947:167).

"The chief property of truth is its exclusiveness; truth excludes falsehood." (Reichenbach 1947:168)

Notion of "proof"

¬, ⊢, ∀, 0

has certain requirements that must be met before the issue of consistency can be settled:

• (2) The theory must contain the notion of deduction or derivation, i.e. it has the metamathematical notion and the symbol ⊢ (yields)
• (3) The theory must have &-elimination: Given that A and B are true formulas, A & B ⊢ A, A & B ⊢ B

Kleene 1952:71ff

Define 3 categories of formal objects:

• 1 list of formal symbols
• 2 finite sequences of formal symbols via the operation of juxtaposition (or concatenation) (p. 70)
• 3 finite sequences of (occurrences of) formal expressions (p. 70)

Establish Formation rules: "define certain subcategoriese of the formal expressions" (p. 72)

• term
• formula
• metamathematical constructs such as abbreviations for formulas
• notion of variable
• substitution of term t for a variable x into and throughout a formula

Define deductive or transformation rules:

• axioms
• axiom schema -- e.g. B → A V B, here A and B are abbreviations for formulas