Theories without equality

Stream: general

[Martin Dvořák]

Sorry for a dumb question...

In the first-order logic, we can study theories with equality as well as theories without equality.
It seems that in Lean, equality always exists.
Does it mean that there are first-order theories that aren't expressible in Lean?

[Daniel Weber]

Equality doesn't always exist in Lean - it is defined in docs#Eq, and if you use prelude you can get Lean without it

[Martin Dvořák]

Definitional equality still exists with prelude. Is it irrelevant?

[Edward van de Meent]

how would you avoid things being defeq to themselves?

[Martin Dvořák]

I am really confused. Is there anything that FOL can express thanks to allowing theories where equality doesn't exist at all?

[Kevin Buzzard]

I have no idea about logic but my understanding is that category theory eschews equality. Can ECTS be expressed in FOL?

[Daniel Weber]

I'm not quite sure what you mean by expressing a theory in Lean

[Martin Dvořák]

https://en.wikipedia.org/wiki/European_Credit_Transfer_and_Accumulation_System ?

[Johan Commelin]

Elementary Theory of a Category of Sets.

[Kevin Buzzard]

I might have got the acronym wrong -- I meant the elementary theory of the category of sets

[Johan Commelin]

ETCS vs ECTS

[Kevin Buzzard]

Apologies :-) I think I've been on too many committees involving undergraduate and masters degree valuations

[Johan Commelin]

Alopogies (-;

[Martin Dvořák]

Daniel Weber said:

I'm not quite sure what you mean by expressing a theory in Lean

That makes two of us!

[Johan Commelin]

If you mean in the sense of Mathlib/ModelTheory/ then there is no problem at all.

[Ruben Van de Velde]

( https://en.wikipedia.org/wiki/European_Train_Control_System ?)

[Martin Dvořák]

Kevin Buzzard said:

I have no idea about logic but my understanding is that category theory eschews equality. Can ECTS be expressed in FOL?

I don't know. However, people here will definitely know whether the Elementary Theory of a Category of Sets can be expressed in Lean.

[Johan Commelin]

There are multiple ways to interpret that statement so that the answer is a definite "yes".

[Martin Dvořák]

And can it be done as an internal model?

[Michael Stoll]

There is also ETCS :smile:

[Michael Stoll]

(Missed that.)