12
$\begingroup$

I was reading the question Consistency and completeness imply soundness? and the first statement in it says:

I understand that soundness implies consistency.

Which I was quite puzzled about because I thought soundness was a weaker statement than consistency (i.e. I thought consistent systems had to be sound but I guess its not true). I was using the informal definition Scott Aaronson was using in his 6.045/18.400 course at MIT for consistency and Soundness:

  1. Soundness = A proof system is sound if all the statements it proves are actually true (everything provable is True). i.e. IF ( $\phi$ is provable) $\implies$ ($\phi$ is True). So IF (there is a path to a formula) THEN (that formula is True)
  2. Consistency = a consistent system never proves A and NOT(A). So only one A or its negation can be True.

Using those (perhaps informal) definitions in mind I constructed the following example to demonstrate that there is a system that is sound but not consistent:

$$ CharlieSystem \triangleq \{ Axioms=\{A, \neg A \}, InferenceRules=\{NOT(\cdot) \} \}$$

The reason it's I thought it was it was a sound system is because by assumption the axioms are true. So A and not A are both true (yes I know the law of excluded middle is not included). Since the only inference rule is negation we get that we can reach both A and not A from the axioms and reach each other. Thus, we only reach True statements with respect to this system. However, of course the system is not consistent because we can prove the negation of the only statement in the system. Therefore, I have demonstrated that a sound system might not be consistent. Why is this example incorrect? What did I do wrong?

In my head this makes sense intuitively because soundness just says that once we start from and axiom and crank the inference rules we only reach at destinations (i.e statements) that are True. However, it does not really say which destination we arrive. However, consistency says that we can only reach destination that are reach either $A$ or $\neg A$ (both not both). So every consistent system must include the law of excluded middle as a axiom, which of course I did not and then just included the negation of the only axiom as the only other axiom. So it doesn't feel I did anything too clever, but somehow something is wrong?


I just realize it could be a problem because I am using Scott's informal definition. Even before I wrote the question I did check wikipedia but their definition didn't make sense to me. In particular the part that they say:

with respect to the semantics of the system

their full quote is:

every formula that can be proved in the system is logically valid with respect to the semantics of the system.

$\endgroup$
  • $\begingroup$ All systems we're interested in can derive contradiction from $A$ and $\lnot A$. $\endgroup$ – Yuval Filmus Feb 19 '18 at 5:12
  • $\begingroup$ @YuvalFilmus I don't think I understand what your comment means...does it mean that with my axioms you can always derive a contradiction? That was sort of my point no? Sorry I don't get it. I think my question is just about the semantics of the word "soundness" and "consistency" since my example just deals with categorizing the "logic system" I made up. $\endgroup$ – Charlie Parker Feb 19 '18 at 5:14
  • $\begingroup$ It means that your system is not so interesting. All systems that come up in research are strong enough to derive contradiction in this setting. $\endgroup$ – Yuval Filmus Feb 19 '18 at 5:36
  • 1
    $\begingroup$ @YuvalFilmus my system isn't suppose to be "interesting" to do real maths, of course I know that. My system was pedagogically defined to make my question clear and simple of course and clarify the confusion I have with respect to soundness and consistency. But in that lecture I linked, Scott says later that Soundness since is talking about "real" Truth, must be consistent because Truth has to be consistent with itself (i.e. True can't be equal to False). So it seems that Sound system just inherit by axiom of excluded middle automatically. Is my current understanding. $\endgroup$ – Charlie Parker Feb 19 '18 at 14:38
  • $\begingroup$ Are $A$ and $\neg A$ both true? If not then how is it sound? $\endgroup$ – user253751 Feb 20 '18 at 4:17
16
$\begingroup$

