Logic - 2017-10-28

user21820

02:07

@Espinoza That's great! Correct explanation. Though it is usually helpful to be symbolically precise. Given any function f from nat into func(nat,{0,1}), let g = ( nat n ↦ 1−f(n)(n) ), and then g ∈ func(nat,{0,1}) but there cannot be a k ∈ nat such that f(k) = g, simply because for any k ∈ nat we have g(k) ≠ f(k)(k).

@Espinoza I created this chat-room because there wasn't any room on Math SE dedicated to logic. Feel free to ask any questions related to logic here.

Many of the conversations have been regarding foundations, but many are also regarding basic logic, so there's a variety.

user131753

05:09

@user21820: A few minutes ago I have posted a question on category theory. Can I discuss with you regarding the question here?

user21820

Sure, but I must say that I have only read a bit about category theory. Post the link here?

user131753

0

Q: Two Questions on Peter Smith's Representation of Category Theory

Background Recently I was going through Peter Smith's Category Theory : A Gentle Introduction. There he writes (in section 1.1), Definition 1. A category $\mathscr{C}$ comprises two kinds of things: (1) $\mathscr{C}$ -objects (which we will typically notate by ‘$A$’, ‘$B$’, ‘$C$’, $\l...

category-theory

user21820

Ah so what's your questions?

user131753

Have you gone through Henning Makholm's answer of my second question?

user131753

And the following comments?

user131753

05:14

@user170039: It does not make any sense to say that "$\operatorname{src}(1_A)\ne \operatorname{src}(1_B)$ but $1_A=1_B$"! If you're supposing that $1_A=1_B$ you're supposing that $1_A$ and $1_B$ are simply different names for the same thing, and the source of that thing will be equal to itself, no matter which of the two names you use to speak about the thing whose source you're taking. — Henning Makholm 12 mins ago

user131753

"For each arrow there is a unique source and target" means that if $1_A$ is indeed the same arrow as $1_B$, then their sources must be the same, i.e. $src(1_A)=src(1_B)$. There's your contradiction, if you also assume $src(1_A)\neq src(1_B)$. — pseudocydonia 10 mins ago

user21820

Yea both are correct.

If 1[A] = 1[B] then by mere substitution we get src(1[A]) = src(1[B]).

user131753

@user21820 Do we? Don't we need a definition of $1_A=1_B$ which permits the substitution?

user21820

No we don't. Any two equal objects can always be substituted. This is just the =-elimination rule.

4

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...

The first part of my post gives the rules for first-order logic, including =-elim.

The second part you can ignore, as it's to get MK set theory not category theory.

user131753

@user21820 But $src$ here is not a function(-symbol).

user21820

05:21

It is a function-symbol, according to the text you quoted.

> For each arrow f, there are unique associated objects src(f) and tar(f), respectively the source and target of f, not necessarily distinct.

Whether or not Peter was being precise in his setup, it's valid for me to say this because definitorial expansion is conservative. See here for definitorial expansion:

5

A: How could we formalize the introduction of new notation?

