2

Obviously this is a bit of an edge case. By the empty logic I mean the one on which all arguments are invalid, i.e. $\Gamma \nvdash \varphi$ for all sets of formulas (premises) $\Gamma$ and any formula (conclusion) $\varphi$.

The textbooks I have checked do not carefully define what constitutes a proof system, relying on examples instead. The usual presentation of Hilbert systems ensures that all Hilbert relations are reflexive ($\Gamma \vdash \varphi$ whenever $\varphi \in \Gamma$), which means there can be no Hilbert system for the empty logic. (In particular, the Hilbert system with no axiom schemata and no rules of inference does not axiomatize the empty logic.) By contrast it is difficult to find any characterization of what exactly constitutes a Gentzen calculus.

Is there a conventional definition of what constitutes a proof system in general that settles the question?

jdonland
  • 197
  • 2
    I can't imagine any reason why a logic whose notion of entailment is the empty relation should be of interest. – Taroccoesbrocco Feb 28 '22 at 16:03
  • 6
    I doubt that there's a single definition of "proof system" general enough to capture everything that people would like to call a proof system. But regardless of the definition, I think the answer is obviously yes: the empty logic is axiomatizable by the proof system that has no rules (or logical axioms). Suppose we write $\Gamma\vdash \varphi$ if we can obtain $\varphi$ as a theorem from premises in $\Gamma$ using the rules of our proof system. If you have no rules for generating theorems, then you have no theorems, so $\Gamma\not\vdash \varphi$ for all $\Gamma$ and all $\varphi$. – Alex Kruckman Feb 28 '22 at 16:08
  • @AlexKruckman If a proof system is just any collection of rules, can rules be defined in a way that isn't circular? Is a rule just a sublogic in disguise? – jdonland Feb 28 '22 at 16:35
  • Well that seems like a different question entirely. You know that e.g. a Hilbert system is defined by a collection of rules. What makes you worry that talking about the empty collection of rules might be "circular" when defining a Hilbert system is not? – Alex Kruckman Feb 28 '22 at 16:39
  • @AlexKruckman I think that on the view that a proof system is any collection of rules, we need to say that Hilbert systems implicitly include a rule allowing one to introduce any premise to a derivation (this is what makes all Hilbert relations reflexive). So then there are three kinds of rules: the ones that allow the specified formula (premise rules), those that allow any substitution instance of the specified formula (axiom schemata), and modus ponens. Can "rule" be defined explicitly in a way that includes all these? If not, then the whole notion of a proof system seems very loosey-goosey. – jdonland Feb 28 '22 at 16:48
  • 2
    (1) Yes, I agree that Hilbert systems include such a rule. (2) Sure, I don't see any problem whatsoever with defining "rule" in such a way that includes all these kind of rules and many more (e.g. the more complicated kinds of rules you get in natural deduction-style systems). (3) There is a big difference between writing down a specific proof system and proving things about it, vs. writing down general definitions of "rule" and "proof system" that will allow you to reason about all proof systems in the abstract. – Alex Kruckman Feb 28 '22 at 17:05
  • 1
    The answer to the question "is the empty logic axiomatizable?" is Yes: by the empty proof system which has no rules. But it seems like the question you're really interested in is "what is a good general definition of rule and proof system"? If that's the case, I recommend you ask a new question or edit this one to remove the stuff about the empty logic, so as to get more to the point. In my view, the answer to the new question is the one I expressed in the first sentence of my first comment above. But you may get helpful references to general definitions people have tried to make. – Alex Kruckman Feb 28 '22 at 17:08
  • @AlexKruckman Thanks for your insights on this! – jdonland Feb 28 '22 at 17:14
  • Rafferty does define a rule in the context of Gentzen relations: if a Gentzen relation validates the (sequent) argument with premises $S$ and conclusion $\Gamma \rhd \Delta$ then "from (a substitution instance of) S conclude (the same substitution applied to) $\Gamma \rhd \Delta$" is a rule of the relation. This seems to point in the direction of rules being the same as sets of (equivalence classes under substitution of) arguments. But these correspond to (structural) logics. So maybe my hunch about rules being sublogics was right? – jdonland Feb 28 '22 at 20:12
  • No rules and no axioms = no arguments, and thus no valid arguments. – Mauro ALLEGRANZA Mar 01 '22 at 08:15
  • I have asked a separate question about rules, and my intuition that rules themselves correspond to logics here. – jdonland Mar 02 '22 at 20:26

0 Answers0