2
$\begingroup$

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!

$\endgroup$
8
$\begingroup$

First of all, thank you for asking this question, before posting that.

From what I see, you do not appear to have a specific question to ask. You describe some system that you came up with, tell people to go to an external site, and hope that they provide "feedback".

That is not what this site is for. From the What types of questions should I avoid asking? page of the Help Center (emphasis added):

You should only ask practical, answerable questions based on actual problems that you face. Chatty, open-ended questions diminish the usefulness of our site and push other questions off the front page.

If you have a specific question that you want to ask about your formalism, that's fine. But simply a request for feedback without a specific question being posed is outside the scope of Mathematics Stack Exchange.

You may be able to find people in some of our chat rooms (the main Mathematics chat room, as well as the Logic and Set Theory rooms) willing to provide the feedback you seek.

$\endgroup$
  • $\begingroup$ Thank you arjafi. That was what I was afraid of. I will try the chat rooms you have suggested. $\endgroup$ – Carlos Freites Mar 20 '17 at 12:38

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .