P. Bernays has pointed out that, in order to prove the consistency of classical number theory, it is necessary to extend Hilbert's finitary standpoint by admitting certain abstract concepts in addition to the combinatorial concepts referring to symbols. The abstract concepts that so far have been used for this purpose are those of the constructive theory of ordinals and those of intuitionistic logic. It is shown that the concept of a computable function of finite simple type over the integers (...) can be used instead, where no other procedures of constructing such functions are necessary except simple recursion by an integral variable and substitution of functions in each other (starting with trivial functions). (shrink)

Dialectical proof procedures in assumption-based argumentation are in general sound but not complete with respect to both the credulous and skeptical semantics (due to non-terminating loops). This raises the question of whether we could describe exactly what such procedures compute. In a previous paper, we introduce infinite arguments to represent possibly non-terminating computations and present dialectical proof procedures that are both sound and complete with respect to the credulous semantics of assumption-based argumentation with infinite arguments. In this (...) paper, we study whether and under what conditions dialectical proof procedures are both sound and complete with respect to the grounded semantics of assumption-based argumentation with infinite arguments. We introduce the class of ω-grounded and finitary-defensible argumentation frameworks and show that finitary assumption-based argumentation is ω-grounded and finitary-defensible. We then present dialectical procedures that are sound and complete wrt finitary assumption-based argumentation. (shrink)

In this paper we present a finitary sequent calculus for the S5 multi-modal system with common knowledge. The sequent calculus is based on indexed hypersequents which are standard hypersequents refined with indices that serve to show the multi-agent feature of the system S5. The calculus has a non-analytic right introduction rule. We prove that the calculus is contraction- and weakening-free, that (almost all) its logical rules are invertible, and finally that it enjoys a syntactic cut-elimination procedure. Moreover, the use (...) of the non-analytic rule can be restricted so that the calculus can be considered as suitable for proof search. (shrink)

This chapter contains sections titled: Foundations and Logical Foundations Foundations for Mathematics Mathematics and Set Theory Sets, Classes, and Logic.

A constructivisation of the cut-elimination proof for sequent calculi for classical, intuitionistic and minimal infinitary logics with geometric rules—given in earlier work by the second author—is presented. This is achieved through a procedure where the non-constructive transfinite induction on the commutative sum of ordinals is replaced by two instances of Brouwer’s Bar Induction. The proof of admissibility of the structural rules is made ordinal-free by introducing a new well-founded relation based on a notion of embeddability of derivations. Additionally, conservativity for (...) classical over intuitionistic/minimal logic for the seven (finitary) Glivenko sequent classes is here shown to hold also for the corresponding infinitary classes. (shrink)

ZusammenfassungP. Bernays hat darauf hingewiesen, dass man, um die Widerspruchs freiheit der klassischen Zahlentheorie zu beweisen, den Hilbertschen flniter Standpunkt dadurch erweitern muss, dass man neben den auf Symbole sich beziehenden kombinatorischen Begriffen gewisse abstrakte Begriffe zulässt, Die abstrakten Begriffe, die bisher für diesen Zweck verwendet wurden, sinc die der konstruktiven Ordinalzahltheorie und die der intuitionistischer. Logik. Es wird gezeigt, dass man statt deesen den Begriff einer berechenbaren Funktion endlichen einfachen Typs über den natürlichen Zahler benutzen kann, wobei keine anderen (...) Konstruktionsverfahren für solche Funktionen nötig sind, als einfache Rekursion nach einer Zahlvariablen und Einsetzung von Funktionen ineinander .P. Bernays has pointed out that, in order to prove the consistency of classical number theory, it is necessary to extend Hilbert's finitary stand‐point by admitting certain abstract concepts in addition to the combinatorial concepts referring to symbols. The abstract concepts that so far have been used for this purpose are those of the constructive theory of ordinals and those of intuitionistic logic. It is shown that the concept of a computable function of finite simple type over the integers can be used instead, where no other procedures of constructing such functions are necessary except simple recursion by an integral variable and substitution of functions in each other. (shrink)

