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)

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)

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 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)

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)

Shared views regarding the moral respect which is owed to children in family life are used as a guide in determining the moral permissibility of nontherapeutic clinical research procedures involving children. The comparison suggests that it is not appropriate to seek assent from the preadolescent child. The analogy with interventions used in family life is similarly employed to specify the permissible limit of risk to which children may be exposed in nontherapeutic research procedures. The analysis indicates that recent (...) writers misconceive how certain moral principles, such as respect for personal autonomy, require us to act toward children. The results are also used to assess proposed federal regulations on research with children. (shrink)

This paper deals with two issues. First, it identifies structured propositions with logical procedures. Second, it considers various rigorous definitions of the granularity of procedures, hence also of structured propositions, and comes out in favour of one of them. As for the first point, structured propositions are explicated as algorithmically structured procedures. I show that these procedures are structured wholes that are assigned to expressions as their meanings, and their constituents are sub-procedures occurring in executed (...) mode. Moreover, procedures are not mere aggregates of their parts; rather, procedural constituents mutually interact. As for the second point, there is no universal criterion of the structural isomorphism of meanings, hence of co-hyperintensionality, hence of synonymy for every kind of language. The positive result I present is an ordered set of rigorously defined criteria of fine-grained individuation in terms of the structure of procedures. Hence procedural semantics provides a solution to the problem of the granularity of co-hyperintensionality. (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)

Swedish hunters sometimes appeal to an inviolate ‘right to exist’ for wolves, apparently rejecting NIMBY. Nevertheless, the conditions existence hunters impose on wolves in practice fundamentally contradict their use of right to exist language. Hunters appeal to this language hoping to gain uptake in a conservation and management discourse demanding appropriately objective ecological language. However, their contradictory use of ‘right to exist' opens them up to the charge that they are being deceptive – indeed, right to exist is a 'disguised (...) NIMBY!' We address this situation by distinguishing hunters’ criticisms of wolves from the procedures for reaching objective policy decisions. (shrink)

