Jump to ContentJump to Main Navigation
Truth Through ProofA Formalist Foundation for Mathematics$

Alan Weir

Print publication date: 2010

Print ISBN-13: 9780199541492

Published to Oxford Scholarship Online: January 2011

DOI: 10.1093/acprof:oso/9780199541492.001.0001

Show Summary Details
Page of

PRINTED FROM OXFORD SCHOLARSHIP ONLINE (www.oxfordscholarship.com). (c) Copyright Oxford University Press, 2017. All Rights Reserved. Under the terms of the licence agreement, an individual user may print out a PDF of a single chapter of a monograph in OSO for personal use (for details see http://www.oxfordscholarship.com/page/privacy-policy). Subscriber: null; date: 26 March 2017

(p.252) Appendix

(p.252) Appendix

Source:
Truth Through Proof
Author(s):

Alan Weir

Publisher:
Oxford University Press

§A.1 Minimax Rules

If we take (single conclusion) sequent rules to have the schematic form:

X 1 P 1 , X 2 P 2 , X n P n 0 i n X i C
then a minimax sequent rule is one in which P1,…Pn minimax entails C—it is not possible (under the Kleene scheme) for the minimum Pi value in a valuation to be greater than the value of C in that valuation. Such rules preserve neo-classical correctness. (The definition of neo-classical entailment, given in Chapter 7, §III, is:

X ╞ C iff in all models M if all of X are true in M then C is true and if C is false and all of X but P are true, then P is false.)

For if all of 0 i n X i are true in valuation v then so are all the Pi, since all the premiss sequents are neo-classically correct; hence so is C by the minimax entailment. Whilst if C is false in v but all of the wffs in 0 i n X i but A are true in v then since the Pi minimax entail C, at least one of the premiss succeedents is false, say Pk; in which case by the neo-classical correctness of Xk ⇒ Pk, A ∊ Xk and is false in v.

Minimax soundness is a mechanically decidable principle, for finite sequent rules. If we wish to set out rules for it, one set has the general form:

X

(1) φ

Given

X

(2) φ[P/Q]

1 MM

(‘MM’ for Minimax) where φ[P/Q] results from φ by uniform substitution of a sub-formula P by Q and where (p.253)

P is

A

and Q is

∼∼A

or P is

∼∼A

and Q is

A

or P is

A & B

and Q is

B & A

or P is

A ∨ B

and Q is

B ∨ A

or P is

A & B

and Q is

∼(∼A ∨ ∼B)

or P is

∼(∼A ∨ ∼B)

and Q is

A & B

or P is

A ∨ B

and Q is

∼(∼A & ∼B)

or P is

∼(∼A & ∼B)

and Q is

A ∨ B

or P is

(A & (B & C))

and Q is

((A & B) & C)

or P is

((A & B) & C)

and Q is

(A & (B & C))

or P is

(A ∨ (B ∨ C))

and Q is

((A ∨ B) ∨ C)

or P is

((A ∨ B) ∨ C)

and Q is

(A ∨ (B ∨ C))

or P is

(A & (B ∨ C))

and Q is

((A & B) ∨ (A & C))

or P is

((A & B) ∨ (A & C))

and Q is

(A & (B ∨ C))

or P is

(A ∨ (B & C))

and Q is

((A ∨ B) & (A ∨ C))

or P is

((A ∨ B) & (A ∨ C))

and Q is

(A ∨ (B & C))

Minimax soundness is easily established by showing that the formula on the left has the same value, in every model, as the formula on the right. In addition standard sequent form natural deduction ∨I, &E and &I rules (without any determinacy restriction on overlapping assumptions in both premiss antecedents) are minimax sound as is the Mingle rule:

X

(1) A & ∼A

Given

X

(2) B ∨ ∼B

1 Mingle

which is a derived rule of the logic RM which extends relevant logic R by addition of the Mingle axiom scheme.1

Most of the minimax rules generalize straightforwardly to the infinitary case. (The distributivity rules are an exception: to extend completeness results for standard languages any significant way into the transfinite one needs extra rules such as the ‘ordinary’ or ‘Chang’ distributivity laws (Karp 1964, p. 41; Dickmann 1975, p. 421). The distributivity schema, for all γ 〈 κ, κ the index of the language, is :

α α γ β β γ φ α , β
where each φα,β is either φδ or ∼φδ, for some δ 〈 γ and for every function f from γ: γ there is an ε 〈 γ such that {φε, ∼φε} ⊆ {φα,f(α): α 〈 γ}.)

§A.2 Soundness of Strict Neo-classical Logic

The proof is of the usual inductive type. The semantics for the operators is the Lukasiewicz/Kleene semantics of Chapter 7. As illustration, the inductive step for the ∨E rule:

(p.254)

X

(1) P ∨ Q

Given

Y,P

(2) C

Given

Z,Q

(3) C

Given

X,Y,Z,

(5) C

1,2,3 ∨E

where (X ∩ (Y ∪ Z)) = Ø is as follows:

Proof: (i) Truth preservation: this is exactly as in the classical case. (ii) Falsity preservation (upwards): suppose that C is false in v and all of X,Y,Z, are true in v but A.

  1. Case (a): A ∉ X. Then, by the (strict) neo-classical correctness of line (1) (inductive hypothesis) P ∨ Q is true in v hence one of the disjuncts is; suppose without loss of generality that it is P. By the correctness of line (2) in the rule above, A ∊ Y and is false.

  2. Case (b): A Y ∪ Z. By the correctness of lines (2) and (3) both P and Q are false in v hence so is P ∨ Q. By the correctness of line (1), A ∊ X and is false in v. By the overlap clause (X ∩ (Y ∪ Z)) = Ø, these two options are exhaustive.2

A similar, somewhat less convoluted, proof establishes the soundness of ∼E. The proof for ∨E generalizes to the parallel ∃E rule:

X

(1) ∃xφx

Given

Y, φx/t

(2) C

Given

X,Y,

(4) C

1,2 ∃E

with the usual clauses on t and where X ∩ Y = Ø. Again truth-preservation is classical.

Falsity preservation. Suppose all of X,Y, but A are satisfied by σ (in model M) but C is false relative to σ.

  1. Case (a) A ∉ X. Then ∃xφx is satisfied by σ hence for some α in the domain of M, φx is satisfied by σ[x/α] hence, since t is not in φ, φx/t is satisfied by σ[t/α]. Since t is not in Y or C, all of Y but A are satisfied by σ[t/α] along with φx/t whilst C is falsified by that variant assignment (this is provable by induction on sentence complexity). Hence by the correctness of line 2, A ∊ Y and is falsified by σ[t/α] hence, using the same lemma, by σ.

  2. Case (b) A ∉ Y. Then by the correctness of 2, φx/t is falsified by σ hence so is φx (since t is new to φ) by σ[x/σ(t)]. Since t does not occur in Y or C the same holds (p.255) for any t-variant σ′ which agrees with σ on all variables and parameters except perhaps t. Thus φx is falsified by every σ[x/α] for all α in the domain so that ∃xφx is falsified by σ. By the correctness of line 1, A ∊ X and is falsified by σ.

By the overlap clause (X ∩ Y) = Ø, these two options are exhaustive. □

Soundness for the conditional rules is complicated by the fact that we require them to be sound under two interpretations of the conditional. Firstly, the non-bivalent conditional where a conditional with true antecedent and untrue consequent, or false consequent and unfalse antecedent, takes the gap value. Secondly, the bivalent conditional in which, in those two cases, the conditional is false. However the soundness proofs for the strict neo-classical rules:

→I:

P

(1) Q

Given

(2) P → Q

1 → I

→E:

X

(1) P → Q

Given

Y

(2) P

Given

X, Y,

(3) Q

1,2 →E

where as usual X ∩ Y = Ø, goes through in essentially the same way in either case. The non-classical cases are the falsity-preservation clauses:

  1. (a) Falsity-preservation and truth preservation, →I: suppose P → Q is untrue in valuation v (in the bivalent case, it will be false). Then either P is true at v and Q untrue, or Q is false at v and P unfalse; both these possibilities contradict the neo-classical correctness of line 1, hence P → Q cannot be untrue at v.

  2. (b) Falsity preservation →E: suppose Q is false and all of X, Y, but A are true.

    1. Case (i): A ∉ X. Then, by the correctness of line (1) P → Q is true in v so that (on either interpretation) P is false. By the correctness of line (2) in the rule above, A ∊ Y and is false.

    2. Case (ii): A ∉ Y. By the correctness of line (2), P is true in v. Since Q is false, so too (on either interpretation) is P → Q. By the correctness of line (1), A ∊ X and is false in v. This exhausts the possibilities. ≤

The two other principles taken as primitive for the conditional3 are:

Contraposition:

X

(1) P → Q

Given

X

(2) ∼Q → ∼P

1, Contrap.

(p.256) Transitivity:

X

(1) P → Q

Given

Y

(2) Q → R

Given

X, Y,

(3) P → R

1,2 Trans. (where X ∩ Y = Ø.)

Soundness for contraposition is straightforward since the respective succeedents in each rule take the same value in every neo-classical model, on either interpretation. For transitivity, in the truth-preservation direction, suppose all of X, Y, are true in v. Then P → Q and Q → R are true. On either interpretation of →, if P is true in v, so is R, if P is gappy, Q is not false hence neither is R. Thus in either case, and also in the third case in which P is false in v, P → R is true (again on either interpretation of →).

For the falsity preservation direction, take the non-bivalent interpretation first of all. If P → R is false in v then P is true in v, R false. Suppose all of X, Y are true there but A. There are two cases:

Case (i): A ∉ X. Then, by the correctness of line (1) P → Q is true in v hence so is Q, so Q → R is false. By the correctness of line (2), A ∊ Y and is false.

Case (ii): A ∉ Y. By the correctness of line (2), Q → R is true in v, hence Q is false so by the correctness of line (1), A ∊ X and is false in v. This exhausts the possibilities.

Next the bivalent interpretation of →. If P → R is false in v then P is not false and R not true, nor do they have the same truth value in v. There are two cases:

  1. Case (i): A ∉ X. Then, by the correctness of line (1) P → Q is true in v. If P is true, Q is true but R is not hence Q → R is false in v. If P is gappy, Q is not false but R is hence once again, Q → R is false in v. Either way, by the correctness of line (2), A ∊ Y and is false.

  2. Case (ii): A ∉ Y. By the correctness of line (2), Q → R is true in v. Hence Q is not true. If Q is false then since P is not false, P → Q is false in v. If Q is gappy, R is gappy, hence P is true so once again P → Q is false. Either way, by the correctness of line (1), A ∊ X and is false in v. This exhausts the possibilities. □

§A.3 Infinitary Rules

The infinitary generalizations of &E and ∨I are obvious. For the other two rules they are ∧I:

Xα

(1.α) Aα

Given for all α 〈 β

α β X α

(2) ∧Aα α 〈 β

1.α α〈β ∧I

whilst ∨E is:

X

(1) ∨Aα α 〈 β

Given

Yα, Aα

(2.α) C

Given, α 〈 β

X , α β Y α

(3) C

1, 2.α, α 〈 β ∨E

(p.257) where X α β Y α = Ø .

The soundness steps in the soundness proof are straightforward generalizations of the finitary case. Thus for ∨E:

  1. (i) Truth preservation is exactly as in the classical case.

  2. (ii) Falsity preservation (upwards): suppose that C is false in v and all of X and all in α β Y α are true in v but P.

    1. Case (a): P X. Then, by the (strict) neo-classical correctness of line (1) (inductive hypothesis) ∨Aα α β is true in v hence one of the disjuncts is; suppose without loss of generality that it is Aγ. By the correctness of line (2.γ) in the rule above, P ∊ Yγ and is false.

    2. Case (b): P α β Y α . By the correctness of all of lines (2.α), α 〈 β, all of the Aα, α 〈 β are false in v hence so is ∨Aα α β. By the correctness of line (1), P ∊ X and is false in v.

      By the overlap clause X α β Y α = Ø , these two options are exhaustive. □

§A.4 IS

As set out in Chapter 8, §VI, with h a bijection from the θβ-sized set of singular terms of the language Lκ of IS onto Vθβ, we write ti for h(ti). To prove negation-completeness for the atoms of Lκ we prove something stronger: that every truth of the diagram of Vθβ, every atomic truth or falsehood concerning identity or membership, is provable.

Firstly, the positive truths. If ujti4 then uj occurs in a disjunct in the right hand side of the ith list comprehension axiom:

x ( x t i ( x = u j ) j J ) .

We then have ├ uj ∊ ti by strict neo-classical reasoning using ∀E (∧E), =I, ∨I and ↔E (i.e. &E and →E).5 Moreover since each set in Vθβ has only one name, the positive identity truths are all provable by =I, reflexivity of identity.

For the negative truths, we reason by induction on the rank of terms ti in uj ≠ ti and uj ∉ ti (where the rank of ti is just the rank of h(ti) in Vθβ). For rank zero, we have ├ ti ∉ t0, for all ti by a strict neo-classically legitimate reductio, using the empty set list axiom and =I.

Turning to identity, uj = t0 is false, for all uj distinct from the empty set, but in that case uj has at least one member tk so that tk features in the right-hand side of the ith (p.258) comprehension axiom and we thereby have ├ tk ∊ uj. Since ├ tk ∉ t0, identity laws and ∼I give us a neo-classical proof of uj ≠ t0.

For the inductive step of this part of the proof, we assume completeness for all identity and membership sentences for terms of rank 〈 α, α 〉 0, (each is provable if true in Vθβ); we have then to show (i) ├ uk ∉ tα and (ii) ├ uj ≠ tα, where uktα and ujtα, for terms uj and uk of rank 〈 α.

(i) Since uktα, uk is distinct from every ultα. By IH, ├ uk ≠ ul for every such tl, l ∊ L, L indexing the members of tα. Hence ├ uk ∉ tα by the following neo-classically correct proof (here the αth comprehension axiom is:

x ( x t α ( x = u l ) l L)) :

1

(1) uk ∊ tα

H

1

(2) ∨(uk = ul) l ∊ L

1 CE

3.l

(3.l) uk = ul

l ∊ L

(4.l) uk ≠ ul

Given l ∊ L

3.l

(5.l) ⊥

3.l, 4.l ∼E

1

(6) ⊥

2, 5.l l ∊ L, ∨E

(7) uk ∉ tα

6 ∼I.

(ii) If ujtα then they have different members. Suppose that tkuj but tktα. By what we have just established, ├ tk ∊ uj and ├ tk ∉ tα. A neo-classically reductio establishes ├ uj ≠ tα. If instead tkuj but tktα the argument is the same since uj is of rank 〈 α. Hence it follows by induction (using symmetry of = and the proof in (i) above for uj, tk jk) that every atomic sentence and every negation of an atomic sentence, whatever the ranks of the terms in the sentences, is provable when true.

The argument that all Vθβ truths are provable generalizes from the proof for atomic sentences by the same inductive argument as in Chapter 8, §VI.

§A.5 Prime Extensions

Start with a theory T which is satisfied by a neo-classical model M. Then it can be expanded to a prime theory T* also satisfied by M.

Proof: At initial stage ⟨ 0,0⟩ we set Δ⟨ 0,0⟩ = T. Well-order all the disjunctions in the language (so we require choice). At stage ⟨ 0,α + 1⟩ we consider the αth disjunction ∨Pi. If Δ⟨ 0,α⟩ ├ ∨Pi then (using choice again) select an arbitrary disjunct Pk such that Pk is true in M (an arbitrary sentence otherwise—but we will prove there is no otherwise) and let Δ⟨ 0,α + 1⟩ = Δ⟨ 0,α⟩, Pk. If it is not the case that Δ⟨ 0,α⟩ ├ ∨Pi then Δ ⟨ 0,α + 1⟩ = Δ⟨ 0,α⟩. At limit stages E9⟨ 0, λ⟩ Δ〈 0,λ〉 = β λ Δ 0 , β whilst Δ〈1,0〉 = β κ Δ 0 , β .

An inductive proof shows that at each stage α up to and including 〈 1,0〉 the associated set Δ〈 0,α〉 is satisfied by M and hence if Δ〈 0,α〉 ├ ∨Pi there always is at least one disjunct Pk such that Δ〈 0,α〉, Pk is true in M, since Δ〈 0,α〉 is satisfied by M.

(p.259) IH: We have by IH that Δ〈 0,α〉 is satisfied by M. If it is not the case that Δ〈 0,α〉 ├ ∨Pi (as before, this the αth disjunction) then Δ〈 0,α+1〉 = Δ〈 0,α〉 and so all its members are true in M. If Δ〈0,α〉 ├ ∨Pi then ∨Pi is true in M, hence at least one disjunct is true in M. Whichever true disjunct Pk is selected, Δ〈 0,α+1〉 = Δ〈 0,α〉, Pk is satisfied by M. At limit stages we have by IH that every member of Δ〈 0,λ〉 = β λ Δ 0 , β is true in M hence Δ〈 0,λ〉 is satisfied by M, likewise for Δ〈 1,0〉.

At stage 〈 1,0 〉 we proceed as before up to stage 〈 2,0 〉 and so on, with at stage 〈 μ, 0〉, Δ〈 μ,0〉 = η μ , β κ Δ η , β . Since our language is of a standard set-theoretic size κ, cardinality considerations show that we must reach a fixed point π such that Δ〈 π+1,0〉 = Δ〈 π,0〉. Call this theory Δ〈 π+1,0〉, which we have seen is also satisfied by M, T*. By dint of the construction, if T* ├ ∨Qi, ∨Qi any disjunction, then for some disjunct Qk, T* ├ Qk.

Note that if φ is gappy in M then, since T* is satisfied by M, we have neither T* ├ φ nor T* ├ ∼φ nor T* ├ (φ ∨ ∼φ) since T* is prime. As an example, take ZFCU and consider a classical model M (no gaps, so the positive and negative extensions for each predicate exhaust the domain) with a countable infinity of urelements so there is a bijection from the subdomain of urelements onto the natural numbers. Expand the language by adding individual constant 0, one one-place function term S, two two-place functions + and × and two one-place predicates N and C. Amend M to a neo-classical model M* by interpreting N and C classically (i.e. with its negative extension the complement of its positive extension) with the urelements as the positive extension of N and the sets as the positive extension of C. Assign Sn0 to the urelement assigned n and interpret + and × by plus and times (thus as fully defined functions) over the extension of N. Now we reinterpret identity. Its positive extension is to stay the same and for α, β both sets or both urelements, 〈α, β〉 is in the negative extension of = iff α ≠ β; otherwise, where one is a set and the other is an urelement, the pair is not in the negative extension.

We thus have to change the theory of identity. We can still have ∀x x = x as an axiom but we amend Leibniz' law to:

xy((Cx & Cy) → (φx & x = y) → φy)) ditto for the restriction to N.