I recommend looking into formal logic beyond vague, hand-wavy descriptions. It's interesting and highly relevant to computer science. Unfortunately, the terminology and narrow focus of even textbooks specifically about formal logic can present a warped picture of what logic is. The issue is that most of the time when mathematicians talk about "logic", they (often implicitly) mean classical propositional logic or classical first-order logic. While these are extremely important logical systems, they are nowhere near the breadth of logic. At any rate, what I'm going to say largely takes place in that narrow context, but I want to make it clear that it is happening in a particular context and need not be true outside of it.

First, if consistency is defined as not proving both $A$ and $\neg A$, what happens if our logic doesn't even have negation or if $\neg$ means something else? Clearly, this notion of consistency makes some assumptions about the logical context within which it operates. Typically, this is that we are working in classical propositional logic or some extension of it such as classical first-order logic. There are multiple presentations, i.e. lists of axioms and rules, that could be called classical propositional/first-order logic but, for our purposes, which doesn't really matter. They are equivalent in some suitable sense. Typically, when we are talking about a logical system we mean a (classical) first-order theory. This starts with the rules and (logical) axioms of classical first-order logic, to which you add given function symbols, predicate symbols, and axioms (called non-logical axioms). These first-order theories are usually what we're talking about as being consistent or inconsistent.

Next, soundness usually means soundness with respect to a semantics. Consistency is a syntactic property having to do with what formal proofs we can make. Soundness is a semantic property that has to do with how we interpret the formulas, function symbols, and predicate symbols into mathematical objects and statements. To even begin to talk about soundness, you need to give a semantics, i.e. an interpretation of the aforementioned things. Again, we have a separation between the logical connectives and logical axioms, and the function symbols, predicate symbols, and non-logical axioms. What makes connectives connectives and logical axioms logical axioms from the semantic point of view is that they get treated specially by semantics while function symbols, predicate symbols, and non-logical axioms do not. The typical semantics for classical first-order logic is to interpret formulas as set-theoretic relations on some (power of a) set called the "domain" given as part of a particular semantics, and the connectives as the more or less obvious set-theoretic analogues, e.g. $[\![\varphi\land\psi]\!]=[\![\varphi]\!]\cap[\![\psi]\!]$ where I use $[\![\varphi]\!]$ as the interpretation of the formula $\varphi$. In particular, $[\![\neg\varphi]\!]=D\setminus[\![\varphi]\!]$ where $D$ is the domain set. The idea is a formula is interpreted as the set of (tuples of) domain elements that satisfy the formula. A closed formula (i.e. one with no free variables) is interpreted as a nullary relation which is to say a subset of a singleton set which can only be that singleton or the empty set. A closed formula is "true" if it isn't interpreted as the empty set. Soundness is then the statement that every provable (closed) formula is "true" in the above sense.

It is easy from here, even from the sketch I've given, to prove that soundness implies consistency (in the context of classical first-order logics and the semantics I've sketched). $$[\![\varphi\land\neg\varphi]\!]=[\![\varphi]\!]\cap(D\setminus[\![\varphi]\!])=\varnothing$$ If your logic is sound, then every provable formula interprets as a non-empty set, but $[\![\varphi\land\neg\varphi]\!]$ is always interpreted as the empty set no matter what formula $\varphi$ is, and so it can't be provable, i.e. your logic is consistent.

