Increasing levels of formality in a trivial physics statement

In this post I start with a trivial observation about Physics concepts and attempt to add layers of formalization through semantic enrichment. Inspired by sTeX, I use pseudo-Latex which has no supported implementation. RDF tags might be more appropriate.

The initial observation is

The relation between period, T, and linear frequency, f, is T = 1/f. Thus frequency as a function of period is f = 1/T.

The purpose of using this as a starting point is that it is simple and easily understood by a human.
The rest of this post explores what semantic additions would be needed for a computer to parse the text.

Each of these transitions can be identified manually. I don't have reliable ways of automating this process.

*********************
The first change is conversion from ASCII to Latex, a common presentation method in Math and Physics. This change only alters presentation. I've highlighted the changes in red.

The relation between period, $T$, and linear frequency, $f$, is
\begin{equation}
T = 1/f.
\end{equation}
Thus frequency as a function of period is
\begin{equation}
f = 1/T.
\end{equation}

*********************

The next change is to bound claims being made.

\claim{1}{The relation between period, $T$, and linear frequency, $f$, is
  \begin{equation}
    T = 1/f.
  \end{equation}
}
Thus \claim{2}{frequency as a function of period is
  \begin{equation}
    f = 1/T.
  \end{equation}
}

*********************

Replace "thus" with the relation between claims.

\claim{1}{The relation between period, $T$, and linear frequency, $f$, is
  \begin{equation}
    T = 1/f.
  \end{equation}
}
\relation_between_claims{claim 2 is derivable from claim 1}
\claim{2}{frequency as a function of period is
  \begin{equation}
    f = 1/T.
  \end{equation}
}

*********************

Within each claim there are variables and symbols. Identify those.
I've inserted parenthesis to make the order of operations clear.

\claim{1}{The relation between \named_variable{period}, \symbol{T}, and \named_variable{linear frequency}, \symbol{f}, is
  \begin{equation}
    \symbol{T} \operator{=} (\integer{1}\operator{/}\symbol{f}).
  \end{equation}
}
\relation_between_claims{claim 2 is derivable from claim 1}
\claim{2}{The \named_variable{frequency} as a function of \named_variable{period} is
  \begin{equation}
    \symbol{f} \operator{=} (\integer{1}\operator{/}\symbol{T}).
  \end{equation}
}

Visually, this could be represented by color-coded boxing

Here claims are red, connections are light green, expressions are dark green, named variables are pink, variables are blue, operators are light blue, and operators are purple.

This visualization seems to relate to discourse representation theory (DRT) though I don't know how to leverage it. See box notation here and here.


*********************
The "T" and "f" symbols are conventions that are used in other papers. We can indicate that by assigning universal identifiers.
Similarly, the operators "/" and "=" are defined in other papers. Those also get a universal ID.
The relation between named variables and symbols needs to be made explicit.
With those associations made, replace the symbols and operators in the expressions.

\def{symbol{T} = pdg2948}                   % the symbol "T" has a (universal) Godel number
\def{symbol{f} = pdg9215}                   % the symbol "f" has a (universal) Godel number
\def{operator{/} = pdg1340}                 % the operator "/" has a (universal) Godel number
\def{operator{=} = pdg8821}                 % the operator "=" has a (universal) Godel number
\def{named_variable{period} = symbol{T}}    % the named variable "period" is equivalent to the symbol "T"
\def{named_variable{frequency} = symbol{f}} % the named variable "frequency" is equivalent to the symbol "f"

\claim{1}{The relation between \named_variable{period}, pdg2948, and \named_variable{linear frequency}, pdg9215, is
  \begin{equation}
    pdg2948 pdg8821 (\integer{1} pdg1340 pdg9215).
  \end{equation}
}
\relation_between_claims{claim 2 is derivable from claim 1}
\claim{2}{The \named_variable{frequency} as a function of \named_variable{period} is
  \begin{equation}
    pdg9215 pdg8821 (\integer{1} pdg1340 pdg2948).
  \end{equation}
}

One of the purposes of associating a symbol "T" with a universal identifier is that the type can be specified. Here "f" and "T" are both Real valued.

At this point the relation between claims 1 and 2 could be converted to SymPy and verified; see
https://derivationmap.net/review_derivation/884319/