This is the first paper on constructive concurrent dynamic logic . For the first time, either for concurrent or sequential dynamic logic, we give a satisfactory treatment of what statements are forced to be true by partial information about the underlying computer. Dynamic logic was developed by Pratt [V. Pratt, Semantical considerations on Floyd–Hoare logic, in: 17th Annual IEEE Symp. on Found. Comp. Sci., New York, 1976, pp. 109–121, V. Pratt, Applications of modal logic to programming, Studia Logica 39 257–274] (...) for nondeterministic sequential programs, and by Peleg [D. Peleg, Concurrent dynamic logic, Journal of the Association for Computing Machinery 34 , D. Peleg, Communication in concurrent dynamic logic, Journal of Computer and System Sciences 35 ] for concurrent programs, for the purpose of proving properties of programs such as correctness. Here we define what it means for a dynamic logic formula to be forced to be true knowing only partial information about the results of assignments and tests. This informal CCDL semantics is formalized by intuitionistic Kripke frames modeling this partial information, and each such frame is interpreted as an idealized concurrent machine . In CCDL, proofs and deductions are ω-height, ω-branching, well-founded labeled subtrees of ωω. These are a generalization of the signed tableaux of Nerode [A. Nerode, Some lectures in modal logic, Technical Report, M.S.I. Cornell University, 1989, CIME Logic and Computer Science Montecatini Volume, Springer-Verlag Lecture Notes, 1990, A. Nerode, Some lectures in intuitionistic logic, Technical Report, M.S.I. Cornell University, 1988, Marktoberdorf Logic and Computation NATO Summer School Volume, NATO Science Series, 1990 ] stemming from the prefix tableaux of Fitting [M.C. Fitting, Proof Methods for Modal and Intuitionistic Logic, Reidel, 1983]. We demonstrate the correctness of our tableau proofs, define consistency properties, prove that consistency properties yield models, construct systematic tableaux, prove that systematic tableaux yield a consistency property, and conclude that CCDL is complete. This infinitary semantics and proof procedure will be the primary guide for defining, in a sequel, the correct finitary CCDL based on induction principles. FCCDL is suitable for implementation in constructive logic software systems such as Constable’s NUPRL or Huet-Coquand’s CONSTRUCTIONS. Our goal is to develop a constructive logic programming tool for specification and modular verification of programs in any imperative concurrent language, and for the extraction of concurrent programs from constructive proofs. Subsequent papers will introduce analogous logics for declarative and functional concurrent languages. (shrink)

We prove that the observational equivalence of third-order finitary Idealized Algol is decidable using Game Semantics. By modelling the state explicitly in our games, we show that the denotation of a term M of this fragment of IA is a compactly innocent strategy-with-state, i.e. the strategy is generated by a finite view function fM. Given any such fM, we construct a real-time deterministic pushdown automaton that recognizes the complete plays of the knowing-strategy denotation of M. Since such plays characterize (...) observational equivalence, and there is an algorithm for deciding whether any two DPDAs recognize the same language, we obtain a procedure for deciding the observational equivalence of third-order finitary IA. Restricted to second-order terms, the DPDA representation cuts down to a deterministic finite automaton; thus our approach gives a new proof of Ghica and McCusker’s regular-expression characterization for this fragment. Our algorithmic representation of program meanings, which is compositional, provides a foundation for model-checking a wide range of behavioural properties of IA and other cognate programming languages. Another result concerns second-order IA with full recursion: we show that observational equivalence for this fragment is undecidable. (shrink)

The lack of specific arithmetical axioms in Book VII has puzzled historians of mathematics. It is hardly possible in our view to ascribe to the Greeks a conscious undertaking to axiomatize arithmetic. The view that associates the beginnings of the axiomatization of arithmetic with the works of Grassman [1861], Dedekind [1888] and Peano [1889] seems to be more plausible. In this connection a number of interesting historical problems have been raised, for instance, why arithmetic was axiomatized so late. This question (...) was first posed and quite conclusively answered by Yanovskaja [1956]. Her major and quite conclusive argument was that “algorithms in arithmetic have absolute character, while in geometry we have to do with reducibility algorithms”. In this paper we are going to draw attention on certain peculiarities of the construction of the arithmetical Books of Euclid’s "Elements" and show that Euclidean arithmetic is constructed by effective procedures. In spite of the use of inference by reductio ad absurdum and methods equivalent to mathematical induction, Euclidean arithmetic retains its finitary character. It is not full arithmetic, but a finitary fragment of classical arithmetic, and thereby there was not any internal reason for its axiomatization. (shrink)