We retain the axioms of ZFC but with all quantifiers restricted to C and add the first-order Peano–Dedekind axioms, all quantifiers restricted to N. The resultant theory, call it NS for numbers/sets, is clearly true in M*. By the previous result we can expand it to a prime theory NS* also satisfied by M*. Since cross-categorical identities such as SS0 = {{Ø}} (set brackets as abbreviations) are indeterminate in M* all of the following fail:

(p.260) NS* ├ SS0 = {{Ø}}; NS* ├ SS0 ≠ {{Ø}};

NS* ├ (SS0 = {{Ø}} ∨ SS0 ≠ {{Ø}})

If our theory T is expressed in a →-free sublanguage and is satisfied by neo-classical M, there must exist a classical model MC which satisfies T. This is generated by assigning arbitrarily either T or F to every atom in the language of T which is gappy in M. By the monotonicity of the →-free language, every sentence with a determinate value in M has the same value in MC. The above Henkin-style construction then generates from MC a theory T** which is prime and which proves every instance of LEM (since MC is classical) hence is negation-complete.

§A.6 Limitative Results in Infinitary Logics

There are pleasing completeness results for some infinitary languages, for example completeness results for standard infinitary propositional languages Lκ, κ inaccessible (Karp 1964, §5.5, pp. 51–3) and for (objectual) quantifier languages of the form Lκ,κ (again κ inaccessible—Karp 1964, p. 131)6 and also, a rather special case, LωI,ω0. Nevertheless, as remarked Chapter 8, §VII, limitative theorems such as Scott's Undefinability Theorems (Scott 1965; Karp 1964, ch. 14) hold for many other cardinals (e.g. successor cardinals κ+). Scott's theorem says that, for these languages, the set of all (codes) of logically true formulae of the language is indefinable in the language and this in turn (given that the length of proofs is bounded above by the index of the language) renders the systems incomplete.

