BRICS RS-99-20 U. Kohlenbach: A Note on Spector’s Quantifier-Free Rule of Extensionality BRICS

Basic Research in Computer Science

A Note on Spector’s Quantifier-Free Rule of Extensionality

Ulrich Kohlenbach BRICS Report Series RS-99-20 ISSN 0909-0878 August 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Ulrich Kohlenbach.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/99/20/

A note on Spector’s quantifier-free rule of extensionality

Ulrich Kohlenbach

BRICS^{∗}

Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C Denmark

March 1999

Abstract

In this note we show that the so-called weakly extensional arithmetic in all finite types, which is based on a quantifier-free rule of extensionality due to C. Spector and which is of significance in the context of Gödel’s functional interpretation, does not satisfy the deduction theorem for additional axioms. This holds already for Π_{1}^{0}- axioms. Previously, only the failure of the stronger deduction theorem for deductions from (possibly open) assumptions (with parameters kept fixed) was known.

∗Basic Research in Computer Science, Centre of the Danish National Research Foundation.

1 Introduction

Let E-HA^{ω} denote the system of extensional intuitionistic arithmetic in all finite types as defined in [5]. Concerning equality, E-HA^{ω} only contains equality =_{0} between numbers as a primitive predicate. For ρ = 0ρ_{k} … ρ_{1}, x_{1} =_{ρ} x_{2} is defined as ∀y_{1}^{ρ_{1}}, …, y_{k}^{ρ_{k}}(x_{1}y_{1} … y_{k} =_{0} x_{2}y_{1} … y_{k}). In the context of Gödel’s functional (‘Dialectica’) interpretation, a variant WE-HA^{ω} (weakly extensional intuitionistic arithmetic in all finite types) of E-HA^{ω} is of relevance which instead of the extensionality axioms (E) for all types only has the following quantifier-free rule of extensionality

QF-ER: \frac{A_{0} → s =_{ρ} t}{A_{0} → r[s] =_{τ} r[t]},

where A_{0} is quantifier-free, s^{ρ}, t^{ρ}, r[x^{ρ}]^{τ} are arbitrary terms of the system and ρ, τ ∈ are arbitrary types. WE-PA^{ω} denotes the variant of WE-HA^{ω} with classical logic. In contrast to (E), Gödel’s functional interpretation trivially satisfies QF-ER which was introduced in [4] for that very reason. It has been observed in the literature ([5](3.5.15 and 1.6.12), see also [6] for corrections) that WE-HA^{ω} doesn’t satisfy the deduction theorem for ‘deductions from open assumptions’ (whose free variables are treated as parameters and hence are not permitted as proper variables in the quantifier rules as formulated in [5]).^{1} The argument proceeds as follows: consider

f =_{1} g ⊢WE-HA^{ω} f =_{1} g,

where f, g are free function variables. QF-ER yields

f =_{1} g ⊢WE-HA^{ω} ∀z^{2}(zf =_{0} zg).

1In order to avoid this consequence, Troelstra uses a weaker form of QF-ER where the premise of the rule is required to be derivable without assumptions. In this paper we deal with Spector’s original rule and our definition of WE-HA^{ω} thereby differs from Troelstra’s definition in [5]. The deduction theorem for deductions from assumption, however, does hold – under an appropriate variable condition – for the quantifier-free fragment qf-WE-HA^{ω} of WE-HA^{ω} (see [1]).

The deduction theorem for derivations under assumptions would yield

⊢WE-HA^{ω} f =_{1} g → ∀z^{2}(zf =_{0} zg),

which is underivable in WE-HA^{ω} as follows from [2] and the fact that WE-HA^{ω} has a functional interpretation in (the weakly extensional version of) Gödel’s T. This, however, leaves it open whether the deduction theorem also fails for assumptions added as axioms, i.e. assumptions which implicitly are understood as universally closed. In this note we show that the deduction theorem (both for WE-HA^{ω} as well as for WE-PA^{ω}) already fails for Π_{1}^{0}-axioms.

2 Results

Theorem 2.1 There exists a Π_{1}^{0}-sentence A and a quantifier-free formula B such that

WE-HA^{ω} + A ⊢ B, but WE-PA^{ω} ⊢ / A → B.

Proof: Let Con_{PA} the standard consistency predicate for Peano arithmetic PA. In WE-HA^{ω}, Con_{PA} can be written as A :≡ ∀x^{0}(t_{PA}x =_{0} 0) for a suitable closed term t_{PA} of WE-HA^{ω}.

WE-HA^{ω} + A ⊢ t_{PA} =_{1} 0^{1},

where 0^{1} := λx^{0}.0^{0}. By QF-ER we obtain

WE-HA^{ω} + A ⊢ x^{2}(t_{PA}) =_{0} x(0^{1}),

where x^{2} is a free variable of type 2. Let’s assume now that

(∗) WE-HA^{ω} ⊢ A → x^{2}(t_{PA}) =_{0} x(0^{1}).

Then a fortiori

WE-HA^{ω} ⊢ A → ∀x ≤_{2} 1^{2}(x(t_{PA}) =_{0} x(0^{1}))

and hence

WE-PA^{ω} ⊢ ∀x ≤_{2} 1^{2}∃y^{0}(t_{PA}y =_{0} 0 → x(t_{PA}) =_{0} x(0^{1})),

where 1^{2} := λx^{1}.S0 and x_{1} ≤_{2} x_{2} :≡ ∀y^{1}(x_{1}y ≤_{0} x_{2}y). By corollary 3.4 from [3] there exists a closed term s^{0} of WE-HA^{ω} such that