We study the matrices, reduced matrices and algebras associated to the systems SAT of structural annotated logics. In previous papers, these systems were proven algebraizable in the finitary case and the class of matrices analyzed here was proven to be a matrix semantics for them.We prove that the equivalent algebraic semantics associated with the systems SAT are proper quasivarieties, we describe the reduced matrices, the subdirectly irreducible algebras and we give a general decomposition theorem. As a consequence we obtain (...) a decision procedure for these logics. (shrink)

In 1936, Gerhard Gentzen published a proof of consistency for Peano Arithmetic using transfinite induction up to ε0, which was considered a finitistically acceptable procedure by both Gentzen and Paul Bernays. Gentzen’s method of arithmetising ordinals and thus avoiding the Platonistic metaphysics of set theory traces back to the 1920s, when Bernays and David Hilbert used the method for an attempted proof of the Continuum Hypothesis. The idea that recursion on higher types could be used to simulate the limit-building in (...) transfinite recursion seems to originate from Bernays. The main difficulty, which was already discovered in Gabriel Sudan’s nearly forgotten paper of 1927, was that measuring transfinite ordinals requires stronger methods than representing them. This paper presents a historical account of the idea of nominalistic ordinals in the context of the Hilbert Programme as well as Gentzen and Bernays’ finitary interpretation of transfinite induction. (shrink)

In the intellectual confusion prevailing since the demise of Marxism and “marxism”, the attempt is made to define democracy as a matter of pure procedure, explicitly avoiding and condemning any reference to substantive objectives. It can easily be shown, however, that the idea of a purely procedural “democracy” is incoherent and self-contradictory. No legal system whatsoever and no government can exist in the absence of substantive conditions which cannot be left to chance or to the workings of the “market” but (...) must be posited as objectives of political activity. The confusion results from a deficient understanding of what makes a society and an empty idea of “freedom”. The objective of politics is not happiness, an affair to be left to the individuals, but it certainly is liberty understood as participation in the governance of the polity; it is also the pursuit of the common good, defined as the sum of the prerequisites and facilitations of individual autonomy depending on collective action, and as the realization of commonly agreed collective goals. (shrink)

A notion of finitary inductively presented (f.i.p.) logic is proposed here, which includes all syntactically described logics (formal systems)met in practice. A f.i.p. theory FS0 is set up which is universal for all f.i.p. logics; though formulated as a theory of functions and classes of expressions, FS0 is a conservative extension of PRA. The aims of this work are (i)conceptual, (ii)pedagogical and (iii)practical. The system FS0 serves under (i)and (ii)as a theoretical framework for the formalization of metamathematics. The general (...) approach may be used under (iii)for the computer implementation of logics. In all cases, the work aims to make the details manageable in a natural and direct way. (shrink)

Abraham Robinson’s framework for modern infinitesimals was developed half a century ago. It enables a re-evaluation of the procedures of the pioneers of mathematical analysis. Their procedures have been often viewed through the lens of the success of the Weierstrassian foundations. We propose a view without passing through the lens, by means of proxies for such procedures in the modern theory of infinitesimals. The real accomplishments of calculus and analysis had been based primarily on the elaboration of (...) novel techniques for solving problems rather than a quest for ultimate foundations. It may be hopeless to interpret historical foundations in terms of a punctiform continuum, but arguably it is possible to interpret historical techniques and procedures in terms of modern ones. Our proposed formalisations do not mean that Fermat, Gregory, Leibniz, Euler, and Cauchy were pre-Robinsonians, but rather indicate that Robinson’s framework is more helpful in understanding their procedures than a Weierstrassian framework. (shrink)