In the recent literature across philosophy, medicine and public health policy, many influential arguments have been put forward to support the use of randomization procedures to allocate scarce life-saving resources. In this paper, I provide a systematic categorization and a critical evaluation of these arguments. I shall argue that those arguments justify using RAND to allocate SLSR in fewer cases than their proponents maintain and that the relevant decision-makers should typically allocate SLSR directly to the individuals with the strongest (...) claims to these resources rather than use RAND to allocate such resources. (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.

According to Alain Badiou, truth’s existence is not dependent upon philosophy because philosophy itself is not a creator of truth. Badiouan thought submits philosophy to the universe of truth through the mediation of truth procedures. Badiou names these procedures love, politics, art and science. In contrast, the instinctual reason of democratic materialism, which Badiou defines as the partnership between parliamentary democracy and neo-liberal pragmatism, replaces love with physical beauty, politics with technical power, art with a marketable talent and (...) science with a competitive genius. These replacements also correspond to post-truth. This article contrasts the concept of “disinterested interest” in Badiou’s truth procedures with “self-interest” reigning over democratic materialism’s reality procedures. Following Badiou, I explain how “self-interested interest” reproduces the human-animal’s instinctual reason, which triggers post-truth politics. Commitment to truth in a post-truth era therefore cannot be sustained by appealing to democratic materialism’s manipulated knowledge but must be guided by disinterested interest. The article argues that knowledge cannot be an antidote to post-truth because democratic materialism often uses knowledge as an instrument or sometimes as a control mechanism, to strengthen the position of post-truth in many circumstances. (shrink)

Max Wertheimer, in his classic Productive Thinking, linked understanding to transfer: Understanding is important because it provides the ability to generalize the solution of one problem to apply to another. Recent work in human and machine learning has led to the development of a new class of generalization mechanism, called here analysis‐based generalization, which can be used to provide a concrete account of the linkage Wertheimer suggested: these mechanisms all, in different ways, use understanding of examples in the generalization process. (...) In this paper I review this class of mechanism, and describe a method for causal attribution that can produce the analyses of examples that the generalization methods require, in the domain of simple procedures in human‐computer interaction. This causal analysis method is linked with analysis‐based generalization to form EXPL, an implemented model which is a concrete, though limited, instontiation of Wertheimer s scheme. EXPL constructs an understanding of an example procedure and generalizes it on the basis of that understanding. Results of an empirical study suggest that some of EXPL's attribution heuristics are used by people, and that while a subclass of analysis‐based methods, called superstitious methods, seem to provide a more plausible account of people's generalization under the conditions of the study than a contrasting class of rationalistic methods, at least some participants appear to use methods from both classes. The results also show that explanation‐based methods, which rely on comprehensive domain theories, must be used in conjunction with a means for extending the domain theory. If thus enhanced, explanation‐based methods are able to mimic the effects of other analysis‐based methods, and can provide a good account of the data, though combinations of other methods must also be considered. Finally, I return to Wertheimer s ideas to argue that none of the current analysis‐based generalization methods fully captures Wertheimer s notion of understanding. Proper choice among different possible analyses of an example is crucial for Wertheimer, but I argue that this problem may be beyond the reach of learning systems. (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)

In this essay I defend an institutional approach to democratic legitimacy against proceduralist approaches that are commonly endorsed by deliberative democrats. Although deliberative democrats defend a complex view of democratic legitimacy that aims to account for both the procedural and substantive dimensions of legitimacy, most accounts of the relationship between these dimensions currently on offer are too proceduralist to be plausible (I). By contrast, I argue that adopting an institutional approach helps provide a more convincing account of the interplay between (...) procedural and substantive aspects of democratic legitimacy which in turn illuminates the intricate relationship between public deliberation and decision-making procedures such as voting (II). This account also enables us to see what is wrong with interpreting the legitimacy of majoritarian and non-majoritarian institutions in terms of an alleged conflict between popular sovereignty and rights protections. In opposition to this view, I argue that the proper standard for judging the democratic legitimacy of both majoritarian and non-majoritarian institutions is whether they enable an ongoing recursive process of deliberative contestation or whether they generate antidemocratic shortcuts instead (III). (shrink)

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.

It is known that every α-dimensional quasi polyadic equality algebra (QPEA α ) can be considered as an α-dimensional cylindric algebra satisfying the merrygo- round properties . The converse of this proposition fails to be true. It is investigated in the paper how to get algebras in QPEA from algebras in CA. Instead of QPEA the class of the finitary polyadic equality algebras (FPEA) is investigated, this class is definitionally equivalent to QPEA. It is shown, among others, that from (...) every algebra in a β-dimensional algebra can be obtained in QPEA β where , moreover the algebra obtained is representable in a sense. (shrink)

A growing number of clinical trials use invasive research procedures to obtain tissue for disease screening and to monitor the effects of drugs. These procedures can be ethically contentious because they often have neither therapeutic nor diagnostic value, and because research participants may not realize this, which could compromise the validity of their consent to the procedure. In the first section of this paper, we describe the burdens, risks, and benefits associated with certain common invasive, nondiagnostic research (...) class='Hi'>procedures. We next offer a series of arguments about the general properties of a valid consent for such procedures, and we close by examining what is currently known about consent quality for invasive research procedures when measured against the standards laid out in the second section. We conclude that there is little evidence to either confirm or dispel concerns about participants’ consent quality for protocols involving invasive, nondiagnostic research procedures. (shrink)

This critical reflection on the ethical concerns of current practice is underpinned by a systematic synthesis of current evidence focusing on why and how children are held or restrained for clinical procedures within acute care and the experiences of those present when a child is held against their wishes. Empirical evidence from a range of clinical settings internationally demonstrates that frequently children are held for procedures to be completed; younger children and those requiring procedures perceived as urgent (...) are more likely to be held. Parents and health professionals express how holding children for procedures can cause feelings of moral distress expressed as uncertainty, guilt and upset and that this act breaches the trusting and protective relationship established with children. Despite this, children's rights and alternatives to holding are not always respected or explored. Children's experiences and perceptions are absent from current literature. Children and young people have a moral right to have their voice and protests heard and respected and for these to inform judgements of their best interests and the actions of health professionals. Without robust evidence, debate and recognition that children are frequently held against their wishes in clinical practice for procedures which may not be urgent, children's rights will continue to be compromised. (shrink)

Research ethics review is a critical aspect of the research governance framework for human subjects research. This usually requires that research protocols be submitted to a research ethics committee for review and approval. This has led to very rapid developments in the domain of research ethics, as RECs proliferate all over the globe in rhyme with the explosion in human subjects research. The work of RECs has increasingly become elaborate, complex, and in many cases urgent, necessitating supporting rules and (...) class='Hi'>procedures of operation. Guidelines for elaborating standard operating procedures for the functioning of RECs have also been proposed. The SOPs of well-placed and well-resourced RECs have tended to pay much attention to details, resulting, as a consequence, in generally long, elaborate, intricate and complex SOPs; a model that can hardly be replicated by other committees, equally under ethics review pressures, but working under much more constraining conditions in resource-destitute environments. In this paper, we looked at the content and length of SOPs from African RECs and compared them to the World Health Organization ’s guidelines as the gold standard. We also looked at the SOPs from the Ethics Review and Consultancy Committee of the Cameroon Bioethics Initiative that we elaborated in a simplified way in 2013, and compared them to the WHO’s guidelines and to the other SOPs. Sixteen SOPs from 14 African countries were collected from various sources. Their average length was of 30 pages. By comparison to the guidance of the WHO, only six of them were found acceptable with more than 70 % of the criteria from the gold standard that were fully described. Among those six, two of them were very long and detailed, while the four remaining SOPs ranged from 16 to 24 pages. The ERCC SOPs are seven pages long but maintain all that is of essence for the rigorous, efficient and timely review of protocols. We are convinced that, because of their brevity, simplicity, clarity and user-friendliness, the ERCC SOPs recommend themselves as a model template to, at least, committees similarly situated and/or circumstanced as the ERCC of the Cameroon Bioethics Initiative is. In fact, brevity, clarity, simplicity and user-friendliness are recognized values. Whatever is brief and clear is better than what is not and saves time. What is simple and user-friendly is better than what is not even though the two have the same aims because it saves both time and mental energy. And if this be true in general, it is even truer of the context and its peculiar constraints that we are addressing. (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)

Kotek et al. argue on the basis of novel experimental evidence that sentences like ‘Most of the dots are blue’ are ambiguous, i.e. have two distinct truth conditions. Kotek et al. furthermore suggest that when their results are taken together with those of earlier work by Lidz et al., the overall picture that emerges casts doubt on the conclusions that Lidz et al. drew from their earlier results. We disagree with this characterization of the relationship between the two studies. Our (...) main aim in this reply is to clarify the relationship as we see it. In our view, Kotek et al.’s central claims are simply logically independent of those of Lidz et al.: the former concern which truth condition a certain kind of sentence has, while the latter concern the procedures that speakers choose for the purposes of determining whether a particular truth condition is satisfied in various scenes. The appearance of a conflict between the two studies stems from inattention to the distinction between questions about truth conditions and questions about verification procedures. (shrink)

The 2005 Report on Social Responsibility and Health of the UNESCO International Bioethics Committee (Ibc) proposes a new approach to implementing the right to healthcare and suggests a number of Courses of Action to be followed in various fields. Based on the latest available data, we intend to present an overview of the current state of European health systems in two of those fields—decision-making procedures and quality assurance in health care—and to attempt a comparison of the situation with the (...) Report’s provisions, in order to pave the way for the identification of what still has to be done to bridge international recommendations and the reality of policy and practice in Europe’s health care. (shrink)

This passage provides invaluable evidence on the procedures pertaining to the admission of new citizens in Classical Athens. The picture that the author has given of the roles that were played by the institutions involved in these procedures is very clear: for the reader's convenience I display it in the form of a diagram in Figure 1. According toAth. Pol., the deme voted on whether a candidate was both of legal age and of free status; if free status (...) was denied by the deme, the candidate could appeal to the Central Court; and at the end of the process the Council of Five Hundred double-checked that the candidate was of legal age. (shrink)

Disability theorists have argued that the belief that we should prevent the birth of people with disabilities is prejudicial against disabled people. Particularly influential has been the Expressivity Objection to reproductive selective procedures aimed at eliminating disability. The Expressivity Objection in its strongest form says that to prevent the birth of a disabled child is to express the view that a disabled life is not worth living. In its weaker form, it says that to prevent the birth of a (...) disabled child is to perpetuate the stigma of disability or send the message that disabled people are not welcome in this world.Disability, as it is spoken of in these contexts, refers to... (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)

This article interrogates whether and how the concept of ‘patriarchy’ is used by UN human rights treaty monitoring bodies (treaty bodies) and special procedures to interpret state obligations to respect and ensure women’s human rights. There are two key points that arise out of this study: first, that several treaty bodies and special procedures purposely and consistently use the concept of ‘patriarchy’ when discussing women’s human rights, and second, that although not all treaty bodies and special procedures (...) have referred to the terms ‘patriarchy’ or ‘patriarchal’, an examination of those that have reveals a marked difference in how the terms are used by treaty bodies when compared with special procedures. While treaty bodies render the meaning of ‘patriarchy’ as being synonymous with certain harmful practices, such as female-genital mutilation (FGM), special procedures utilise ‘patriarchy’ as a system of power, permeating every facet of society. In this article I will argue that the current state of dissonance between the understandings of ‘patriarchy’ by treaty bodies and special procedures creates an unnecessary ambiguity that does nothing to advance gender equality. Furthermore, utilising a nuanced understanding of patriarchy, as articulated by intersectional and anti-essentialist feminist scholars, would potentially equip treaty bodies and special procedures for more meaningful interpretation of rights themselves, and greater protection of women’s human rights. (shrink)

The model presented by Lee and Schwarz provides a novel explanation for the elementary mechanisms of psychological cleansing. I argue that the model could be extended to account for complex instances of psychological cleansing where the grounded procedures are not isolated and the opposing motives of separation and connection are entangled in a strategic interplay.

Universal Grammar (UG) can be interpreted as a constraint on the form of possible grammars (hypothesis space) or as a constraint on acquisition strategies (selection procedures). In this response to Herschensohn we reiterate the position outlined in Epstein et al. (1996a, r), that in the evaluation of L2 acquisition as a UG- constrained process the former (possible grammars/ knowledge states) is critical, not the latter. Selection procedures, on the other hand, are important in that they may have a (...) bearing on development in language acquisition. We raise the possibility that differences in first and second language acquisition pertaining to both attainment of the end-state and course of development may derive from differences in selection procedures. We further suggest that for these reasons age effects in the attainment of nativelike proficiency must necessarily be separated from UG effects. (shrink)

This article concerns the implementation of new EU Directives coordinating the procedures for awarding public contracts in European Union Member States. In a number of countries, including Poland, the process of their implementation (Directive 2014/24/eu of the European Parliament and of the Council of 26 February 2014 on public procurement; Directive 2014/25/eu of the European Parliament and of the Council of 26 February 2014 on procurement by entities operating in the water, energy, transport, and postal services sectors; Directive 2014/23/eu (...) of the European Parliament and of the Council of 26 February 2014 on the award of concession contracts) was delayed. In most cases, the modernization of EU regulations on public procurement required a thorough modification of national regulations in this respect. As a result of the introduction of the package of new Directives, the European Union public procurement market has undergone substantial changes. The need to adjust legal regulations to the changing political, social, and economic situations in a better way has resulted in the transposition of the modernized EU Directives concerning public procurement to the Polish legal system, affecting the final shape of the new Polish Public Procurement Law. The implementation of the package of new Directives has significantly affected the functioning of the Polish public procurement market. For the entities operating in this market, this means the necessity to expand their knowledge, so as to become familiar with the new legal solutions in this respect. (shrink)

This commentary provides an interpretation of the effects of grounded procedures in terms of the goal-generalization processes involved in coping with negative feelings and identifies some implications that might not yet have been considered.

Firm managers make ethical decisions regarding the form and quality of disclosure. Disclosure can have long-term implications for performance, earnings manipulation, and even fraud. We investigate the impact of venture capital (VC) backing on the quality and informativeness of disclosure controls and procedures for newly public companies. We find that these controls and procedures are stronger, as evidenced by fewer material weaknesses in internal control under Section 302 of the Sarbanes–Oxley Act, when companies are VC-backed. Moreover, these disclosures (...) are informative and are more likely to be followed by subsequent financial statement restatements than are disclosures made by non-VC-backed IPO companies. (shrink)

Interest in children’s agency within the research process has led to a renewed consideration of the relationships between researchers and children. Child protection concerns are sometimes not recognised by researchers, and sometimes ignored. Yet much research on children’s lives, especially in health, has the potential to uncover child abuse. University research guidance should be in place to safeguard both researchers and the populations under scrutiny. The aim of this study was to examine university guidance on protecting children in research contexts.

Physicians’ resistance to implementing innovative medical procedures due to a perceived risk of liability can adversely affect the public’s health. This resistance prevents public access to procedures that could better treat communicable or chronic diseases. Innovative procedures, for the purpose of this article, are medical practices that require physicians to modify current clinical approaches to treating or diagnosing a patient’s condition and incorporate: newly developed tests, treatments, drugs or devices ; or novel methods not commonly used by (...) a majority of physicians. Innovative procedures do not include treatments provided during clinical research or those beyond a physician’s scope of practice. (shrink)

This study drew on three theoretical perspectives – attribution theory, power, and role identity theory – to compare the job-related outcomes of sexual harassment from organizational insiders and organizational outsiders in a sample of UK police officers and police support staff. Results showed that sexual harassment from insiders was related to higher intentions to quit, over-performance demands, and lower job satisfaction, whereas sexual harassment from outsiders was not significantly related to any of the outcome variables investigated. We also examined two (...) moderator variables: equal opportunity support and confidence in grievance procedures. Consistent with our hypotheses, equal oppor- tunity support mitigated the effects of sexual harassment from supervisors on intent to quit and over-performance demands. Confidence in grievance procedures moderated the relationship between sexual harassment from supervisors and all outcome variables. Implications for theory and practice are discussed. (shrink)

Recent programs aimed at the independent living of persons with disabilities, allow them to be costumers of sectors in which they have never had full access in the past. The Lisbon Treaty has distinctly recognized the existence of a community tourist area within the primary law, and CRPD has defined the principles of accessibility and accessible tourism as tools for the inclusion. In addition, tourism and transportation stakeholders must guarantee non-discriminatory services; they must approach persons with disabilities as every other (...) customer, by taking in consideration their needs and rights, especially when it comes to their accessibility, assistance, and information. Companies of transportation must cooperate with DPOs in order to define disability-related training procedures. (shrink)

We study the semantics of dialectical proof procedures. As dialectical proof procedures are in general sound but not complete wrt admissibility semantics, a natural question here is whether we could give a more precise semantical characterization of what they compute. Based on a new notion of infinite arguments representing loops, we introduce a stricter notion of admissibility, referred to as strict admissibility, and show that dialectical proof procedures are in general sound and complete wrt strict admissibility.

By combining the methods of two former papers of ours we develop a finitary ordinal analysis of the axiom system KPi of Kripke-P atek set theory with an inaccessible universe. As a main result we obtain an upper bound for the provably recursive functions of KPi.