WE-HA^{ω} ⊢ ∀y ≤_{0} s(t_{PA}y =_{0} 0) → ∀x ≤_{2} 1(x(t_{PA}) =_{0} x(0^{1})).

By the computability of every fixed closed term s in WE-HA^{ω}, there exists a number n ∈ IN such that

WE-HA^{ω} ⊢ s =_{0} \overline{n}.

Since (by Σ_{1}^{0}-completeness of WE-HA^{ω})

WE-HA^{ω} ⊢ ∀y ≤_{0} \overline{n}(t_{PA}y =_{0} 0),

we get

WE-HA^{ω} ⊢ ∀x ≤_{2} 1^{2}(x(t_{PA}) =_{0} x(0^{1}))

and therefore

WE-HA^{ω} ⊢ t_{PA} =_{1} 0, i.e.
WE-HA^{ω} ⊢ Con_{PA},

which contradicts Gödel’s second incompleteness theorem, since WE-HA^{ω} is conservative over Heyting arithmetic HA (as follows by formalizing the model HEO of all hereditarily effective operations in HA, see [5]). Hence (∗) above is false. So the theorem holds with B :≡ (x^{2}(t_{PA}) =_{0} x(0)) and A as above.

Corollary 2.2 The deduction theorem for both WE-PA^{ω} and WE-HA^{ω} fails already for closed Π_{1}^{0}-axioms.

Remark 2.3 The argument above can be applied also to stronger systems which allow a functional interpretation by majorizable functionals. Then we have to use a consistency predicate for a sufficiently strong system.

Final Comments: The failure of the deduction theorem for WE-PA^{ω} (already for Π_{1}^{0}-axioms) might suggest that a system like Troelstra’s [5] PA^{ω} (=(HA^{ω})^{c}) which is neutral with respect to extensionality but still only contains equality for numbers as a primitive predicate, would be more favorable in the context of functional interpretation. However, we believe that for applications to mathematics and the extraction of data from given proofs it is desirable to have as much extensionality avalaible as possible. If we work in WE-PA^{ω} +A and want to shift A to an implicative premise of the conclusion, then we can do this provided that we restrict + to ⊕ where WE-PA^{ω} ⊕ A means that A must not be used in the proof of the premise of an application of QF-ER. This is a less severe restriction than to work in PA^{ω} + A.

References

[1] Bezem, M., Equivalence of bar recursors in the theory of functionals of finite type. Arch. Math. Logic 27, pp. 149–160 (1988).

[2] Howard, W.A., Hereditarily majorizable functionals of finite type. In: Troelstra (ed.), Metamathematical investigation of intuitionistic arithmetic and analysis, pp. 454-461. Springer LNM 344 (1973).

[3] Kohlenbach, U., Pointwise hereditary majorization and some applications. Arch. Math. Logic 31, pp. 227-241 (1992).

[4] Spector, C., Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. In: Recursive function theory, Proceedings of Symposia in Pure Mathematics, vol. 5 (J.C.E. Dekker (ed.)), AMS, Providence, R.I., pp. 1–27 (1962).

[5] Troelstra, A.S. (ed.) Metamathematical investigation of intuitionistic arithmetic and analysis. Springer Lecture Notes in Mathematics 344 (1973).

[6] Troelstra, A.S., Metamathematical investigation of intuitionistic arithmetic and analysis. Corrections to the first edition. ILLC Prepublication Series X-93-04, Universiteit van Amsterdam (1993).

Recent BRICS Report Series Publications

RS-99-20 Ulrich Kohlenbach. A Note on Spector’s Quantifier-Free Rule of Extensionality. August 1999. 5 pp. To appear in Archive for Mathematical Logic.

RS-99-19 Marcin Jurdziński and Mogens Nielsen. Hereditary History Preserving Bisimilarity is Undecidable. June 1999. 18 pp.

RS-99-18 M. Oliver Möller and Harald Rueß. Solving Bit-Vector Equations of Fixed and Non-Fixed Size. June 1999. 18 pp. Revised version of an article appearing under the title Solving Bit-Vector Equations in Gopalakrishnan and Windley, editors, Formal Methods in Computer-Aided Design: Second International Conference, FMCAD ’98 Proceedings, LNCS 1522, 1998, pages 36–48.

RS-99-17 Andrzej Filinski. A Semantic Account of Type-Directed Partial Evaluation. June 1999. To appear in Nadathur, editor, International Conference on Principles and Practice of Declarative Programming, PPDP99 ’99 Proceedings, LNCS, 1999.

RS-99-16 Rune B. Lyngsø and Christian N. S. Pedersen. Protein Folding in the 2D HP Model. June 1999. 15 pp.

RS-99-15 Rune B. Lyngsø, Michael Zuker, and Christian N. S. Pedersen. An Improved Algorithm for RNA Secondary Structure Prediction. May 1999. 24 pp. An alloy of two articles appearing in Istrail, Pevzner and Waterman, editors, Third Annual International Conference on Computational Molecular Biology, RE-COMB 99 Proceedings, 1999, pages 260–267, and Bioinformatics, 15, 1999.

RS-99-14 Marcelo P. Fiore, Gian Luca Cattani, and Glynn Winskel. Weak Bisimulation and Open Maps. May 1999. To appear in Longo, editor, Fourteenth Annual IEEE Symposium on Logic in Computer Science, LICS ’99 Proceedings, 1999.

RS-99-13 Rasmus Pagh. Hash and Displace: Efficient Evaluation of Minimal Perfect Hash Functions. May 1999. 11 pp. A short version to appear in Algorithms and Data Structures: 6th International Workshop, WADS ’99 Proceedings, LNCS, 1999.