In this short paper I note that a key metatheorem does not hold for the bilateralist inferential framework: harmony does not entail consistency. I conclude that the requirement of harmony will not suffice for a bilateralist to maintain a proof theoretic account of classical logic. I conclude that a proof theoretic account of meaning based on the bilateralist framework has no natural way of distinguishing legitimate definitional inference rules from illegitimate ones (such as those for tonk). Finally, as an appendix (...) to the main argument, I propose an alternative non-bilateral formal solution to the problem of providing a proof-theoretic account of classical logic. (shrink)

Community engagement (CE) contributes to successful research. There is, however, a lack of literature on the effectiveness of different models of CE and, specifically, on CE strategies for the conduct of genomic research in sub-Saharan Africa. There is also a need for models of CE that transcend the recruitment stage of engaging prospective individuals and communities and embed CE throughout the research process and after the research has concluded. The qualitative study reported here was designed to address these knowledge gaps (...) and comprised of 36 key informant semi-structured interviews and fifteen focus groups with 50 participants. We interviewed selected stakeholders in genomic research in Nigeria: biomedical researchers, community rulers, opinion leaders, community health workers, and prospective research participants. We explored these stakeholders’ views on their understanding of community engagement, their expectations, experiences, and their opinions on acceptable processes of community consultation in genomic research. The methodological design, adapted from grounded theory, used the constant comparative method of data analysis; while normative conclusions were made using the symbiotic empirical ethics approach. Data analysis revealed five main themes important for successfully engaging communities in genomic research: effective communication, diversity of community gatekeeping, trust, cultural integration of research, and conservation of the research setting. From these themes, we have developed a four-stage model of community engagement that covers all stages of the research process; namely, the Community Approach, Intermediate phase, Collaboration and Post-research Cordiality model (CICP). This model could be used to improve the integration of CE in genomic research among local communities. (shrink)

In this paper I present a formalist philosophy mathematics and apply it directly to Arithmetic. I propose that formalists concentrate on presenting compositional truth theories for mathematical languages that ultimately depend on formal methods. I argue that this proposal occupies a lush middle ground between traditional formalism, fictionalism, logicism and realism.

We are used to the idea that computers operate on numbers, yet another kind of data is equally important: the syntax of formal languages, with variables, binding, and alpha-equivalence. The original application of nominal techniques, and the one with greatest prominence in this paper, is to reasoning on formal syntax with variables and binding. Variables can be modelled in many ways: for instance as numbers (since we usually take countably many of them); as links (since they may `point' to a (...) binding site in the term, where they are bound); or as functions (since they often, though not always, represent `an unknown'). None of these models is perfect. In every case for the models above, problems arise when trying to use them as a basis for a fully formal mechanical treatment of formal language. The problems are practical—but their underlying cause may be mathematical. The issue is not whether formal syntax exists, since clearly it does, so much as what kind of mathematical structure it is. To illustrate this point by a parody, logical derivations can be modelled using a Gödel encoding (i.e., injected into the natural numbers). It would be false to conclude from this that proof-theory is a branch of number theory and can be understood in terms of, say, Peano's axioms. Similarly, as it turns out, it is false to conclude from the fact that variables can be encoded e.g., as numbers, that the theory of syntax-with-binding can be understood in terms of the theory of syntax-without-binding, plus the theory of numbers (or, taking this to a logical extreme, purely in terms of the theory of numbers). It cannot; something else is going on. What that something else is, has not yet been fully understood. In nominal techniques, variables are an instance of names, and names are data. We model names using urelemente with properties that, pleasingly enough, turn out to have been investigated by Fraenkel and Mostowski in the first half of the 20th century for a completely different purpose than modelling formal language. What makes this model really interesting is that it gives names distinctive properties which can be related to useful logic and programming principles for formal syntax. Since the initial publications, advances in the mathematics and presentation have been introduced piecemeal in the literature. This paper provides in a single accessible document an updated development of the foundations of nominal techniques. This gives the reader easy access to updated results and new proofs which they would otherwise have to search across two or more papers to find, and full proofs that in other publications may have been elided. We also include some new material not appearing elsewhere. (shrink)

By operations on models we show how to relate completeness with respect to permissivenominal models to completeness with respect to nominal models with finite support. Models with finite support are a special case of permissive-nominal models, so the construction hinges on generating from an instance of the latter, some instance of the former in which sufficiently many inequalities are preserved between elements. We do this using an infinite generalisation of nominal atoms-abstraction. The results are of interest in their own right, (...) but also, we factor the mathematics so as to maximise the chances that it could be used off-the-shelf for other nominal reasoning systems too. Models with infinite support can be easier to work with, so it is useful to have a semi-automatic theorem to transfer results from classes of infinitely-supported nominal models to the more restricted class of models with finite support. In conclusion, we consider different permissive-nominal syntaxes and nominal models and discuss how they relate to the results proved here. (shrink)

Nominal terms extend first-order terms with binding. They lack some properties of first- and higher-order terms: Terms must be reasoned about in a context of ‘freshness assumptions’; it is not always possible to ‘choose a fresh variable symbol’ for a nominal term; it is not always possible to ‘α-convert a bound variable symbol’ or to ‘quotient by α-equivalence’; the notion of unifier is not based just on substitution.Permissive nominal terms closely resemble nominal terms but they recover these properties, and in (...) particular the ‘always fresh’ and ‘always rename’ properties. In the permissive world, freshness contexts are elided, equality is fixed, and the notion of unifier is based on substitution alone rather than on nominal terms’ notion of unification based on substitution plus extra freshness conditions.We prove that expressivity is not lost moving to the permissive case and provide an injection of nominal terms unification problems and their solutions into permissive nominal terms problems and their solutions.We investigate the relation between permissive nominal unification and higher-order pattern unification. We show how to translate permissive nominal unification problems and solutions in a sound, complete, and optimal manner, in suitable senses which we make formal. (shrink)

We build on an existing a term-sequent logic for the λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-terms into first order logic. We prove a cut-elimination result and then offer an application of cut-elimination by giving a notion of uniform proof for λ-terms. We suggest how this allows us to view the calculus of untyped αβ-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen).