This paper reports on an investigation of issues surrounding the use of ethical codes/codes of conduct in Irish based companies. Using a comprehensive questionnaire survey, the paper examines the incidence, content and enforcement of codes of conduct among a sample of the top 1000 companies based in Ireland. The main findings indicate that the overall usage of codes of conduct amongst indigenous Irish companies has increased significantly from 1995 to 2000. However, in line with prior research, these codes focus primarily (...) on issues surrounding company and employee protection as opposed to society protection. Almost half of all codes are written by company personnel or provided by head office. Revisions of codes are common but formal ongoing methods of instructing new staff about codes are not prevalent. Less than one-third of companies with codes have formal channels for reporting violations but a high percentage have formal disciplinary procedures in place for breaches of codes. (shrink)

While there has been significant discussion in the health sciences and ethics literatures about problems associated with publication practices (e.g., ghost- and gift-authorship, conflicts of interest), there has been relatively little practical guidance developed to help researchers determine how they should fairly allocate credit for multi-authored publications. Fair allocation of credit requires that participating authors be acknowledged for their contribution and responsibilities, but it is not obvious what contributions should warrant authorship, nor who should be responsible for the quality and (...) content of the scientific research findings presented in a publication. In this paper, we review arguments presented in the ethics and health science literatures, and the policies or guidelines proposed by learned societies and journals, in order to explore the link between author contribution and responsibility in multi-author multidisciplinary health science publications. We then critically examine the various procedures used in the field to help researchers fairly allocate authorship. (shrink)

Empirical evidence suggests that some health professionals believe consent procedures for the emerging technology of non-invasive prenatal diagnosis (NIPD) should become less rigorous than those currently used for invasive prenatal testing. In this paper, we consider the importance of informed consent and informed choice procedures for protecting autonomy in those prenatal tests which will give rise to a definitive result. We consider whether there is anything special about NIPD that could sanction a change to consent procedures for (...) prenatal diagnosis or otherwise render informed decision-making less important. We accept the claim that the absence of risk of miscarriage to some extent lessens the gravity of the decision to test compared with invasive methods of testing. However, we also claim that the definitive nature of the information received, and the fact that the information can lead to decisions of great significance, makes NIPD an important choice. This choice should only be made by means of a rigorous and appropriately supported decision-making process (assuming that this is what the pregnant woman wants). We conclude that, on balance, consent procedures for NIPD should mirror those for invasive testing, albeit without the need to emphasise procedure-related risk. (shrink)

Stephanie Collins’ Group Duties offers interesting new arguments and brings together numerous interconnected issues that have hitherto been treated separately. My critical commentary focuses on two particularly original and central claims of the book: (1) Only groups that are united under a group-level decision-making procedure can bear duties. (2) Attributions of duties to other groups should be understood as attributions of “coordination duties” to each member of the group, duties to take steps responsive to the others with a view to (...) the group’s φ-ing or express willingness to do so. In support of the first claim, Collins argues that only groups that can make decisions can bear duties, and that the ability to make decisions requires the relevant sort of decision-making procedure. I suggest that both parts of this argument remain in need of further support. I furthermore argue that Collins’ account of coordination duties gets certain kinds of cases wrong, and suggest that attributions of duties to groups without decision-making procedures are more plausibly understood as attributing shared duties. (shrink)

It is largely undisputed that nurses should obtain consent prior to nursing care procedures. This article reports on a qualitative study examining the way in which nurses obtain such informed consent. Data were collected through focus group discussion and by using a critical incident technique in order to explore the way in which nurses approach consent prior to nursing care procedures. Qualified nurses in two teaching hospitals in England participated in the study. An analysis of the data provides (...) evidence that consent was often not obtained by those who participated in the study and that refusals of care were often ignored. In addition, participants were often uncertain how to proceed with care when the patient was unable to consent. Consent prior to nursing care procedures is an essential but undeveloped concept, for which a new ethos is required. (shrink)

