0

When I asked whether the empty logic (the one on which no argument is valid) is axiomatizable, the consensus was that it is, and that it is axiomatized by a proof system having no rules whatsoever.

Is this in fact a proof system? If a proof system is determined by its rules, then what is a rule, exactly?

The answer here characterizes a derivation in some system as a legally-labelled (well-founded) tree, where the rules of the proof system determine the legality of labellings.

It seems to me that the rules of a Hilbert system correspond to logics: the rules that allow leaves to be labelled with axioms correspond to logics for each axiom schemata $\alpha$ which validate just substitution instances of $\vdash \alpha$ while the rule for non-leaves (i.e., modus ponens) corresponds to the logic which validates just substitution instances of $\varphi \to \psi, \varphi \vdash \psi$. Perhaps the "rule" (not standardly described as such) that one may also label a leaf node with any premise corresponds to the logic validating just the arguments $\vdash \gamma$ where $\gamma$ is a premise (but not necessarily any substitution instance thereof).

This line of thinking applies just as well to, e.g., Gentzen calculi by moving from formulas and arguments to sequents and sequent arguments.

If this is right, can we then see the logic axiomatized by a proof system as being generated somehow by the logics corresponding to its rules? Can we avoid circularity here? Maybe the system with no rules is a sort of base case, the bottom element of a lattice of proof systems?

jdonland
  • 197
  • There's a correspondence between proof systems and sets of rules (and in particular between single rules and single-rule proof systems), so you could define a lattice of proof systems corresponding to the natural lattice of rule sets (as long as your definitions are general enough to accommodate all the proof systems of interest). What's the circularity you're worried about? Maybe I'm missing something about how you're formalizing things. – Karl Mar 02 '22 at 20:07
  • @Karl I guess my concern about circularity is that if proof systems are collections of rules, and rules are really just logics, then maybe we're inclined to say that a logic is axiomatizable when it has a proof system composed of logics which are themselves axiomatizable, and then we would clearly need a base case. – jdonland Mar 02 '22 at 20:22
  • Yours is a typical example of "stretching" the intuition (like the young students perplexed with the empty set...) A proof system is defined in order to "prove" something: without axioms and rules we cannot have derivations and neither theorems: thus it is a "proof system" of what? – Mauro ALLEGRANZA Mar 03 '22 at 07:18
  • A derivation can be defined mathematically as a sequence of formulas: thus, what is the empty sequence? a null-derivation... And a tree without nodes? – Mauro ALLEGRANZA Mar 03 '22 at 07:21
  • What is a "logic" in abstract? See Logical Consequence: "A logic system $\text L$ [is] $\text L=⟨ L,\vdash_L ⟩$ with the understanding that $L$ is the language of $\text L$ and $\vdash_L$ its consequence relation." – Mauro ALLEGRANZA Mar 03 '22 at 09:56
  • @MauroALLEGRANZA I think it's clear from the question that I understand what a logic is in the abstract: a relation between sets of formulas and formulas. The question is whether the rules of a proof system (in general) are themselves equivalent to logics. If you don't think the question is well-posed, then explain why not. – jdonland Mar 03 '22 at 14:33
  • I think I follow. It seems like the "rules are really just logics" part of your thinking is what creates the difficulty in defining axiomatizability. Like you said, you at least need a (nonempty) base case for what constitutes a rule or a rule-based logic. Then "combining rule sets" of axiomatizable logics should be equivalent to taking the union of their consequence relations. – Karl Mar 03 '22 at 20:25
  • @Karl That's exactly right. And more broadly I wonder whether this line of thinking would let you prove theorems like "a logic is X if and only if it is axiomatized by a proof system in which all the rules are X". – jdonland Mar 03 '22 at 21:42

0 Answers0