First order logic: Soundness, Completeness, Decidability

Click For Summary

Discussion Overview

The discussion revolves around the metatheorems of first order logic (FOL), specifically focusing on soundness, completeness, Godel's Incompleteness Theorem, and undecidability. Participants express confusion regarding how these concepts interrelate, particularly in the context of proofs and models.

Discussion Character

  • Exploratory
  • Debate/contested
  • Technical explanation

Main Points Raised

  • Some participants assert that soundness means any derivation from the axioms and inference rules is valid, and that first order logic is sound.
  • Completeness is described by some as the property that any formula valid in a model can be proven from the axioms, with a consensus that FOL is complete.
  • There is confusion about Godel's Incompleteness Theorem, with some participants questioning how it does not contradict the completeness of FOL, suggesting it pertains to truths valid in specific models rather than all models.
  • Some participants clarify that Godel's Incompleteness Theorem indicates there are truths in a first order language that cannot be proven from the axioms, raising questions about the implications for completeness.
  • Undecidability is discussed as a separate concept, with some participants noting it refers to the existence of an algorithmic method to determine the truth or falsity of statements in a theory, and that completeness does not imply decidability.
  • There are differing views on the relationship between completeness and decidability, with some arguing that if a theory is decidable, it must be complete, while others challenge this assumption.
  • Some participants highlight that undecidability can mean a statement is neither provable nor disprovable within a theory, which complicates the understanding of completeness.

Areas of Agreement / Disagreement

Participants express a range of views, with some agreeing on definitions of soundness and completeness, while others disagree on the implications of Godel's Incompleteness Theorem and the relationship between completeness and decidability. The discussion remains unresolved regarding the nuances of these concepts.

Contextual Notes

Participants note that the completeness of FOL may refer to semantic completeness, while Godel's Incompleteness Theorem relates to syntactic completeness. There is also mention of the need for clarity on the definitions of terms like "recursive" and "decidable" in this context.

  • #31
asdf60 said:
I'm trying to get a concrete example.
By set defined by a wff, i mean, the wff has one free variable, so any substitution of the free variable by an element of the universe that makes the wff true belongs to the set being defined.
Okay. In that case, the negation will define the complement of the first set, which will have two elements. I'm not sure what this is a concrete example of though.
 
Physics news on Phys.org
  • #32
Okay.
I guess the question is, is it possible that one of the sentences is (that is, the wff substituted with an element) is undecidable, meaning it is neither true or false.
If I understand correctly, it's not possible, because that's not what undecidability says.
So to clarify, given a full model/intepretation, it is always possible to verify whether a given sentence is true in the model. And if it isn't true, then it's negation is.
Is this correct?
 
Last edited:
  • #33
asdf60 said:
Okay.
I guess the question is, is it possible that one of the sentences is (that is, the wff substituted with an element) is undecidable, meaning it is neither true or false.
This is not what undecidable means. As I said earlier in the thread, truth and provability should not be confused. If a sentence is undecidable it means it is unprovable, but it will still be either true or false for a given interpretation. For instance, the undecidable Gödel sentences in theories of arithmetic are always true for the interpretation of natural numbers.

If I understand correctly, it's not possible, because that's not what undecidability says.
So to clarify, given a full model/intepretation, it is always possible to verify whether a given sentence is true in the model. And if it isn't true, then it's negation is.

Is this correct?
It might not always be possible to verify whether a given sentence is true in the model, but the definition of truth for an interpretation states that if any formula is not true then its negation is.
 
  • #34
Sorry, but I'm going to have another go at this, since I would like to be able to explain this stuff without making people more confused.

A first-order theory (according to one definition, at least) is a set of wffs closed under logical consequence.

Truth and falsehood are not defined in terms of theories, but in terms of interpretations. We do not say that a wff is true for a theory, only that it belongs to (or is provable) in that theory. We can say that a wff is true for some interpretation though.

If some wff \phi is undecidable in a theory, then there will be an model of that theory (an interpretation which makes all the wffs in the theory true) for which \phi is true and a model for which \phi is false. This follows from the theorem that all consistent theories have models.

In your example, if you have an interpretation consisting of a domain with five elements, and a wff \phi(x) defining a subset of this domain with three elements, then the negation of that wff will define the set's complement. There is no mention of theories here, so it doesn't make sense to talk about the wff being decidable. This is why I didn't see the point of your example.
 
Last edited:

Similar threads

Graduate Second-order arithmetic
  • · Replies 34 ·
2
Replies
34
Views
3K
Undergrad About the undecidability of first-order-logic
  • · Replies 26 ·
Replies
26
Views
4K
Graduate Second order logic and completeness
  • · Replies 11 ·
Replies
11
Views
3K
Undergrad Syntactic vs semantic logical consequence (entailment)
  • · Replies 5 ·
Replies
5
Views
3K
Undergrad Deductive proof in logic formal systems
  • · Replies 4 ·
Replies
4
Views
902
Graduate Are formal systems of first order logic incomplete?
  • · Replies 14 ·
Replies
14
Views
4K
Undergrad Questions about SMT logic solvers
  • · Replies 2 ·
Replies
2
Views
2K
Graduate First order logic and set theory: who comes first?
  • · Replies 2 ·
Replies
2
Views
3K
Graduate Transcription from SQL to FOL (First Order Logic)
  • · Replies 3 ·
Replies
3
Views
3K
Undergrad What is truth in the completeness theorem?
  • · Replies 7 ·
Replies
7
Views
2K