This research aimed to analyse inclusive practice in academic integrity in the teaching, support, policies and procedures involved at one UK HE institution. Data was collected through two sets of stakeholder interviews: three students from disadvantaged groups who had experienced academic conduct investigations; eleven staff with key roles in academic integrity. A third set of data comprised four institutional academic integrity documents which were analysed in terms of meeting Universal Design for Learning principles for inclusion. The four main findings (...) emerging from the study are: academic conduct processes create high levels of anxiety among students, particularly related to perceived judgement; students experience difficulty understanding academic integrity documents which lack consistency and do not meet inclusive criteria; students from certain backgrounds including widening participation, students with a disability and international non-native speakers need more institutional support in order to follow academic conduct processes and assimilate expected practice; there is a willingness among staff to try to develop more inclusive practice. The research findings led to a revised, more inclusive and educative institutional academic conduct procedure. The implication for practice is that attention is urgently needed to improve inclusive approaches to academic integrity. (shrink)

The small sample properties of estimators and tests are frequently too complex to be useful or are unknown. Much econometric theory is therefore developed for very large or asymptotic samples where it is assumed that the behaviour of estimators and tests will adequately represent their properties in small samples. Refined asymptotic methods adopt an intermediate position by providing improved approximations to small sample behaviour using asymptotic expansions. Dedicated to the memory of Michael Magdalinos, whose work is a major contribution to (...) this area, this book contains chapters directly concerned with refined asymptotic methods. In addition, there are chapters focusing on new asymptotic results; the exploration through simulation of the small sample behaviour of estimators and tests in panel data models; and improvements in methodology. With contributions from leading econometricians, this collection will be essential reading for researchers and graduate students concerned with the use of asymptotic methods in econometric analysis. (shrink)

The “somewhat vague, intuitive” notion from computability theory of an effective procedure (method) or algorithm can be fairly precisely defined even if it is not sufficiently formal and precise to belong to mathematics proper (in a narrow sense)—and even if (as many have asserted) for that reason the Church–Turing thesis is unprovable. It is proved logically that the class of effective procedures is not decidable, i.e., that no effective procedure is possible for ascertaining whether a given procedure is effective. (...) This undecidability result is proved directly from the notion itself of an effective procedure, without reliance on any (partly) mathematical lemma, conjecture, or thesis invoking recursiveness or Turing-computability. In fact, there is no reliance on anything very mathematical. The proof does not even appeal to a precise definition of ‘effective procedure’. Instead, it relies solely and entirely on a basic grasp of the intuitive notion of an effective procedure. Though the result that effectiveness is undecidable is not surprising, it is also not without significance. It has the consequence, for example, that the solution to a decision problem, if it is to be complete, must be accompanied by a separate argument that the proposed ascertainment procedure invariably terminates with the correct verdict. (shrink)

Originally applied on domestic and lab animals, assisted reproduction technologies (ARTs) have also found application in conservation breeding programs, where they can make the genetic management of populations more efficient, and increase the number of individuals per generation. However, their application in wildlife conservation opens up new ethical scenarios that have not yet been fully explored. This study presents a frame for the ethical analysis of the application of ART procedures in conservation based on the Ethical Matrix (EM), and (...) discusses a specific case study—ovum pick-up (OPU) procedures performed in the current conservation efforts for the northern white rhinoceros (Ceratotherium simum cottoni)—providing a template for the assessment of ART procedures in projects involving other endangered species. (shrink)

Is it necessary to contrast the spreading process of genetic engineering in the agri-food stuff sector? Can EU rules really consider the impact of this brand new technologies on biology and, consequently, on public health? Despite the general trend, a firm opposition is what is happening in some Regions of Italy, where GMOs production and placing on the market are foibidden.

I argue for the use of the adjunction operator (adding a single new element to an existing set) as a basis for building a finitary set theory. It allows a simplified axiomatization for the first-order theory of hereditarily finite sets based on an induction schema and a rigorous characterization of the primitive recursive set functions. The latter leads to a primitive recursive presentation of arithmetical operations on finite sets.

