In mathematical textbooks (for instance the Kelly's General Topology or the Spivak's Calculus) a theorem has hypotheses and a thesis.
In formal mathematics is different: A theorem of a formal theory L is a wff φ of L such that φ is the last wff of some proof in L. Such a proof is called a proof of φ in L.
However, in in formal mathematics there is something like hypotheses found in textbooks:
A wff φ is said to be a consequence, in a formal theory L, of a finite set $\Gamma$ of wffs if and only if there is a sequence $\beta_1,...,\beta_k$ of wffs such that φ is $\beta_k$ and, for each i, either $\beta_i$ is an axiom or $\beta_i$ is in $\Gamma$, or $\beta_i$ is a direct consequence by some rule inference of some of the preceding wfs in the sequence. Such a sequence is called a proof φ from $\Gamma$. The members of $\Gamma$ are called the hypotheses of the proof. In this case we will write $\Gamma$ ⊢ φ to abbreviate 'φ is a consequence of $\Gamma$'
In the case the set $\Gamma$ is empty is said that φ is a theorem and $⊢_L$ φ to emphasize that φ is a theorem of L and if that is clear, ⊢ φ is written to say that φ is a theorem.
So the mathematical textbooks idea of theorem is lost in formal mathematics.
I am working in a formal theory in which well formed formulas $wff_{PotentialTheorem}$ must have a finite no empty set of normal wffs named hypotheses (in the above sense) and a normal wwf φ named thesis, in the sense of being the target a potential proof that if it is build turn $wff_{PotentialTheorem}$ into $wff_{Theorem}$. It has been done by trying adding to ZFC the idea of context in a formal way. Quantification resemble bounded quantification but it is handled in a so inner way that the standard definitions
$\forall (x \in A) ( φ ) \Leftrightarrow \forall x (x \in A \Rightarrow φ)$
$\exists (x \in A) ( φ ) \Leftrightarrow \exists x (x \in A \wedge φ)$
can not be applied, intuitively because in $\exists (x \in A)( φ )$, the atomic formula $(x \in A)$ is part of the 'context' of φ
I have little academic mathematical background and I don't know how to test my system, I will be happy if you can see it in mathdialog.com and give me some feedback.
Can I post this in math.stackexchange.com with a soft-question tag?
Thank you so much!
