PeteOlcott wrote: ↑Mon May 13, 2019 11:40 pm
Logik and I had a fundamental disagreement in that he believed that 1=0 and could not be convinced otherwise.

And now that I am back I can simply ask: What do you mean by "equals"?

I am not alone in asking this question:

https://www.youtube.com/watch?v=WfDcrN5_1wA&t=42s
Firstly, because you fail to understand the implications of the Curry-Howard-Lembek correspondence (which is the grounding for proof-theory in Univalent mathematics) you fail to grasp why that is significant for all

Identity types
In intensional type theory under the propositions as types paradigm, an identity type (or equality type) is the incarnation of equality. That is, for any type A and any terms x,y:A, the type IdA(x,y) is “the type of proofs that x=y” or “the type of reasons why x=y”.

From the above "1 = 0" is a proposition whose truth-value is yet to be proven and the reason you and I can't agree on it is because you have failed to state the types of your terms. What type of Mathematical objects are {0, 1} ? Until you state the types of your terms the truth-value of your proposition is undecidable.

And it doesn't stop there:

Different kinds of equality
Here is a list of distinctions between different notions of equality, in different contexts, where possibly all the following pairs of notions are, in turn, “the same”, just expressed in terms of different terminologies:

the difference between axiomatic and defined equality;

the difference between identity and equality,

the difference between intensional and extensional equality,

the difference between equality judgements and equality propositions,

the difference between equality and isomorphism,

the difference between equality and equivalence,

the possibility of operations that might not preserve equality.

What your misunderstanding prevents you from recognizing is that "1 = 0" could be any one of the above (in)equalities.

You were further provided an example where 1 = 0. An example which you failed to acknowledge.

https://en.wikipedia.org/wiki/Zero_ring
The zero ring is the unique ring in which the additive identity 0 and multiplicative identity 1 coincide

So to answer your question directly. Yes - some of us understand formal mathematical proofs. The question is: do you?

Apparently you come from a software background, so

this video should help you close your gap in understanding, by explaining to you why none of the popular programming languages in use today actually support

dependent types.