In this paper we study finitary extensions of the nilpotent minimum logic or equivalently quasivarieties of NM-algebras. We first study structural completeness of NML, we prove that NML is hereditarily almost structurally complete and moreover NM\, the axiomatic extension of NML given by the axiom \^{2}\leftrightarrow ^{2})^{2}\), is hereditarily structurally complete. We use those results to obtain the full description of the lattice of all quasivarieties of NM-algebras which allow us to characterize and axiomatize all finitary extensions of (...) NML. (shrink)

Obtaining prospective written consent from women to participate in trials when they are experiencing an obstetric emergency is challenging. Alternative consent pathways, such as gaining verbal consent at enrolment followed, later, by obtaining written consent, have been advocated by some clinicians and bioethicists but have received little empirical attention. We explored women’s and staff views about the consent procedures used during the internal pilot of a trial, where the protocol permitted staff to gain verbal consent at recruitment. Interviews with (...) staff and participating women. Data were analysed thematically and interviews were cross-compared to identify differences and similarities in participants’ views about the consent procedures used. Women and some staff highlighted benefits to obtaining verbal consent at trial enrolment, including expediting recruitment and reducing the burden on those left exhausted by their births. However, most staff with direct responsibility for taking consent expressed extreme reluctance to proceed with enrolment until they had obtained written consent, despite being comfortable using verbal procedures in their clinical practice. To account for this resistance, staff drew a strong distinction between research and clinical care and suggested that a higher level of consent was needed when recruiting into trials. In doing so, staff emphasised the need to engage women in reflexive decision-making and highlighted the role that completing the consent form could play in enabling and evidencing this process. While most staff cited their ethical responsibilities to women, they also voiced concerns that the absence of a signed consent form at recruitment could expose them to greater risk of litigation were an individual to experience a complication during the trial. Inexperience of recruiting into peripartum trials and limited availability of staff trained to take consent also reinforced preferences for obtaining written consent at recruitment. While alternative consent pathways have an important role to play in advancing emergency medicine research, and may be appreciated by potential recruits, they may give rise to unintended ethical and logistical challenges for staff. Staff would benefit from training and support to increase their confidence and willingness to recruit into trials using alternative consent pathways. This qualitative research was undertaken as part of the GOT-IT Trial. Date of registration 26/03/2014. (shrink)

Finitary sketches, i.e., sketches with finite-limit and finite-colimit specifications, are proved to be as strong as geometric sketches, i.e., sketches with finite-limit and arbitrary colimit specifications. Categories sketchable by such sketches are fully characterized in the infinitary first-order logic: they are axiomatizable by σ-coherent theories, i.e., basic theories using finite conjunctions, countable disjunctions, and finite quantifications. The latter result is absolute; the equivalence of geometric and finitary sketches requires (in fact, is equivalent to) the non-existence of measurable cardinals.

This paper is about the epistemology of practical reason and, in particular, the function of trust as an end to be pursued rationally in praxis. Our purpose is threefold: first, to present an outline of the structure of practical reason; secondly, to compare practical reason and scientific reason in order to determine the main differences between these two basic manifestations of human reason; finally, to argue in favour of a non-utilitarian model of practical reason in the light of some results (...) of contemporary economic theory. (shrink)

Dialogue is one of the fundamental pillars of social life and an essential means of communication. It enables individuals to express their needs, desires, feelings, positions, problems, and methods for managing various aspects of their lives. Furthermore, dialogue fosters the development of ideas and experiences, facilitating expression, creativity, and participation in a civilized society. Through dialogue, communication and interaction with others occur. This study aims to explore effective methods for teaching the Arabic language through dialogue and its application to non-native (...) speakers at the primary level at Mara University of Technology. Specifically, it will investigate whether dialogue aids students in acquiring vocabulary. Vocabulary is a crucial component of language, alongside sounds and structures. Teaching vocabulary is an essential part of foreign language programs, including Arabic. However, despite its significance, the learning and teaching of Arabic vocabulary to non-native learners face several challenges, contributing to their weaknesses in this area. Notes are statistically significant differences between two groups: those "using dialogue" and those "not using it" in learning Arabic vocabulary. (shrink)