We give some lectures on the work on formal logic of Jacques Herbrand, and sketch his life and his influence on automated theorem proving. The intended audience ranges from students interested in logic over historians to logicians. Besides the well-known correction of Herbrand’s False Lemma by Goedel and Dreben, we also present the hardly known unpublished correction of Heijenoort and its consequences on Herbrand’s Modus Ponens Elimination. Besides Herbrand’s Fundamental Theorem and its relation to the Loewenheim-Skolem-Theorem, (...) we carefully investigate Herbrand’s notion of intuitionism in connection with his notion of falsehood in an infinite domain. We sketch Herbrand’s two proofs of the consistency of arithmetic and his notion of a recursive function, and last but not least, present the correct original text of his unification algorithm with a new translation. (shrink)

Realizability notions in mathematical logic have a long history, which can be traced back to the work of Stephen Kleene in the 1940s, aimed at exploring the foundations of intuitionistic logic. Kleene’s initial realizability laid the ground for more sophisticated notions such as Kreisel’s modified realizability and various modern approaches. In this context, our work aligns with the lineage of realizability strategies that emphasize the accumulation, rather than the propagation of precise witnesses. In this paper, we introduce a new notion (...) of realizability, namely herbrandized modified realizability. This novel form of (cumulative) realizability, presented within the framework of semi-intuitionistic logic is based on a recently developed star combinatory calculus, which enables the gathering of witnesses into nonempty finite sets. We also show that the previous analysis can be extended from logic to (Heyting) arithmetic. (shrink)

