Presenters will discuss issues related to core logic and the logic of term-forming operators.
Participants:
Ethan Brauer: Tennant's Soundness Conjecture
Abstract: Tennant's soundness conjecture for Core Logic states that every provable sequent of core logic is a substitution instance of a perfectly valid sequent. Various partial results are known, but the full conjecture is open. An observation by Milne suggests that the proper context for proving the result is a multiple conclusion sequent calculus. I formulate a multiple conclusion sequent calculus for Core Logic and explore the method of coarsening proofs as an approach to the soundness problem.
Ludovica Conti: TBA
Abstract: TBA
Charles Crumpler: Cut for Negative Free Classical Core Logic with a Variable-Binding, Term-Forming Operator
Abstract: We extend Tennant's cut admissibility result for classical core logic to its negative free counterpart with an arbitrary variable-binding, term-forming operator. It is first observed that Tennant's proof extends to the negative free classical core case quite naturally. We then observe that Tennant's conversion procedures can be understood as manifestations of a few underlying conversion forms. We then observe that Tennant's proof can be extended to the negative free case with a variable-binding, term-forming operator with only slight additions to the cut algorithm. We conclude by observing that, since conversions are instances of more general forms, that our extension of the cut algorithm applies to extensions of negative free classical core logic with a variable-binding, term-forming operator to systems with arbitrarily many variable-binding, term-forming operators.
Andrzej Indrzejczak: Cut-free sequent calculus for Tennant's logic of classes
Abstract: The logic of classes was first introduced by Quine under the name virtual theory of classes (VTC) and formalised by Scott in the setting of positive free logic. Significantly different variant, under the name Fregean logic of sets, was proposed by Neil Tennant on the basis of negative free logic. Despite the differences, both approaches can be treated as forms of weak logicism reconstructing the logic of our discourse on sets in the safe, non-committal way, i.e. without assuming the existence of some special sets. We present well-behaved formalisation of Tennant's logic of classes in terms of cut-free sequent calculus.
Nils Kürbis: Proof-Theoretic Logicism. Some thoughts and questions
Abstract: Logicism is the view, originally put forward and developed by Frege, that arithmetic is nothing but logic: the laws of arithmetic are analytic truths and derivable solely from the laws of logic and definitions (together with proofs that establish the legitimacy of these definitions, see Grundlagen §3). Deductive Semantics (aka proof-theoretic semantics or inferentialism) is the view that the meanings of the logical constants are defined by the rules of inference governing them, provided they satisfy certain criteria. It originates with Gentzen and was developed by Dummett, Prawitz and Schroeder-Heister. Proof-theoretic Logicism combines deductive semantics and logicism. That is, according to it, some fundamental concepts of arithmetic are logical constants the meanings of which are defined by the rules of inference governing them. (Others may be defined explicitly.) This is an attractive position: deductive semantics provides a neat account of logic, which, paired with logicism, would extend to a neat account of arithmetic. My aim in this presentation is to assess the prospects of defending proof-theoretic logicism and to raise three questions that would need to be addressed. More precisely, my question is whether we can combine the logicism put forward by Frege in Grundlagen and modified, developed and defended by Bob Hale and Crispin Wright (and a couple of others) with (my version of) deductive semantics. Proof-theoretic logicism is not new. Neil Tennant has proposed precisely such a view. I do, however, have views on deductive semantics that, I think, diverge from Tennant's. My views on the matter are admittedly austere. The aim in my talk is less to assess Tennant's approach, but to see whether relative to my own views on deductive semantics, some (plausible) form of proof theoretic logicism is defensible.
Peter Milne: TBA
Abstract: TBA
Neil Tennant: Classical Core with Single-Barreled Rules for Abstraction Operators
Abstract: We consider how best to extend Classical Core to deal with identity, enabling direct formalization of substitutions of identicals as they occur in informally rigorous mathematical reasoning; and how to set the resulting system free.
We formulate free ‘single-barreled’ rule-pairs for the definite description term-forming operator ι and the set-abstraction term-forming operator {x | . . x . . .}; and we formulate the reductions that will be needed to establish the Cut Admissibility Theorem for the free extensions of C+ that deal with those operators.
Peter Verdée: A supervaluationistic truthmaker semantics for Core Logic
Abstract: We will provide a Kit Fine style exact truthmaker semantics for (intuitionistic) Core Logic, with the following features: each state in a model can be seen as a part of a Kripke frame for intuitionistic logic and states make all and only those sentences true/false that are true/false in all possible worlds of which the states are a part. So states can then be seen, from a supervaluationist point of view, as containing merely partial information and they make (super)true whatever is true in all admissible completions of the state. The relevance features characteristic of Core Logic are semantically obtained by means of a notion of exact impossibility. To give an idea of what the latter means: states that make p both true and false are exactly impossible, while state that make p true and false but also make q true, are still impossible, but merely inexactly so.