The exponential rise in transgender self-identification invites consideration of what constitutes an ethical response to transgender individuals’ claims about how best to promote their well-being. In this paper, we argue that ‘accepting’ a claim to medical transitioning in order to promote well-being would be in the person’s best interests iff at the point of request the individual is correct in their self-diagnosis as transgender (i.e., the distress felt to reside in the body does not result from another psychological and/or societal (...) problem) such that the medical interventions they are seeking will help them to realise their preferences. If we cannot assume this—and we suggest that we have reasonable grounds to question an unqualified acceptance in some cases—then ‘acceptance’ potentially works against best interests. We propose a distinction between ‘acceptance’ and respectful, in-depth exploration of an individual’s claims about what promotes their well-being. We discuss the ethical relevance of the unconscious mind to considerations of autonomy and consent in working with transgender individuals. An inquisitive stance, we suggest, supports autonomous choice about how to realise an embodied form that sustains well-being by allowing the individual to consider both conscious and unconscious factors shaping wishes and values, hence choices. (shrink)

Notini et al 1 offer a timely addition in the wake of a significant increase in young people identifying as transgender and gender diverse. The authors focus specifically on the case of 18-year-old Phoenix’s request for ongoing puberty suppression to affirm a non-binary gender identity. A central issue raised by Phoenix’s predicament, and that I suggest we can extend to ethical consideration of requests for other types of medical intervention by binary and non-binary TGD individuals, is whether we should ‘affirm’ (...) the claims made by TGD young people about what promotes their well-being. As a clinician working with TGD young people who have undergone a range of medical interventions to align their bodies with their gender identity, my starting presumption is that it is important to respect what people think will help them: there are some TGD young people for whom, all things considered, medical interventions to affirm gender identity promote their well-being. Well-being has become an important conceptual currency in ethical debates and lies at the core of the authors’ analysis of Phoenix’s case. While the authors do not ground their argument in favour of OPS in a specific theory of well-being, welfarist considerations 2 appear to underpin …. (shrink)

Notini _et al_ 1 offer a timely addition in the wake of a significant increase in young people identifying as transgender and gender diverse. The authors focus specifically on the case of 18-year-old Phoenix’s request for ongoing puberty suppression to affirm a non-binary gender identity. A central issue raised by Phoenix’s predicament, and that I suggest we can extend to ethical consideration of requests for other types of medical intervention by binary and non-binary TGD individuals, is whether we should ‘affirm’ (...) the claims made by TGD young people about what promotes their well-being. As a clinician working with TGD young people who have undergone a range of medical interventions to align their bodies with their gender identity, my starting presumption is that it is important to respect what people think will help them: there are some TGD... (shrink)

In this paper we analyse in the framework of constructive mathematics (BISH) the validity of Farkas' lemma and related propositions, namely the Fredholm alternative for solvability of systems of linear equations, optimality criteria in linear programming, Stiemke's lemma and the Superhedging Duality from mathematical finance, and von Neumann's minimax theorem with application to constructive game theory.

Halin in 1965 proved that if a graph has [Formula: see text] many pairwise disjoint rays for each [Formula: see text] then it has infinitely many pairwise disjoint rays. We analyze the complexity of this and other similar results in terms of computable and proof theoretic complexity. The statement of Halin’s theorem and the construction proving it seem very much like standard versions of compactness arguments such as König’s Lemma. Those results, while not computable, are relatively simple. They only (...) use arithmetic procedures or, equivalently, finitely many iterations of the Turing jump. We show that several Halin-type theorems are much more complicated. They are among the theorems of hyperarithmetic analysis. Such theorems imply the ability to iterate the Turing jump along any computable well ordering. Several important logical principles in this class have been extensively studied beginning with work of Kreisel, H. Friedman, Steel and others in the 1960s and 1970s. Until now, only one purely mathematical example was known. Our work provides many more and so answers Question 30 of Montalbán’s Open Questions in Reverse Mathematics in 2011. Some of these theorems including ones in Halin in 1965 are also shown to have unusual proof theoretic strength as well. (shrink)

This is a short expository account of the regularity lemma for stable graphs proved by the authors, with some comments on the model theoretic context, written for a general logical audience.