What you may be looking for in your formal system is variously called full abbreviation power or definitorial expansion. Basically, it comprises rules that allows you to create on the fly new symbols extending the original language. We need one type of rule for each kind of symbol: $\def\eq{\left...

By his assertion that src(f) is unique for each arrow f, he is asserting a unique existential sentence that can be used in definitorial expansion so that we can in fact treat src as a function-symbol.

user131753

I see. In that case it is clear.

user21820

That's great. I should note that src is not a function (in set-theory sense).

Just like powerset symbol P is not a function in ZFC set theory, but can be treated as a function-symbol without essentially changing what can be proven in the system.

user131753

@user21820 Yes. That's what confused me. I simply treated it as an object.

user21820

Ah. Same as in ZF[C]/MK set theory, category theory has the problem with the universe not being an object.

So there are plenty of definable things that aren't objects.

No category of all categories, for example.

Kirill

07:40

Here at the moment, @user21820

user21820

Okay I'll try to be quick.

in Mathematics, 25 mins ago, by Kirill

The relation on $\mathbb{R}$ is defined as: $xRy$, wenn $x-y \in \mathbb{Q}$. I show that the thing is transitive: Let $a,b,c \in \mathbb{R}$ and $aRb, bRc$. $aRb$ means that $a-b \in \mathbb{Q}$. $bRc$ means that $b-c \in \mathbb{Q}$. As the sum of two rational numbers is a rational number, $(a-b)+(b-c) = a - c$ is also an element of $\mathbb{Q}$. But that means, that $aRc$ and the relation is transitive.
Do you like the argumentation?

in Mathematics, 24 mins ago, by user21820

@Kirill I'll not use "let a,b,c ..." but rather "given/take any a,b,c ..." Other than that it's a fine argument.

in Mathematics, 22 mins ago, by Kirill

@user21820 yes, I have a point here. The formal definition requiers the transitivity to work for all elements of the given set. At the same time I cannot work with all elements of the set, but pick 3 random elements.

in Mathematics, 18 mins ago, by user21820

When you have a real number x, you find nothing wrong with saying "let y = 3x^2−4", which uses "let" to mean that you actually name an existing object (given by a previously deduced existential statement). So I see no reason to overload "let" to also mean something else when English doesn't even support it.

in Mathematics, 6 mins ago, by Kirill

@user21820 not really. Every proof in German starts with something like "Let $a \in \mathbb{R}$", what actually means "prepare your workspace and put a real number on it you going to operate on". So, is your point about tht the usage in English, or about the logic in general?

Kirill

@user21820 sorry for that, I just have to learn and proove much today

user21820

The basic point is that the use of "let" (or whatever word in your language) is totally different in "let y = 3x^2−4" (in a context where you have real x) and in "let r be a rational".

This is commonly found in (English) textbooks.

Kirill

so, we have an overloaded "let" :)

user21820

If your language uses the same word for both as in my examples, then you have the same problem.

Kirill

07:43

in the first case you say: "I define $y$ as", in the second "take $y$".

user21820

Right. And I say this for good reason.

Because consider "take any rational r such that r^2 = 3".

Would you use "let"?

If you do, it's very likely to mislead students.

It suggests that it actually exists.

Kirill

such usage would be strange even for me

so, no, I would not do that

user21820

And that's the same issue that crops up all over the place in more advanced mathematics because often it's not clear whether some mathematical objects we are reasoning about actually exist.

For example in your case.

You have a relation ~ on reals.

It's true that there are plenty of reals. But consider "take any reals a,b,c such that a ~ b ~ c"

Kirill

the idea of "sei" in German - which means "let" in English comes from the word "to be". So, "let $y$ be a rational number" e.g. The point in the proof I've written is about: I have to name what I operate on, and at the same time I must show that it works for all elements in the given set.

user21820

In the case of your ~, there are such instances of a,b,c. But for general ~, there may not be any.

For example, the empty relation on reals, namely false for every pair of reals, is in fact transitive!

And still the proof could start with "take any reals a,b,c such that a ~ b ~ c", but it would be utterly strange to start with "let a,b,c be reals such that a ~ b ~ c".

Kirill

07:48

cause there are no such reals?

user21820

Yeap.

Kirill

How would you introduce some set, or variable, or a function?

lets take a curve

user21820

In what context? Give me an example?

Kirill

we need an opened subset of $\mathbb{R}$, an $n$-dimensional field on real numbers and the function that orders every real number a vector in $\mathbb{R}^n$. In German it would be "sei $I \subseteq \mathbb{R}, f: I \to \mathbb{R}^n$. We say $f$ is a curve, if...

how would you introduce these components that are necessary to define a curve?

please correct me if my English is too bad

user21820

