Demonstration of proving a statement is unprovable

Question

Similar questions have been asked, but this is not a duplicate.

I'm looking for a proof itself, not a description of methods.

Related:

• How do we prove that something is unprovable?
• is possible to make a concrete boundary between provable problems and unprovable problems in a certain axiomatic system
• Using a proof by contradiction with unprovable statement

The Most Trivially Unprovable Statement

(Or at least the most trivial one I could think of)

Given/Assuming

• The axioms of propositional logic are consistent
• P is true

Goal: Prove Q is true

((Prove that the goal is unprovable under the assumptions))

Not Theory: The Practical / Algorithmic Side

I've written a logic solver program that uses term-rewriting.

While it prefers simplification, when stuck it can use tautologies to expand statements like P into not(not(P)) or not(not(not(not(P)))) and it can generate Q or not(Q) from nothing. However, given P prove Q would cause it to expand forever (given infinite memory).

Yet, while it spends infinite time, we personally waste almost 0 time thinking about the same task because we instantly recognize given P prove Q is unprovable.

The precursor to my real question is: How can we algorithmically detect/prove this kind of unprovablility?

Existing Answers

The TLDR from other Q&A's is:

1. Add an assumption that makes the goal true
2. Restart and add an assumption that makes the goal false
3. Show that neither case would contradict the axioms/givens

The Problem/Question with Those

Step #1 and #2 are trivial in code, my problem and real-question is precisely about step #3 (prove consistency). I do not know how, and actually because of Godël, feel like it is impossible to complete step 3. Even for a trivially true case like show "given P, prove Q" is unprovable.

So please, if someone can show a formal proof for the trivial example above, I think I will be able to apply it generically.

AFTER a proof is shown (or a claim that there is no proof) I would be happy to have discussions of meta-systems, soundness, consistency, etc. But I need to see the concrete first, then I will be able to see the patterns and understand the theory

Clarifications

I do want to follow the human method (e.g. knowing that Q is not a member of the infinite set of all possible substitutions of P). And I'm completely find with using meta systems to get there, even if the meta systems themselves are not guaranteed to ever reach a stopping point.

Answer 1

Thanks @Bram28 and @Mauro ALLEGRANZA, your comments of meta logic and tautologies was just enough for the relationship between satisfiability and step #3 to click together.

Please correct me if any of this is wrong (particularly in the "term rewriting" part of the algorithm at the bottom)

Proof

Show that Given P, prove Q is unprovable

Step 1, Meta System

Create a meta system, by treating the proof itself as an expression.
Expression: $P \implies Q$

More generically

• Given [...givens], Prove goal
  

Becomes

• Expression: $(\text{given1} \land \text{given2} \land \text{ ... }) \implies \text{goal}$

Step 2, Burden of proof

• If the expression is a tautology, then indeed goal is proved by [...givens]
• If the expression is unsatisfiable, then ¬goal is proved by [...givens]
• If the expression is neither (aka contingent), then goal is unprovable given only [...givens]

Step 3, Truth table

Any method that resolves the burden of truth works fine, and the most easy for this example is the truth table.

___________________________________________________________________________________
|   P   |   Q   || P -> Q | comment                                                |
|----------------------------------------------------------------------------------|
| True  | True  || True   | okay so its at least satisfiable                       | 
| True  | False || False  | and its also not a tautology, so it must be contingent |
|                         | (we dont even need to finish the truth table)          |
-----------------------------------------------------------------------------------

Step 4, Conclusion

Since P -> Q is contingent, proving Q while given only P is therefore impossible.

Algorithm

For covering more advanced cases, I wrote out this algorithm.

# truth table
if there are few enough variables
then 
    brute force an answer to "it is a tautology, unsatisfiable, or neither (aka contingent)?"
    then go to the resolution step below

# pattern match
if the expression matches a pattern that is:
    known to be a tautology
    or known to unsatisfiable
    or known to be contingent
then
    then go to the resolution step below

# term rewriting
for tautological and unsatisfiable expressions
given the already-known expressions
use rules of inference to generate derivative tautological/unsatisfiable expressions

for contingent expressions
given the already-known contingent expressions
use truth-preserving rules of inference to generate new contingent expressions

go back to pattern match (possibly infinite loop here and thats fine)

# resolution
if the top expression is a tautology: like (A -> A)
    then the whole proof is true (and obviously provable because it was proved true)
else if the top level expression is an unsatisfiable expression: like (A -> ¬A)
    then the whole proof is false (and obviously provable because it was proved false)
else if the expression is contingent: like (A -> B)
    then the whole proof is unprovable
```