Inflectional morphology has been taken as a paradigmatic example of rule-governed grammatical knowledge (Pinker, 1999). The plausibility of this claim may be related to the fact that it is mainly based on studies of English, which has a very simple inflectional system. We examined the representation of inflectional morphology in Serbian, which encodes number, gender, and case for nouns. Linguists standardly characterize this system as a complex set of rules, with disagreements about their exact form. We present analyses of a (...) large corpus of nouns which showed that, as in English, Serbian inflectional morphology is quasiregular: It exhibits numerous partial regularities creating neighborhoods that vary in size and consistency. We then asked whether a simple connectionist network could encode this statistical information in a manner that also supported generalization. A network trained on 3,244 Serbian nouns learned to produce correctly inflected phonological forms from a specification of a word's lemma, gender, number, and case, and generalized to untrained cases. The model's performance was sensitive to variables that also influence human performance, including surface and lemma frequency. It was also influenced by inflectional neighborhood size, a novel measure of the consistency of meaning to form mapping. A word-naming experiment with native Serbian speakers showed that this measure also affects human performance. The results suggest that, as in English, generating correctly inflected forms involves satisfying a small number of simultaneous probabilistic constraints relating form and meaning. Thus, common computational mechanisms may govern the representation and use of inflectional information across typologically diverse languages. (shrink)

An infinite binary sequence X is Kolmogorov–Loveland random if there is no computable non-monotonic betting strategy that succeeds on X in the sense of having an unbounded gain in the limit while betting successively on bits of X. A sequence X is KL-stochastic if there is no computable non-monotonic selection rule that selects from X an infinite, biased sequence.One of the major open problems in the field of effective randomness is whether Martin-Löf randomness is the same as KL-randomness. Our first (...) main result states that KL-random sequences are close to Martin-Löf random sequences in so far as every KL-random sequence has arbitrarily dense subsequences that are Martin-Löf random. A key lemma in the proof of this result is that for every effective split of a KL-random sequence at least one of the halves is Martin-Löf random. However, this splitting property does not characterize KL-randomness; we construct a sequence that is not even computably random such that every effective split yields two subsequences that are 2-random. Furthermore, we show for any KL-random sequence A that is computable in the halting problem that, first, for any effective split of A both halves are Martin-Löf random and, second, for any computable, nondecreasing, and unbounded function g and almost all n, the prefix of A of length n has prefix-free Kolmogorov complexity at least n−g. Again, the latter property does not characterize KL-randomness, even when restricted to left-r.e. sequences; we construct a left-r.e. sequence that has this property but is not KL-stochastic and, in fact, is not even Mises–Wald–Church stochastic.Turning our attention to KL-stochasticity, we construct a non-empty class of KL-stochastic sequences that are not weakly 1-random; by the usual basis theorems we obtain such sequences that in addition are left-r.e., are low, or are of hyperimmune-free degree.Our second main result asserts that every KL-stochastic sequence has effective dimension 1, or equivalently, a sequence cannot be KL-stochastic if it has infinitely many prefixes that can be compressed by a factor of α<1. This improves on a result by Muchnik, who has shown that were they to exist, such compressible prefixes could not be found effectively. (shrink)

We discuss automorphisms of saturated models of PA and boundedly saturated models of PA. We show that Smoryński's Lemma and Kaye's Theorem are not only true for countable recursively saturated models of PA but also true for all boundedly saturated models of PA with slight modifications.

Handbook of Mathematical Induction: Theory and Applications shows how to find and write proofs via mathematical induction. This comprehensive book covers the theory, the structure of the written proof, all standard exercises, and hundreds of application examples from nearly every area of mathematics. In the first part of the book, the author discusses different inductive techniques, including well-ordered sets, basic mathematical induction, strong induction, double induction, infinite descent, downward induction, and several variants. He then introduces ordinals and cardinals, transfinite induction, (...) the axiom of choice, Zorn’s lemma, empirical induction, and fallacies and induction. He also explains how to write inductive proofs. The next part contains more than 750 exercises that highlight the levels of difficulty of an inductive proof, the variety of inductive techniques available, and the scope of results provable by mathematical induction. Each self-contained chapter in this section includes the necessary definitions, theory, and notation and covers a range of theorems and problems, from fundamental to very specialized. The final part presents either solutions or hints to the exercises. Slightly longer than what is found in most texts, these solutions provide complete details for every step of the problem-solving process. (shrink)

