After reading Gödel's incompleteness theorem, I wonder if there are any systems whose axioms are sound and complete. I realize that Gödel's arguments (at least from my sources) only apply to arithmetic logic. So, I wonder if it applies to propositional logic as well.

If propositional logic is not sound and complete, are there any systems of axioms which are? I find it strange because then the system would almost become circular in a way. I hope I made some sense, I apologize if I misrepresented some theorems or terms.

  • 1
    Yes, so is predicate calculus (without additional axioms), Presburger arithmetic (with no multiplication), and Tarski's elementary Euclidean geometry, see Wikipedia.
    – Conifold
    Commented Aug 8, 2018 at 18:53
  • 2
    Maybe you aren't aware, but there are two different uses of the term "complete" in regards to logic that sometimes get confused (e.g. you can find many questions of people asking how Gödel's completeness and incompleteness theorems don't contradict each other, they're talking about two different things.) The issue is that soundness is usually talked about together with the completeness that Gödel proved, that semantic validity implies provability. That's what we mean when we say "a system of logic and it's deductive system are sound and complete".
    – Not_Here
    Commented Aug 8, 2018 at 19:04
  • 1
    But in your title, you seem to be talking about the other form of completeness, the one that Gödel proved his incompleteness theorems about. I just want to make sure that you're clear on the concepts you're using, because again "soundness and completeness" almost always refers to deductive systems, and the other type of completeness which I think you're asking about is different and doesn't really have anything to do with soundness in the way the other use of the word does.
    – Not_Here
    Commented Aug 8, 2018 at 19:05
  • 3
    Distinguish between two kinds of completeness: semantic completeness and syntactic completeness. Semantic completeness means that given a formal logic and a proof system, if a sentence A is true in every model of the system, then A is provable from the deduction rules of that system. This is what Gödel's completeness theorem proves for first order logic, it is also the converse of soundness. Syntactic completeness means, for a given formal theory, if A is a sentence in the language of the theory, then either A or ~A is provable from that theory. This is what Gödel's incompleteness theorem uses
    – Not_Here
    Commented Aug 8, 2018 at 19:14
  • 2
    So, it seems as if your question is talking about syntactic completeness, and asking if there are any systems which are syntactically complete (Conifold gave some examples) but the use of soundness in your question seems to be a red herring, which is why I am concerned you might be a little confused, because soundness is usually put together with semantic completeness, not syntactic, because semantic completeness and soundness are the converse of each other. Hopefully if you were at all confused this helped clear it up.
    – Not_Here
    Commented Aug 8, 2018 at 19:16

2 Answers 2


Yes, you can give axioms and rules of inference so that all and only the tautologies are derivable. Propositional calculus is better behaved than first order logic in that sense. That doesn't mean you can find the proofs quickly though, unless P=NP.


Goedel's 1930 completeness theorem showed that first-order predicate calculus is complete in the sense that every valid formula is a theorem. There are many calculi that have as theorems all and only the tautologies, that is, the valid formulas of propositional logic, as pointed out in the answer given previously by Kjos-Hanssen. Furthermore, as stated in the comment by Conifold, Presburger arithmetic and Tarski's formulation of secondary-school geometry also possess systems in which every valid formula is a theorem.

You must log in to answer this question.

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