Let S be a deductive system such that S-derivability (⊦s) is arithmetic and sound with respect to structures of class K. From simple conditions on K and ⊦s, it follows constructively that the K-completeness of ⊦s implies MP(S), a form of Markov's Principle. If ⊦s is undecidable then MP(S) is independent of first-order Heyting arithmetic. Also, if ⊦s is undecidable and the S proof relation is decidable, then MP(S) is independent of second-order Heyting arithmetic, HAS. Lastly, when ⊦s is many-one (...) complete, MP(S) implies the usual Markov's Principle MP. An immediate corollary is that the Tarski, Beth and Kripke weak completeness theorems for the negative fragment of intuitionistic predicate logic are unobtainable in HAS. Second, each of these: weak completeness for classical predicate logic, weak completeness for the negative fragment of intuitionistic predicate logic and strong completeness for sentential logic implies MP. Beth and Kripke completeness for intuitionistic predicate or sentential logic also entail MP. These results give extensions of the theorem of Gödel and Kreisel (in [4]) that completeness for pure intuitionistic predicate logic requires MP. The assumptions of Godel and Kreisel's original proof included the Axiom of Dependent Choice and Herbrand's Theorem, no use of which is explicit in the present article. (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 perform a proof-theoretical investigation of two modal predicate logics: global intuitionistic logic GI and global intuitionistic fuzzy logic GIF. These logics were introduced by Takeuti and Titani to formulate an intuitionistic set theory and an intuitionistic fuzzy set theory together with their metatheories. Here we define analytic Gentzen style calculi for GI and GIF. Among other things, these calculi allows one to prove Herbrand’s theorem for suitable fragments of GI and GIF.

Two themes are developed here: one, general, enters into the analysis of the notion of object, the other, more specific but also complex, takes up the rehabilitation of Hilbert’s Program, thus paying tribute to the great work of Mic Detlefsen. He shows how the destruction of this program by Gödel’s theorem is a delusion, despite the greatness and the importance of Gödel’s work in the History of Logic. The refocusing of Hilbert’s work then opens up perspectives on the analysis of (...) the notion of object and on the idea of effectiveness to which mathematical practice invites us. (shrink)

Any intermediate propositional logic can be extended to a calculus with epsilon- and tau-operators and critical formulas. For classical logic, this results in Hilbert’s $\varepsilon $ -calculus. The first and second $\varepsilon $ -theorems for classical logic establish conservativity of the $\varepsilon $ -calculus over its classical base logic. It is well known that the second $\varepsilon $ -theorem fails for the intuitionistic $\varepsilon $ -calculus, as prenexation is impossible. The paper investigates the effect of adding critical $\varepsilon $ - (...) and $\tau $ -formulas and using the translation of quantifiers into $\varepsilon $ - and $\tau $ -terms to intermediate logics. It is shown that conservativity over the propositional base logic also holds for such intermediate ${\varepsilon \tau }$ -calculi. The “extended” first $\varepsilon $ -theorem holds if the base logic is finite-valued Gödel–Dummett logic, and fails otherwise, but holds for certain provable formulas in infinite-valued Gödel logic. The second $\varepsilon $ -theorem also holds for finite-valued first-order Gödel logics. The methods used to prove the extended first $\varepsilon $ -theorem for infinite-valued Gödel logic suggest applications to theories of arithmetic. (shrink)

Gentzen’s sequent calculi LK and LJ are landmark proof systems. They identify the structural rules of weakening and contraction as notable inference rules, and they allow for an elegant statement and proof of both cut elimination and consistency for classical and intuitionistic logics. Among the undesirable features of those sequent calculi is that their inferences rules are low-level and frequently permute over each other. As a result, large-scale structures within sequent calculus proofs are hard to identify. In this paper, we (...) present a different approach to designing a sequent calculus for classical logic. Starting with Gentzen’s LK proof system, we examine the proof search meaning of his inference rules and classify those rules as involving either don’t care nondeterminism or don’t know nondeterminism. Based on that classification, we design the focused proof system LKF in which inference rules belong to one of two phases of proof construction depending on which flavor of nondeterminism they involve. We then prove that the cut rule and the general form of the initial rule are admissible in LKF. Finally, by showing that the inference rules for LK are all admissible in LKF, we can give a relative completeness proof for LKF provability with respect to LK provability. We shall also apply these properties of the LKF proof system to establish other meta-theoretic properties of classical logic, including Herbrand’s theorem. (shrink)

ellucci, C., Existential instantiation and normalization in sequent natural deduction, Annals of Pure and Applied Logic 58 111–148. A sequent conclusion natural deduction system is introduced in which classical logic is treated per se, not as a special case of intuitionistic logic. The system includes an existential instantiation rule and involves restrictions on the discharge rules. Contrary to the standard formula conclusion natural deduction systems for classical logic, its normal derivations satisfy both the subformula property and the separation property and (...) allow to establish a version of the midsequent theorem and Herbrand's theorem. (shrink)

This technical and sophisticated book has a misleading title. In only 140 pages it has chapters entitled: Truth Functions, Sentence Logic, Model Theory, Predicate Logic, Recursive Functions, Formalized Arithmetic, Free-Variable Arithmetic, and Axiomatic Set Theory. Goodstein says little about, let alone studies, the historical development of any of these topics. The history consists of a few references to some of the individuals who have played a role in the development of the field; but not always to the major figures. For (...) instance, his chapter on model theory contains no discussion of the development of classical model theory. Only Herbrand is noted as a developer of model theory. However, even if these eight studies in mathematical logic do not tell much about the development of the topics, they still have considerable value. The first chapter on truth functions and the seventh on free-variable arithmetic are the most intriguing because they contain more of what is not usually presented in logic books. The first two chapters on sentential logic are not the standard textbook treatment. This really is a book for other working logicians and mathematicians. Quickly, Goodstein moves into treating truth functions for any number of truth values as functions in modulo arithmetic and investigates the topic of finding Sheffer functions, viz., a function from which all others for a given number of truth values can be obtained. In the second chapter, he is soon presenting Intuitionistic sentential logic and has some remarks about sentential logics between Intuitionistic logic and classical logic. He also presents sequent calculi. Since the first two chapters contain only 36 pages, this suggests that the book would be suitable as a text only for advanced and sophisticated students. (shrink)

In 1957, Gödel proved that completeness for intuitionistic predicate logic HPL implies forms of Markov's Principle, MP. The result first appeared, with Kreisel's refinements and elaborations, in Kreisel. Featuring large in the Gödel-Kreisel proofs are applications of the axiom of dependent choice, DC. Also in play is a form of Herbrand's Theorem, one allowing a reduction of HPL derivations for negated prenex formulae to derivations of negations of conjunctions of suitable instances. First, we here show how to deduce Gödel's (...) results by alternative means, ones arguably more elementary than those of Kreisel. We avoid DC and Herbrand's Theorem by marshalling simple facts about negative translations and Markov's Rule. Second, the theorems of Gödel and Kreisel are commonly interpreted as demonstrating the unprovability of completeness for HPL, if means of proof are confined within strictly intuitionistic metamathematics. In the closing section, we assay some doubts about such interpretations. (shrink)

In this paper a method for the replacement, in formulas, of strong quantifiers by functions is introduced that can be considered as an alternative to Skolemization in the setting of constructive theories. A constructive extension of intuitionistic predicate logic that captures the notions of preorder and existence is introduced and the method, orderization, is shown to be sound and complete with respect to this logic. This implies an analogue of Herbrand's theorem for intuitionistic logic. The orderization method is applied (...) to the constructive theories of equality and groups. (shrink)

This paper is a sequel to the papers Baaz and Iemhoff [4] and [6] in which an alternative skolemization method called eskolemization was introduced that, when restricted to strong existential quantifiers, is sound and complete for constructive theories. In this paper we extend the method to universal quantifiers and show that for theories satisfying the witness property it is sound and complete for all formulas. We obtain a Herbrand theorem from this, and apply the method to the intuitionistic theory (...) of equality and the intuitionistic theory of monadic predicates. (shrink)

A translation of the Écrits logiques, edited by Jean Van Heijenoort, published in 1968.

In February 2015 the UK became the first country to legalise high-profile mitochondrial replacement techniques, which involve the creation of offspring using genetic material from three individuals. The aim of these new cell reconstruction techniques is to prevent the transmission of maternally inherited mitochondrial disorders to biological offspring. During the UK debates, MRTs were often positioned as a straightforward and unique solution for the ‘eradication’ of mitochondrial disorders, enabling hundreds of women to have a healthy, biologically-related child. However, many questions (...) regarding future applications and potential users remain. Drawing on a current qualitative study on reproductive choices in the context of mitochondrial disorders, this article illustrates how the potential limitations of MRTs have been obscured in public debates by contrasting the claims made about the future beneficiaries with insights from families affected by mitochondrial disorders and medical experts. The analysis illuminates the complex choices with which families and individuals affected by mitochondrial disorders are faced, which have thus far remained invisible. An argument is presented for improved information for the public as well as an intensification of critical empirical research around the complex and specific needs of future beneficiaries of new reproductive biotechnologies. (shrink)

Cet ouvrage est une réédition numérique d’un livre paru au XXe siècle, désormais indisponible dans son format d’origine.

With the continued expansion and commercialisation of fertility treatments, the selection and matching of donors have become more sophisticated and technologised. As part of this landscape, new form of genetic screening: ‘expanded carrier screening’ (ECS) is being offered as a technique to avoid the risk of donors passing on genetic conditions to future offspring. Allowing donors to be tested for hundreds of genetic conditions simultaneously, ECS marks a considerable departure from traditional ‘family history’ models of screening, which rely on an (...) individual's knowledge of family health. There is growing evidence of a drive towards the use of ECS within the fertility sector, and a growing number of clinics are offering it for a fee, as part of an egg or sperm donation cycle or as an add‐on to IVF treatment. In this article, we use methods of critical reflection to synthesise data from two studies to explore how ECS is being used to avoid genetic risk in IVF treatment using donor gametes. We suggest that ECS is a new form of repro‐genetic selection—a selective reproductive technology—with specific and important implications for donors, recipients and clinicians and with the potential to reconfigure the scope and application of gamete donation. We examine these implications and conclude that the existing policy blind spot relating to this development in fertility treatment practice needs to be urgently addressed. (shrink)

This book presents a paragraph-by-paragraph analysis of all of the major arguments and explanations in the "aesthetic" of Kant's Critique of Pure Reason. The first part of the book aims to provide a clear analysis of the meanings of the terms Kant uses to name faculties and types of representation, the second offers a thorough account of the reasoning behind the "metaphysical" and "transcendental" expositions, and the third investigates the basis for Kant's major conclusions about space, time, appearances, things in (...) themselves, and the cognitive constitution of the subject. A major goal of the work is to establish that Kant takes spatiotemporal form to be originally given through the constitution of the subject's receptive faculty, not generated through synthetic procedures of the imagination or understanding. (shrink)

As artificial intelligence (AI) continues to advance, one key challenge is ensuring that AI aligns with certain values. However, in the current diverse and democratic society, reaching a normative consensus is complex. This paper delves into the methodological aspect of how AI ethicists can effectively determine which values AI should uphold. After reviewing the most influential methodologies, we detail an intuitionist research agenda that offers guidelines for aligning AI applications with a limited set of reliable moral intuitions, each underlying a (...) refined cooperative view of AI. We discuss appropriate epistemic tools for collecting, filtering, and justifying moral intuitions with the aim of reducing cognitive and social biases. The proposed methodology facilitates a large collective participation in AI alignment, while ensuring the reliability of the considered moral judgments. (shrink)

The core doctrine of ethical intuitionism is that some of our ethical knowledge is non-inferential. Against this, Sturgeon has recently objected that if ethical intuitionists accept a certain plausible rationale for the autonomy of ethics, then their foundationalism commits them to an implausible epistemology outside ethics. I show that irrespective of whether ethical intuitionists take non-inferential ethical knowledge to be a priori or a posteriori, their commitment to the autonomy of ethics and foundationalism does not entail any implausible non-inferential (...) knowledge in areas outside ethics (such as the past, the future, or the unobservable). However, each form of intuitionism does require a controversial stand on certain unresolved issues outside ethics. (shrink)

Dummett's case against platonism rests on arguments concerning the acquisition and manifestation of knowledge of meaning. Dummett's arguments are here criticized from a viewpoint less Davidsonian than Chomskian. Dummett's case against formalism is obscure because in its prescriptive considerations are not clearly separated from descriptive. Dummett's implicit value judgments are here made explicit and questioned. ?Combat Revisionism!? Chairman Mao.

Literature on consumers’ ethical decision making is rooted in a rationalist perspective that emphasizes the role of moral reasoning. However, the view of ethical consumption as a thorough rational and conscious process fails to capture important elements of human cognition, such as emotions and intuitions. Based on moral psychology and microsociology, this paper proposes a holistic and integrated framework showing how emotive and intuitive information processing may foster ethical consumption at individual and social levels. The model builds on social (...) class='Hi'>intuitionism to show how consumers’ a priori affect-laden intuitive moral judgments impact their post hoc reflective moral reasoning. Symbolic interactionism is used to interpret consumers as interdependent and socially embedded agents that self-construct their social identity through interactions with other consumers. The proposed social intuitionist framework of consumers’ ethical decision making shows that other-oriented moral emotions—such as elevation, gratitude, and empathy—interact with persuasion and social influence in ethical consumption. Consequently, moral emotions and intuition drive interpersonal persuasion among ethical consumers. Theoretical propositions and implications for consumer ethics theory and practice are discussed. (shrink)

Walter Sinnott-Armstrong has argued against moral intuitionism, according to which some of our moral beliefs are justified without needing to be inferred from any other beliefs. He claims that any prima facie justification some non-inferred moral beliefs might have enjoyed is removed because many of our moral beliefs are formed in circumstances where either (1) we are partial, (2) others disagree with us and there is no reason to prefer our moral judgement to theirs, (3) we are emotional in (...) a way that clouds our judgement, (4) the circumstances are conducive to illusion, or (5) the source of our moral beliefs is unreliable or disreputable. I take issue with the elements of Sinnott-Armstrong’s argument that centre on (1) to (3) and (5), concluding that his case against moral intuitionism is unpersuasive. (shrink)

This study is the first part of an attempt to settle a vigorous debate among historians of medieval philosophy by harnessing the resources of analytic philosophy. The debate is about whether Avicenna's epistemology is rationalist or empirical. To settle the debate, I first articulate in this article the three core theses of rationalism and one core thesis of empiricism. Then, I probe Avicenna's epistemology in his major works according to the first core thesis of rationalism (the intuition thesis). In the (...) end, I find Avicenna committed to this thesis in at least one substantive way, namely, in his claim to intuit the intelligible forms or essences. This suffices to count Avicenna as rationalist. In a subsequent article, I shall probe Avicenna's epistemology according to the other two core theses of rationalism, presenting further evidence that he was a rationalist, not an empiricist. (shrink)

Herbrand’s theorem is a central fact about classical logic, [9, 10]. It provides a constructive method for associating, with each first-order formula X, a sequence of formulas X1, X2, X3, . . . , so that X has a first-order proof if and only if some Xi is a tautology. Herbrand’s theorem serves as a constructive alternative to..

In this article (1) I extract from Brentano’s works (three) formal arguments against “genealogical explanations” of ethical claims. Such explanation can also be designated as “naturalism” (not his appellation); (2) I counter these arguments, by showing how genealogical explanations of even apodictic moral claims are logically possible (albeit only if certain unlikely, stringent conditions are met); (3) I show how Nietzsche’s ethics meets these stringent conditions, but evolutionary ethics does not. My more general thesis is that naturalism and intuitionism (...) in ethics need not be mutually incompatible. (shrink)

Thinking about morality -- Story of contemporary intuitionism -- Moral knowledge -- New challenges to intuitionism -- Grounds of morality -- Right and the good reconsidered -- Intuitionism's rivals -- Being moral: how and why.

In this paper, I argue against the view, most eloquently advocated by Dieter Schönecker, that Kant is what I call a “sensualist intuitionist.” Kant’s text does not accommodate a sensualist intuitionist reading; the fact of reason is cognized by reason, not intuition. I agree with Schönecker that the feeling of respect for the moral law makes us feel its obligatory character, but I disagree that this feeling constitutes cognition of the normative content of the moral law. We do not cognize (...) the validity of the moral law through feeling. I argue instead for what I take to be the standard view: We feel through respect for the moral law the limiting and humiliating effect that rational cognition of the moral law has on our sensibility. (shrink)

We review the state of the art in moral psychology to answer 6 questions: 1) Where do moral beliefs and motivations come from? 2) How does moral judgment work? 3) What is the evidence for the social intuitionist model? 4) What exactly are the moral intuitions? 5) How does morality develop? And 6) Why do people vary in their morality? We describe the intuitionist approach to moral psychology. The mind makes rapid affective evaluations of everything it encounters, and these evaluations (...) (intuitions) shape and push subsequent moral reasoning. This approach to moral judgment has a variety of implications for moral philosophy and for the law in that it questions common assumptions about the reliability and causal efficacy of private, conscious reasoning. (shrink)

In Chapter 7 of The Taming of the True, Neil Tennant provides a new argument from Michael Dummett's ``manifestation requirement'' to the incorrectness of classical logic and the correctness of intuitionistic logic. I show that Tennant's new argument is only valid if one interprets crucial existence claims occurring in the proof in the manner of intuitionists. If one interprets the existence claims as a classical logician would, then one can accept Tennant's premises while rejecting his conclusion of logical revision. Thus, (...) Tennant has provided no evidence that should convince anyone who is not already an intuitionist. Since his proof is a proof for the correctness of intuitionism, it begs the question. (shrink)