General view of Theorems

Question

I'm trying to see almost all theorems ( at least the non-existential ones ) as affirming that some formula ( mostly of first-order logic language ) is a logical consequence of other formulas.

So, given a Theorem, if its hypothesis are $A_i$ and it's conclusion is $C$, it would be affirming that :
$$\left\{ {A_1 ,A_2 , A_3,..,A_n} \right\} \models C$$

Then by Deduction Theorem, this is the same as affirming that the following formula is logically valid.
$$A_1 \wedge A_2 \wedge A_3 \wedge ... \wedge A_n \to C$$

But to say that that formula is logically valid, is the same as saying that, for example, the following also is :

$$A_3 \to ( A_1 \wedge A_2 \wedge A_4 \wedge ... \wedge A_n \to C )$$

Or that the following ( reduction ad absurdum ) is logically valid ....
$$[\neg (A_1 \wedge A_2 \wedge A_3 \wedge ... \wedge A_n \to C) \to B ] \wedge [ \neg (A_1 \wedge A_2 \wedge A_3 \wedge ... \wedge A_n \to C) \to \neg B ] \to (A_1 \wedge A_2 \wedge A_3 \wedge ... \wedge A_n \to C) $$

Or that for example, the following formula is logically valid ( by doing some equivalences and using contrapositive ).
$$(A_1 \wedge \neg C \wedge A_3 \wedge A_4) \to ( A_5 \wedge .... \wedge A_n \wedge A_2) $$

Which would be affirming that :
$$ \left\{ {A_1,\neg C , A_3, A_4 } \right\} \models ( A_5 \wedge .... \wedge A_n \wedge A_2) $$

Which could be thought as a new theorem. And the previous formulas could also thought as representing some theorem.

And the list could go on, providing logically equivalent formulas, by using the axiom schemmas of propositional logic, equality and first-order-logic.

So i have two questions :

1 - Is this to say that actually each one of those logically equivalent formuals represents a theorem that is equivalent to the theorem represented by our initial formula ? Is this to say that actually a theorem represents a bunch of equivalent theorems and we can choose to prove any representative of that "Theorem Equivalence class" , and by proving that we will have proved all our other representatives, including our initial representative of the theorem ( that were given in the problem or that were written initially ) ?

2 - Now, if the first question has a positive answer. The most important question ( for me ): If have a proof of some representative of some "Theorem Equivalence class" ( as i'm calling the set of all theorems represented by formulas that are logically equivalent to one another ) , are we sure that there exists a proof of each representative of that "Theorem Equivalence class" ? I think ( but i'm not sure ) that this is the same as asking, that if a theorem can be proved by a specific method ( supppose some direct proof ), are we 100% sure it can be proven by all other valid methods ( all other direct proofs, proof by contradiction, etc,etc ) ?

As an example, our Theorem is :

$$ \text{Suppose } a,b \text{ and } c \text{ are real numbers and } a>b. \text{ If } ac \leq bc \text{ then } c \leq0 .$$

I'm interpreting this theorem as affirming that :
$$ \left\{ "\text{a,b,c are real numbers, "a>b"}" \right\} \models (ac \leq bc \to c\leq 0 ) $$

Then by deduction-theorem, exportation and contrapositive, we could reach the following formula :
$$ \left\{ "c > 0 ", (ac \leq bc ), "a>b" \right\} \models \text{ "a,b,c are not real numbers" } $$

Which could be thought as representing the following theorem :
$$ \text{Suppose } c>0 \text{ ,} ac \leq bc.\text{ If a>b, then a,b or c are not real numbers} $$

Now, since we are able to prove the initial theorem ( by doing contrapositive on the last two formulas ) does this means that we could also prove the theorem whose conclusion is a,b,c are not real numbers and also all others possibly obtained by logical equivalences ?

Thanks a bunch !

Answer 1

Question 2)

If I understand well your example, from :

$[(\mathbb R(a) \land \mathbb R(b) \land \mathbb R(c)) \land (a > b)] \rightarrow [(ac \le bc) \rightarrow (c \le 0)]$

through the tautology : $[(A \land B) \rightarrow (C \rightarrow D)] \leftrightarrow [(\lnot D \land B \land C) \rightarrow \lnot A]$

we can derive :

$[(c > 0) \land (a > b) \land (ac \le bc)] \rightarrow \lnot (\mathbb R(a) \land \mathbb R(b) \land \mathbb R(c))$.

Note. Please, be careful with the "reading" of the consequent : it says that one of $a,b,c$ is not a real number.

Of course, all the "intermediate" transformation licensed by logical rules are all theorems of your theory.

Question 1)

Let $A$ the above formula; saying that it is a theorem of a theory $T$ means that there is a set $\Gamma$ of non-logical axioms [the axioms of $T$], such that :

$\Gamma \vdash A$.

Now, if $A'$ is an "equivalent" transformation of $A$, i.e.if $\vdash A \leftrightarrow A'$, then simply with modus ponens we have that :

if $\Gamma \vdash A$, then $\Gamma \vdash A'$.

Added

We can "systhematize" this issue referring to Joseph Shoenfield, Mathematical Logic (1967), page 33 :

