negation, contradiction, absurdity

Back to title page

7. Miscellaneous

7.1. Negation as Contradiction or Absurdity

The idea behind this approach is as follows: let us define ~B (i.e. "B is false") as "B implies absurdity". So, let us add to our first order language a predicate constant f (meaning "false", or "absurdity"), and let us replace all negation expressions ~F by F->f. Then, the three negation axioms will take the following forms:

L₉: (B->C)->((B->~C)->~B),

L₉': (B->C)->((B->(C->f))->(B->f)),

L₁₀: ~B->(B->C),

L₁₀': (B->f)->(B->C),

L₁₁: Bv~B,

L₁₁': Bv(B->f).

After this, surprisingly, the axiom L₉' becomes derivable from L₁-L₂! Indeed,

Hence, by Deduction Theorem 1, [L₁, L₂, MP] |- (B->C)->((B->(C->f))->(B->f)).

Second observation: L₁₀': (B->f)->(B->C) can be replaced simply by f->C. Indeed, if we assume f->C, then L₁₀' becomes derivable:

Hence, by Deduction Theorem 1, [L₁, L₂, f->C, MP] |- (B->f)->(B->C).

Third observation. As we know from Theorem 2.4.9: [L₁, L₂, L₉, MP] |- ~B->(B->~C), in the minimal logic we can prove 50% of L₁₀: "Contradiction implies that all is wrong". After our replacing negations by B->f the formula (B->f)->(B->(C->f) becomes derivable from L₁-L₂. Indeed,

Hence, by Deduction Theorem 1, [L₁, L₂, MP] |- (B->f)->(B->(C->f)).

Thus, we see that L₁ (and not L₉!) is responsible for provability of the 50% "crazy" formula ~B->(B->~C). Is L₁ 50% as "crazy" as L₁₀? Yes! Let us compare:

L₁₀: ~B->(B->C) states that "Contradiction implies anything".

L₁: B->(C->B) states that "If B is true, then B follows from anything".

Let us recall our "argument" for L₁₀ from Section 1.3: "...we do not need to know, were C "true" or not, if ~B and B were "true" simultaneously. By assuming that "if ~B and B were true simultaneously, then anything were true" we greatly simplify our logical apparatus."

Now, similarly: if B is (unconditionally) true, then we do not need to know, follows B from C or not. By assuming that "if B is true, then B follows from anything" we greatly simplify our logical apparatus.

In a sense, the axiom L₉ "defines" the negation of the minimal logic, the axioms L₉ and L₁₀ "define" the negation of the constructive logic, and L₉-L₁₁ "define" the negation of the classical logic. Is our definition of ~B as B->f equivalent to these "definitions"? Yes!

Theorem 7.1.1. For any formula F, let us denote by F' the formula obtained from F by replacing all sub-formulas ~G by G->f. Then, for any formulas B₁, ..., B_n, C:

[L₁-L₉, MP]: B₁, ..., B_n |- C, iff [L₁-L₈, MP]: B'₁, ..., B'_n |- C'.

Proof.

1) ->.

Let us consider a proof of [L₁-L₉, MP]: B₁, ..., B_n |- C. In this proof:

- let us replace each formula G by its "translation" G',

- before each instance of L₉, let us insert a proof of the corresponding instance of L'₉ in [L₁, L₂, MP] (see above).

In this way we obtain a proof of [L₁-L₈, MP]: B'₁, ..., B'_n |- C'. Indeed,

a) If some formula B is an instance of L₁-L₈, then B' is an instance of the same axiom (verify!).

b) (B->D)' is B'->D', hence, if the initial proof contains a conclusion by MP from B and B->D to D, then, in the derived proof, it is converted into a conclusion by MP from B' and B'->D' to D'.

c) If the initial proof contains an instance of L₉, then the derived proof contains the corresponding instance of L'₉ preceded by its proof in [L₁, L₂, MP].

Q.E.D.

2) <-.

Let us recall the above translation operation: for any formula F, we denoted by F' the formula obtained from F by replacing all sub-formulas ~G by G->f. Now, let us introduce a kind of a converse operation - the re-translation operation: for any formula F, let us denote by F" the formula obtained from F: a) by replacing all sub-formulas G->f by ~G, and after this, b) by replacing all the remaining f's (f means "false"!) by ~(a->a), where a is some closed formula of the language considered.

