Timeline for Decidability of completeness in propositional logic
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 20, 2022 at 2:00 | comment | added | Sprotte | Thank you all - this has been very informative for me! | |
| Apr 20, 2022 at 1:58 | vote | accept | Sprotte | ||
| Apr 19, 2022 at 10:52 | comment | added | Karel Chvalovský | @EmilJeřábek Ahoj Emile, done :) | |
| Apr 19, 2022 at 10:49 | answer | added | Karel Chvalovský | timeline score: 6 | |
| Apr 19, 2022 at 10:14 | comment | added | Emil Jeřábek | @KarelChvalovský Ahoj Karle, that’s great. Since it completely answers the question, can you post it as an answer rather than a comment? | |
| Apr 19, 2022 at 9:41 | comment | added | Karel Chvalovský | 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. | |
| Apr 19, 2022 at 8:23 | comment | added | Emil Jeřábek | (The computed mgu will have formulas represented as circuits, i.e., directed acyclic graphs rather than trees.) An alternative way to phrase the unification argument is as follows: if $A$ has a proof with $k$ steps, it has a proof with $k$ steps in which all formulas have circuit size polynomial in $k$ and $|A|$ (hence the whole proof can be represented by a polynomial-size object). A direct proof of this is given e.g. in Lemma 4.4.4 of Krajíček, Bounded arithmetic, propositional logic, and proof complexity (where it is formulated in terms of formula depth rather than circuit size). | |
| Apr 19, 2022 at 7:21 | comment | added | Emil Jeřábek | ... compute the most general unifier. Then any other valid proof with the given skeleton is a substitution instance of the mgu, thus it suffices to check (in polynomial time) whether the target formula is a substitution instance of the end-formula of the mgu. | |
| Apr 19, 2022 at 7:18 | comment | added | Emil Jeřábek | This is decidable (in NP, if $k$ is given in unary) for all propositional logics axiomatized by finitely many schematic rules and axioms. For a given $k$, there are only finitely many proof skeletons (i.e., directed acyclic graphs with labels indicating for each node from which nodes it is derived and what rule is used) of size $k$, and you can enumerate them algorithmically. For a fixed skeleton, an assignment of formulas to nodes that makes a valid derivation is a first-order syntactic unification problem; thus, we can determine in polynomial time whether it has a solution, and if so, ... | |
| Apr 19, 2022 at 0:06 | comment | added | Sprotte | @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? | |
| Apr 18, 2022 at 8:07 | comment | added | Emil Jeřábek | 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. | |
| Apr 17, 2022 at 17:50 | history | edited | user44143 | CC BY-SA 4.0 |
streamlined
|
| Apr 17, 2022 at 17:06 | history | edited | Sprotte | CC BY-SA 4.0 |
changed the title to hopefully make it more accurate of the whole question
|
| Apr 17, 2022 at 0:38 | comment | added | user44143 | 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 | |
| Apr 17, 2022 at 0:24 | comment | added | Sprotte | @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). | |
| Apr 16, 2022 at 23:36 | history | asked | Sprotte | CC BY-SA 4.0 |