Some Concerns Regarding Ternary-relation Semantics and Truth-theoretic Semantics in General Ross T. Bradyú La Trobe University, Melbourne, VIC, Australia <ross.brady@latrobe.edu.au> Abstract This paper deals with a collection of concerns that, over a period of time, led the author away from the Routley–Meyer semantics, and towards prooftheoretic approaches to relevant logics, and indeed to the weak relevant logic MC of meaning containment. Keywords: completeness deception, meaning discrepancies, proof-theoretic methods, Routley–Meyer semantics, truth-theoretic semantics 1 Introduction It is hoped that the concerns dealt with in this paper will help to round out the philosophical discussion around ternary relation semantics, which was the subject of the Third Workshop, held at the University of Alberta, Edmonton, Canada, during May 16–17, 2016, for which this paper was written. Whilst these concerns form a rather motley collection, the main point to be made is that proof theory and semantics have distinct interpretations, with special reference to disjunction and existential quantification. (See Section 3.1 below for the details.) One should especially note that the author supports the proof-theoretic interpretation over the semantic one, this contributing to the concern about semantics in general. (See Section 3.2 for this point.) Though the author has given some úI wish to thank the audiences of the Third Workshop, held at the University of Alberta, Edmonton, May 16–17, 2016, and the Australasian Association for Logic conference, held at La Trobe University, Melbourne, during June and July, 2016, to which this paper was presented. A special thanks goes to Kit Fine, Alasdair Urquhart, Arnon Avron, Mike Dunn, David Ripley and Lloyd Humberstone for their discussion and comments. Vol. 4 No. 3 2017 IFCoLog Journal of Logics and Their Applications Brady earlier presentations of these two distinct interpretations, this is the first time such material would appear in published form. Another major point is the importance of decidability in establishing a twovalued meta-logic, whilst completeness is of lesser value than the current literature espouses. (Sections 3.3 and 3.4 deal with these respective points.) This again covers new ground. 2 Some Concerns about the Routley–Meyer Semantics 2.1 The Complexity of Fine's Semantics for Quantified Relevant Logics Logics need to include quantifiers and lead into (non-logical) applications in order for logic to be applied and thus be a worthwhile study. The central value of logic is in its application to mathematics, computer science, science in general, and to familiar everyday arguments. However, sentential matters largely define the logic one is using, since the main dierentiation between logics occurs at the sentential level. The addition of quantifiers is more clear-cut and its other premises are determined largely by the (non-logical) concepts to which one is applying the logic. So, sentential logic is still a worthwhile study in itself, but one still should be able to indicate how such a logic would be extended into applications, which would pass through quantification. At the sentential level, the ternary-relation semantics of Routley and Meyer, culminating in their book [43], does have a somewhat bearable complexity, with its string of semantic postulates capturing the appropriate properties of the ternary relation R, and Priest in [39] sets out corresponding tree methods that can byand-large be used to determine validity or invalidity of sentential formulae. Bear in mind that some strong relevant logics such as R and T are undecidable at the sentential level. This result being due to Urquhart in [48], but nevertheless some weaker relevant logics such as RW, TW, DW and DJ are decidable (see Fine [26] and Brady [10, 11] and [15]). The undecidability for these strong logics does mean that there is a certain inner complexity in them. (For axiomatizations of the above logics, see Section 2.3 below.) However, when we pass to Fine's variable-domain semantics for quantified relevant logics in [28], there is a step up in complexity mainly due to the variability of domains from world to world. This complexity is so much so that there is a general lack of corresponding use in the literature to determine the validity or otherwise of quantified formulae. Further, there is also a general lack of research work into Fine's quantified semantics, with Mares' addition of the identity relation and his and 756 Some Concerns Regarding Ternary-relation Semantics . . . Goldblatt's alternative semantics being the main contributions the author is aware of. (See Mares [31] and Mares and Goldblatt [29].) Also, Priest in [40] sets out a tree method for the quantified relevant logic BQ and its familiar relevant extensions, and with identity, but for constant-domain semantics only. Without knowledge of completeness for a quantified logic such as B with respect to such a semantics, this tree method also works by-and-large, as it does for the strong sentential logics such as R in his [39]. Furthermore, one also has the task of interpreting Fine's semantics, leaving one with the two questions of what a semantics for a logic ought to look like and what the logical concepts of the connectives and quantifiers are. (More on this in Sections 3.1 and 4.1.) Recall too that Routley in [42] put forward the proposal for a constantdomain quantified semantics, but Fine showed that the logic RQ is incomplete with respect to this type of semantics. As far as the author is aware, this incompleteness is still an open question for weaker relevant logics such as DW or DJ, though this will seem doubtful when Section 3.4 is taken into account. It was at this point that the author started to become disillusioned with the ternary semantics in general, especially as I had spent a lot of time trying to make this constant-domain semantics work.1 Here, I was having diculty in establishing witnesses for existential quantification within a domain that is constant across worlds. The author is now of the view that in applying quantified inferential logic, the domain of quantification should be constant. It is understandable that for quantified modal logics that possible worlds might have diering domains from world to world, but this is not clear for practical non-modalized examples such as Peano arithmetic. Indeed, logical applications generally have fixed domains of objects, such as natural numbers or sets, and one should not have to vary such a domain when replacing classical logic by a supposedly superior logic. Further, in any proof theory with quantification, except maybe in a modal logic, it is understood that each quantifier is applied to the same domain, although sub-domains can be determined by a restricting predicate. (There will be some more on this point later in Section 4.1.) The author's general concern with complexity is as follows. Put oneself in the mind of a reasoner conducting a simple inference step and ask the question: what is the rationale or justification for the inference? Here, we are assuming that any complexity that does occur results from the transitivity of a sequence of inferences. One can understand if the reasoner says that he or she is preserving truth in that the truth of the consequent or conclusion follows, given the truth of the premises and/or antecedent. One can also understand if the reasoner says that he or she 1Indeed, this paper will sketch out the subsequent journey undertaken by the author over many years, although not in strict historical order. 757 Brady is preserving meaning through a meaning analysis of premises and/or antecedents. The author cannot think of any other criteria that could be going on in the mind of such a reasoner, except perhaps a combination of both, though many systems have been created and their semantics has been studied over the years. In the case of a combination however, one can reduce it to single inference steps involving only one of the two preservations. Further, such criteria need to be simple as such a reasoner is not going to embrace much complexity in making and justifying a single inference step. The logic governing the step would be clean and clear, based on well-understood concepts. (There is some complexity to follow, but the reason for it will be explained in each circumstance.) 2.2 The Lack of a Single Logical Concept Captured by the Routley– Meyer Semantics In a group paper Beall et al. [3], it was argued that the inferential concept captured by the ternary relation R of the Routley–Meyer semantics was that of conditionality. This is a broad concept intended by the above group of authors to accommodate the various logics which can be given such a semantics and this is very inclusive, ranging from B to R and beyond to classical logic, with very few logics missing out. However, this does not tell us what the specific inferential concepts pertaining to these logics are. Len Goddard verbally made the point at the time when the Routley–Meyer semantics was introduced in the early 1970s that the semantic postulates are just in one-one correspondence with the axioms. Essentially, his idea was that one could more-or-less determine the semantic postulate for a given axiom and vice versa. What he thought was needed here was a semantics that characterised a particular logic through a semantic rendition of a particular concept of inference. The problem for relevant logics is that there are far too many of them and, as such, there is a lack of definition in the concept of relevance. If we take relevance as meaning relatedness, which is its immediately intuitive concept, this is, by itself, not a suitable concept upon which to base a logic as it is too vague. Relevance, as determined in its sharper form by the variable-sharing property (if A ae B is a theorem then A and B share a sentential variable), has been taken as a necessary condition for a good logic, but not a sucient one, leaving a plethora of systems to consider. The strong relevant logics such as R, satisfying this property, are based on technical criteria such as the neatness in the presentation of their natural deduction systems rather than on a specific logical concept. (That natural deduction systems are more complex for logics weaker than R can be seen in Brady [6].) This lack of concept makes application dicult, as there needs to be some logical concept 758 Some Concerns Regarding Ternary-relation Semantics . . . prior to the non-logical applied concepts so that the application can be completed by embracing both logical and non-logical concepts. Historically, this diculty has borne out in a number of ways. Meyer tried to prove that the Disjunctive Syllogism rule, ≥A, A ae B ∆ B, was admissible for relevant arithmetic based on the logic R, but ultimately a counter-example was found (see Meyer and Friedman [36]). This is an example of what was seen as an important admissible rule of the logic R, not extending to arithmetic based on R. Furthermore and more clearly, Meyer showed that the irrelevant implication, x = y ae .p ¡ p, is derivable from the Extensionality Axiom in the form: x = y ae . x oe { x : p } ¡ y oe { x : p }, also based on R. This example shows up the diculty of maintaining relevance in an application, given that the variable-sharing property holds for this form of Extensionality Axiom when applied to free variables. (See Meyer [35] and [33] on relevant arithmetic and Brady [12] for Meyer's example from set theory.) So, one does need some further specification to fix upon a particular logic, which we will consider within the following section. 2.3 The Lack of Facility to Drop the Distribution Axiom in the Routley–Meyer Semantics As an answer to Section 2.2 and as stated in Section 2.1, there are essentially two key semantic concepts relating to logic, that of truth and meaning. These two concepts can be used to provide an understanding of inferential connectives and rules. Truthpreservation clearly applies to rules A ∆ B, these being meta-theoretic in nature and based on the notion of a deductive argument. (See Brady [23] for discussion of this, and also the relationship between this (classical) deduction and relevant deduction.) The material implication ∏ of classical logic is essentially truth-preservation, expressed as a connective, as can be seen from its truth-table. Furthermore, the relationship between the classical connective A ∏ B and the rule A ∆ B can be seen from their deductive equivalence, assuming that the Law of Excluded Middle (LEM), A‚≥A, and the Disjunctive Syllogism (DS), ≥A, A‚C ∆ C, both hold for the antecedent A. (We base the deductive equivalence on the basic system Bd, which is the logic B with the addition of the meta-rule: if A ∆ B then C ‚ A ∆ C ‚ B.) The inferential connective associated with meaning is an entailment, representing the containment of the meaning of the consequent in that of the antecedent. Such a logic, called MC, based on the connective ae representing meaning containment was introduced by Brady, after some tweaking which dropped the distribution axiom from an earlier version DJd, set out in Brady [12] and [18]. The logic DJd, was initially determined using 'set-theoretic containment' properties which are in evidence in its content semantics (see below in Section 4.1 for such content seman759 Brady tics). This was then modified to 'intensional set-theoretic containment' to form the distribution-less MC, as set out in Brady and Meinander [5], where MC was introduced. The axiomatisation of MC and also its quantificational extension MCQ are below. Indeed, there is a strong case made in Brady and Meinander [5] for dropping the distribution in axiom-form from such a logic, as distribution does not follow from the standard meanings of conjunction and disjunction. Although the problem with distribution was initially pointed out in a review of Brady [18] by Restall in [41], it was Schroeder-Heister in [45] who made it clear to the author that the introduction and elimination rules for conjunction and disjunction suced to uniquely specify these two concepts, i.e., without the addition of distribution. (See also SchroederHeister [44].) What Schroeder-Heister showed was the following. Let & and &Õ satisfy the introduction and elimination rules: A B A & B A B A &Õ B A & B A A & B B A &Õ B A A &Õ B B Then: A & B A &Õ B and A &Õ B A & B Thus, A & B and A &Õ B are equivalent and can be substituted in all contexts of the logic. The same sort of argument applies to A ‚ B and A ‚Õ B, where the introduction and elimination rules that apply to ‚ also apply to ‚Õ. Thus, we also have the following equivalence: A ‚ B A ‚Õ B A ‚Õ B A ‚ B So, the introduction and elimination rules uniquely specify standard conjunction and disjunction concepts. Anderson and Belnap in [2] indicated, for their natural deduction systems for strong relevant logics such as R, that distribution requires a separate rule, i.e., &‚, over and above the introduction and elimination rules for conjunction and disjunction. The separation of this rule is also required for logics weaker than R, as can be seen in Brady [6]. The logic MC is set out as follows: Primitives: ≥, &, ‚, ae. Axioms: 1. A ae A 2. A & B ae A 760 Some Concerns Regarding Ternary-relation Semantics . . . 3. A & B ae B 4. (A ae B) & (A ae C) ae . A ae B & C 5. A ae A ‚ B2 6. B ae A ‚ B 7. (A ae C) & (B ae C) ae . A ‚ B ae C 8. A ae ≥B ae . B ae ≥A 9. ≥≥A ae A 10. (A ae B) & (B ae C) ae . A ae C (conjunctive syllogism) Rules: 1. A, A ae B ∆ B 2. A, B ∆ A & B 3. A ae B, C ae D ∆ B ae C ae . A ae D Meta-rule: 1. If A, B ∆ C, then D ‚ A, D ‚ B ∆ D ‚ C This two-premise meta-rule is deductively equivalent to the one-premise metarule 'if A ∆ B then C‚A ∆ C‚B', together with the distribution rule 'A&(B‚C) ∆ 2Over the years, there has been some discussion as to whether A ae A ‚ B and B ae A ‚ B should be included as axioms in a logic based on meaning containment. Indeed, Kit Fine raised this issue in Edmonton and we exchanged a series of e-mails on this topic. The objections to these axioms, in accordance with Analytic Implication, first introduced by Parry (see his account in [38]) and more recently taken up by Fine (see his re-publication in [27]), are based on the respective lack of B in A and of A in B in these axioms. However, I contend that logic is a representation of the meanings of the connectives and quantifiers and other non-logical concepts, expressed in a logical language. This language is only a vehicle for transmitting the logical meanings and one must thus look into the meaning of A ‚ B as an 'either . . . or' rather than how it is expressed syntactically. A (alternatively B) clearly adds to the meaning of 'either A or B' by creating the witness, establishing that the meaning of A ‚ B is contained within A (and within B). Further, Lloyd Humberstone pointed out in discussion that A ¡ A & (A ‚ B) holds in MC (as originally pointed out by Dunn) and if the right hand equivalent is substituted for the first A in A ae A ‚ B then it becomes A & (A ‚ B) ae A ‚ B, which is then an instance of A & B ae B, which is not under contention. This then has the eect of linking A ae A ‚ B with its De Morgan dual A & B ae A. 761 Brady (A&B)‚(A&C)'. Thus, distribution in rule-form still holds in MC, with the inclusion of MR1. For the general purposes of this paper, we extend the logic MC to MCQ with the following quantificational additions: Primitives: ', ÷. a, b, c, . . . range over free variables. x, y, z, . . . range over bound variables. Terms s, t, u, . . . can be individual constants (when introduced) or free variables. Quantificational Axioms: 1. 'xA ae At/x, for any term t. 2. 'x(A ae B) ae . A ae 'xB 3. At/x ae ÷xA, for any term t. 4. 'x(A ae B) ae . ÷xA ae B Quantificational Rule: 1. Aa/x ∆ 'xA, where a is not free in A. Meta-Rule: 1. If A, Ba/x ∆ Ca/x, then A, ÷xB ∆ ÷xC, where QR1 is not used to generalize on any free variables occurring in the A nor in the Ba/x of the rule A, Ba/x ∆ Ca/x. This restriction on QR1 also applies to the rule A, B ∆ C of MR1 for the sentential component. Note that the existential distribution rule, A & ÷xB ∆ ÷x(A & B), follows from R2 and QMR1. However, as with intuitionist logic, the universal distribution rule, 'x(A ‚ B) ∆ A ‚ 'xB, fails, as the universal quantifier ' and the disjunction ‚ are essentially the same for intuitionist logic as for MCQ, since they are both constructively interpreted concepts. Largely, the sentential distribution axiom is an add-on, except where it falls into place in extensional contexts such as classical logics. Routley–Meyer semantics, set in classical meta-logic, has no means at its disposal of dropping distribution, without some further complexity, as can essentially be seen from Dunn and Allwein [1] on linear logic. Thus, the Routley–Meyer semantics cannot be used as it stands for the logic MC of meaning containment. For proof theory however, the lack of distribution generally simplifies the rules and makes results easier to prove. For the Fitch-style natural deduction systems, which can be seen in Anderson and Belnap [2] and in Brady [6], there is an additional distribution rule &‚, over and above the introduction and 762 Some Concerns Regarding Ternary-relation Semantics . . . elimination rules for conjunction and disjunction. This rule would be removed for a distribution-less system. For Gentzen systems, the lack of distribution usually allows one to have only one structural connective instead of two, as can be seen from Dunn's Gentzenization of R+ in Anderson and Belnap [2], which has two structural connectives. Compare this with Brady [13] and [14], where there is only one structural connective required in the final Gentzen systems for a range of distribution-less contraction-less logics, with the added bonus of decidability at the quantificational level. Thus, whilst the lack of distribution would add significant complexity to the Routley–Meyer semantics when attempted, such a lack would considerably simplify the standard proof theories. So, this lack of distribution essentially puts paid to the standard ternary semantics and we will need to consider other structures to provide such a semantics and to enable invalidity of formulae and other results to be shown. Here, the structures need not be the same as these two functions do dier, unlike the Routley–Meyer semantics and other semantics that attempt to play both the role of semantics and the role of being a technical vehicle for the proof of a range of results. (There is further discussion on this point in Section 4.3.) 3 Some Concerns about Truth-theoretic Semantics in General 3.1 The Discrepancy in the Meanings of Disjunction and Existential Quantification The most telling dierentiation between proof theory and semantics is the discrepancy in the meanings of disjunction and existential quantification. Both disjunction and existential quantification are characterised by the expression 'at least one of . . . ', the disjunction applying to two sentences and the existential quantification applying to a predicate expression. The issue is whether this means that there is a witness disjunct and a witness existential instantiation or whether there need not be such witnesses. Note that the priming property, 'if A ‚ B then either A or B' requires a disjunctive witness and the existential property, 'if ÷xA then Aa/x, for some a' requires an existential witness. In standard semantics, which are all based on formula-induction, there must be such witnesses, as seen by the Henkin-style completeness proofs where a canonical model is built up so as to ensure that all such witnesses are in place. This is achieved by constructing the canonical model using an enumeration of formulae and, as each formula is selected, a decision is made on whether to admit it to the constructed 763 Brady model or not, so as to ensure each required witness is present. In his completeness proof for the predicate calculus in [30], Henkin added existential witnesses in the construction of maximally consistent sets based on an initial consistent set. Since the LEM holds in classical logic, we can alternatively replace maximal consistency (ensuring negation-completeness) with disjunctive closure, i.e., requiring that each disjunction be witnessed by one of its disjuncts, yielding negation-completeness in particular. Indeed, disjunctive closure occurs in the completeness proof for the Routley–Meyer semantics, and this can be used for classical logic as well with some additional semantic postulates. (See Chapter 4 of Routley, Meyer, Plumwood and Brady [43].) Fine's semantics in [27] makes this point clearer. There, Fine uses theories to capture conjunction and implication, whilst prime theories are used to capture disjunction and negation. (Fine used the term 'saturated theories'.) Thus, Fine separated theories and prime theories in his semantics, instead of bundling them all into worlds, which are all prime, as in the Routley–Meyer semantics. This emphasises the fact that it is negation and disjunction that minimally require priming. The reason negation is aected here is largely because of De Morgan's Laws which relate disjunction with conjunction through negation. In proof theory however, there is no requirement for such witnesses. Consider the ‚E and ÷E rules of Fitch-style natural deduction below, where a general argument to a common conclusion suces, whether for each disjunct or for any possible instantiation. ‚S: If A ‚ Ba, A ae Cb and B ae Cb, then Cafib. ÷E: If ÷xAa and 'x(A ae B)b, then Bafib. Both these rules can have a restriction on the index sets a and b, in accordance with the particular logic involved. (See Brady [6] for details of this.) This is appropriate as hypotheses can be disjunctive or existential, where no specification of a witness would be required. An assumption of A ‚ B need not spell out which disjunct applies and an assumption of ÷xA need not spell out which instantiation of x in A applies. This is quite appropriate as A ‚ B or ÷xA can be assumptions or premises of an argument, where it may not be part of such an assumption to name or imply a particular disjunct or a particular existential instantiation. So, there is a discrepancy in the meaning of disjunction and existential quantification between the semantics and this proof theory (and other proof theories follow suit). And, it does seem overly restrictive to insist on a witness disjunct or existential instantiation that may not exist in many cases. 764 Some Concerns Regarding Ternary-relation Semantics . . . It depends too on one's view of logic here, i.e., whether logic is about arguments from premises to conclusions or about worlds specified by formula-induction based on atoms. 3.2 What is Logic About? To attempt to answer this last question, we need to briefly examine the classical account and its influence on worlds semantics. There, logic is about propositions which are either true or false, but not both. This essentially locks in classical twovalued logic, with its truth-tables determining the truth-values of the connectives and hence its subsequent analyticities. It relies on a body of truths, initially taken from the real world. Falsity is just a fall-back position for sentences that are not true, since there is no other value they can take. Worlds are built up from atomic propositions by using a formula-induction process, which then extends to the universal and existential quantifiers. The objects of the domain of quantification initially consist of the existing things of the real world. As Quine said "To be is to be the value of a bound variable." In such a case, logic is abstracted from the real world. However, this domain can be extended in various ways by using truth-bearers. It is this world semantics that is taken to be the semantics of the classical predicate logic, and extended to possible worlds by Kripke for modal logics, using binary relations between these worlds. Then, Routley and Meyer, using ternary relations, extended this style of semantics to include relevant implications and entailments, but importantly the worlds can be impossible as well as possible. (Initially, such worlds were called set-ups by Routley to distinguish them from possible worlds.) And, people like David Lewis have attempted to give some reality to possible worlds whilst Meinong and Priest attempted to give some sort of reality to impossible worlds. Nevertheless, such semantics is still based on worlds of a sort, which are determined using formulainduction, based on atoms, but incorporating binary or ternary relations between worlds, largely to capture modal and inferential concepts, whilst maintaining the true-false dichotomy. One should note that for the Routley–Meyer semantics, the ú-function is used, under the Australian Plan, to maintain this true-false dichotomy, despite its negation being non-classical. The main alternative is to take logic to be about the proof of conclusions from premises. This broadens logic to include arguments and concepts that do not fit the worlds picture, i.e., as considered in Section 3.1 above, they may include witness-less disjunctions and existentials. In the case of classical worlds, before one can even proceed with a piece of reasoning, every question must have a yes-or-no answer in order to establish the two values, truth and falsity. In most practical reasoning, not every question is answered, though allowances are made for this in the Routley–Meyer 765 Brady semantics through the use of their ú-function but not in Kripke semantics. Nevertheless, Routley–Meyer semantics still requires each disjunction to have a witness, and an extension of the semantics to include quantifiers over a constant domain would still require every existential quantification to have an instantiation. Further, a proof account does attempt to capture the logical and non-logical concepts being dealt with in its axioms, premises and rules. However, a concept may not be completely captured in the logical system that underspecifies it, giving rise to negation-incompleteness. On the other hand, concepts may sometimes be overspecified in a logical system, giving rise to contradictions, but here we generally try to eliminate them by removing a conceptual clash or tightening up the concepts so that they are not overspecified. (Brady [24] and [25] has some recent discussion on this point.) This attempt to capture concepts axiomatically is, we believe, at the heart of logic and the worlds approach is too restrictive as not all logical concepts precisely fit the worlds picture. Indeed, most logical reasoning proceeds without all questions being answered and without all witnesses being determined in advance. 3.3 What is the Meta-logic? What is not generally realized is that a proof-theoretic view of logic requires one to review the meta-logic. Firstly, the meta-logic should be the same logic as that used for the object language, specialised to that logic which applies to formal systems. Following on from Section 3.2, in the classical account, the meta-logic would be classical as it is pre-determined by the nature of propositions, regardless of whether they apply in the object theory or its meta-theory. This carries over to the Kripke semantics for classical modal logics as well. For the Routley–Meyer semantics, even though negation can be non-classical, the use of the Routley ú enables the metatheory to be two-valued in that each valuation in the semantics can only take the values T and F. So, for such semantics as these, classical meta-logic is universally used. Part of the reason for this too is that formalized logic is taken to be an object of mathematical study and that mathematics uses classical logic, having done so for at least a century. Whilst this is hard to shift, one should consider logic seriously, for its own sake, and hence apply it in accordance with its own principles to metatheory and to mathematics generally, despite the fact that more work is needed in this process. We now consider the case where logic is about proof. Here, decidability is important for a classical meta-logic as any undecided formula would clearly amount to a proof-gap, which would then become a truth-value-gap for the meta-logic. This would make the meta-logic three-valued with respect to proof, given the formal system is not contradictory regarding proofs. Such a contradiction would require a 766 Some Concerns Regarding Ternary-relation Semantics . . . formula to be both provable and not provable, and we would assume this to be not so, on the grounds that a formal system is a conceivable concept, with 'not provable' at least lying within the classical fall-back position of 'non-proof'. A decidable logical system would then have a classical two-valued meta-logic, as each formula could be either proved or its non-proof be established as not provable. However, a problem here is that some strong relevant logics such as R, E and T are undecidable even at the sentential level (see Urquhart [48]). Nevertheless, the logic DJd, which is of some related interest, is decidable at the sentential level (see Fine [26] and Brady [15] and [16]). And, the logic MC is decidable using normalised natural deduction, as sketched in Section 4.3, whilst its quantified logic MCQ has good prospects for being decidable. However, this latter result is still work to be completed. 3.4 The Deception of Completeness Semantic completeness is deceptive in that it fails for many applied logics and holds mainly for pure logics and, as argued in Section 2.1 above, logics need to be applied to be worthwhile. Soundness, however, is not a problem and so we do focus on completeness. If one considers the classical semantics for predicate logic, for example, completeness is proved in Henkin [30]. In the application to Peano arithmetic, assuming consistency, completeness will fail, due to Gödel's first theorem. In order to make such a Henkin-style completeness proof work for standard truth-theoretic semantics for a quantified logic, one would need an infinite supply of existential witnesses, which may not be available if one is focussed on a specific domain as one often is for applications, where a standard model is invoked. Consider Peano arithmetic with its standard domain of natural numbers, where one cannot add an infinite number of witnesses that may be needed over and above the natural numbers. That is, one cannot guarantee that a given domain is adequate for all the witnesses needed in a completeness proof. Even for disjunctive witnesses, one may need to add disjuncts that may be too specific for the concepts that are being captured in some other applications. A case here would be a concept based on an unwitnessed disjunctive property. So, logics need to be applied and completeness can quite often fail for such applications. To clarify this, the dierence between pure and applied logics is that standard models are used in applications that have domains specific to the application. Pure logics, on the other hand, use all models that are appropriate for the generality of the connectives and quantifiers. This then provides sucient generality for completeness to be proved using disjunctive and existential witnesses. Further, as we saw in Section 2.1, there are diculties even for the pure quantified relevant logics to be 767 Brady complete with respect to constant-domain semantics, due to this need for existential witnesses, and constant-domain semantics is appropriate for applications generally. This would then reduce the main completeness results to the sentential level for such logics, which reduces their usage even further. As seen from Section 3.3 above, decidability is important for all logics, so that they can have a classical meta-logic and indeed this is more important than completeness that can easily fail above the sentential level. In operating applied systems such as arithmetic, one needs to go back to the mathematical-style of proof, which consists of a Hilbert-style axiomatization, with some use of natural deduction to make deductions easier and more perspicuous. Semantical methods, such as truth-trees, are not of much value here. So, the use of completeness is largely limited to pure logics and of major value for sentential logics at that. Completeness, together with soundness, enables one to say that proof theory and semantics are dierent representations of the logic involved. However, logic is about capturing concepts, and proof theory and semantics do dier conceptually in their interpretation of disjunction and existential quantification, as argued above in Section 3.1. Further, we favoured proof theory in Section 3.2, as truth-theoretic semantics does not capture the connectives and quantifiers precisely, and prooftheoretic semantics, as studied for example by Schroeder-Heister in [44] and [45], could oer a better capture of these concepts. 4 Concluding Directions In conclusion, we examine two alternatives to standard semantics, followed by discussion of some proof-theoretic systems. 4.1 Content Semantics Content semantics, as set out in Brady [12] and [18], oers a good capture of logical concepts. The contents used are logical contents that are best understood as analytic closures. One considers a sentence, engages in repeated meaning analysis of concepts from the sentence until such a process closes, and the set of sentences thus obtained is the analytic closure of that initial sentence. This analytic closure of the sentence is then its logical content, which is a deductively closed set. We can then quite reasonably use this to capture an entailment A ae B, based on meaning containment by simply taking its content as that of the set-theoretic containment statement of the content of the consequent B in the content of the antecedent A. However, more recently after dropping distribution in Brady and Meinander [5], we have had 768 Some Concerns Regarding Ternary-relation Semantics . . . to modify this set-theoretic containment to reflect the absence of distribution, as argued in Section 2.3. Now, we use the term 'intensional set-theoretic containment' instead, in order to represent set-theoretic containment but narrowed down to reflect the intensional meanings of conjunction, disjunction and the two quantifiers, in particular. We now consider the contents of the connectives and quantifiers. The content of a conjunction of two sentences is the closure of the set-theoretic union of the two contents. The reason the closure is needed is that the two sentences may interact in producing conclusions that are not provable from either of the two sentences individually. The content of a disjunction is simply the set-theoretic intersection of their respective contents, whilst the content of an entailment is as described above. Negations can be dealt with using the dual concept of range, related to contents via De Morgan properties, but below we use the simpler ú-function on contents. (Note that in Brady [18], it was seen that this ú-function relates ranges and contents through its definition, but in the final analysis the ranges can be dropped in favour of the ú.) The contents of the two quantifiers are similar unions and intersections to those of conjunction and disjunction, but are set unions and intersections where the set is controlled by the individual predicates used to generate them. We also have to take bound variables into account. With apologies, the quantificational extension of the content semantics is omitted which, though understandable in its interpretation, does add quite some complexity, due to the predicates and the bound variables. However, as discussed below and also in Section 4.3, being a semantics of meaning rather than truth, it is not so clear cut in its determinations and hence not so able to act as a vehicle for wide-ranging technical results. The content semantics for the logic MC is set out as follows, as in Brady [18], but taking into account the tweaking of the logic occurring in Brady and Meinander [5] and the adopting of Mares' treatment of the closed union as a content of the set-theoretic union of two contents in his [32].3 A content model structure (c.m.s) consists of the following 4 concepts: T, C, ú, c, where C is a set of sets (called contents), T "= ÿ, T TM C (the non-empty set of all true contents), ú is a 1-place function on C (the ú-function on contents), and c is a 1-place function from containment sentences, c1   c2, and also unions c1 fi c2, concerning contents c1 and c2 of C, to members of C, subject to the semantic postulates p1– p15, below. The concepts fl, fi, = and  , are taken from the background set theory, fi and fl being a 2-place functions on C (the union and intersection of contents, 3Mares in his [32, on p. 202], expresses this union as c(c1 fi c2), where c is the same content operator as used for c1   c2 but applied to the set-theoretic union c1 fi c2. This is preferable to the author's treatment in [12] and [18], as it reinforces the use of standard set-theoretic concepts within the content semantics. 769 Brady respectively), = being a 2-place relation on C (identity), and   being a 2-place relation on C (content containment). The semantic postulates are: p1. c(c1 fi c2)   c1, c(c1 fi c2)   c2 p2. If c1   c2 and c1   c3, then c1   c(c2 fi c3). p3. c1   c1 fl c2, c2   c1 fl c2 p4. If c1   c3 and c2   c3, then c1 fl c2   c3. p5. cúú1 = c1 p6. If c1   c2, then cú2   cú1. p7. If c1   c2 and c1 oe T , then c2 oe T . p8. If c1 oe T and c2 oe T , then c(c1 fi c2) oe T . p9. If c1 fl c2 oe T , then c1 oe T or c2 oe T . p10. c(c(c1   c2) fi c(c2   c3))   c(c1   c3) p11. c(c(c1   c2) fi c(c1   c3))   c(c1   c(c2 fi c3)) p12. c(c(c1   c3) fi c(c2   c3))   c(c1 fl c2   c3) p13. c(c1   c2)   c(cú2   cú1) p14. c(c1   c2) oe T i c1   c2. p15. If c1   c2, then c(c3   c1)   c(c3   c2) and c(c2   c3)   c(c1   c3). An interpretation I on a c.m.s. is an assignment, to each sentential variable, of an element of C. An interpretation I is extended to all formulae, inductively as follows: (i) I(≥A) = I(A)ú (ii) I(A & B) = c(I(A) fi I(B)) (iii) I(A ‚ B) = I(A) fl I(B) (iv) I(A ae B) = c(I(A)   I(B)) 770 Some Concerns Regarding Ternary-relation Semantics . . . A formula A is true under an interpretation I on a c.m.s. M i I(A) oe T . A formula A is valid in a c.m.s. M i A is true under all interpretations I on M . A formula A is valid in the content semantics i A is valid in all c.m.s. Soundness (if A is a theorem of MC then A is valid in the content semantics) follows readily and completeness (if A is valid in the content semantics then A is a theorem of MC) follows by the usual Lindenbaum method for algebraic-style semantics, but here there is a slight dierence. In constructing the canonical models, instead of taking equivalence classes of formulae as the contents, we put the content [A] of A as { C : A ae C oe T Õ }, where T Õ is constructed as a prime extension of the set of theorems which does not include a non-theorem B. This essentially means that these canonical contents are closed under entailment, i.e., they are analytic closures of the sentence (or sentences) involved, since the set T of theorems is already prime, due to the logic MC being metacomplete (see Section 4.2). Since entailments here are understood as meaning containments, closure under entailment is closure under meaning containment and hence closure under the analysis of the meanings of words. Thus, this semantics captures the meaning of the logical concepts in that it has transparency of concepts, shown by using the real set theoretic concepts of union, intersection, identity and containment in setting up the semantics. With the use of ranges to capture negation, this semantics is a "real" semantics, this being quite dierent from the use of semantic primitives with postulates, which have completely general interpretations restricted only by the postulates themselves, as occurs in the algebraic-style of content semantics in Brady [8] and [9]. Unlike truth-theoretic semantics, this semantics requires some understanding of content containment to work the semantics in showing invalidity (as was pointed out by Restall in discussion). As such, it would reject the axiom-form of distribution, for example. Further, this content semantics represents the logics MC and MCQ alone, unlike the author's earlier contents semantics of [8] and [9], which were quite wideranging, generally applying to logics in the range from BB right through to classical logic. 4.2 Metavaluations Metavaluations combine features of proof theory and semantics to yield a technique that can produce results that would be hard or impossible for a truth-theoretic semantics to emulate. In particular, it can be used to prove the simple consistency of Peano arithmetic using finitary methods, for a quantified version of the logic MC (see Brady [21]). Though metavaluations are set up using truth-functions, it is essentially a proof theory, using formula-induction without worlds to capture that part of proof that behaves in a formula-inductive fashion. This inductive part of proof focuses on 771 Brady that part of a formula that sits between maximal entailment sub-formulae and the whole formula in a formula tree, i.e., the technique does not enable one to access any sub-formula inside a maximal entailment sub-formula. However, there is an exception for negated entailments where, for the so-called M2-metavaluations (see below), the metavaluation is essentially expressed in terms of its antecedent and its negated consequent. Meyer introduced metavaluations in his [34] where he showed that the metavaluation technique can be very generally applied to positive logics, both sentential and quantified. However, the technique only works for certain logics once negation is added, as shown by Slaney in [46] and [47]. Once soundness and completeness is derived, with or without negation, such a logic is called a metacomplete logic. Slaney in [47] introduced two types of metavaluation, M1 and M2, depending respectively on whether there are no negated entailment theorems in the logic or whether a negated entailment is a theorem if and only if its antecedent and its negated consequent are both theorems. Indeed, the corresponding M2-logics have A, ≥B ∆ ≥(A ae B) as a derived rule, with the converse as an admissible rule, where for corresponding M1-logics this derived rule is absent from the logic. MC and MCQ are M1-metacomplete logics, and as such contain no negated entailment theorems. Thus, they are entailment-focussed logics. Slaney's metavaluations v and vú are as follows, with my symbolism and a slightly simplified layout: (i) v(p) = F ; vú(p) = T , for sentential variables p. (ii) v(A & B) = T i v(A) = T and v(B) = T ; vú(A & B) = T i vú(A) = T and vú(B) = T . (iii) v(A ‚ B) = T i v(A) = T or v(B) = T ; vú(A ‚ B) = T i vú(A) = T or vú(B) = T . (iv) v(≥A) = T i vú(A) = F ; vú(≥A) = T i v(A) = F . (v) v(A ae B) = T i „ A ae B, if v(A) = T then v(B) = T , and if vú(A) = T then vú(B) = T . vú(A ae B) = T , for M1-logics. vú(A ae B) = T i, if v(A) = T then vú(B) = T , for M2-logics. We add the quantificational metavaluations, as follows: (vi) v('xA) = T i v(At/x) = T , for all terms t. vú('xA) = T i vú(At/x) = T , for all terms t. 772 Some Concerns Regarding Ternary-relation Semantics . . . (vii) v(÷xA) = T i v(At/x) = T , for some term t. vú(÷xA) = T i vú(At/x) = T , for some term t. The following key properties are then derivable (see Meyer [34] and Slaney [46] and [47]): Completeness: If v(A) = T then „ A, for all formulae A, and hence if vú(A) = F then „ ≥A. Consistency: If v(A) = T then vú(A) = T . Soundness: If „ A then v(A) = T , and hence if „ ≥A then vú(A) = F . Metacompleteness: „ A i v(A) = T , and hence „ ≥A i vú(A) = F . Priming Property: If „ A ‚ B then „ A or „ B. Negated Entailment Property: Not-„ ≥(A ae B) (for M1-logics); „ ≥(A ae B) i „ A and „ ≥B (for M2-logics). Existential Property: If „ ÷xA then „ At/x, for some term t. The metavaluational technique can reject some non-theorems of the stronger metacomplete logics for which the technique applies. In particular, it can be used to reject the LEM, A ‚ ≥A, and the Modus Ponens Axiom, A & (A ae B) ae B in the logic MC. Still to be researched is the good prospect of further metavaluations affecting negated entailments in dierent ways, which would reject other non-theorems in particular metacomplete logics. (This possibility is flagged in Slaney [46].) As stated above, Peano arithmetic can be shown to be simply consistent using finitary methods using metavalutions and this proof relies heavily on specific properties of metavaluations that cannot be duplicated using standard truth-theoretic semantics. (Here, in accordance with finitary methodology, mathematical induction is incorporated into the formulation of the metavaluations for the quantifiers, so as to ensure that all universal formulae can be proved through use of mathematical induction.) The specific properties of metacomplete logics can also be used to establish the simple consistency of naive set theory, the proof of which uses a single transfinite sequence of metavaluations (see Brady [22] for details). 4.3 Proof-Theoretic Methods More familiar proof-theoretic methods include cut-free Gentzen systems and normalized natural deduction systems. Both of these can take advantage of the lack of distribution to make simplifications. Of the three cut-free Gentzen systems set out in Brady [18, pp. 93–140], the best one for our purposes would be the left-handed cut-free Gentzen system for the logic DJ, which is MC + A&(B ‚C) ae (A&B)‚ (A&C) ≠ MR1, i.e., essentially adding back the distribution axiom. Such a Gentzen system just consists of structures, to which an initial axiom together with rules apply. As it stands, the system has 773 Brady four structural connectives, and one would expect to delete the extensional and the corresponding k-intensional ones, with the removal of distribution as required for MC. That would leave us with what are called the i-intensional and j-intensional structural connectives, the i-intensional one ':' being interpreted as cotenability ü, defined as A ü B =df ≥(A ae ≥B), and the j-intensional one ';' being interpreted as fusion '¶', axiomatically introduced by the two-way rule, A ¶ B ae C ... A ae . B ae C. The j-intensional connective can be inverted around the standard iintensional connective, much as Belnap did in his [4] paper on Display Logics, with each derivable structure having an i-intensional connective as its main structural connective, which serves in lieu of a turnstile. To illustrate, these inversion rules, for structures –, - and ", are as follows (see Brady [18, p. 133]): (Ii) – : (- : ") / (– ; -) : " (Ij) – : (- ; ") / (" : –) : - Further, as stated in Brady [16, pp. 350–351], quantifiers can be added to this Gentzen system in a fairly standard way. However, there is a problem with proving decidability of DJ with this system in that the rule, (CSij) (– ; -) : (– ; ") / – : (- : "), representing conjunctive syllogism, is a form of contraction for the structure –, with the structures - and " as parametric. Though decidability of DJ has been proved in Fine [26], and in Brady [15] and [16] by a semantic method, it remains to be proved in this setting. It should be noted that this semantic method as it stands, cannot be used once the distribution axiom is removed from DJ to form the logic MC. In any case, Gentzen systems are rather stylized and are good if suitable systems are available for the logics of interest. This leads us to our preferred proof-theoretic method of representing the logics MC and MCQ or indeed other similar logics, that is, by normalized natural deduction systems. This is because they would capture reasoning most closely, roughly as it would occur in practice in closely reasoned contexts and, due to normalisation, in a way that proceeds straight to the point of the conclusion without detouring in and out of connectives and quantifiers. In Brady [19], there is such a system for DW, which is DJ ≠ (A ae B) & (B ae C) ae .A ae C. This would need further work to make it suitable for MC in not only removing the distribution axiom but also adding conjunctive syllogism. Another version of normalized natural deduction, called 'Free Semantics', appears in Brady [20], where, in the process of establishing a semantics based on natural deduction, a normalized version of that is given for the logic LDW, which is DW without the distribution axiom. Here, we would need to add to the restrictions on the T ae E rule to embrace conjunctive syllogism, i.e., we add case (iii) to T ae E (i) and (ii) below. So, in Brady [20], the logic MC is covered as well as LDW, giving a normalised natural deduction system for MC in the process of establishing such a "free semantics." 774 Some Concerns Regarding Ternary-relation Semantics . . . We set up the following natural deduction system MMC for the logic MC. The system MMC is a modified natural deduction system that is set up as a preliminary system so that normalization can then take place. MMC is somewhat simpler, but we will subsequently indicate what is needed for this normalisation process. MMC is taken from Brady [19], which contains a normalized natural deduction system for the logic DW, but we make a slight simplification to remove distribution and we also extend it to include conjunctive syllogism, yielding a system for MC. Reference to this normalised natural deduction system is made in Brady [20], but there the principle focus was on tableau and reductio systems for the logic LDW rather than that for MC. We now present the rules of MMC, which is a Fitch-style natural deduction system, set out in the manner of Anderson and Belnap [2], but with modifications to help pin down the structure of it to suit the logic in hand. As part of this process, we use signed formulae TA and FA instead of a formula A, and structure them inductively as follows. (1) If S is a sign T or F , and A is a formula then SA is a structure. (2) If – and - are structures then (–, -) is a structure. Each whole structure has a single index set, which is of one of the two types: ÿ or a complete set of natural numbers { j, . . . , k }, which is a finite set of natural numbers in order with no numerical gaps. Structures are to be understood disjunctively and threads of proof within a subproof are obtained by following the signed formulae through in a particular position within a structure, just like a subproof within the subproof. (These threads of proof are defined in detail on [19, pp. 40–42], except, to remove distribution, one needs to remove the concept of a thread of proof extending another thread of proof, but the linkage between the previous thread of proof and the its continuation after the removal of these extended threads of proof remains. See [20, p. 522] for details of this.) That is, threads act as mini-subproofs, but without introducing a new index in the process as occurs in Anderson and Belnap [2]. Hyp. A signed formula of the form TH may be introduced as the hypothesis of a new subproof, with a subscript { k }, where k is the depth of this new subproof in the main proof. (Depth is defined as on p. 70 of Anderson and Belnap [2], but is called 'rank'. Also, see Brady [7] for 'depth relevance'.) Any hypothesis thus introduced must subsequently be eliminated by an application of the rule T ae I below. T ae I. From a subproof with conclusion TBa on a hypothesis TA{ k }, infer TA ae Ba≠{ k } in its immediate superproof, where a = { j, . . . , k } and either: (i) a ≠ { k } = ÿ with j = k = 1, or 775 Brady (ii) a ≠ { k } = { j, . . . , k ≠ 1 } with k Ø 2, 1 AE j AE k ≠ 1. The conclusion and hypothesis need not be distinct in (i). In both cases, TA ae B can also occur inside a structure, within a thread of proof. T ae E. From TAa and TA ae Bb, infer TBafib. (Direct version) From FBa and TA ae Bb, infer FAafib. (Contraposed version) Whilst TAa (or FBa) and its conclusion TBafib (or FAafib) are located in a proof P , either TA ae Bb is in the main proof or it is located in P 's immediate superproof, in accordance with the proviso below. T ae E carries the proviso that either: (i) b = ÿ, in which case a fi b = a, or (ii) a = { k }, k Ø 2, b = { j, . . . , k ≠ 1 }, 1 AE j AE k ≠ 1, in which case a fi b = { j, . . . , k }, or (iii) a = { j, . . . , k }, k Ø 2, b = { j, . . . , k ≠ 1 }, 1 AE j AE k ≠ 1, and hence a fi b = { j, . . . , k }. We say that T ae E is applied to a proof containing TA ae B into a proof containing TA (or FB) and TB (or FA). Such applications of T ae E (ii) must be made en bloc (into a proof) to all the signed formulae of a (whole) structure, thereby, maintaining its common index set. However, T ae E (iii) can be subsequently applied singly, i.e., to a single thread of proof, with the following exception. For T ae E (iii) to be applied for the first time into a thread of proof, it must also be applied to its adjacent thread(s) of proof. (See F & E and T ‚ E below for adjacent threads of proof. Also, F & E and T ‚ E can initiate further adjunct pairs to which T ae E (iii) would also be applied in this case.) Subsequent applications of T ae E (iii) into these threads of proof can then be made singly. T≥I. From FAa, infer T≥Aa. T≥E. From T≥Aa, infer FAa. F≥I. From TAa, infer F≥Aa. F≥E. From F≥Aa, infer TAa. T & I. From TAa and TBa, infer TA & Ba. (all applied within the same thread) T & E. From TA & Ba, infer TAa. From TA & Ba, infer TBa. F & I. From FAa, infer FA & Ba. From FBa, infer FA & Ba. F & E. From FA & Ba, infer (FAa, FBa). (introducing an adjacent pair of threads) 776 Some Concerns Regarding Ternary-relation Semantics . . . T ‚ I. From TAa, infer TA ‚ Ba. From TBa, infer TA ‚ Ba. T ‚ E. From TA ‚ Ba, infer (TAa, TBa). (introducing an adjacent pair of threads) F ‚ I. From FAa and FBa, infer FA ‚ Ba. (all applied within the same thread) F ‚ E. From FA ‚ Ba, infer FAa. From FA ‚ Ba, infer FBa. , E. From SAa, SAa, infer SAa. (eliminating an adjacent pair of threads) A formula A is a theorem of MMC i TAÿ is provable in the main proof (with a null index set). To convert MMC into the normalized natural deduction system NMC, we need to be able to contrapose an entire subproof in the process, and to do this we distinguish T and F -subproofs, introduce two new rules, F ae I and F ae E, which are contraposed versions of the corresponding T ae E and T ae I rules, interchange the signs T and F , and also interchange each thread with a corresponding strand. These strands are introduced in a similar way to that of threads but through T & E and F ‚E and eliminated through T &I and F ‚I. Thus, these strands are conjunctively separated, in a similar way to the separation of threads by disjunction. (See Brady [19] for further details about how all this is done.) As in Brady [19], any formula instance B occurring in a normalized proof of a formula A is a subformula of A, and the index set a of such a formula instance B lies in a subproof whose depth, max(a), is equal to the depth of B in A. (We take max(ÿ) to be 0 and the depth of the main proof to be 0, to make this identity work.) Thus, using these properties, decidability can be shown for MC, as it is for DJ in Brady [17], for DW in Brady [19] and for LDW in Brady [20]. However, the quantificational logic MCQ still needs a normalised natural deduction system, and this still needs to be researched. 4.4 In Conclusion In reference to the diering interpretations of proof theory and semantics, as presented in Section 3.1, we conclude the discussion by considering two related pairs of concepts that need separating: truth and meaning, on one hand, and semantics and technical systems used for proving results, on the other. The content semantics shows us that meaning does not need to be expressed using truth-conditions, and this real semantics expressing the meanings of the logical words is not necessarily ideal for the proof of results, as it may not have the sharpness required to produce good technical results. 777 Brady Truth and meaning drive dierent inferences: deductive inference and meaning containment. Deductive inference preserves truth, but is represented by a rule '∆', as it concerns deduction within the formal system as a whole, whilst meaning containment is represented by a connective 'ae', relating two sentences. (See Brady [23] for discussion on this.) It is instructive in this regard to examine negated inferences. Truth-preservation can be easily falsified when the antecedent or premise is true and the consequent or conclusion is false. It is not so easy to falsify meaning containment and there are dierent positions one can take on this. This can be clearly seen by considering the M1and M2-metavaluations, where the corresponding M1logics have no negated entailment theorems whilst for the corresponding M2-logics ≥(A ae B) is a theorem i A and ≥B are theorems. And, as predicted in Slaney [46], there are likely to be other metavaluations where negated entailment theorems have dierent properties again. This illustrates the diculty in pinning down meaning containment. The true-false dichotomy provides a sharpness which is needed for proofs of technical results and so truth-theoretic semantics is ideal for such purposes. On the other hand, meaning is not so clear-cut and thus real semantics is less suitable for these technical purposes. This adds an interesting twist to the direction of this paper, giving some value to the truth-theoretic approach to semantics. References [1] Gerard Allwein and J. Michael Dunn. Kripke models for linear logic. Journal of Symbolic Logic, 58:514–545, 1993. [2] Alan R. Anderson and Nuel D. Belnap. Entailment: The Logic of Relevance and Necessity, volume I. Princeton University Press, Princeton, NJ, 1975. [3] Jc Beall, Ross Brady, J. Michael Dunn, A. P. Hazen, Edwin Mares, Robert K. Meyer, Graham Priest, Greg Restall, David Ripley, John Slaney, and Richard Sylvan. On the ternary relation and conditionality. Journal of Philosophical Logic, 41:595–612, 2012. [4] Nuel D. Belnap. Display logic. Journal of Philosophical Logic, 11:375–417, 1982. [5] R. T. Brady and A. Meinander. Distribution in the logic of meaning containment and in quantum mechanics. In K. Tanaka, F. Berto, E. Mares, and F. Paoli, editors, Paraconsistency: Logic and Applications, pages 223–255. Springer, Dordrecht, 2013. 778 Some Concerns Regarding Ternary-relation Semantics . . . [6] Ross T. Brady. Natural deduction systems for some quantified relevant logics. Logique et Analyse, 27:355–377, 1984. [7] Ross T. Brady. Depth relevance of some paraconsistent logics. Studia Logica, 43:63–73, 1984. [8] Ross T. Brady. A content semantics for quantified relevant logics – I. Studia Logica, 47:111–127, 1988. [9] Ross T. Brady. A content semantics for quantified relevant logics – II. Studia Logica, 48:243–257, 1989. [10] Ross T. Brady. The gentzenization and decidability of RW. Journal of Philosophical Logic, 19:35–73, 1990. [11] Ross T. Brady. The gentzenization and decidability of some contraction-less relevant logics. Journal of Philosophical Logic, 20:97–117, 1991. [12] Ross T. Brady. Relevant implication and the case for a weaker logic. Journal of Philosophical Logic, 25:151–183, 1996. [13] Ross T. Brady. Gentzenizations of relevant logics without distribution – I. Journal of Symbolic Logic, 61:353–378, 1996. [14] Ross T. Brady. Gentzenizations of relevant logics without distribution – I. Journal of Symbolic Logic, 61:379–401, 1996. [15] Ross T. Brady. Semantic decision procedures for some relevant logics. Australasian Journal of Logic, 1:4–27, 2003. [16] Ross T. Brady, editor. Relevant Logics and Their Rivals, vol. II. A Continuation of the Work of R. Sylvan, R. Meyer, V. Plumwood and R. Brady. Number 59 in Western Philosophy Series. Ashgate, Burlington, VT, 2003. [17] Ross T. Brady. Normalized natural deduction systems for some relevant logics II: Other logics and deductions. Talks at conferences of the Australasian Association for Logic, 2003 and 2004. [18] Ross T. Brady. Universal Logic. CSLI Publications, Stanford, CA, 2006. [19] Ross T. Brady. Normalized natural deduction systems for some relevant logics I: The logic DW. Journal of Symbolic Logic, 71(1):35–66, 2006. 779 Brady [20] Ross T. Brady. Free semantics. Journal of Philosophical Logic, 39:511–529, 2010. [21] Ross T. Brady. The consistency of arithmetic, based on a logic of meaning containment. Logique et Analyse, 55:353–383, 2012. [22] Ross T. Brady. The simple consistency of naive set theory using metavaluations. Journal of Philosophical Logic, 43:261–281, 2014. [23] Ross T. Brady. Logic – The big picture. In J.-Y. Beziau, M. Chakraborty, and S. Dutta, editors, New Directions in Paraconsistent Logic, pages 353–373. Springer, Dordrecht, 2015. [24] Ross T. Brady. The use of definitions and their logical representation in paradox derivation. Talk at the 5th Universal Logic Conference, Istanbul, Turkey, 2015. [25] Ross T. Brady. On the law of excluded middle. Talk at the Logic Seminar, University of Melbourne, 2015. [26] Kit Fine. Models for entailment. Journal of Philosophical Logic, 3:347–372, 1974. [27] Kit Fine. Analytic implication. Notre Dame Journal of Formal Logic, pages 169–179, 1986. [28] Kit Fine. Semantics for quantified relevance logic. Journal of Philosophical Logic, 17:27–59, 1988. [29] Robert Goldblatt and Edwin D. Mares. An alternative semantics for quantified relevant logic. Journal of Symbolic Logic, 71(1):163–187, 2006. [30] Leon Henkin. The completeness of the first-order functional calculus. Journal of Symbolic Logic, 14:159–166, 1949. [31] Edwin D. Mares. Semantics for relevance logic with identity. Studia Logica, 51: 1–20, 1992. [32] Edwin D. Mares. Relevant Logic. A Philosophical Interpretation. Cambridge University Press, Cambridge, UK, 2004. [33] Robert K. Meyer. Arithmetic formulated relevantly. Typescript, A.N.U. [34] Robert K. Meyer. Metacompleteness. Notre Dame Journal of Formal Logic, 17:501–516, 1976. 780 Some Concerns Regarding Ternary-relation Semantics . . . [35] Robert K. Meyer. The consistency of arithmetic. Typescript, A.N.U. [36] Robert K. Meyer and Harvey Friedman. Can we implement relevant arithmetic? Technical Report TR–ARP–12/88, Automated Reasoning Project, R.S.S.S., A.N.U., 1988. 11 pp. [37] Jean Norman and Richard Sylvan, editors. Directions in Relevant Logic. Number 1 in Reason and Argument. Kluwer, Dordrecht, 1989. [38] W. T. Parry. Analytic implication, its history, motivation and possible varieties. In J. Norman and R. Sylvan, editors, Directions in Relevant Logic, volume 1 of Reason and Argument, pages 101–117. Kluwer, Dordrecht, 1989. [39] G. Priest. An Introduction to Non-Classical Logic. Cambridge University Press, Cambridge (UK), 1st edition, 2001. [40] G. Priest. An Introduction to Non-Classical Logic. From If to Is. Cambridge University Press, Cambridge (UK), 2nd edition, 2008. [41] G. Restall. Review of Universal Logic. Bulletin of Symbolic Logic, 13:544–547, 2007. [42] R. Routley. Problems and solutions in the semantics of quantified relevant logics. In A. I. Arruda, R. Chuaqui, and N. C. A. da Costa, editors, Proceedings of the fourth Latin American Symposium on Mathematical Logic, pages 305– 340, Amsterdam, 1980. North-Holland. [43] Richard Routley, Robert K. Meyer, Val Plumwood, and Ross T. Brady. Relevant Logics and Their Rivals, volume 1. Ridgeview Publishing Company, Atascadero, CA, 1982. [44] P. Schroeder-Heister. Validity concepts in proof-theoretic semantics. Synthese, 148:525–571, 2006. [45] P. Schroeder-Heister. Proof theoretic semantics. 2007. [46] J. K. Slaney. A metacompleteness theorem for contraction-free relevant logics. Studia Logica, 43:159–168, 1984. [47] J. K. Slaney. Reduced models for relevant logics without WI. Notre Dame Journal of Formal Logic, 28:395–407, 1987. [48] Alasdair Urquhart. The undecidability of entailment and relevant implication. Journal of Symbolic Logic, 49:1059–1073, 1984. Received 13 July