Many times in mathematics there is a natural dichotomy betweendescribing some object from the inside and from the outside. Imaginealgebraic varieties for instance; they can be described from theoutside as solution sets of polynomial equations, but one can also tryto understand how it is for actual points to move around inside them,perhaps to parameterize them in some way. The concept of formalproofs has the interesting feature that it provides opportunities forboth perspectives. The inner perspective has been largely overlooked,but in fact (...) lengths of proofs lead to new ways to measure informationcontent of mathematical objects. The disparity between minimallengths of proofs with and without ``lemmas'' provides an indicationof internal symmetry of mathematical objects and their descriptions.A principal observation of this paper is that mathematicalstructures can be embedded into spaces of logical formulae and inheritadditional structure from proofs. We shall look at finitely-generatedgroups, rational numbers and SL(2,Z), and examples fromtopology and analysis. (shrink)

Levelt et al. describe a model of speech production in which lemma access is achieved via input from nondecompositional conceptual representations. They claim that existing decompositional theories are unable to account for lexical retrieval because of the so-called hyperonym problem. However, existing decompositional models have solved a formally equivalent problem.

Preparing words in speech production is normally a fast and accurate process. We generate them two or three per second in fluent conversation; and overtly naming a clear picture of an object can easily be initiated within 600 msec after picture onset. The underlying process, however, is exceedingly complex. The theory reviewed in this target article analyzes this process as staged and feedforward. After a first stage of conceptual preparation, word generation proceeds through lexical selection, morphological and phonological encoding, phonetic (...) encoding, and articulation itself. In addition, the speaker exerts some degree of output control, by monitoring of self-produced internal and overt speech. The core of the theory, ranging from lexical selection to the initiation of phonetic encoding, is captured in a computational model, called WEAVER++. Both the theory and the computational model have been developed in interaction with reaction time experiments, particularly in picture naming or related word production paradigms, with the aim of accounting for the real-time processing in normal word production. A comprehensive review of theory, model, and experiments is presented. The model can handle some of the main observations in the domain of speech errors (the major empirical domain for most other theories of lexical access), and the theory opens new ways of approaching the cerebral organization of speech production by way of high-temporal-resolution imaging. (shrink)

Ehrenfeucht’s lemma asserts that whenever one element of a model of Peano arithmetic is definable from another, they satisfy different types. We consider here the analogue of Ehrenfeucht’s lemma for models of set theory. The original argument applies directly to the ordinal-definable elements of any model of set theory, and, in particular, Ehrenfeucht’s lemma holds fully for models of set theory satisfying V=HOD. We show that the lemma fails in the forcing extension of the universe by (...) adding a Cohen real. We go on to formulate a scheme of natural parametric generalizations of Ehrenfeucht’s lemma, namely, the principles of the form EL, which asserts that P-definability from A implies Q-discernibility. We also consider various analogues of Ehrenfeucht’s lemma obtained by using algebraicity in place of definability, where a set b is algebraic in a if it is a member of a finite set definable from a. Ehrenfeucht’s lemma holds for the ordinal-algebraic sets, we prove, if and only if the ordinal-algebraic and ordinal-definable sets coincide. Using a similar analysis, we answer two open questions posed earlier by the third author and C. Leahy, showing that algebraicity and definability need not coincide in models of set theory and the internal and external notions of being ordinal algebraic need not coincide. (shrink)

We provide a fine‐grained analysis on the relation between König's lemma, weak König's lemma, and the decidable fan theorem in the context of constructive reverse mathematics. In particular, we show that double negated variants of König's lemma and weak König's lemma are equivalent to double negated variants of the general decidable fan theorem and the binary decidable fan theorem, respectively, over a nearly intuitionistic system containing a weak countable choice only. This implies that the general decidable (...) fan theorem is not equivalent to the binary decidable fan theorem in the absence of a strong countable choice. In addition, we introduce a principle which fills the gap between König's lemma and weak König's lemma, and show that König's lemma is equivalent to weak König's lemma plus this principle. We also solve several problems arising from the investigation. (shrink)

We analyze Zorn's Lemma and some of its consequences for Boolean algebras in a constructive setting. We show that Zorn's Lemma is persistent in the sense that, if it holds in the underlying set theory, in a properly stated form it continues to hold in all intuitionistic type theories of a certain natural kind. (Observe that the axiom of choice cannot be persistent in this sense since it implies the law of excluded middle.) We also establish the persistence (...) of some familiar results in the theory of (complete) Boolean algebras--notably, the proposition that every complete Boolean algebra is an absolute subretract. This (almost) resolves a question of Banaschewski and Bhutani as to whether the Sikorski extension theorem for Boolean algebras is persistent. (shrink)