Well there are a couple of ways I would consider logically perfect. You can use "Take any I ⊆ R and f : I → R^n." right upfront and then use I,f as you like. Alternatively if the definition is short you could say "For any ... , we say that ...".

Kirill

07:55

so, "let" would be a bad choice here, too?

user21820

In my opinion, yes.

Of course, many textbooks don't seem to share my opinion.

Though more logicians do.

Kirill

Some textbooks do to make difference between the curve, and the trace of the curve, what is really badly I think. So, I am pretty sensitive to the right usage of words.

(even though my grammar can be aweful) :)

user21820

@Kirill I'm guessing those textbooks are differentiating between the function (an abstract object) and the graph of the function (as a subset of the Euclidean space).

Kirill

I think the usage is pretty different according to the school or an instituion you are in. Generally, we never use function for a graph. A function can been seen as a process, or as a dead set of pairs. To it is either a function, or a set. Graphs are usually used in the graph theory, so we do not use them either. Instead, we use "image" of $f$, or something like that. I am sure, the terminology would be totally different even in some other instituion.

So, may I conclude your point? In your opinion, "let" would be suitable in the context of "define $a$ through something I've already known". Is that right?

user21820

@Kirill Yea I typically don't see much need to talk about the graph (or whatever other term) of a function. But in measure theory it does matter to consider the embedding of the graph in Euclidean space, not just the image.

@Kirill Yes right.

It claims the existence of something and names it.

Kirill

08:04

I've got your point and will keep that in mind. Thank you very much!

user21820

@Kirill: You're welcome!

Kirill

Btw, that small proof is a part of the proof that claims that Vitali measures do not exist.

I am studying measures theory at the moment :)

user21820

Ah!

Kirill

@user21820 the context of speaking about the graph is usefull, if you want to ask somebody to draw an image of the curve.

user21820

@Kirill Yes. Also, since you really are studying measure theory, what I was referring earlier is that we say a real function is measurable when the region bounded under its graph is measurable.

This is one way of defining measurability of a real function.

Kirill

08:08

I have got the first two lections. They are about the idea, the V-measure and $\sigma$-algebras. I think the definition of the measurability is going to come on Monday.

I propose, we will do that abstracter.

user21820

Ah I see. There are many varied approaches to measure theory and yours sounds like the more algebraic flavour, so don't be surprised that they don't use my definition. In any case measurable functions should come later, not so early in the course.

Kirill

I see. Yes, at this point we are about the induces algebras. The word "measureable" meens nothing to me at the moment. But, it will come.

Thank you once again, and I will go further in the material!

or, through the material

user21820

You're welcome! See you around and feel free to drop by here! =)

Kirill

Ok!

user131753

14:31

@user21820 In the following answer an alternative approach to answer my question is suggested,

user131753

1

A: Two Questions on Peter Smith's Representation of Category Theory

I would like to point out that Maarten Fokkinga's 1992 introduction to category theory, A Gentle Introduction to Category Theory: the calculational approach, addresses this head-on by defining a notion of "pre-category" where hom-sets are not required to be disjoint. This, arguably, more naturall...

user131753

15:04

In fact after going through the paper I think I understand what Peter Smith probably wanted to mean when he said "For each arrow $f$, there are unique associated objects $src(f)$ and $tar(f)$."

user131753

The informal version of the full argument may be stated as following: Since for each arrow $f$, there are unique associated objects $src(f)$ and $tar(f)$, and since $1_A:A\to A$, it follows that for all object $C$ such that $1_A:C\to C$ we have $A=C$. But since $1_A=1_B$ and $1_B:B\to B$ we conclude that $1_A:B\to B$ (here we use =-elimination rule) and hence by our above discussion it follows that $A=B$.

user131753

Is that reasoning correct @user21820?

user21820

15:22

@user170039 I don't understand your reasoning at all, because it's convoluted and arguably circular. You wrote "it follows that for all object $C$ such that $1_A:C\to C$ we have $A=C$" but it does not follow at all without using the exact same kind of substitution that you seem to want to attempt to avoid.