$\endgroup$
  • 2
    $\begingroup$ feel free to recommend me a book on logic, I don't really know what a good reference is, especially for beginner in logic. The funny thing is that I have take algorithms and real analysis, so I've never actually thought rigorously about the logic itself. $\endgroup$ – Charlie Parker Feb 19 '18 at 14:33
  • 1
    $\begingroup$ interesting, I always thought that "truth" meant that we mapped a statement to boolean values 0 and 1. But it seems that was incorrect. I guess we can sort of fix my wrong model by having empty set map to 0 and non-empty to 1. Otherwise, I'm not sure how one is able to re-write your proof in "my definition of truth as the function mapping to 1 or 0". $\endgroup$ – Charlie Parker Feb 19 '18 at 18:32
  • 1
    $\begingroup$ That's the typical semantics for classical propositional logic, which can be viewed as a special case of classical first-order logic where all predicates are nullary. The Boolean "truth" values do indeed map to the empty set and the singleton set in this view. One of the not-so-blatant points of my first paragraph was to suggest that different logics have different notions of semantics. Even for a fixed logic, there are multiple possible semantics that could be given for it. There's a reason I say "the typical semantics" and not just "the semantics". $\endgroup$ – Derek Elkins Feb 19 '18 at 18:42
  • 1
    $\begingroup$ Derek, if you have time do you mind perhaps making a concrete example of the domain and how it indeed leads to the empty set? (I am also happy to make a new question if you prefer) I had in mind an example but didn't know how to complete it. The example was showing that 2 is rational AND 2 is irrational lead to the empty set (or with $\sqrt 2$). I had in mind D is tuple of integers. Then $[\![ 2 \text{ is rational} ]\!] $ mapped to $(2,1)$ but I wasn't sure what $[\![ 2 \text{ is irrational }]\!] $ mapped to. Do you know how to finish this example in a sensible way?Or point me to an example? $\endgroup$ – Charlie Parker Feb 19 '18 at 18:57
  • 1
    $\begingroup$ That's where ones philosophy of math may come in. Platonists believe the truth of the set theoretic statements (say) are just knowable without needing recourse to logic. Arguably for them, the set theoretic expressions are the meaning of logical formulas. Formalists will use syntactic, rather than semantic approaches, i.e. "true"="provable". Constructivists have a different notion of "truth" and the more computation-oriented sub-school of them would witness the "truth" via a program. $\endgroup$ – Derek Elkins Feb 19 '18 at 22:34
3
$\begingroup$

Soundness and consistency are properties of deductive systems. Soundness can only be defined with respect to some semantics that is assumed to be given independently from the deductive system.

In the realm of semantics the two properties are related

Definition 1(Soundness[Semantics] -- borrowed from Wikipedia) Soundness of a deductive system is the property that any sentence that is provable in that deductive system is also true on all interpretations or structures of the semantic theory for the language upon which that theory is based.

Definition 2(Consistency[Semantics]) A set of sentences $A$ in the language $\mathfrak{L}$ is consistent if and only if there exist a structure of the language $\mathfrak{L}$ that satisfies all sentences in $A$. A deductive system is consistent if there exist a structure that satisfies all formulas provable in it.

With the two definitions given above it is clear that soundness implies consistency. I.e. if the set of all provable sentences holds in all structures of the language then there exists at least one structure that satisfies them.

$\endgroup$
  • 1
    $\begingroup$ actually I avoided wikipedia explicitly because I don't understand what "with respect to semantics means". Do you mind clarifying what that means? Also do you mind explaining a bit more clearly why its clear soundness implies consistency? Of course its not clear to me since this question exists :p $\endgroup$ – Charlie Parker Feb 19 '18 at 14:49
  • $\begingroup$ @CharlieParker I read your comments under other posts. I am not sure there exists a text for beginners that explains the basics of proof systems and model theory better than the introductory chapters of "Model Theory" by Hodges. One exception being "A Shorter Model Theory" by the same author. I confess, in my post I cheated and defined consistency as satisfiability, because the point of speaking about consistency is to have a characterization of satisfiability within the proof system. $\endgroup$ – Dmitri Chubarov Feb 19 '18 at 16:52
  • $\begingroup$ Thanks! I will check those out! Actually, I don't need a "beginner book" and good book is good. If the book also emphasizes intuitions and ideas rather than only proofs that would be even better! $\endgroup$ – Charlie Parker Feb 19 '18 at 21:56
2
$\begingroup$

Your proof system is neither sound nor consistent, since $A$ is not a true proposition unless $A \equiv \top$, In which case $\lnot A \equiv \bot$ is not a true proposition. This argument shows that every sound proof system is also consistent.