Ways out: The proper relata of causal statements are large complexes of (macroscopic) conditions. For example: the spark, in the presence of oxygen together with flammable material and low humidity etc. The entailment is made virtue of the general macroscopic laws of flammable materials, humidity etc.

This concise text treats logic as a tool, “generated so that half the work involved in thinking is done for you by somebody else (the rules and laws of the logic).” Gabbay explains in a clear and careful manner how formal features of, and formal relations between, ordinary declarative sentences are captured by the systems of propositional and predicate logic.

An intensional sentential context is one where such intersubstitutivity fails: It is informative that A It is known that A It is necessary that A The fact that A caused it to be that B Some authors characterise intensional contexts by the failure of the intersubstitution of co-referring terms. Such a characterisation is problematic.

A famous proposed solution to the one over many problem is found in Plato. For example, it appears in The Parmenedies and is introduce by Zeno arguing that . . . if being is many, it must be both like and unlike, and that this is impossible, for neither can the like be unlike, nor the unlike like-is that your position? and Socrates responds: do you not further think that there is an idea of likeness in itself, and another idea (...) of unlikeness, which is the opposite of likeness, and that in these two, you and I and all other things to which we apply the term many, participate-things which participate in likeness become in that degree and manner like; and so far as they participate in unlikeness become in that degree unlike, or both like and unlike in the degree in which they participate in both? And may not all things partake of both opposites, and be both like and unlike, by reason of this participation? Where is the wonder? and the discussion moves on to the interesting question that.. (shrink)

In this paper we make some observations about Natural Deduction derivations [Prawitz, 1965, van Dalen, 1986, Bell and Machover, 1977]. We assume the reader is familiar with it and with proof-theory in general. Our development will be simple, even simple-minded, and concrete. However, it will also be evident that general ideas motivate our examples, and we think both our specific examples and the ideas behind them are interesting and may be useful to some readers. In a sentence, the bare technical (...) content of this paper is: Extending natural deduction with global well-formedness conditions can neatly and cheaply capture classical and intermediate logics. The interest here is in the ‘neatly’ and ‘cheaply’. By ‘neatly’ we mean ‘preserving proof-normalisation’,1 and ‘maintaining the subformula property’, and by ‘cheaply’ we mean ‘preserving the formal structure of deductions’ (so that a deduction in the original system is still, formally, a deduction in the extended system, and in particular it requires no extra effort to write just because it is in the extended system). To illustrate what we have in mind consider intuitionistic first-order logic (FOL) [van Dalen, 1986] as a paradigmatic example of a formal notion of deduction. A natural deduction derivation (or deduction) is an inductively defined tree structure where each node contains an instance of a formula. A deduction is valid when each successive node follows from its predecessors in accordance with some predetermined inference rules. A particular attraction of Natural Deduction is its clean and economical presentation. Here for example are deduction (fragments) proving A ∧ B from A and B, and ∀x. (P (x) ∧ Q(x)) from ∀x. P (x) and ∀x. Q(x): ∀x. P (x) (∀E). (shrink)

In this paper I present the strategy behind the proof-theoretic justification of logical inference. I then discuss how this strategy leads to the famous requirement that the inference rules for the logical constants should be in harmony. I argue that the proof-theoretic justification of the logical constants can be used to justify classical logic. To substantiate this I present a new normalisation theorem for first order classical logic involving Sheffer Stroke. The proof of this theorem can be modified to yield (...) a normalisation result for classical logic with conjunction, negation and the universal quantifier. (shrink)