We analyze Zorn's Lemma and some of its consequences for Boolean algebras in a constructive setting. We show that Zorn's Lemma is persistent in the sense that, if it holds in the underlying set theory, in a properly stated form it continues to hold in all intuitionistic type theories of a certain natural kind. We also establish the persistence of some familiar results in the theory of Boolean algebras--notably, the proposition that every complete Boolean algebra is an absolute (...) subretract. This resolves a question of Banaschewski and Bhutani as to whether the Sikorski extension theorem for Boolean algebras is persistent. (shrink)

We study the computational content of the Brouwer Fixed Point Theorem in the Weihrauch lattice. Connected choice is the operation that finds a point in a non-empty connected closed set given by negative information. One of our main results is that for any fixed dimension the Brouwer Fixed Point Theorem of that dimension is computably equivalent to connected choice of the Euclidean unit cube of the same dimension. Another main result is that connected choice is complete for dimension greater than (...) or equal to two in the sense that it is computably equivalent to Weak Kőnig’s Lemma. While we can present two independent proofs for dimension three and upward that are either based on a simple geometric construction or a combinatorial argument, the proof for dimension two is based on a more involved inverse limit construction. The connected choice operation in dimension one is known to be equivalent to the Intermediate Value Theorem; we prove that this problem is not idempotent in contrast to the case of dimension two and upward. We also prove that Lipschitz continuity with Lipschitz constants strictly larger than one does not simplify finding fixed points. Finally, we prove that finding a connectedness component of a closed subset of the Euclidean unit cube of any dimension greater than or equal to one is equivalent to Weak Kőnig’s Lemma. In order to describe these results, we introduce a representation of closed subsets of the unit cube by trees of rational complexes. (shrink)

We explore the connections between Dickson’s lemma and weak Ramsey theory. We show that a weak version of the Paris–Harrington principle for pairs in c colors and miniaturized Dickson’s lemma for c-tuples are equivalent over \. Furthermore, we look at a cascade of consequences for several variants of weak Ramsey’s theorem.

The commentaries provide a multitude of perspectives on the theory of lexical access presented in our target article. We respond, on the one hand, to criticisms that concern the embeddings of our model in the larger theoretical frameworks of human performance and of a speaker's multiword sentence and discourse generation. These embeddings, we argue, are either already there or naturally forgeable. On the other hand, we reply to a host of theory-internal issues concerning the abstract properties of our feedforward spreading (...) activation model, which functions without the usual cascading, feedback, and inhibitory connections. These issues also concern the concrete stratification in terms of lexical concepts, syntactic lemmas, and morphophonology. Our response stresses the parsimony of our modeling in the light of its substantial empirical coverage. We elaborate its usefulness for neuroimaging and aphasiology and suggest further cross-linguistic extensions of the model. (shrink)

Bishop's Lemma is a centrepiece in the development of constructive analysis. We show that its proof requires some form of the axiom of choice; and that the completeness requirement in Bishop's Lemma can be weakened and that there is a vast class of non‐complete spaces that Bishop's Lemma applies to.

Classically, weak König's lemma and Brouwer's fan theorem for detachable bars are equivalent. We give a direct constructive proof that the former implies the latter.

How can one conceive of the neuronal implementation of the processing model we proposed in our target article? In his commentary (Pulvermüller 1999, reprinted here in this issue), Pulvermüller makes various proposals concerning the underlying neural mechanisms and their potential localizations in the brain. These proposals demonstrate the compatibility of our processing model and current neuroscience. We add further evidence on details of localization based on a recent meta-analysis of neuroimaging studies of word production (Indefrey & Levelt 2000). We also (...) express some minor disagreements with respect to Pulvermüller's interpretation of the “lemma” notion, and concerning his neural modeling of phonological code retrieval. Branigan & Pickering discuss important aspects of syntactic encoding, which was not the topic of the target article. We discuss their well-taken proposal that multiple syntactic frames for a single verb lemma are represented as independent nodes, which can be shared with other verbs, such as accounting for syntactic priming in speech production. We also discuss how, in principle, the alternative multiple-frame-multiple-lemma account can be tested empirically. The available evidence does not seem to support that account. Footnotes1 BBS Note: The original manuscript of this Response article was received on January 14, 2000. (shrink)

