0

Basically is there any algorithm for proving a tautology? (even if it runs in exponential time?)

Additionally, is it possible for a propositional calculus to be such that a tautology is presented in a way in which it is clear that it is a tautology (so that, just by looking at it one would see it is a tautology?

AnalysisProof
  • 51

2 Answers2

1

Yes, there are a few methods: truth tables, axiomatic (or "Hilbert-style") systems, natural deduction, and others. The method of truth tables is probably the easiest to prove complete and correct, and it runs in exponential time at worst (the problem is actually co-NP complete).

I'm not sure what your additional question asks. Any formal system for propositional logic has only finitely many axioms or axiom schemas (e.g. "$(A\to(B\to A))$ is an axiom, for any well-formed formulas $A, B$") and finitely many deduction rules. It's usually clear that the axioms/axiom schemas/starting set of truths are tautologies, and for formulas of human-friendly lengths, we can usually see whether they're instances. But tautologies can be arbitrarily long. Given notations currently in use, for formulas longer than some threshold (say, $10^{10}$ symbols), there's no way anyone can see if a formula is a tautology just by looking at it.

BrianO
  • 16,579
  • Kind of off point, but is the truth-table method considered a propositional proof system (in the eyes of computer scientists) if proofs can only be done in exponential time? In regards to the second question of my OP, what I was asking is if it's possible for there to be some system in which tautologies have some feature which makes them instantly recognizable as tautologies – AnalysisProof Dec 09 '15 at 06:15
  • @Stacked It's definitely an algorithm, even if it only turns out to run in (nothing better than) exponential time. In computer science the problem 3SAT, satisfiability for propositional formulas with 3 variables, is NP-complete. The dual problem of $n$-SAT is $n$-VALID, whether a formula in $n$ variables is a tautology. Clearly the problem is in the complexity class EXP — the standard brute-force method shows that — but actually we can do a little better: the problem of recognizing tautologies is co-NP complete. I added a little to clarify this. – BrianO Dec 09 '15 at 06:26
  • Re your 2nd question: I suppose you could, for example, "tag" all formulas that the system generates/derives with an extra symbol up front. What sort of features did you have in mind? This and others like it wouldn't help much: we'd still have the problem of looking at an ordinary formula, without the new decoration(s), and determining whether its decorated version is provable :) – BrianO Dec 09 '15 at 06:30
  • More precise/correct version of 1st line of my 2nd to last comment: It's definitely an algorithm, although it runs in exponential time. That just means it's not a feasible algorithm for anything except small-ish problems. Maybe there is a better deterministic algorithm for recognizing tautologies, but at present we don't know enough about the class co-NP to say. – BrianO Dec 09 '15 at 06:50
  • Does that help? – BrianO Dec 09 '15 at 07:38
  • I believe so. Thanks – AnalysisProof Dec 09 '15 at 07:40
  • "Yes, there are a few methods: truth tables, axiomatic (or "Hilbert-style") systems, natural deduction, and others." Axiomatic systems don't provide an algorithm for proofs from the axioms. And what if the propositional calculus only has infinite valued models, such as Lukasiewicz infinite-valued logic? – Doug Spoonwood Dec 09 '15 at 16:01
  • @DougSpoonwood re axiomatic system. True, they're not algorithms, of course. I didn't want to get too verbose. An axiomatic system + a program that systematically generates all consequences of a set of premises does give an algorithm. It's safe to assume that "propositional calculus" as intended by OP does not mean or even encompass infinite-valued propositional logic. – BrianO Dec 10 '15 at 03:53
1

Truth tables can get converted into a set of equations which exhaustively cover all possible truth-value assignments for a given well-formed formula. Those equations can get transformed into steps in a substitution and detachment proof in a system for a propositional calculus with functorial variables. For details of how this works see here or p. 65-66 of Arthur Prior's Formal Logic.

So, there exists an algorithm for proving any finite-valued tautology.

Doug Spoonwood
  • 11,211
  • "However, there is no algorithm for proving a given well-formed formula from a set of formulas and a set of rules. " Would it be interesting if there was one, even if it was grossly inefficient? Or is it not thought to be possible, regardless of being efficient or not? – AnalysisProof Dec 09 '15 at 18:39
  • @Stacked I take that back about no algorithm existing for formal proofs. There often enough does exist the possibility of doing what can get called a level saturation search. It depends on what we want to prove as to whether that comes as interesting or not. Often enough a level saturation search isn't all that interesting, though it can be. – Doug Spoonwood Dec 10 '15 at 01:57