In Peter's text it is clear that "1[A] : C → C" is mere short-hand for src(1[A]) = C and tar(1[A]) = C.

And the axiom gives src(1[A]) = A.

So A = C by substitution.

The thing is that you are invoking so many axioms just to prove the original claim, when the original claim is true independent of all the axioms.

That's why I said I don't understand what you're attempting to do.

Wait are you trying to say "the informal version of the full argument for the second part"?

user131753

@user21820 Yes.

user21820

Oh okay then your argument makes sense. But the original intended argument is still far easier than yours.

In fact. My argument is even shorter.

If 1[A] = 1[B] then A = src(1[A]) = src(1[B]) = B.

That's it. First and last equality by definition of 1[A] and 1[B]. Middle equality by substitution.

user131753

@user21820 The axiom (which I think to be an informal version of unique-type axiom from the paper linked here) not only gives that $src(1_A)=A$, it also implies that if $1_A:C\to D$ then $A=C=D$. I don't think here we need any substitution.

user21820

@user170039 You need to pick one text and stick to it. Different people will use different axiomatizations that may be compatible but switching back and forth in the early stages easily leads to circular reasoning.

In Peter's text, the argument is just 1-line and has nothing to do with quantification or unique-type axiom as in other texts.

If you understand my explanation 3−4 comments above, that's all there is to it. The reason it's so clean is that Peter explicitly has function-symbols src and tar.

(Which, from a CS point of view, is natural anyway.)

In fact, from a proof-theory point of view, even if you take away src and tar and replace them by unique existentials, you will still have to use substitution in the proof (when unraveled).

user131753

15:38

