Can it be that the only way to prove a theorem is based on generation of new tautologies?

66 Views Asked by At

We can use a language of a given logic (for example propositional logic or predicate logic) to formulate statements. We can also use rules of inference to reformulate single statements (derive "new" statements from "old" ones) or to combine two existing statements to generate a new statement.

We can also say that we might have a minimal complete set of inference rules (we do not need more rules and we cannot remove any rules).

Can it be the case for a given statement (or a set of statements) none of the inference rule is applicable but a combination of them is applicable?

Here is what I mean in a bit extended form. Inference rules are tautologies likee: $A \land B \iff B \land A$, $A \land (B \lor C) \iff (A \land B) \lor (A \land C)$. We can combine these tautologies to create more complex (larger) tautologies. Now, I can imagine that one of these "larger" tautologies can be applied to one of my statements (or a combination of two statements) to generate a new statements that follows (in a logical sense) from the "old" statement(s).

Can it be the case that it would be impossible to go from the "old" statement(s) to the "new" one just by applying the original (basic, atomic) tautologies but it is possible to get the "new" statement if we combine the original (basic, atomic) tautologies to get a more complex one and then we apply it to derive a "new" statement from the old one?

ADDED

I feel like I need to clarify my question. In a logic (for example propositional logic) we have a small and limited set of inference rules (let's call the "basic rules") that we can use to derive "new" statements (theorems) from "old" statements (old theorems and axioms). The whole process of derivations can be imagined as applying "basic rules" to existing statements to generate new statements until we reach the statement we need.

However, alternatively, one can combine "basic rules" with each other to derive new rules (let's call them "derived rules"). For example, if the first basic rules is "a + b = b + a" and the second basic rule is "a * (b + c) = (a * b) + (a * c)", then we can combine these two rules to generate a new "derived" rule: "a * (b + c) = (a * c) + (a * b)". And then, as soon as we have a new rule, we can apply it to a statement, to transform it. For example if we have a "statement" "2 * (3 + 4)" we can transform it using our new "derived rule" to get "(2 * 4) + (2 *3)".

So, my question was, if it might be the case that some statements ("theorems") are unreachable by "basic rules" only. So, in that case, instead of applying our "basic rules" to the statements, we need first to combine our "basic rules" to get new rules ("derived") and then apply the derived rules to our statements.

2

There are 2 best solutions below

1
On

This is somewhat ambiguous. An inference rule is just a rule that tells you what sentences you can derive from other sentences. A tautology is a sentence that is true on every interpretation. The term usually refers to sentences in propositional logic that are true for any assignment of truth values to atoms. In this sense, using the standard axiomatisation of propositional logic, we can prove any tautology. This isn't very dramatic: truth tables are themselves a quasi-formal system, just not one consisting of strings of symbols. For this reason propositional logic is called "complete". We might also wonder about things true on every interpretation in predicate logic (although tautology has a stricter meaning here). It turns out we have a positive result here called Godel's Completeness Theorem. This says that a statement in predicate logic is provable if and only if there it has a model, or interpretation. However, models are a tricky business. Peano Arithmetic, the standard first-order formalism for arithmetic, has non-standard models, which behave nothing like we imagine numbers working.

You might ask, can every true statement in a theory be proven. If you're bound by the apparent laws of physics, then the answer is no. Godel's First Incompleteness Theorem states that no sufficiently expressive computable (emulatable on a computer) formal system can be both consistent (not prove contradictions) and complete (in this context, give every sentence of the theory a true or false value). This matters because there is no evidence that physics itself can do anything more than a computer, with the (possible) exception of randomisation, which wouldn't help you to make a formal logic that you actually believed in. So, there will always be sentences about certain things that you can't decide are true or false using your favourite formal system. So you would have to add new rules to any formal system you could actually use to derive them. Of course, this would include the formal system you're using in your brain (if your the human brain actually has consistent fundamental rules of reason), so after a certain point you wouldn't be able to work out whether or not you should add them.

0
On

If I interpret your question correctly, it seems to me you are asking:

If you can prove a theorem using "derived" rules, is it possible to prove it using only "atomic" rules?

This is a very interesting question, and is actually the content of Gentzen's cut elimination theorem, which he needed to prove consistency of arithmetic.

Cut elimination concerns a special rule called the "cut" rule, which is written

$$\frac{\Gamma\vdash A\quad \Delta,A\vdash B}{\Gamma,\Delta\vdash B}$$

and is read "If $A$ can be proved from hypotheses $\Gamma$, and if $B$ can be proved from hypotheses $\Delta,A$, then $B$ can be proved from hypotheses $\Gamma,\Delta$".

The content of this rule is that $A$ can be viewed as a lemma (or "derived" rule, as you put it), and this rule allows you to use this lemma in your proof of $B$.

The cut elimination theorem tells us that this rule is actually not needed. This theorem actually gives us an algorithm for converting a proof that uses the cut rule into a proof that does not use it (that is only uses "atomic" rules). The caveat is that the resulting proof may be exponentially larger than the original proof using cut.