We refine the constructions of Ferrante-Rackoff and Solovay on iterated definitions in first-order logic and their expressibility with polynomial size formulas. These constructions introduce additional quantifiers; however, we show that these extra quantifiers range over only finite sets and can be eliminated. We prove optimal upper and lower bounds on the quantifier complexity of polynomial size formulas obtained from the iterated definitions. In the quantifier-free case and in the case of purely existential or universal quantifiers, we show that Ω quantifiers (...) are necessary and sufficient. The last lower bounds are obtained with the aid of the Yao-Håstad switching lemma. (shrink)

q-derivatives are part of so called quantum calculus. In this paper we investigate how such derivatives can possibly be used in Itô’s lemma. This leads us to consider how such derivatives can be used in a social science setting. We conclude that in a Itô Lemma setting we cannot use a macroscopic version of the Heisenberg uncertainty principle with q-derivatives.

The deductive strengths of three variations of Rado's selection lemma are studied in set theory without the axiom of choice. Two are shown to be equivalent to Rado's lemma and the third to the Boolean prime ideal theorem. MSC: 03E25, 04A25, 06E05.

I derive a Gleason-type contradiction from assumptions weaker than those needed to reach a Bell inequality. By establishing the inconsistency between local realism and QM's perfect EPR-type anticorrelations, the proof fills in a gap left open by Bell arguments.

We show how to interpret weak Kőnig's lemma in some recently defined theories of nonstandard arithmetic in all finite types. Two types of interpretations are described, with very different verifications. The celebrated conservation result of Friedman's about weak Kőnig's lemma can be proved using these interpretations. We also address some issues concerning the collecting of witnesses in herbrandized functional interpretations.

A general algorithm is given for determining whether or not a given set of pair distributions allows for the construction of all the members of a specified set of higher-order distributions which return the given pair distributions as marginals. This mathematical question underlies studies of quantum correlation experiments such as those of Bell or of Clauser and Horne, or their higher-spin generalizations. The algorithm permits the analysis of rather intricate versions of such problems, in a form readily adaptable to the (...) computer. The general procedure is illustrated by simple derivations of the results of Mermin and Schwarz for the symmetric spin-1 and spin-3/2 Einstein-Podolsky-Rosen problems. It is also used to extend those results to the spin-2 and spin-5/2 cases, providing further evidence that the range of strange quantum theoretic correlations does not diminish with increasing s. The algorithm is also illustrated by giving an alternative derivation of some recent results on the necessity and sufficiency of the Clauser-Horne conditions. The mathematical formulation of the algorithm is given in general terms without specific reference to the quantum theoretic applications. (shrink)

The so-called weak König's lemma WKL asserts the existence of an infinite path b in any infinite binary tree . Based on this principle one can formulate subsystems of higher-order arithmetic which allow to carry out very substantial parts of classical mathematics but are Π 2 0 -conservative over primitive recursive arithmetic PRA . In Kohlenbach 1239–1273) we established such conservation results relative to finite type extensions PRA ω of PRA . In this setting one can consider also a (...) uniform version UWKL of WKL which asserts the existence of a functional Φ which selects uniformly in a given infinite binary tree f an infinite path Φf of that tree. This uniform version of WKL is of interest in the context of explicit mathematics as developed by S. Feferman. The elimination process in Kohlenbach [10] actually can be used to eliminate even this uniform weak König's lemma provided that PRA ω only has a quantifier-free rule of extensionality QF-ER instead of the full axioms of extensionality for all finite types. In this paper we show that in the presence of , UWKL is much stronger than WKL: whereas WKL remains to be Π 2 0 -conservative over PRA, PRA ω ++ UWKL contains full Peano arithmetic PA. We also investigate the proof–theoretic as well as the computational strength of UWKL relative to the intuitionistic variant of PRA ω both with and without the Markov principle. (shrink)

J. S. Bell's classic 1966 review paper on the foundations of quantum mechanics led directly to the Bell nonlocality theorem. It is not widely appreciated that the review paper contained the basic ingredients needed for a nonlocality result which holds in certain situations where the Bell inequality is not violated. We present in this paper a systematic formulation and evaluation of an argument due to Stairs in 1983, which establishes a nonlocality result based on the Bell-Kochen-Specker “paradox” in quantum mechanics.