Of course, for any formula F, (F')" is F (verify).

Note. Replacing f by a formula preceded by negation, is crucial - it will allow using Theorem 2.4.9: [L₁-L₉, MP]: ~B->(B->~C) instead of the Axiom L₁₀: ~B->(B->C).

Now, let us consider a proof of [L₁-L₈, MP]: B'₁, ..., B'_n |- C'. In this proof, let us replace each formula G by its re-translation G". Then C' becomes C, and B'₁, ..., B'_n become B₁, ..., B_n, but what about the remaining formulas contained in the proof?

a) Instances of the axioms L₁-L₈.

L₁: B->(C->B)

If B is not f, then (B->(C->B))" is B"->(C"->B"), i.e. re-translation yields again an instance of L₁.

If B is f, then (f->(C->f))" is ~(a->a)->~C". This formula is provable in [L₁-L₉, MP]. Indeed,

Thus, re-translation of any instance of L₁ is provable in [L₁-L₉, MP].

L₂: (B->(C->D))->((B->C)->(B->D))

If C and D are not f, then re-translation yields again an instance of L₂.

If C is f, and D is not, then re-translation yields (B"->(~(a->a)->D"))->(~B"->(B"->D")). This formula is provable in [L₁-L₉, MP]. Indeed,

Hence, by Deduction Theorem 1, [L₁-L₉, MP] |- (B"->(~(a->a)->D"))->(~B"->(B"->D")).

If D is f, and C is not, then re-translation yields (B"->~C")->((B"->C")->~B"). This formula is provable in [L₁-L₉, MP]. Indeed,

Hence, by Deduction Theorem 1, [L₁-L₉, MP] |-(B"->~C")->((B"->C")->~B").

If C and D both are f, then re-translation yields (B"->~~(a->a))->(~B"->~B"). This formula is provable in [L₁-L₉, MP]. Indeed,

Thus, re-translation of any instance of L₂ is provable in [L₁-L₉, MP].

L₃: B&C->B

If B is not f, then re-translation yields again an instance of L₃.

If B is f, then re-translation yields via ~(f&C) the formula ~(~(a->a)&C). This formula is provable in [L₁-L₉, MP]. Indeed,

Thus, re-translation of any instance of L₃ is provable in [L₁-L₉, MP].

L₄: B&C->C

Similarly to L₃ - re-translation of any instance of L₄ is provable in [L₁-L₉, MP].

L₅: B->(C->B&C)

Re-translation yields again an instance of L₅.

L₆: B->BvC

Re-translation yields again an instance of L₆.

L₇: C->BvC

Re-translation yields again an instance of L₇.

L₈: (B->D)->((C->D)->(BvC->D)

If D is not f, then re-translation yields again an instance of L₈.

If D is f, then re-translation yields ~B->(~C->~(BvC)). By Theorem 2.4.10(b), this formula is provable in [L₁-L₉, MP] .

Thus, re-translation of any instance of L₈ is provable in [L₁-L₉, MP].

Hence, re-translations of all (i.e. L₁-L₈) axiom instances are provable in [L₁-L₉, MP]. What about applications of MP in the initial proof? If the initial proof contains a conclusion by MP from B and B->D to D, then the following situations are possible:

a) If B and D are not f, then, in the derived proof, this conclusion is converted into a conclusion by MP from B" and B"->D" to D".

b) If B is f, and D is not, then, in the derived proof, this conclusion is converted into a conclusion by MP from ~(a->a) and ~(a->a)->D" to D".

c) If D is f, and B is not, then, in the derived proof, this conclusion is converted into three formulas: B", ~B", ~(a->a). To derive ~(a->a) from B" and ~B", we can use MP and Theorem 2.4.9: [L₁-L₉, MP] |- ~B"->(B"->~(a->a)).

d) If B and D are both f, then, in the derived proof, this conclusion is converted into three formulas: ~(a->a), ~~(a->a), ~(a->a). Simply drop the third formula from the proof.

Thus, the re-translation operation, when applied to all formulas of a proof of [L₁-L₈, MP]: B'₁, ..., B'_n |- C', yields a sequence of formulas that are provable in [L₁-L₉, MP] from hypotheses B₁, ..., B_n. Hence, so is C.

Q.E.D.

This completes the proof of Theorem 7.1.1.

Corollary 7.1.2. a) A formula C is provable in the minimal propositional logic [L₁-L₉, MP], iff [L₁-L₈, MP] |- C'.

b) A formula C is provable in the constructive propositional logic [L₁-L₁₀, MP], iff [L₁-L₈, f->B, MP] |- C'.

c) A formula C is provable in the classical propositional logic [L₁-L₁₁, MP], iff [L₁-L₈, f->B, L'₁₁, MP] |- C'.

Proof. a) Consider an empty set of hypotheses in Theorem 7.1.1.

