Discussion (III)

Conversation started Oct 28, 2017 at 16:51.

Henning Makholm

Oct 28, 2017 16:51

Hey.

user21820

@HenningMakholm: Nice to see you here! Please feel free to join in any discussion here. =)

Henning Makholm

Just following the link from 170039's question to see if it would shed light on what he's on about.

user21820

@HenningMakholm It appears that he didn't realize that having src and tar as function-symbols in Peter's presentation already encode the uniqueness.

Henning Makholm

I suppose we might say that $x=y \Rightarrow \varphi(x) \Rightarrow \varphi(y)$ is a logical axiom (schema), and that is what we're invoking.

user21820

@HenningMakholm Yes if we go Hilbert-style. I always go Fitch-style where it's just =-elim.

The point is that the rule/schema we are invoking is inbuilt into first-order logic and has nothing specific to do with category theory.

Henning Makholm

Oct 28, 2017 16:57

Indeed.

Perhaps he's brought up on a formulation of first-order logic that doesn't treat $=$ specially? The first introduction to logic I saw (way back in the day) worked that way, and later treated "first-order logic with equality" as a special case of that, where $=$ is not necessarily a predicate letter, but $t=u$ is just some wff with two term-shaped holes that your theory can prove certain properties about. In that case the insistence on having a "definition of equality" would make some sense.

user21820

@HenningMakholm Perhaps. But in the past I have shown him the post I linked above:

A: Predicate logic: How do you self-check the logical structure of your own arguments?

Truth tables are not enough to capture first-order logic (with quantifiers), so we use inference rules instead. Each inference rule is chosen to be sound, meaning that if you start with true statements and use the rule you will deduce only true statements. We say that these rules are truth-preser...

Hence I assumed that he knew =-elim.

And most modern textbooks have equality inbuilt. Though it's a curious thing that in the past equality was philosophically treated in various ways. Though one should stick to modern first-order logic when dealing with modern mathematics?

jaspreet

I must confess that I have very little exposure to formal logic. So, when somebody says x = y in arbitrary context, what can you say about x and y? Does that mean, if a statement is true for x, then it must be true for y? Can you give examples.

I agree that, if one is working in a formal system, which already defines equality, then one should not define the same term again. But, if one is choosing to employ different formal system, in which there is pre-notion of equality, then one can define the relation "=". Here is a link to first order logic without equality: en.wikipedia.org/wiki/…

Henning Makholm

I don't know if I agree with that "should". I find it useful to know both styles and to which extent they're equivalent.

user21820

@HenningMakholm Yea I agree it's good to know the various philosophical issues and viewpoints. But for a beginner it's just not worth the confusion. =)

@jaspreet Yes. In (modern) first-order logic we say that "x=y" to literally mean that x is the same object as y.

For example when we say "2 = 1+1" we literally mean that the expressions "2" and "1+1" both refer to exactly the same object.

Henning Makholm

Oct 28, 2017 17:13

Generally, if one says $x=y$ in an arbitrary context (and has not very explicitly stated otherwise) it can be assumed that one at least is talking about a relation that implies that $x$ can be replaced by $y$ anywhere in any formula without changing its truth value.

user21820

@jaspreet This first-order logic without equality is what Henning was alluding to earlier. It's not typical in most modern presentations of first-order logic.

@HenningMakholm <− @jaspreet: What Henning says here can be treated as the syntactic interpretation of "=", which is the same as having the =-elim rule.

What I said above, that "x=y" literally means that x is the same object as y, can be treated as the semantic interpretation of "=".

All we need to do first-order logic is the syntactic interpretation, but it's nice to understand the semantic interpretation (which is the motivation for the syntactic rule) as well.

Does this make sense? I'm trying to compress a lot into concise bits.

Because I've to go off soon haha..

Henning Makholm

It makes sense to me (but then again I already know what you're trying to say :)

Conversation ended Oct 28, 2017 at 17:19.

all rooms

Oct '1728