@user21820 I don't understand the relevance of saying this. If you disagree that the axiom is an informal version of unique-type axiom from the paper linked here) then that's fine (in fact it doesn't have any significant bearing on what I said).

user131753

However if you think that this comment is wrong then please give reasons for it.

user21820

@user170039 The relevance is exactly the reason Henning is saying the same thing. In Peter's system you have src and tar, so you immediately get what you said in that comment: A = src(1[A]) = C and A = tar(1[A]) = D. Both by substitution. Secondly, you are indeed wrong in claiming that there is no substitution needed. You can't use unique existentials without substitution (unless you have extra deductive rules that are not usually included due to redundancy).

Just answer my question first: Do you understand the 1-line proof I gave you? We will go from that.

user131753

@user21820 I understood that but I am trying to understand what Peter was possibly trying to mean and not another way to prove the same result.

user21820

Peter meant exactly the same as my 1-line proof.

Just that his presentation was in the opposite direction.

His proof goes:

If A ≠ B:
  A = src(1[A]).
  B = src(1[B]).
  src(1[A]) ≠ src(1[B]).
  ...

Where the last line is by substitution. Sorry I accidentally pressed Enter just now.

My proof is shorter merely because the chain of equalities is implicitly performing a couple of substitutions for me.

If A ≠ B:
  A = src(1[A]).
  B = src(1[B]).
  src(1[A]) ≠ src(1[B]).
  If 1[A] = 1[B]:
    src(1[A]) = src(1[B]).
    Contradiction.
  Therefore 1[A] ≠ 1[B].

user131753

Let me just try to understand something. What will be the formal version of Peter's axiom @user21820?

user21820

15:51

Do you see that Peter's proof (above) is clearly the same as mine?

@user170039 See the comment just before yours. It's a complete formalization of Peter's argument. I think you need to revise the deductive rules for first-order logic...

You can read off the axioms used:

user131753

@user21820 I am not talking about formalization of Peter's argument, I am talking about a formalized version of his axiom (of which we are talking about). Please read carefully what I wrote before commenting.

user21820

  A = src(1[A]).
  B = src(1[B]).

I know what you wrote, but it's obvious.

Any line that did not follow from the previous ones must be an axiom.

Anyway I used exactly the same 2 axioms in my version of the proof, and you said you understood it?

user131753

I am asking for a formalization of the following axiom:

user131753

Sources and targets For each arrow $f$, there are unique associated objects $src(f)$ and $tar (f)$, respectively the source and target of $f$, not necessarily distinct.

user21820

@user170039 No axiom needed for that!

user131753

15:59

@user21820 I don't understand. What do you mean to say?

user21820

I said precisely what I meant. There is no axiom needed for that, since it is inbuilt into the language Peter chose.

user131753

@user21820 Then you didn't understand what I meant. I am asking you to write the axiom in symbolic terms.

user21820

That's why I took so much trouble earlier to say that we treat src and tar as function-symbols in Peter's text, because it is the crucial point.

And I keep saying that there are no axioms for that sentence!!!

Please don't keep assuming I'm wrong...

When you talk about a group G and you say that * is a binary operation on G, there is no axiom for that. Instead * is a 2-input function-symbol in the language you pick.

Espinoza

Those are interesting distinctions @user21820. Where could I read more about that sort of thing?

user21820

@Espinoza First-order logic involves a language and a deductive system. Any standard introductory text will cover it. You should first look at Forallx linked from here:

9

A: What are the prerequisites for studying mathematical logic?

I think for starting material you can't beat P.D. Magnus' book forall x, which clearly explains the intuitions behind logic culminating in Fitch-style natural deduction. (I described a programming-inclined variant here.) After that you can read Stephen Simpson's Mathematical Logic lecture notes a...

@user400188: Argh. I realize that Forallx does not even talk about function-symbols. Only predicate-symbols. =(

user131753

16:07

@jaspreet: I think this is what you were suggesting, isn't it?

user21820

@Espinoza: But Forallx is still worth reading, because it has Fitch-style ND. But you're going to have to look elsewhere about function-symbols. Try Hannes' notes.

Espinoza

Does Smullyan's FOL cover that? I ordered that book though it still hasn't arrived

user21820

@user170039 (I know you're pinging @jaspreet) Note that there's no 'definition of the equality' needed, because there is no notion of equality used here other than classical equality, for which all you need is =-introduction and =-elimination.

@Espinoza I don't know. I've heard good things about Smullyan's writings, but some of it is confusing if I recall correctly.

@Espinoza: Just look at Hannes' notes. They are very readable and start with mathematical examples.

And if you want to jump straight to it, it's section 2.2

Espinoza

I'll take a look, thanks!

user21820

@user170039: Let me try to make the point clear, in case you still don't get it. By choosing to have a function-symbol in the language, you are making the implicit assumption of closure under some operation. And the syntactic structure of first-order logic forces those function-symbols to behave 'like functions', having unique output for each input.

There is no axiom for it, and in fact there cannot be any axioms that can replace the choice of language.

@Espinoza You see that he calls them "predicates" and "function signs" and "constants". For me I will always call them "predicate-symbols" and "function-symbols" and "constant-symbols" to make it clear, because "predicate" is often used for more general expressions over the language.

jaspreet

16:18

Suppose you do not have any definition of equality of morphisms. Then, how can you say that any two morphisms are equal?

user21820

@jaspreet You are talking about extensionality. That is an independent issue from the other one.

@jaspreet: As mentioned in the room, there is no notion of definition here in Peter's text. (Of course, you could email him and clarify, if you think I'm interpreting him wrongly.) Specifically, in his text $src,tar$ are function-symbols in his chosen first-order language of category theory, so mere substitution (=-elimination) is enough to get from $f=g$ to $src(f)=src(g)$ and $tar(f)=tar(g)$. Your example of extensionality as a possible further requirement is correct, and you need an axiom if you want that. — user21820 6 secs ago

Namely, in the specific block of quoted text in the question, there is no axiom of extensionality. We of course are going to like it, so we'd expect to see it elsewhere in the text.

But no axioms beyond what I stated above are needed in the question.

jaspreet

Any difference between a definition and an axiom?

user21820

@Espinoza @user170039: Note that in Peter's text, "1[A]" itself should be understood as having a function-symbol id and "1[A]" is just syntactic sugar for "id(A)". I don't know whether Peter is intentionally being vague so that his presentation can be treated in a multi-sorted theory, but even if you want it 1-sorted, you just need to restrict the axioms suitably:

> ∀A∈Objects ( id(A)∈Arrows ∧ src(id(A)) = A ∧ tar(id(A)) = A ).

@jaspreet Yes. Let me find a post on it.

@jaspreet: Here:

34

A: Why do we not have to prove definitions?

The other answers did not explain the background of logic that is the key to understanding this issue. In any formal system where we write proofs, we have to use some formal language that specifies the valid syntax of sentences, and we must follow some formal rules that specify which sentences we...

Basically, treat a definition as a syntactic short-hand for some expression in the original language.

In contrast an axiom is an assertion that you assume (and can use anywhere) within your formal system:

15

A: Meaning of the word "axiom"

Axioms Originally, "axioms" meant "self-evident truths", or at least what seemed self-evident. But the more important question is what axioms are used for. From the beginning, logic in some form has been an essential part of reasoning, and we reason about things all the time. Then whenever we wa...

Without axioms, you can only prove purely logical tautologies that hold in every world. But you can do without any definitions at all, just that your theorems and proofs will be extremely long and cumbersome to read.

@user170039: Is there something wrong with your internet? Just wondering. I see you pop in and out very frequently lol.

jaspreet

16:40

In the original proof in question, author states that two identity morphisms on two distinct objects are different because their sources are different. This appears to be using the definition that, if two arrows have different sources, then arrows are different. Right? As if the definition was not used i.e. if arrows can have different sources, but still be equal, then knowing only about sources of two arrows cannot allow one to conclude that two arrows are equal.

user21820

@jaspreet Wrong.

jaspreet

Please read the next sentence too.

user21820

Did you read the whole conversation above where I painstakingly explained the reason there is no definition and no axiom involved in the proof?

jaspreet

No.

user21820

Start here and the next few comments.

Then go here for an absolutely formal translation of Peter's proof.

Both are obviously equivalent if you are familiar with standard first-order deductive systems.

Both only use the axioms I stated here.

@jaspreet: And if you are not familiar with a deductive system for first-order logic see here.

If you want even purer first-order logic, see here and the next comment and then look at the following proof:

Given A,B∈Objects:
  If id(A) = id(B):
    A = src(id(A)) = src(id(B)) = B.  [all by =-elim]

Note that I claim "all by =-elim" because we are effectively using transitivity of equality, which is typically not inbuilt into the deductive system, and which requires =-elim.

@HenningMakholm: Hello!

Henning Makholm

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

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:

4

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

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 :)

user21820

Yea I was asking them, not you. =)

@jaspreet @user170039: If you have further questions you can definitely ping @HenningMakholm to ask him. =)

jaspreet

@user21820 I follow your proof now. Assuming first order logic with equality, it follows that if two identity arrows are the same, the statement that " source (id(A))= A" must be true of second identity arrow too, since they are the same object. Therefore, no need to define equality.

user21820

@HenningMakholm: Hope to see you around here next time! It's sometimes quiet in here. =)

@jaspreet Absolutely correct. That's great!

See you next time!

jaspreet

17:21

Bye!

Henning Makholm

Perhaps. Several years ago I allowed SE chat to consume most of my waking hours, so I'm trying to hold back :-)

user21820

@HenningMakholm Oops. Perhaps I'm falling into the same hole.

@HenningMakholm: But I think my decision to create this chat-room was a good one; lots of very interesting discussions have transpired here, amidst some more 'simple' ones. No two really equal either. =P

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic