命题演算Post完全性证明求助：添加非定理公理后系统不一致

Hey there! Glad you're joining the conversation here—let's walk through how to prove this property clearly, step by step. I’ll keep things straightforward since you mentioned this is your first post and your English is still a work in progress.

First, let's recap key definitions to make sure we're aligned:

• Post Completeness: A logical system is Post complete if adding any non-theorem as an axiom schema makes the system inconsistent (meaning you can prove every formula in the language).
• Classical Propositional Calculus (PC): We’ll assume we’re working with standard PC, which has three critical properties:
  • Semantically complete (all tautologies are theorems)
  • Consistent (you can’t prove both a formula and its negation)
  • Closed under substitution (if a formula is a theorem, all its substitution instances are also theorems)

Proof Outline #

Here’s the core reasoning to show PC has Post completeness:

1. Start with a non-theorem formula
   Let A be any formula that is not a theorem of PC. By PC’s semantic completeness, this means A is not a tautology—there exists at least one truth assignment that makes A false.

2. Turn the non-theorem into a contradiction via substitution
   Since A fails under some truth assignment, we can create a substitution rule that replaces each propositional variable in A to force the whole formula to be false everywhere:

   • For each variable p:
     • If the assignment makes p true, replace p with a tautology like p ∨ ¬p
     • If the assignment makes p false, replace p with a contradiction like p ∧ ¬p
       The resulting substitution instance of A will be false under all truth assignments—it’s a full contradiction (we’ll write this as ⊥ for shorthand).

3. The new system can prove the contradiction
   Since we added A as an axiom schema, every substitution instance of A counts as a theorem in the new system PC + A. That means our contradiction ⊥ is a theorem here.

4. A contradiction breaks consistency
   In classical PC, once you can prove ⊥, you can prove any formula B. Why? The formula ⊥ → B is a tautology, which is already a theorem of PC. Using modus ponens (PC’s main inference rule), we can derive B from ⊥ and ⊥ → B.

5. Final conclusion
   Adding any non-theorem A to PC results in a system where every formula is provable—so the system is inconsistent. This is exactly the definition of Post completeness.

Quick Clarifications #

• We rely on PC’s semantic completeness here—if you haven’t proven that yet, you can use a truth table method or Henkin’s completeness proof to establish it first.
• The substitution step is crucial: axiom schemas let us tweak A arbitrarily, so we can always turn a non-tautology into a full contradiction when we add it as an axiom.

内容的提问来源于stack exchange，提问作者Ay-jay