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)

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