# Is the Proof Mathematical Object as a Function?

While I am discussing over the definition of the proof with my friends, one says

"proof is definitely a mathematical object which maps a formal representation of mathematical objects into two classification which is true and false which are also mathematical objects."

But I wonder whether the collection of formal representation of a mathematical object, which works as a "Function Domain" upon the above statement, is well-defined/uniquely existing or not.

Since I've never thought of whether the formal representations could be represented as a composition of sets, moreover as far as I know, all formal representations could not be dealt as a set such as "Set of All sets"

How do you think? Is an any mathematical proof function or not?

• Maybe related Brouwer–Heyting–Kolmogorov interpretation. – Mauro ALLEGRANZA Apr 14 '18 at 7:56
• Could you provide a little more context? What are these formal representations you are referring to? – Giorgio Mossa Apr 14 '18 at 9:23
• @GiorgioMossa Actually that part is obviously still ambiguous to me. I've read some related articles they are formally take well-formed-formulas... but it's just a sequence of given alphabet set.. – delinco Apr 14 '18 at 9:26
• Could you give a link to any of these articles? – Giorgio Mossa Apr 14 '18 at 9:50
• @GiorgioMossa google.co.kr/… – delinco Apr 14 '18 at 10:11

I am not entirely sure if this address your doubts, your question is not fully clear to me but let's try it anyway.

In theory you can regard a formal system, that is a formal description of language with rules of inference as some sort of algebra.

The idea is that the elements of this algebra are formulas (which are strings build according to some grammar) and the inference rules are some basic operations on these formulas (these operations takes some inputs formulas, having a specific form, and give you as output other formulas).

As an example you can consider the propositional calculus, where the well-formed formulas are those build out of propositional variables using the logical connectives.

The modus ponens provides an inference-rule operation: $$\begin{array}{ccc}A \rightarrow B && A \\\hline &B\end{array}$$ that takes in input two formulas in the form $A \rightarrow B$ and $A$ (where $A$ and $B$ can be any propositional formulas) and returns the formula $B$.

From this perspective you can think of proofs as being operations build from these basic inference-rules-operations. In this regard proofs becomes functions.

Of course that is not the only possible way to regard to proofs, neither is necessarily the best one. For instance you could define a proof to be a tree of formulas build through the application of inference rules (which becomes operations that build these tree-proofs), or you could define a proof as a term in a formal system named $\lambda$-calculus. But that is probably a story for another day.