Undecidability is the property of a statement or problem that cannot be settled as true or false within a formal system. In Formal Logic I, it marks a hard limit on what symbols, axioms, and rules can prove.
Undecidability is the point where a formal system runs out of proof power. In Formal Logic I, it means there are well-formed statements or problems that your system cannot settle, even if the system is consistent and the rules are applied correctly.
That does not mean the statement is meaningless. It means the system cannot derive a proof of it or a proof of its negation from the axioms and inference rules it has. So the issue is not whether a human can imagine an answer, but whether the formal machinery can force an answer.
This idea shows up most clearly in the background of Gödel's Incompleteness Theorems. Gödel showed that any consistent formal system strong enough to express arithmetic will leave some true statements unprovable inside that same system. That is a narrower claim than saying everything is undecidable, but it points to the same boundary: there is no perfect axiom set that captures every truth of arithmetic.
A second classic example is the Halting Problem. The question is whether a given computer program will eventually stop or keep running forever. Turing showed there is no single algorithm that can solve that question for all programs. In logic terms, that problem is undecidable because no general procedure can decide every case.
A useful way to think about undecidability is to separate three ideas: true, false, and settled by the system. A statement can be true in the intended interpretation but still undecidable within a given formal setup. That gap is what makes undecidability such a big deal in logic, because it shows formal proof and mathematical truth are not always the same thing.
You will usually meet undecidability near questions about the limits of axioms, proof, and computation. It is not a flaw in logic. It is one of the main results that tells you what logic can do, and what it cannot do no matter how carefully you build the system.
Undecidability is one of the main limit results in Formal Logic I, so it changes how you think about proof. Earlier topics like validity and soundness can make logic feel complete and mechanical, but undecidability shows that even a perfectly formed system can leave some questions unresolved.
It matters most when you are comparing syntax and semantics. A statement may be true in the intended mathematical structure, but no proof rules inside the system can reach it. That distinction comes up whenever you ask whether axioms are enough, whether a proof system is complete, or whether a decision procedure can exist for a class of problems.
The idea also connects logic to computer science. The Halting Problem is a standard example because it turns a question about programs into a question about formal limits. If you can recognize why the Halting Problem is undecidable, you can also see why some algorithmic tasks cannot be automated in a general way.
In class, undecidability often becomes the reason certain proof searches or decision procedures fail. Instead of expecting every symbolic question to have a yes or no algorithmic answer, you learn to ask whether the system can settle the claim at all. That shift is central to understanding the boundary of formal reasoning.
Keep studying Formal Logic I Unit 13
Visual cheatsheet
view galleryGödel's Incompleteness Theorems
Gödel's Incompleteness Theorems supply the famous logical context for undecidability. They show that a consistent formal system with arithmetic cannot prove every truth it can express. When you see an undecidable statement in arithmetic, Gödel explains why the system cannot close every gap just by adding more derivations.
Formal System
Undecidability only makes sense relative to a formal system, because the same statement can be settled in one system and unsettled in another. The axioms and inference rules determine what counts as provable. So when a problem is undecidable, you are really seeing the limits of that particular formal setup.
Decidability
Decidability is the opposite idea, where there is a procedure that can determine the answer for every case in the domain. Comparing it with undecidability helps you see the difference between solvable and unsolvable problem classes. In logic and computation, that comparison often appears in questions about algorithms or proof procedures.
Turing Machine
Turing machines give the standard model for discussing algorithmic limits. The Halting Problem is framed in terms of what a Turing machine can or cannot decide about another machine's behavior. If you are studying undecidability, Turing machines give the formal setup that makes the limit precise.
A problem set question may ask you to tell whether a statement is decidable, provable, or refutable in a given system. You would show that undecidability means no general proof procedure settles every case, then connect that to a familiar example like the Halting Problem.
Short-answer and essay prompts often ask you to explain why this matters for formal logic. The strongest move is to distinguish truth from provability: a statement can be true in the intended model and still be undecidable inside the system. If the question mentions Gödel or Turing, you should use them as the reason the limit exists, not just as names to drop.
If the class gives you a scenario about an algorithm, a proof search, or a symbolic rule system, ask whether it guarantees an answer for every input. If it does not, that is where undecidability enters your explanation.
Decidability is the condition where a problem has a general method for reaching a yes or no answer in every case. Undecidability is the failure of that condition. The confusion is common because both terms talk about whether a problem can be settled, but they point in opposite directions.
Undecidability means a formal system cannot prove or disprove certain statements, even when the system's rules are applied correctly.
A statement can be true and still be undecidable inside a specific system, so truth and provability are not always the same thing.
Gödel's Incompleteness Theorems explain why arithmetic-rich consistent systems leave some truths unsettled.
The Halting Problem is the classic computational example of undecidability, showing that no universal algorithm can solve every case.
When you see undecidability in Formal Logic I, think about the limits of axioms, proof rules, and decision procedures.
Undecidability is when a statement or problem cannot be settled as true or false within a formal system. In Formal Logic I, that usually means the system does not have enough proof power or no general algorithm exists to decide every case. It is one of the main ways logic shows its own limits.
Not exactly. Unprovable means you cannot derive the statement from the system's axioms, while undecidable usually means you cannot prove it or its negation within that system. In logic classes, undecidability often points to this stronger two-sided failure.
The Halting Problem is the standard example. It asks whether a program will stop running or keep going forever, and there is no single algorithm that can answer that for all programs. That makes it a clean example of undecidability in computation.
Gödel showed that any consistent formal system strong enough to express arithmetic will leave some statements neither provable nor disprovable inside the system. That is a major source of undecidability in logic. It is one reason Formal Logic I treats proof systems as powerful, but not all-powerful.