How I can express in a pure symbolic way common reasoning? Examples inside.

Question

I have a broad question here, I know, but I will go define it clearly through examples.

I want to know how express reasoning in a pure symbolic way, with no words, this is possible?

Example: I was reading about inner product, in particular about euclidian inner product that is defined as

$$\langle\mathbf{x}|\mathbf{y}\rangle:=\sum_{k=1}^{n}x_ky_k\quad ;\mathbf{x},\mathbf{y}\in\mathbb R^n\tag{1}$$

Now I can express some consequences from this definition, and I want to do it only using symbols. By example, this is correct?

$$(1)\vdash\langle\mathbf{x}|\mathbf{x}\rangle\ge0$$

or maybe I must use some arrow instead to denote consequence (something like $\implies$ or $\rightarrow$)?

Continue: after the definition of euclidian inner product I read (same book, some lines below) the definition of euclidian norm as

$$\|\mathbf{x}\|:=\sqrt{\langle\mathbf{x}|\mathbf{x}\rangle}$$

Now the Cauchy-Schwarz inequality:

$$|\langle\mathbf{x}|\mathbf{y}\rangle|\le\|\mathbf{x}\|\|\mathbf{y}\|$$

is understood as a consequence of $x^2\ge0$. Now, the question that opened this topic is... how I can express only with symbols that the triangular inequality is a consequence of the loss of negative of any square of any real number?

I was thinking to write something like

$$|\langle\mathbf{x}|\mathbf{y}\rangle|\le\|\mathbf{x}\|\|\mathbf{y}\| \because\forall x\in\mathbb R (x^2\ge0)$$

This is correct? There are others symbols more than $\because$ to express causality in the reverse order, something like a reverse $\vdash$ or a reverse $\models$, some reverse arrow like $\leftarrow$?

In general, exist a way to write concepts like "property" (or properties), "possibly", "a possibility", "cause of", "if" (condition) in a formal way? It is possible to write maths only with symbols?

By example, this is possible to write a list of properties of a definition in a pure symbolic way, with no words at all?

If is possibly I want some bibliography, if exist, about this topic. To be clear: some bibliography about the way to express natural reasoning in a pure symbolic language.

Thanks in advance.

P.S.: Im not considering this question a duplicate, I know that similar questions about the use of symbols exist on mathexchange... but they are not the same imo. This question put the focus on write natural reasoning, in a broad sense, more than the correct or incorrect use of some logical symbol. Anyway if you consider this question is duplicate in some way (maybe I dont search correctly and I have missed some similar questions) is ok that you notice it.

Answer 1

To answer shortly: Yes, we can formalize mathematics in a 1st order language.

To give lengthy extra information: I had the same questions myself two years ago so I learned how to do it. Basically you just need to study [First Order Logic] (FOL) 1, do some formalization exercises and apply this knowledge to the axioms of ZFC-Set Theory (<-- you shoul really check this one). The book that introduced me to these concepts was an old book: Elliott Mendelson's Introduction to Mathematical Logic (only the first two chapters will suffice). After reading that you could check the general idea in Wikipedia of a "formal system". Not only there is one symbolic language in which we can do this, but once you know what a formal system is and how it works you can even design one of your own. A very famous relatively "new formal system" to develop mathematics is the language of Homotopy Type Theory.

Learning the language of FOL also helps to understand a lot the mathematical reasoning behind proofs. Nevertheless, when I started writing everything in a pure symbolic way, people usually didn't understand it, so I wouldn't recommend to do that. If you're not going to study logic and design or work with proof assistants, it is probably not recommended that you formalize everything in any language (not just FOL), just knowing that it can be done will be good. The most important thing to remember is that you have to communicate your ideas to other people, and people usually use a combination of FOL with the natural language.

To answer the rest of your questions:

A very vague way in which (1) could be written in FOL+ZFC is: $$\vdash\forall n\in\mathbb{N}\forall x\in\mathbb{R}^n\forall y\in\mathbb{R}^n[x=(x_1,x_2,\dots,x_n) \land y=(y_1,y_2,\dots,y_n)\rightarrow \langle x,y\rangle:=\sum_{k=1}^nx_ky_K]$$ Pay attention in how "every" variable should appear next to a quantifier $\forall$ (even my formula is incorrect because $x_1,y_1,\dots,x_n,y_n$ are not bounded by a quantifier). Also notice that every quantifier appears before the content of the formula. Writing it after it is "incorrect" in the language of FOL. The same applies for the first deduction you show: $\vdash\forall x\in\mathbb{R}^n[\langle x,x\rangle\geq 0]$

The deduction that you are asking for ($|\langle x,y\rangle|\leq\|x\|\|y\|\because\forall x\in\mathbb{R}[x^2\geq0]$) is rather long in any deduction system mainly because it not only depends on the fact that every squared real number is greater or equal to 0, but it also depends on knowing that "the sum of any non-negative real numbers is grater or equal to 0", "multiplication and addition of reals gives you as output a real" and many more rules from FOL.

Concerning the symbols:

• The "because" symbol $\because$ is not used in FOL but you can use it informally whenever you forgot to list a condition before your deduction.
• "Property" is a meta-theoretic concept and is represented as a variable ranging over formulas of FOL. We generally say "let $\varphi$ be a property with free variables $x_1,\dots,x_n$, then ..."
• "Possibly" can be expressed saying that the probability of the event is greater or equal to zero ($P[A]\geq0$).
• "if+then" is written with the material implication symbols $\rightarrow$ and $\Rightarrow$ (observe that you can use this backwards $\leftarrow$ or $\Leftarrow$ for the "something if cause").
• The symbol $\vdash$ with nothing before it, at least in FOL, literally means "it is a theorem that" and when something is before it like in $\varphi,\psi\vdash\gamma$ it is saying that "$\gamma$ is a (syntactical) consequence of assuming $\varphi$ and $\psi$.
• Similarly, the symbol $\models$ with nothing before it means "it is logically valid that" and when something is before it like in $\varphi,\psi\models\gamma$ it is saying that "$\gamma$ is a (semantical) consequence of assuming $\varphi$ and $\psi$.