@famesyasd You can indeed encode (finite) strings from an alphabet A as finite (ordered) tuples from A. They can also be encoded as functions from [0..n] to A for some natural n.

@BeginningMath: Since it's relevant to you, I'll say here: Don't feed the troll. This one is a well-known one who has been disturbing the Math SE community since nearly the beginning of Math SE. The moderators know about it, and once had to tell him to stop.

didn't mean to troll, just to understand and learn

i was not aware that he's being a troll, this is why i asked

@BeginningMath I totally understand that.

It's not well-known that there are such users.

@BeginningMath: Are you busy now? If not I can explain in more detail why his comments about formal systems are totally false.

@user21820 I started reading mcmp.philosophie.uni-muenchen.de/students/math/… yesterday

@famesyasd Ah okay. Please feel free to ask any question you may have about it and I'll try to explain.

@user21820 he says: "we will prove some thing about first-order languages, models and proofs " but the thing is that we proof in metalanguage or something so these proofs should not be considered really legal right? I mean unlike the proofs in formal languages

@famesyasd You are right to be suspicious. Unfortunately, that is the way it is in logic and in mathematics in general. Theorems (about first-order logic) are called meta-theorems and are proven (by us) within some meta-system MS. Often people say that we can choose MS to be ZFC, but in practice people use largely natural language and a couple of symbols here and there, not pure ZFC.

But experts can easily translate our natural language proofs into some suitable truly formal meta-system such as ZFC.

Also, note that a lot of these meta-theorems can be proven in very weak meta-systems, and do not need the 'strength' of ZFC.

Does this make sense? I could be more specific, but at this point what you can do is to just check every step of reasoning (through a proof of a meta-theorem) and see whether you personally believe that that step is valid. If you have a problem with some step, then you should ask here, and I can give you a more precise/formal justification of that step.

@user21820 So on the meta level all theorems and stuff basically comes to the both side agreement and we can not really prove that we have not done any mistakes in our meta-reasoning? But we can translate our reasoning to ZFC to be somewhat sure that it is logically correct or something?

@famesyasd To answer the first question, yes before we can study logic as a mathematical field (or any other mathematical field) we have to first agree on a foundational system (which here I called meta-system just to distinguish it from formal systems that we are studying). The majority of modern mathematicians have agreed upon ZFC, largely for historical and sociological reasons, but it is not the only possible foundational system, and in the past people used more handwavy reasoning.

oh okay I got it

We cannot prove with absolute certainty that we have not made any mistakes in our meta-reasoning, but if we truly formalize it in some foundational system, we can write a computer program to check our formalized proof, and be 99.9999% sure that our proof is valid in that foundational system. Whether we believe that that foundation makes sense is a separate issue.

The remaining 0.0001% (probably much less) is reserved for bugs in our program and glitches in computer hardware and so on.

To answer the second question, it depends on whether you believe ZFC makes sense. Almost all set theorists do, of course, but some logicians are more wary. That's why it's sometimes worth to see how weak MS can be to achieve some meta-theoretic results.

For example, a weak system called ACA (that only deals with natural numbers and sets of natural numbers) can prove a reasonably direct translation of Godel's incompleteness theorems for every computable formal system that can reason about basic arithmetic. So if one doubts the incompleteness theorems one would have to doubt ACA too!

But you probably shouldn't bother too much about these for the moment. =)

Just reason along with Hannes and see whether you buy his arguments.

okay no well, I feel like I can digest what you have written soon, so we can check BOTH proofs in meta-reasoning and proofs written in the formal languages by the computer?

Yes! That's the good thing about modern mathematics, and was one of the goals of the inventors of axiomatic theories.

@user21820 and metasystems include not only the axioms of some system but also some logical rules as well, right?

Not to say that they envisioned "computer-verification of proofs", of course. Since computers came much later. But they designed axiomatic systems so that their reasoning could be checked and confirmed/denied objectively based on the agreed upon rules.

@famesyasd Almost all meta-systems are built upon classical logic (basically first-order logic).

yeah I see that, computers are basically just good helpers for checking formalised proofs right? in principal you could do that as well by hand except that the error would be much higher

Right.

so yeah, so for example ACA uses its axioms and rules of classical logic (for example from conjuctiong P /\ Q you can get P and Q

Correct.

okay nice!

there is baiscally one thing left in your post that I did not understand but right now that's enough for me

Sure!

You can note it down somewhere and ask later if you like.

And if I'm not around you can ask @LeakyNun as well.

oh, okay

I don't know anything about ACA

@LeakyNun Not about ACA, but about basic first-order logic.

And of course, you how some of how it may be applied to other fields of mathematics like abstract algebra (your favourite?).

=P

How's school going by the way?

fine

@user21820 yesterday I drew a category-theoretic proof of why group homomorphism preserve identity

Ah.

so, what's the shortest proof that you know?

Well, f(1) = f(1·1) = f(1)·f(1) and hence 1 = f(1) by cancellation.

@LeakyNun =O

but cancellation is a theorem

i think you just get the same proof as the bottom line

It's just multiplying both sides by inverse of f(1).

Yup.

right, but you implicitly used associativity

Somehow I can't say "Yup." twice...

What a joke.

lol

Try saying "lol" again.

can't say the same thing in short succession

lol

needs to have a separating message

That's ridiculous. They must have just added this feature.

I know I never had this problem before.

nah it's been there for a long time

I had this problem before

That's... unsettling. I never had to say the same thing twice in succession before?

Lol!

@LeakyNun So, why is the diagram so big? I expected a much smaller diagram.

each column corresponds to the expression below it

I thought you had some elegant way of expressing the fact.

it isn't elegant

it's checking the axioms

because we have something called group object in category theory

so i wanted to check the axioms for those

I see.

@LeakyNun Wait, there may be something interesting here. It's in general true that homomorphism on any structure preserves purely universal formulae about that structure. This means that if you can transform a theory (such as group theory) into a ∀-axiomatized theory, then it is preserved under homomorphism. In this case, add a constant-symbol for identity and function-symbol for inverse. Then i(1) = 1 gives i(f(1)) = f(1).

Isomorphism of course preserves all formulae.

> The basic results of elementary group theory apply to group objects in any category with finite products. (Arguably, it is precisely the elementary results that apply in any such category.)

https://ncatlab.org/nlab/show/group+object