b) If [L₁-L₁₀, MP] |- C, then [L₁-L₉, MP]: B₁, ..., B_n |- C, where hypotheses are instances of the axiom L₁₀. By Theorem 7.1.1, [L₁-L₈, MP]: B'₁, ..., B'_n |- C'. As established above, B'₁, ..., B'_n can be proved by using the axiom schema f->B, i.e. [L₁-L₈, f->B, MP] |- C'. Q.E.D.

Now, if [L₁-L₈, f->B, MP] |- C', then,

c) If [L₁-L₁₁, MP] |- C, then [L₁-L₉, MP]: B₁, ..., B_n |- C, where hypotheses are instances of the axioms L₁₀ and L₁₁. Return to case (b). Q.E.D.

Corollary 7.1.3. a) A formula C is provable in the minimal predicate logic [L₁-L₉, L₁₂-L₁₅, MP, Gen], iff [L₁-L₈, L₁₂-L₁₅, MP, Gen] |- C'.

b) A formula C is provable in the constructive predicate logic [L₁-L₁₀, L₁₂-L₁₅, MP, Gen], iff [L₁-L₈, f->B, L₁₂-L₁₅, MP, Gen] |- C'.

c) A formula C is provable in the classical predicate logic [L₁-L₁₁, L₁₂-L₁₅, MP, Gen], iff [L₁-L₈, f->B, L₁₁', L₁₂-L₁₅, MP, Gen] |- C'.

Exercise 7.1.1. Prove the Corollary 7.1.3.

7.2. Finite interpretations - Trakhtenbrot's theorem

Warning! Draft text follows.

S.Simpson

http://www.math.psu.edu/simpson/courses/math457/misc/trakh.pdf (with proofs)

Boris Trakhtenbrot

B.A. Trakhtenbrot. The impossibility of an algorithm for the decision problem for finite models. Dokl. Akad. Nauk SSSR, 70:596--572, 1950. English translation in: AMS Transl. Ser. 2, vol.23 (1063), 1--6.

http://www.mcs.le.ac.uk/~istewart/moreIAS/BriefDCT.html by Iain Stewart:

Trakhtenbrot's theorem (1950): "The set of first-order sentences, over some signature including a relation symbol that is not unary, which are valid over finite structures is not r.e. but is co-r.e.". These early results appeared sporadically and tended to be "finite considerations" of analogous results in model theory. This is true of Trakhtenbrot's result where the analogous result in model theory is due to Goedel (1930): "The set of valid first-order sentences is r.e. but not co-r.e.".

Sergei Vorobyov. The "Hardest" Natural Decidable Theory. LICS: IEEE Symposium on Logic in Computer Science, 1997 (PDF):

In 1936 L. Kalmar proved that the first order theory of a binary relation is undecidable, which greatly simplified undecidability proofs, as compared to those based on straightforward encodings of Turing machines, see, e.g. M. Rabin [13] B. Trakhtenbrot [19] and later R. Vaught [20] proved even stronger Theorem 10 . Let L be the first order language with the unique binary relation symbol. The set of valid sentences of L and the set of sentences of L refutable by some finite model are recursively inseparable.

S.Vorobyov

See at http://www.cs.nyu.edu/pipermail/fom/2000-July/004215.html

FOM: No Weakest Axiom of Infinity

Allen Hazen [email protected]
Thu, 06 Jul 2000 15:58:16 +0800

Recent posts from Simpson and Urquhart have mentioned the theorem that "there is no weakest axiom of infinity." I have been puzzled by this for a long time. This probably says more about me than about the intrinsic difficulty of the issue. I think I've de-puzzled myself; since I don't know of a self-contained textbook account, here is mine. (Thanks to Urquhart for suggestions.)

--
The Theorem about Axioms of Infinity
A: Trakhtenbrot on finite satisfiability
B: there is no weakest axiom of infinity
C: a surprise about the Axiom of Choice
D: Compactness and a request
--

-----A-----
The key here is the fact that "There is no weakest Axiom of Infinity" is a corollary of Trakhtenbrot's theorem that the set of first-order formulas valid in FINITE models (i.e. whose negations are not FINITELY satisfiable) is undecidable. This follows from Goedel 1931. There is no complete axiomatization of the Pi-1-1 sentences of arithmetic (i.e., the set of Pi-1-1 truths is not r.e.). A proper initial segment of the natural numbers, however, can be thought of as a finite model. So, (*), if finite satisfiability was decidable, we'd have have a way of proving arbitrary Pi-1-1 truths of arithmetic: just carry out the decision procedure and note that no finite model knocks out the candidate sentence! (The fiddly bit, (*), has to do with a bit of change to the sentence: finite segments of omega are not closed under addition and multiplication, so what we would have to test in finite models was a variant: put a bound on the initial universal quantifiers of the Pi-1-1 sentence (using a new constant), and check that the bounded sentence holds in models that go enough higher than the bound to include denotations for all the terms appearing.)

-----B-----
An axiom of infinity is a sentence of n-th order logic, for some n, which is true in all and only models with an infinite domain of individuals. We can limit our attention to sentences containing no non-logical vocabulary, since a sentence with predicate constants can have them treated as variables bound by initial existential quantifiers. One axiom of infinity is said to be WEAKER than another if it is derivable from it in an axiomatizable fragment of higher-order logic but not vice versa. (Reference: section 57 of Church 1956, "Introduction to Mathematical Logic.") So. Suppose there were a weakest Axiom of Infinity, Q. It would have to be derivable from EVERY other axiom of infinity. Now choose an arbitrary 1st order formula, P. On the supposition that Q exists, we can test P for finite validity as follows. First, form P* by treating the non-logical constants of P as variables and existentially quantifying them. Note that, if P is finitely valid, then P*, if satisfiable at all, is an axiom of infinity. Now we start two mindless-search algorithms side by side: (a) search for a finite model falsifying P, (b) search for a formal proof of (P* -> Q). One of these is bound to terminate; if (a) succeeds P is not finitely valid, and if (b) does it is. Comments:
(i) Since P* is formed by existentially quantifying a 1st-order sentence, it doesn't matter whether P* is unsatisfiable or an axiom of infinity: either way, (P* -> Q) will be provable.
(ii) Church, op. cit., discusses only 2nd order axioms of infinity, but the result obviously holds for higher orders as well.
(iii) If a 1st order sentence (e.g. the negation of P, above) is finitely satisfiable, an exhaustive search will IN PRINCIPLE find a model. Note, however, that this is a thoroughly unbounded algorithm. From Trakhtenbrot's theorem it follows that, for any recursive function f, there is a natural number i such that for some 1-st order sentence S of length i, S is finitely satisfiable but its smallest model has size > f(i). We're talking EFFECTIVE computability, not FEASIBLE!

-----C-----
The surprising thing about the result of part B is that it is DIFFERENT from the other well-known fact about axioms of infinity. Elementary set-theory textbooks give two definitions of INFINITE SET: Dedekind-infinite and non-inductive. Famously, these (or the Axioms of Infinity formed from them) can only be shown equivalent by use of the Axiom of Choice. Leaving the naive reader (me) with the impression "Yes there are non-equivalent Axioms of Infinity, but the Axiom of Choice saves the day and lets you prove them equivalent."
WRONG! This is a different phenomenon; even if we include the Axiom of Choice in the axiomatized fragment of higher order logic considered above, there is STILL an infinite sequence of ever weaker Axioms of Infinity.

-----D-----
In a way this shouldn't surprise us. Consider the infinite sequence of 1st order (with identity) sentences
"There is at least one thing"
"There are at least two things"
"There are at least three things"
and so on. They are jointly satisfiable only in infinite domains, so they can be thought of as constituting, not an Axiom of Infinity, but an "Axiomatization of Infinity." All of them ought to be derivable from any sentence calling itself an Axiom of Infinity: any Axiom of Infinity is at least as strong as this "Axiomatization." By compactness, however, no Axiom of Infinity is derivable from it! Thus, any Axiom of Infinity is properly stronger than the 1st order "Axiomatization." So if there were a weakest Axiom of Infinity, there would be a **gap**. Which would be a surprising and disturbing fact.

HOWEVER... I don't actually know of any Axiom of Infinity weaker than
(*) There is a nonempty family of sets containing a proper superset of each of its members.
I am fond of (*) for a number of reasons. It is close to Whitehead and Russell's Inf Ax. It amounts to saying that the universe is infinite in the non-Dedekind sense from introductory set theory texts. It is in a language (Monadic Third Order logic: closely related to the "Framework" of David Lewis's "Parts of Classes") that I have spent time with. By (B), above, there are weaker Axioms of Infinity. Can anyone give me an example of a properly weaker one? (Reasonably short, natural, non-pathological examples not encoding complex statements about Turing machines preferred.)
Allen Hazen
Philosophy Department
University of Melbourne

See also

www.math.psu.edu/simpson/courses/math557/misc/trakhtenbrot.pdf

www.cs.indiana.edu/classes/foc-leiv/trakh.ps

Back to title page

negation, contradiction, absurdity