$\endgroup$
  • $\begingroup$ Whats wrong with having a function $Truth(\cdot)$ that maps things to True or False. $A$ and $\neg A$ are symbols mapping to both True (as in the system I defined). I'm not sure what is technically wrong with that beyond not being "interesting" for doing real maths. But defining a real system for doing maths wasn't the goal of my question. $\endgroup$ – Charlie Parker Feb 19 '18 at 14:35
  • $\begingroup$ Truth has a semantic definition: evaluating to true under all truth assignments. You don't get to choose how you define this term. $\endgroup$ – Yuval Filmus Feb 19 '18 at 14:38
  • $\begingroup$ Perhaps thats where I am confused hence my question. Though technically Scott mentioned truth can't be defined mathematically...but lets ignore that technicality for the sake of argument so I can understand the issue. Can you explain again what Truth means? thanks for your patience. :) $\endgroup$ – Charlie Parker Feb 19 '18 at 14:40
  • 1
    $\begingroup$ In the context of propositional logic, a formula is a tautology if it is true under all truth assignments. A propositional proof system is sound if all formulas it proves are tautological. $\endgroup$ – Yuval Filmus Feb 19 '18 at 15:02
  • $\begingroup$ I know your trying to help and I appreciate it but somehow ur proof is too short to really explain to me what went wrong with my example in the original post. If you can clarify that would be awesome. I guess my question is, what truth assignments bring problems to the system I suggested? $\endgroup$ – Charlie Parker Feb 19 '18 at 21:49
2
$\begingroup$

Often when we come up with logical systems, they are motivated by an attempt to describe a pre-existing phenomenon. For example, Peano arithmetic is an attempt to axiomatize the natural numbers along with the operations of addition and multiplication.

Soundness can only be defined relative to the phenomenon you're attempting to describe, and essentially means that your axioms and inference rules really do describe the thing in question. So, for example, Peano arithmetic is sound because its axioms and inference rules really are true of the natural numbers.

This, of course, implies that you have a concept of "natural numbers" beyond Peano's definition of them, and some notion of what is true or false for the natural numbers without having derived these truths from any particular set of axioms. Trying to explain where those truths come from or how they can be verified can land you in philosophical hot waters. But if you take it as a given that there ARE natural numbers, and there is some collection of true facts about them, then you can view the axiomatization project as simply attempting to come up with a concise formal specification from which many of the most important truths can be derived. Then an axiomatization is sound if everything it can prove actually is in the pre-specified collection of truths, that is, if its properties and consequences match up with the interpretation you have in mind.

(Note in particular that your formal specification isn't going to prove everything that is true about the natural numbers, and moreover will not uniquely describe the natural numbers in that there are other structures, different from the natural numbers, in which Peano's axioms are also true.)

In first order logic, at least, a theory is consistent iff it has any models at all. Soundness means it has the specific model you wanted: the particular structure you were attempting to describe with your theory really is a model of your theory. From this perspective, it's clear why soundness implies consistency.

As an example of a theory that is consistent but not sound: Peano arithmetic, PA, is capable of encoding logical formulae as arithmetical constructions, and in particular you can encode the sentence "PA is consistent" ("there is no proof of falsehood from the axioms of PA"). Call this sentence Con(PA). You may also be aware that (since it is sound, and therefore consistent) PA can't prove Con(PA), by Gödel's first incompleteness theorem. This also means that the theory PA + $\neg$Con(PA) can't prove a contradiction, so it must be consistent. But it's not sound: it claims there exists a natural number encoding a proof of falsehood from the axioms of PA, but there can't possibly be such a number in the "real" natural numbers, since otherwise we'd be able to extract a genuine proof of the inconsistency of PA from it.

PA + $\neg$Con(PA) has models, but they're models which must include "extra" objects, "non-standard natural numbers", including one which it claims encodes the "proof" in question. The theory is simply not equipped with the necessary tools to distinguish these non-standard elements from the genuine bona-fide members of $\mathbb N$, or to demonstrate that the proof is not a legitimate proof.

