Tuesday, March 3, 2020

The well-formed formulas of a propositional or predicate calculus can get recursively generated.  All well-formed formulas of a propositional calculus have a length which we can use a natural number to measure.  All natural numbers that we know of belong to a finite set.  There exists a countable infinity of natural numbers all of which are greater than any natural numbers we know.  Similarly, there exists a countable infinity of tautologies longer than the complete set of known tautologies (all known and knowable tautologies are short). 

No claim or conjecture is a theorem until proven.  Every proof is finite, and thus no claim or conjecture becomes a theorem without adequate physical objects, or communication, to prove the conjecture.  The number of possible physical objects in existence is finite.  Thus, there do not exist enough materials, nor will there ever exist enough materials to prove all tautologies.

But there exist tautologies which require more materials to prove than is possible.  Thus, not every tautology can become a theorem.

Therefore, all claims of completeness are incorrect.

But, if a claim that some well-formed formula is a tautology needs to get validated in order for that well-formed formula to qualify as a tautology, then the number of tautologies is also finite.  Since generating theorems by various techniques, including by theorem provers, seems to overwhelmingly produce more well-formed formulas which are theorems than validating processes seem to produce tautologies, that implies that either there exists some small set of tautologies which have not gotten validated, or completeness claims are likely correct.