0

I'm a novice in this field of logic. While reading about soundness and completeness of a method, I read this line: "a logical system has the soundness property if and only if every formula that can be proved in the system is logically valid with respect to the semantics of the system." Here is its Source.

Part of it says, every formula that can be proved, is valid. (my interpretation)

Does it mean, the formula that can be proved, can't be invalid?? If it is so, why can't we have a proof of an invalid formula?

( A falsifying interpretation can be useful as a counterexample, to prove that a formula is invalid, isn't it? )

It's quite confusing for me.. Can someone please help and explain? Thanks in advance.

Improve this question

1 Answer 1

Reset to default
1

The definitions are relevant to a Logical system and can be extended to Formal mathematical theories.

See the Wiki's page (some lines below your quote):

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. Strong soundness of a deductive system is the property that any sentence P of the language upon which the deductive system is based that is derivable from a set Γ of sentences of that language is also a logical consequence of that set.

This means:

if provable, then valid.

The converse of that definition is that of completeness:

A deductive system with a semantic theory is strongly complete if every sentence P that is a semantic consequence of a set of sentences Γ can be derived in the deduction system from that set.

This means:

if valid, then provable.

Informally, a soundness theorem for a deductive system expresses that all provable sentences are true. Completeness states that all true sentences are provable.

In formal system, a "proof" is a formal proof (aka: derivation).

A falsifying interpretation can be useful as a counterexample, to prove that a formula is invalid, isn't it?

Correct. In propositional logic we have the truth table method that can be applied to every formula to verify (in a finite number of steps) if the formula is valid or not. A single row in the truth table that "outputs" FALSE is enough to show that the formula is invalid.

In the same way, truth tree method will produce a counterexample, if any, showing the invalidity of the formula.

Having found a counterexample, we apply soundness ("if provable, then valid") to conclude that the formula (being not valid) is not derivable in the calculus.

The discussion above id related to the decidability topic.

In propositional logic we have the method of truth table that can be used to verify (in a finite number of steps) for every formula if the formula is valid or not.

A corresponding method is not available for first-order logic. This means that, completeness ensures that if formula P is valid then we have a prove of it.

But we have no general method to verify in advance if P is valid or not.

This means that validity if FOL is not decidable.

See also the post: How is First Order Logic complete but not decidable?

Improve this answer
7
  • Hi, Thanks for your answer. In your answer, "This means, if provable, then valid." is exactly what I am unable to understand. Why provable doesn't include invalid formulae? because proof can be for anything, valid or invalid formula.
    – user8616916
    Commented Jun 25, 2020 at 9:27
  • @user8616916 - the "usual" logical systems are designed to be sound, i.e. only valid formulas can be proved. In addition, they are also strongly sound in order to ensure that only true mathematical theorem can be proved from true mathematical axioms.
    – Mauro ALLEGRANZA
    Commented Jun 25, 2020 at 9:30
  • Thank you. What about the invalid formula? How do we prove them?
    – user8616916
    Commented Jun 25, 2020 at 9:35
  • Regarding the line in the answer, "Correct, but this is not a "derivation" in the system, also if it is the simplest way to show that a formula is invalid (and thus not derivable).", semantic argument method works to prove all branches are closed.. and if some branch remains open, that defines the falsiying interpretation. So, in a way, the semantic argument proof method does derive the falsifying interpretation. Isn't it?
    – user8616916
    Commented Jun 25, 2020 at 9:45
  • Hi, thanks a lot for the edit. I think, this comment of yours answers the question that I have - " the "usual" logical systems are designed to be sound, i.e. only valid formulas can be proved. In addition, they are also strongly sound in order to ensure that only true mathematical theorem can be proved from true mathematical axioms." There is a way to derive single interpretation as a counterexample, as a matter of proof of invalidity, although we may not prove the entire domain of values that make the formula invalid, as in your answer, the domain of natural numbers. But maybe it's convention
    – user8616916
    Commented Jun 25, 2020 at 10:02

You must log in to answer this question.

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