Deduction Theorem. Let $A$ be a closed formula in $T$. For every formula $B$ of $T$, $\vdash_T A \rightarrow B$ iff $B$ is a theorem of $T \cup \{ A \}$.

This is the fact we already know.

See also page 41 :

The primary object of a formal system is to provide a framework for proving theorems. Hence a particularly important problem for any formal system $\mathcal F$ is: find a necessary and sufficient condition that a formula of $\mathcal F$ be a theorem of $\mathcal F$.

This is called the characterization problem for $\mathcal F$. [...] There is a trivial solution to the characterization problem for a theory $T$: a formula is a theorem iff it has a preof.

Clearly whether or not $A$ is a theorem of $T$ depends strongly on what the nonlogical axioms of $T$ are. Hence we must expect the condition for $A$ to be a theorem of $T$ to refer not only to $A$, but also to the nonlogical axioms of $T$.

Page 42 :

If $\Gamma$ is a set of formulas in the theory $T$, then $T \cup \Gamma$ is the theory obtained from $T$ by adding all of the formulas in $\Gamma$ as new nonlogical axioms.

Reduction Theorem. Let $\Gamma$ be a set of formulas in the theory $T$, and let $A$ be a formula of $T$. Then $A$ is a theorem of $T \cup \Gamma$ iff there is a theorem of $T$ of the form $B_1 \rightarrow ( ... \rightarrow ( B_n \rightarrow A)...)$, where each $B_i$ is the closure of a formula in $\Gamma$ [obviously, the proof make use of the Deduction Th].

The reduction theorem reduces the characterization problem for $T \cup \Gamma$ to that for $T$. Now any theory $T'$ is $T \cup \Gamma$, where $T$ is obtained from $T'$ by omitting all nonlogical axioms and $\Gamma$ is the set of nonlogical axioms of $T'$.

Hence to solve the characterization problem for all theories, it suffices to solve it for theories with no nonlogical axioms.

For simplicity, we can use the example [page 22] regarding the :

elementary theory of groups, designated by $G$. The only non-logical symbol of $G$ is the binary function symbol $\circ$. The nonlogical axioms of $G$ are:

$G_1$. $\forall x \forall y \forall z [(x \circ y) \circ z = x \circ (y \circ z)]$

$G_2$. $\exists x[\forall y(x \circ y = y) \land \forall y \exists z(z \circ y = x )]$.

By a model of a theory $T$, we mean a structure for $L(T)$ [the language of the theory] in which all the non-logical axioms of $T$ are true.

A formula is true in $T$ if it is true in every model of $T$; equivalently, if it is a logical consequence of the nonlogical axioms of $T$.

In conclusion a theorem of group theory is a formula $A$ such that :

$\Gamma = \{ G_1, G_2 \} \vdash A$.

$A$ is true in every model of $\Gamma$, i.e.in every structure which satisfy the group axioms.

This fact does not imply that $A$ is logically (or universally) valid, i.e.true in every structure.

But, by the above results :

$G_1 \land G_2 \rightarrow A$

is valid.

Answer 2

"Is this to say that actually each one of those logically equivalent formuals represents a theorem that is equivalent to the theorem represented by our initial formula ?"

All theorems are logically equivalent anytime you have a you have the formulas [(p$\rightarrow$(q$\rightarrow$p)] and {(p$\rightarrow$q)$\rightarrow$[(q$\rightarrow$p)$\rightarrow$(p=q)]} as axioms or theorems ("theses" hereafter... "=" indicates logical equivalence, I've also assumed uniform substitution and detachment here). If you have a deduction meta-theorem (which oftentimes doesn't say anything about conjunctions), then you have [(p$\rightarrow$(q$\rightarrow$p)] as a thesis. And we do have {(p$\rightarrow$q)$\rightarrow$[(q$\rightarrow$p)$\rightarrow$(p=q)]} for what you've referenced. So, the answer to your question is "yes".

That doesn't imply though that each thesis has the same power in that you can derive the same consequences solely from some thesis T as you can from thesis S under the same rule (because you might not have the ability to derive [(p$\rightarrow$(q$\rightarrow$p)] or {(p$\rightarrow$q)$\rightarrow$[(q$\rightarrow$p)$\rightarrow$(p=q)]}).

"Now, if the first question has a positive answer. The most important question ( for me ): If have a proof of some representative of some "Theorem Equivalence class" ( as i'm calling the set of all theorems represented by formulas that are logically equivalent to one another ) , are we sure that there exists a proof of each representative of that "Theorem Equivalence class" ?"

If there cannot exist a proof of X, then there does not exist a theorem X. If X does qualify as a theorem, then there can exist a proof X. X comes as arbitrary here. So, the answer to your question here is again "yes".

" I think ( but i'm not sure ) that is the same as asking, that if a theorem can be proved by a specific method ( supppose some direct proof ), are we 100% sure it can be proven by all other valid methods ( all other direct proofs, proof by contradiction, etc,etc ) ?"

This sounds different to me. One might include axioms as part of the method. It is not the case that if an axiom set under a set of rules of inference will enable you to prove a theorem, then any other axiom set under the same set of rules of inference will enable you to prove a theorem.