Back to the on-screen lesson ·
distinguish a proof-system property from a claim about one proof
Paper packet. Every task here also exists on screen, where it is checked automatically; answers written on paper are not assessed by Nydus. When you are back at a device, enter your answers there.
You will distinguish a proof-system property from a claim about one proof, recording the intermediate model values and the precise reason each conclusion follows.
Recall the truth conditions for not, and, or and if-then. Those rules still govern compound formulas here, but atomic truth now comes from objects and predicate extensions or from a world's valuation. Identify which new structure this lesson introduces before using a familiar propositional rule.
| Term | What it means |
|---|---|
| Interpretation | A declared domain and meanings for the nonlogical symbols; a modal interpretation also specifies worlds, accessibility and valuations. |
| Assignment | A choice of domain object for a free variable during an evaluation; it is not itself another domain object. |
| Witness | An eligible object or accessible world satisfying the property required by an existential or possibility claim. |
| Counterexample | An eligible case where the required condition fails; a countermodel to an inference additionally makes every premise true. |
| Validity | Truth in every interpretation of the specified kind, a stronger claim than truth in one supplied model. |
Soundness of a proof system says that its derivations preserve semantic consequence: what it proves from premises follows from those premises in the intended class of interpretations. For theorems with no premises, provability implies validity. Completeness gives the converse direction: semantic consequence can be captured by a derivation, or every valid formula is a theorem in the corresponding no-premise statement.
Draw two sets, valid formulas and provable formulas. Soundness places the provable set inside the valid set. Completeness places the valid set inside the provable set. Both together make the sets coincide. A proof of an invalid formula refutes soundness. A valid formula established to be unprovable refutes completeness. Not having found a proof yet does not establish unprovability.
The properties concern an entire system and a specified semantics. Checking four sample formulas can expose a failure but cannot prove that all formulas satisfy the required inclusion. A soundness proof typically checks the basic rules and then reasons over the structure of derivations. Completeness requires a different argument connecting semantic consequence to derivability.
Classical first-order logic has sound and complete standard proof calculi. This does not mean that every true sentence of an intended mathematical structure is provable from a chosen theory, or that an algorithm always decides first-order validity. Completeness of the logical calculus and incompleteness phenomena for sufficiently strong axiomatic theories address different questions. Keep the premises, system and meaning of true explicit before comparing the claims.
Another way: An explicit audit sheet
Keep four parts on the page: the declared objects or worlds, the meaning of each symbol, the intermediate values, and the conclusion. A changed interpretation belongs on a new sheet so the premises and conclusion are never checked in different models.
A hypothetical proof system has an exhaustive audit of these sample formulas: A, B, C, D. Exactly A, B are valid. Exactly A, B are provable. Treat 'not provable' as supplied information, not as failure to find a proof. Count proved invalid formulas, valid unproved formulas, and formulas satisfying both validity and provability. This sample can reveal a failure; it cannot establish a global system theorem.
Formula A is valid and is provable in the supplied audit. A valid and provable formula fits both desired directions, but that one success cannot establish a theorem about every formula in the system.
Formula B is valid and is provable in the supplied audit. A valid and provable formula fits both desired directions, but that one success cannot establish a theorem about every formula in the system.
Formula C is invalid and is not provable in the supplied audit. Its status must be compared with the direction being tested: soundness starts from provability, whereas completeness starts from validity. A failure of one direction need not be a failure of the other.
Formula D is invalid and is not provable in the supplied audit. Its status must be compared with the direction being tested: soundness starts from provability, whereas completeness starts from validity. A failure of one direction need not be a failure of the other.
Proved invalid formulas: 0. Soundness requires every provable formula to be valid. Search among the provable formulas for one outside the valid set. Any such example is enough to refute soundness for the purported system and semantics. If none appears in a finite sample, report only that the sample contains no counterexample; a global soundness theorem must cover all proofs, usually by an argument about the rules.
Valid unproved formulas: 0. Completeness requires every valid formula to be provable. Search the valid set for a formula outside the provable set. The audit explicitly gives nonprovability, which is much stronger than saying a learner has not yet found a proof. The latter is not a completeness counterexample. Keep the quantification over all formulas in view when moving from sample checks to system-level claims.
Both valid and provable: 2. The intersection records successes shared by the two sets. Counting these successes does not answer either failure question on its own. A system could prove many valid formulas while also proving one invalid formula, which would destroy soundness. It could prove only valid formulas while missing others, making it sound but incomplete. The two properties govern different inclusions, not how impressive a proof looks.
Compare system soundness with a sound argument. The latter means a valid argument whose premises are true in the intended situation. System soundness is a general relation between permitted derivations and the semantics. A sound proof system can be used with false premises without making it unsound: its guarantee is that true premises cannot lead by its rules to a false conclusion. These levels must remain separate.
A hypothetical proof system has an exhaustive audit of these sample formulas: A, B, C, D, E. Exactly A, B are valid. Exactly A are provable. Treat 'not provable' as supplied information, not as failure to find a proof. Count proved invalid formulas, valid unproved formulas, and formulas satisfying both validity and provability. This sample can reveal a failure; it cannot establish a global system theorem.
Formula A is valid and is provable in the supplied audit. A valid and provable formula fits both desired directions, but that one success cannot establish a theorem about every formula in the system.
Formula B is valid and is not provable in the supplied audit. Its status must be compared with the direction being tested: soundness starts from provability, whereas completeness starts from validity. A failure of one direction need not be a failure of the other.
Formula C is invalid and is not provable in the supplied audit. Its status must be compared with the direction being tested: soundness starts from provability, whereas completeness starts from validity. A failure of one direction need not be a failure of the other.
Formula D is invalid and is not provable in the supplied audit. Its status must be compared with the direction being tested: soundness starts from provability, whereas completeness starts from validity. A failure of one direction need not be a failure of the other.
Formula E is invalid and is not provable in the supplied audit. Its status must be compared with the direction being tested: soundness starts from provability, whereas completeness starts from validity. A failure of one direction need not be a failure of the other.
Proved invalid formulas: 0. Soundness requires every provable formula to be valid.
Valid unproved formulas: 1. Completeness requires every valid formula to be provable.
Both valid and provable: 1. The intersection records successes shared by the two sets.
Compare system soundness with a sound argument. The latter means a valid argument whose premises are true in the intended situation. System soundness is a general relation between permitted derivations and the semantics. A sound proof system can be used with false premises without making it unsound: its guarantee is that true premises cannot lead by its rules to a false conclusion. These levels must remain separate.
A hypothetical proof system has an exhaustive audit of these sample formulas: A, B, C, D, E, F. Exactly A, B, C are valid. Exactly A, B, C, F are provable. Treat 'not provable' as supplied information, not as failure to find a proof. Count proved invalid formulas, valid unproved formulas, and formulas satisfying both validity and provability. This sample can reveal a failure; it cannot establish a global system theorem.
Formula A is valid and is provable in the supplied audit. A valid and provable formula fits both desired directions, but that one success cannot establish a theorem about every formula in the system.
Formula B is valid and is provable in the supplied audit. A valid and provable formula fits both desired directions, but that one success cannot establish a theorem about every formula in the system.
Formula C is valid and is provable in the supplied audit. A valid and provable formula fits both desired directions, but that one success cannot establish a theorem about every formula in the system.
Formula D is invalid and is not provable in the supplied audit. Its status must be compared with the direction being tested: soundness starts from provability, whereas completeness starts from validity. A failure of one direction need not be a failure of the other.
Formula E is invalid and is not provable in the supplied audit. Its status must be compared with the direction being tested: soundness starts from provability, whereas completeness starts from validity. A failure of one direction need not be a failure of the other.
Formula F is invalid and is provable in the supplied audit. Its status must be compared with the direction being tested: soundness starts from provability, whereas completeness starts from validity. A failure of one direction need not be a failure of the other.
Proved invalid formulas: 1. Soundness requires every provable formula to be valid.
Valid unproved formulas: 0. Completeness requires every valid formula to be provable.
Both valid and provable: 3. The intersection records successes shared by the two sets.
Compare system soundness with a sound argument. The latter means a valid argument whose premises are true in the intended situation. System soundness is a general relation between permitted derivations and the semantics. A sound proof system can be used with false premises without making it unsound: its guarantee is that true premises cannot lead by its rules to a false conclusion. These levels must remain separate.
Imagine a small audit ledger listing formulas A, B, C, and D. Semantic analysis marks A, B, and C valid. A proposed calculus has proofs of A and B only. In this finite ledger, every proved formula is valid, while C is a valid formula missing from the proof list. The first observation concerns the soundness direction; the second concerns the completeness direction. The ledger does not itself prove a global theorem about the calculus, because formulas and proofs outside the ledger remain unexamined.
Now suppose the calculus also produces a proof of D, which has a verified countermodel. That pair—a derivation plus a falsifying interpretation—exposes a soundness failure for the claimed calculus and semantics. Adding many correct proofs would not remove the failure. A universal guarantee that every theorem is valid is defeated by one genuine exception.
The completeness direction has a different diagnostic burden. Failing to find a proof of C during a search does not establish that C is unprovable. The search might be unfinished. To refute completeness, one needs a semantically valid claim together with an appropriate demonstration that the system cannot derive it. In a worksheet that explicitly declares a finite ledger exhaustive, a set difference is enough for that bounded exercise. Outside that stipulation, absence from a list must not be mistaken for impossibility of proof.
Soundness of an individual argument is another usage of the same word. It requires validity and actually true premises. A sound proof system can manipulate a false premise without becoming an unsound system: its preservation guarantee is conditional on the premises being true. For example, deriving Q from P and P -> Q is permitted even when an actual investigation finds P false. The formal derivation is intact; the argument's factual basis is not.
Keep the objects of each claim explicit: an argument in an actual situation, a finite audit sample, or an entire calculus relative to a semantics. This prevents a correct observation at one level from being inflated into an unsupported theorem at another.
Imagine a rule engine used in a training simulation. An independent semantic audit identifies two sample conclusions as valid under the simulation's rules and two as invalid. The engine proves one valid conclusion and one invalid conclusion. The invalid proof is enough to show that this engine is not sound for the stated semantics. The successful valid proof does not cancel that failure.
Suppose the audit also establishes that a second valid conclusion cannot be proved by the engine's complete declared rule set. That supplies a completeness failure. This is stronger than a user saying that they tried several searches and found no proof. A failed search might simply have missed a longer derivation. The exercise supplies true nonprovability as part of its hypothetical audit so the distinction is not hidden.
An engine that proves only valid conclusions but misses some valid ones may be sound and incomplete. An engine that proves every valid conclusion and also invalid ones may be complete and unsound. These possibilities show why the two words are not interchangeable compliments. Each describes a specific inclusion between proof and validity.
For deployment, one would need a general correctness argument about the implementation and rules, not merely this four-case sample. The classroom audit trains the direction of the concepts. It also shows what a single example can legitimately establish: a counterexample can defeat a universal guarantee, while a few positive examples cannot establish that guarantee. The same asymmetry appeared earlier when evaluating universal claims over an incompletely checked range.
A correct evaluation answers the stated question for its stated interpretation. Do not turn a true instance into a universal rule or a successful example into a proof of validity. When the task is a proof audit, keep local assumptions and fresh parameters within their declared scope.
Record the interpretation and the question.
A hypothetical proof system has an exhaustive audit of these sample formulas: A, B, C, D, E. Exactly A, B are valid. Exactly B, E are provable. Treat 'not provable' as supplied information, not as failure to find a proof. Count proved invalid formulas, valid unproved formulas, and formulas satisfying both validity and provability. This sample can reveal a failure; it cannot establish a global system theorem.
Use the declared objects and meanings throughout this calculation: Proved invalid formulas is the first requested result.
Determine the requested value: Proved invalid formulas.
1
Soundness requires every provable formula to be valid.
Determine the requested value: Valid unproved formulas.
1
Completeness requires every valid formula to be provable.
Determine the requested value: Both valid and provable.
1
The intersection records successes shared by the two sets.
Collect the results in the requested order.
1 / 1 / 1
Each result belongs to its own entry: Proved invalid formulas; Valid unproved formulas; Both valid and provable.
Record the interpretation and the question.
A hypothetical proof system has an exhaustive audit of these sample formulas: A, B, C, D, E, F. Exactly A, B, C are valid. Exactly A, B, C are provable. Treat 'not provable' as supplied information, not as failure to find a proof. Count proved invalid formulas, valid unproved formulas, and formulas satisfying both validity and provability. This sample can reveal a failure; it cannot establish a global system theorem.
Use the declared objects and meanings throughout this calculation: Proved invalid formulas is the first requested result.
Determine the requested value: Proved invalid formulas.
0
Soundness requires every provable formula to be valid.
Determine the requested value: Valid unproved formulas.
0
Completeness requires every valid formula to be provable.
Determine the requested value: Both valid and provable.
3
The intersection records successes shared by the two sets.
Collect the results in the requested order.
0 / 0 / 3
Each result belongs to its own entry: Proved invalid formulas; Valid unproved formulas; Both valid and provable.
Record the interpretation and the question.
A hypothetical proof system has an exhaustive audit of these sample formulas: A, B, C, D, E, F, G. Exactly A, B, C are valid. Exactly A are provable. Treat 'not provable' as supplied information, not as failure to find a proof. Count proved invalid formulas, valid unproved formulas, and formulas satisfying both validity and provability. This sample can reveal a failure; it cannot establish a global system theorem.
Use the declared objects and meanings throughout this calculation: Proved invalid formulas is the first requested result.
Determine the requested value: Proved invalid formulas.
0
Soundness requires every provable formula to be valid.
Determine the requested value: Valid unproved formulas.
2
Completeness requires every valid formula to be provable.
Determine the requested value: Both valid and provable.
1
The intersection records successes shared by the two sets.
Collect the results in the requested order.
0 / 2 / 1
Each result belongs to its own entry: Proved invalid formulas; Valid unproved formulas; Both valid and provable.
Test which alteration would change the conclusion.
Compare system soundness with a sound argument. The latter means a valid argument whose premises are true in the intended situation. System soundness is a general relation between permitted derivations and the semantics. A sound proof system can be used with false premises without making it unsound: its guarantee is that true premises cannot lead by its rules to a false conclusion. These levels must remain separate.
The altered interpretation checks the dependence of these answers on the stated model, rather than replacing it during the calculation.
Determine the requested value: Proved invalid formulas.
1
Soundness requires every provable formula to be valid.
Determine the requested value: Valid unproved formulas.
Determine the requested value: Both valid and provable.
A hypothetical proof system has an exhaustive audit of these sample formulas: A, B, C, D, E, F, G. Exactly A, B, C are valid. Exactly B, G are provable. Treat 'not provable' as supplied information, not as failure to find a proof. Count proved invalid formulas, valid unproved formulas, and formulas satisfying both validity and provability. This sample can reveal a failure; it cannot establish a global system theorem.
| Computed result | |
|---|---|
| Proved invalid formulas | |
| Valid unproved formulas | |
| Both valid and provable |
A hypothetical proof system has an exhaustive audit of these sample formulas: A, B, C, D, E, F, G, H, I. Exactly A, B, C, D are valid. Exactly B, I are provable. Treat 'not provable' as supplied information, not as failure to find a proof. Count proved invalid formulas, valid unproved formulas, and formulas satisfying both validity and provability. This sample can reveal a failure; it cannot establish a global system theorem.
Find provable formulas outside the valid set.
b0
The requested entry concerns proved invalid formulas; retain its stated scope.
Find valid formulas outside the provable set.
b1
The requested entry concerns valid unproved formulas; retain its stated scope.
Count the intersection of the two sets.
b2
The requested entry concerns both valid and provable; retain its stated scope.
A hypothetical proof system has an exhaustive audit of these sample formulas: A, B, C, D, E, F, G, H. Exactly A, B, C, D are valid. Exactly A, B, C, D are provable. Treat 'not provable' as supplied information, not as failure to find a proof. Count proved invalid formulas, valid unproved formulas, and formulas satisfying both validity and provability. This sample can reveal a failure; it cannot establish a global system theorem.
Proved invalid formulas: b0
Valid unproved formulas: b1
Both valid and provable: b2
A hypothetical proof system has an exhaustive audit of these sample formulas: A, B, C, D, E, F, G. Exactly A, B, C are valid. Exactly A are provable. Treat 'not provable' as supplied information, not as failure to find a proof. Count proved invalid formulas, valid unproved formulas, and formulas satisfying both validity and provability. This sample can reveal a failure; it cannot establish a global system theorem.
Proved invalid formulas: b0
Valid unproved formulas: b1
Both valid and provable: b2
A hypothetical proof system has an exhaustive audit of these sample formulas: A, B, C, D, E, F, G, H. Exactly A, B, C, D are valid. Exactly A, B, C, D, H are provable. Treat 'not provable' as supplied information, not as failure to find a proof. Count proved invalid formulas, valid unproved formulas, and formulas satisfying both validity and provability. This sample can reveal a failure; it cannot establish a global system theorem.
Proved invalid formulas: b0
Valid unproved formulas: b1
Both valid and provable: b2
An educational rule engine is compared with an independently established semantic audit of its sample conclusions. The data below form the complete invented audit. A hypothetical proof system has an exhaustive audit of these sample formulas: A, B, C, D, E, F, G, H. Exactly A, B, C, D are valid. Exactly A, B, C, D are provable. Treat 'not provable' as supplied information, not as failure to find a proof. Count proved invalid formulas, valid unproved formulas, and formulas satisfying both validity and provability. This sample can reveal a failure; it cannot establish a global system theorem.
Proved invalid formulas: b0
Valid unproved formulas: b1
Both valid and provable: b2
Lesson test: one question per skill, one attempt each, no hints. Your answers are checked when you submit.
A hypothetical proof system has an exhaustive audit of these sample formulas: A, B, C, D, E, F, G, H, I. Exactly A, B, C, D are valid. Exactly A are provable. Treat 'not provable' as supplied information, not as failure to find a proof. Count proved invalid formulas, valid unproved formulas, and formulas satisfying both validity and provability. This sample can reveal a failure; it cannot establish a global system theorem.
Proved invalid formulas: b0
Valid unproved formulas: b1
Both valid and provable: b2
You can distinguish a proof-system property from a claim about one proof. Reconstruct the three audit entries from a fresh model without consulting the examples; explain what change to the interpretation would change one answer.
14. Complete the next model audit, step 2
0
Completeness requires every valid formula to be provable.
14. Complete the next model audit, step 3
3
The intersection records successes shared by the two sets.