One important point to make is that one necessary condition of application for Scott's results, the definability of the basic syntactic notions inside the object language itself, does not apply in our quasi-substitutional case, essentially generalized propositional logic. Although there is no inconsistency in the neo-formalist engaging in some model theory, for example assigning a domain of referents for each singular term in Lκ, note that every such domain of individuals must be of cardinality 〈 κ. For generalizations are infinitary regular conjunctions and disjunctions and each such is of length 〈 κ.

Since the cardinality of any such language, the number of its wffs, is ≥ κ (= κ, for κ inaccessible) this means that we cannot characterize the syntax of the language up to isomorphism by a theory expressible in the language: we cannot even quantify over all symbols or terms of the language. What this shows is that the neat generalization of first-order language to the vastly more expressive infinitary languages Lκ, κ (p.261) inaccessible, has come, in our case, at a lethal cost. We patently can describe the syntax of English in English (albeit our theories thereof are far from perfect) and construct self-referential ‘diagonalization’ attributions. Hence the languages Lκ fail to regiment crucial aspects of real language. The paradoxes are not even stateable. Again the moral I draw is the need to return to naïve set theory.

Notes:

(1) See Anderson and Belnap (1975, §29.5), especially the theorem ∼(A → A) → (B → B) together with theorem RM67 (p. 397) (A → A) ⇔ (∼A ∨ A).

(2) In the more liberal system in which we treat axioms as if they were part of the logic (see Chapter 8, §III), the overlap condition is amended to the requirement that only axioms feature in X ∩ (Y ∪ Z). Since axioms are true in the admissible models (by definition) we can still rule out the third case, in the falsity-preservation direction, that A ∊ X ∩ (Y ∪ Z). For then A is an axiom and so true, along with all the other premisses, contradicting downward truth-preservation, given the falsity of C. The same argument applies in the other cases.

(3) By complicating the → I rule to allow conditional sentences only in the antecedent of the premiss we can render the transitivity and contraposition rules redundant whilst preserving soundness.

(4) Here ‘∊’ is a term both of the object language and one of the informal metalanguage, with its usual meaning.

(5) I will annotate the derivability of one side of an instance of a comprehension axiom from the other by CE. It is assumed, as before, that the mathematical axioms are immune from the overlap restrictions.

(6) These results depend on extensions of distributivity principles (laws of dependent and independent choices) to govern the interaction between quantifiers and sentential operators.