You can alternatively interpret this as: PA + $\neg$Con(PA) is a perfectly legitimate logical system -- it just doesn't accurately describe the natural numbers, and the natural numbers aren't a model of it.

One more thing: we don't assume that axioms are true by definition. All axioms are by definition is just the basic building blocks of proofs. They're just claims: they're only true or false when applied to particular mathematical objects. You can have false axioms, it's just pretty silly, because your system will then necessarily and immediately not be sound.

$\endgroup$
1
$\begingroup$

To have a concise (and intuitive) answer I will paraphrase what Scott Aaronson said in his 6.045/18.400 MIT lecture. He said something like this:

Soundness means everything provable is true. Since consistency means there are no contradictions and soundness already involved the concept of truth and truth must be consistent (i.e. True != False), then its must mean Sound systems are also consistent. So Soundness implies consistency because (truly) true things don't have contradictions.

Now that I reflect I realize that I had some incorrect assumptions/ideas:

  1. I didn't realize soundness was about semantics. Thus, I failed to realize that just using inference rules from the axioms is not enough to lead to true consequences (and that it doesn't guarantee it, which I thought was impossible to reach contradictory things as long as we started from the axioms and used valid inference rules).
  2. I thought that as long as the axioms were true and the inference rules made sense everything that proceeded would be true. Which I now realize might not be true since if we just have a giant list of axioms and inference rules its hard to reason if everything that follows will be true. i.e. just starting from an axiom and using a valid inference rule is not enough to guarantee that the next step will be true.
  3. The previous is essentially coupled with the fact that I didn't realize that there are two levels of complexity, 1) semantics 2) syntactics. Cranking the symbols crunching game may lead to contradictions.
  4. I didn't realize I didn't know the proper characterization of truth, which derek made a great job in characterizing.
$\endgroup$
  • $\begingroup$ "I thought that as long as the axioms were true and the inference rules made sense everything that proceeded would be true." For a suitably precise notion of "made sense" this IS correct. If your system is unsound then (at least) one of your axioms is false, or rules of inference invalid. $\endgroup$ – Ben Millwood Feb 20 '18 at 3:43
  • $\begingroup$ @BenMillwood but thats wrong, no? Because of Godel's second incompleteness theorem. For any formal system F that encompasses arithmetic, one cannot prove its consistency within F. I took that to mean that my assumption of soundness is impossible (i.e. we can't have have a formal system that everything provable in it is True because that would imply consistency which is impossible it seems, unless of course I have some misconception about the 2nd incompleteness theorem). To be honest I'm ok if we don't have completeness, what I find disturbing is we can't even have consistency. $\endgroup$ – Charlie Parker Feb 20 '18 at 14:45
  • $\begingroup$ F certainly can be consistent, you just can't find a proof of that fact in F. You have to appeal either to some more powerful system, or informal arguments, or just accept some kind of uncertainty that even though F may be consistent you won't be able to construct a watertight argument that it is so. $\endgroup$ – Ben Millwood Feb 20 '18 at 16:48
  • $\begingroup$ @BenMillwood I guess thats what I am assuming in my answer. That there is uncertainty that proofs actually work and a next step could lead to some falsehood. If I knew that were not true then I'd know for sure somehow that I won't ever reach a contradiction which violates Godel's 2nd incompleteness theorem. Or thats what I understand so far right now. $\endgroup$ – Charlie Parker Feb 20 '18 at 16:50
  • $\begingroup$ @BenMillwood I guess I've abandoned the belief that applying inference rules gives us next statements that are true statement with 100%. Instead I think I've implicitly assumed the belief that moving forward is just a matter of syntactics rather than of semantics...could be wrong of course, this subject seems confusing and subtle. $\endgroup$ – Charlie Parker Feb 20 '18 at 16:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.