Rauszer and Sabalski proved in [2] that distributivity with respect to infi- nite joins and meets is a sucient and necessary condition making the RasiowaSikorski Lemma valid in distributive lattices. The main part of their proof is a direct construction of a required filter under distributivity. In this note we show that a generalization of the result can be obtained from the Rasiowa-Sikorski Lemma for Boolean algebras by using Gornemann’s result in [1] instead of a direct con- ¨ (...) struction. Suppose A is a distributive lattice and Q; R 2 A f;g. We call A complete if 8M 2 Q9 M 2 A and 8N 2 R9 F N 2 A. M 2 Q is -dis if 9 M 2 A and 8a 2 A a t M = m2M. N 2 R is F -dis if 9 F N 2 A and 8a 2 A a u F N = F n2N. is called distributive if every M 2 Q is -dis and every N 2 R is F -dis. Suppose A is complete and C; D A. By rC we mean the filter in A generated by C, in particular, let r; = ; = ;. is called complete if and , where 8M 2 Q 9m 2 MrC \ D[fmg = ;) 8N 2 R 9n 2 NrC[fng \ D = ;). (shrink)

We continue the work of [14, 3, 1, 19, 16, 4, 12, 11, 20] investigating the strength of set existence axioms needed for separable Banach space theory. We show that the separation theorem for open convex sets is equivalent to WKL 0 over RCA 0 . We show that the separation theorem for separably closed convex sets is equivalent to ACA 0 over RCA 0 . Our strategy for proving these geometrical Hahn-Banach theorems is to reduce to the finite-dimensional case (...) by means of a compactness argument. (shrink)

We develop measure theory in the context of subsystems of second order arithmetic with restricted induction. We introduce a combinatorial principleWWKL (weak-weak König's lemma) and prove that it is strictly weaker thanWKL (weak König's lemma). We show thatWWKL is equivalent to a formal version of the statement that Lebesgue measure is countably additive on open sets. We also show thatWWKL is equivalent to a formal version of the statement that any Borel measure on a compact metric space is (...) countably additive on open sets. (shrink)

We continue the work of [14, 3, 1, 19, 16, 4, 12, 11, 20] investigating the strength of set existence axioms needed for separable Banach space theory. We show that the separation theorem for open convex sets is equivalent to WKL$_0$ over RCA$_0$. We show that the separation theorem for separably closed convex sets is equivalent to ACA$_0$ over RCA$_0$. Our strategy for proving these geometrical Hahn-Banach theorems is to reduce to the finite-dimensional case by means of a compactness argument.

In this paper, we propose a weak regularity principle which is similar to both weak König's lemma and Ramsey's theorem. We begin by studying the computational strength of this principle in the context of reverse mathematics. We then analyze different ways of generalizing this principle.

This paper is dedicated to Prof. Dr. Günter Asser, whose work in founding this journal and maintaining it over many difficult years has been a major contribution to the activities of the mathematical logic community.At first sight it appears highly unlikely that Urysohn's Lemma has any significant constructive content. However, working in the context of an apartness space and using functions whose values are a generalisation of the reals, rather than real numbers, enables us to produce a significant constructive (...) version of that lemma. (shrink)

By , we denote the system of second-order arithmetic based on recursive comprehension axioms and Σ10 induction. is defined to be plus weak König's lemma: every infinite tree of sequences of 0's and 1's has an infinite path. In this paper, we first show that for any countable model M of , there exists a countable model M′ of whose first-order part is the same as that of M, and whose second-order part consists of the M-recursive sets and sets (...) not in the second-order part of M. By combining this fact with a certain forcing argument over universal trees, we obtain the following result : if proves X!Y with arithmetical, so does . We also discuss several improvements of this results. (shrink)

We introduce a herbrandized functional interpretation of a first-order semi-intuitionistic extension of Heyting Arithmetic and study its main properties. We then extend the interpretation to a certain system of second-order arithmetic which includes a (classically false) formulation of the FAN principle and weak König's lemma. It is shown that any first-order formula provable in this system is classically true. It is perhaps worthy of note that, in our interpretation, second-order variables are interpreted by finite sets of natural numbers.

We consider the relation between versions of Ramsey’s Theorem and König’s Infinity Lemma, in the absence of the axiom of choice.