6
$\begingroup$

Propositional logic can be presented as in Mendelson’s book, with the sole inference rule of modus ponens, and with the following three axioms: $$B \Rightarrow (C \Rightarrow B)$$ $$(B \Rightarrow (C \Rightarrow D)) \Rightarrow ((B \Rightarrow C) \Rightarrow (B \Rightarrow D))$$ $$((\neg C) \Rightarrow (\neg B)) \Rightarrow (((\neg C) \Rightarrow B) \Rightarrow C)$$ This is a sound and complete theory, as are several other theories for propositional logic.

I have questions about similar theories for propositional logic:

  1. Given a complete set of logical connectives and a finite set of sound axioms and inference rules, can we algorithmically determine if the resulting theory is complete?

  2. Given a finite set of axioms and inference rules $X$ (not necessarily sound) and a formula $\alpha$ in the underlying language of propositional connectives, can we algorithmically determine if $\alpha$ can be derived from $X$?

Improve this question
$\endgroup$
11
  • $\begingroup$ @MattF. I wish to allow arbitrary substitutions of formulas in for the variables (which means there are say infinitely many proofs of a given length). In the case of say $L$ above, this would always yield tautologies, whereas with an arbitrary $X$, we will just get a whole bunch of formulas (many of which are not tautologies if the original axioms/inference rules aren't sound). $\endgroup$
    – Sprotte
    Commented Apr 17, 2022 at 0:24
  • $\begingroup$ This question seems most interesting for logics with infinitely many distinct sentences — like intuitionist propositional logic with the Rieger-Nishimura lattice: en.wikipedia.org/wiki/Intuitionistic_logic#Syntax $\endgroup$
    – user44143
    Commented Apr 17, 2022 at 0:38
  • $\begingroup$ Q2 is undecidable, as one can take for $X$ an axiomatization of an undecidable propositional logic such as one of the relevance logics considered by Urquhart: The undecidability of entailment and relevant implication. Q1 is most likely undecidable as well, but this requires a different argument. $\endgroup$
    – Emil Jeřábek
    Commented Apr 18, 2022 at 8:07
  • $\begingroup$ @EmilJeřábek Thank you - that reference is very helpful! Do you happen to know if any of these undecidable propositional logics every have the property that for a fixed formula $A$ and positive integer $k$, we can determine if there is a proof of $A$ in $k$ steps? $\endgroup$
    – Sprotte
    Commented Apr 19, 2022 at 0:06
  • 1
    $\begingroup$ It was shown already by Post and Linial that the question whether a set of propositional formulae together with the rule of modus ponens axiomatizes exactly the classical propositional logic is algorithmically undecidable. $\endgroup$
    – Karel Chvalovský
    Commented Apr 19, 2022 at 9:41

1 Answer 1

Reset to default
6
$\begingroup$

It is undecidable, because it is even undecidable to recognize whether a finite set of axioms together with the rule of modus ponens axiomatizes exactly classical propositional logic by the Post-Linial theorem. This was shown in 1948 by Linial and Post, see their announcement (p. 50), but the first published proof is by Yntema. There are many similar results for other propositional logics.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .