Logic - 2017-09-30 (page 3 of 3)

user21820

15:02

@LeakyNun Sort of. Both of you know programming, so I'm going to use program-style notation. Let ( x ↦ E ) denote the program that when run on input x will output E.

Mathmore

Con(FM) means FM doesn't prove 0=1. But since FM is arithmetically-consistent then FM does not prove Con(FM) i.e FM does not prove that ( FM doesn't prove that 0=1 ). that means FM proves that 0=1. contradiction?

user21820

@Mathmore Last sentence before "contradiction" is invalid.

Mathmore

Okay

user21820

Let diag = ( f ↦ ( x ↦ f( t ↦ x(x)(t) ) ) ). Intuitively diag(f) returns a program that takes input x and applies f to a program that behaves exactly like x(x) would. Here any string can be interpreted as a program and run on any string including itself.

Leaky Nun

why would FM does not prove that ( FM doesn't prove that 0=1 ) mean FM proves that 0=1? @Mathmore

user21820

15:05

@LeakyNun It doesn't.

Mathmore

@LeakyNun because i misinterpreted "does not prove(does not prove)" as we do in case of "not(not)".

so again pardon

Leaky Nun

I see

user21820

@Mathmore Correct. That's exactly right.

Let Y = ( f ↦ diag(f)(diag(f)) ).

Mathmore

@user21820 I am not good in programming. I don't know this "diag" notation :(

user21820

It's just a program. What programming language do you know?

I can write it in Javascript if you want.

Mathmore

15:08

@user21820 I don't know any lol.

Leaky Nun

@Mathmore aren’t you teaching computer science?

Mathmore

I urge you to stay on mathematical logic if possible.

@LeakyNun I am teaching discrete mathematics. With simple applications to algorithms. Yeah I am in IT department. I will switch the department next year. I wanna join Maths department.

user21820

@Mathmore Oh hmm then that's a bit of a problem, because everything in logic is inextricably tied with computability.

You don't need to know actual programming languages, but you must know ideal programs.

Mathmore

@user21820 Oh!! :o suggest me a programming language then.

Leaky Nun

lambda caculus /s

user21820

15:11

Python 3.

But I will quote myself to explain ideal programs.

Mathmore

I will trylearning that language

Leaky Nun

I mean you’re using lambda notation now

why not go full lambda mode

Mathmore

ideal programs as in? @user21820

user21820

A program is a string that specifies a sequence of actions, each of which is either a basic string manipulation step or a conditional jump. In a basic string manipulation step we can refer to any strings by name. Initially all strings named in the program are empty, except for the string named input, which contains the input to the program. A conditional jump allows us to test if some basic condition is true (say that a number is nonzero) and jump to another step in the program iff it is so.

We can easily implement a k-fold iteration of a sequence of actions by using a natural number counter that is set to k before that sequence and is decreased by 1 after the sequence, and jumping to the start of the sequence as long as k is nonzero.

The execution of a program on an input is simply following the program (with input containing the input at the start) until we reach the end, at which point the program is said to halt, and whatever is stored in the string named output will be taken as the output of the program.

@LeakyNun Yes I am, but one can never understand what programs are really like without actually running them on a real computer.

@LeakyNun The other reason is that lambda calculus does not have (native) string manipulation, so it does not serve my purpose well at all.

Mathmore

I will join you later. Going for dinner.

user21820

15:14

@Mathmore I will only be here for a few minutes more today.

So see you next time if you're going off now.

Mathmore

@user21820 okay no problem. We will continue the discussion from where we left.

BTW did we achieved our goal? that is to understand incompleteness theorem?

user21820

Nearly. If you grant the existence of Q then we have proven the generalized incompleteness theorem.

It is convenient to assume that every natural number is a string (say using binary encoding).

Mathmore

Fine then. Glad to have this discussion. Bye!

user21820

@Mathmore See you!

@LeakyNun: I owe you a short explanation of why we need the generalized version to dispel all doubt that Hilbert's program cannot be achieved.

Leaky Nun

hmm?

user21820

15:18

Many (real) people have claimed that Godel's result only applies to classical logic, or even more specifically a particular interpretation of Principia Mathematica.

That is technically true, because Godel only proved the limited version. But my generalization shows that the underlying idea that Godel discovered also applies to all kinds of logic including intuitionistic systems.

Leaky Nun

it applies to any recursively enumerably sustem that encodes PA

user21820

Yes that's one way to put it. The encoding here is the key. A lot of textbooks merely say "system that extends PA".

That's too weak.

Intuitionistic version of PA (called HA) also can interpret PA.

Leaky Nun

so?

user21820

So one could easily argue that there may be a formal system that avoids incompleteness just by using non-classical logic. They may say there is no need to extend PA.

But by the well-known negative translation, they also cannot have a system that computably encodes HA.

They still might claim there may be some way out that we haven't discovered yet.

And many real people have made this claim to me.

It is untenable for reasons that I will now explain.

I purposely chose string manipulation because it is more obviously a core feature that we want any foundational system to have. Simply because any logical reasoning is going to be string manipulation.

Leaky Nun

now can you tell us what sort of classical reasoning we perform?

user21820

15:25

Sorry I don't get your last question.

Leaky Nun

you said it applies for any system that can perform classical reasoning on strings?

user21820

Yes.

It is enough to ask for the foundational system to be able to correctly reason about program execution. This is something concrete, as you can actually observe in real programming languages (ignoring memory limits).

It turns out that very few axioms are needed to be able to do this.

Leaky Nun

so what are the axioms?

user21820

TC (theory of concatenation) as I linked to earlier gives just 4 axioms.

Let me find the message.

5 hours ago, by user21820

3

A: How can Peano ever be proved consistent?

You ask: How can Peano ever be proved consistent? Firstly, Peano is a person, and I'm certain that nobody can prove that he is consistent. I assume you're asking for an absolute proof of consistency of (first-order) PA. That was more or less Hilbert's goal, namely to give a finitist proof...

@LeakyNun: I would be curious to know whether you object (philosophically) to any of those 4 axioms.

Leaky Nun

the fourth?

user21820

15:32

Did you read the fourth and see what it means?

It just says that if you can cut a string in two ways then you can match up the two cuttings' prefixes and suffixes with a middle part.

Leaky Nun

oh ok

no objection, go on

user21820

So those 4 axioms are all the axioms in TC. But TC is essentially incomplete, and so any formal system that interprets TC is arithmetically-incomplete too.

Why I still use "arithmetically" is because TC can intepret PA−.

Leaky Nun

PA-?

user21820

It's just that PA− has so many axioms and some may think that the incompleteness arises due to interaction between addition and multiplication.

Peano axioms

In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are a set of axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly unchanged in a number of metamathematical investigations, including research into fundamental questions of whether number theory is consistent and complete. The need to formalize arithmetic was not well appreciated until the work of Hermann Grassmann, who showed in the 1860s that many facts in arithmetic could be derived from more basic facts about...

I believe I did link to it earlier, but here it is again.

Click the link to go to the section on PA−.

Leaky Nun

ok go on

user21820

15:39

For anecdotal example, I myself thought that the interaction of addition and multiplication was crucial to incompleteness, because Presburger arithmetic (by omitting multiplication) is complete.

And a lot more people who don't understand logic think it is induction that causes problems.

TC shows that neither is the problem.

Leaky Nun

so in the end what is it?

user21820

From logic point of view, there is no escape from incompleteness because every formal system must use syntactic rules.

From my real world point of view the problem is (1), closure of strings under concatenation.

If you're really interested in the philosophical issues here, you can see this:

9

A: What are the arguments for and against "one true arithmetic"?

In short: The so-called definition of natural numbers as those that can be obtained from 0 by adding 1 repeatedly is circular, but there is no viable alternative, which already makes it impossible to uniquely pin down natural numbers mathematically. Worse still, there does not seem to be ontologi...

Incompleteness comes directly from being able to reason about program execution one step at a time.

So there's really no escape for any candidate foundational system.

The thing is that one must have a sufficiently general incompleteness theorem that can catch all of the potential candidates that people may propose.

=D

Leaky Nun

why is “”=“0” false?

user21820

We can prove its negation in TC.

If you want an easier time, you could include some extra axioms like ""+x = x = x+"" for any string x.

Actually we don't have to talk about provability to say it's false. The empty string is simply not equal to a non-empty string.

@LeakyNun: Hmm on looking closer it seems I may have made a mistake in my presentation of the axioms of TC in that post. I don't have time to think through it carefully right now, but the axiom in question is:

> (3) Existence of at least two distinct strings.

It seems that it is too weak and we actually need:

> (3) Existence of at least two distinct symbols (a symbol is a non-empty string that cannot be split into two non-empty strings).

Leaky Nun

15:58

so why is it false?

user21820

In the latter we define zero to be one of those symbols.

So by definition it is non-empty.

I thought earlier that we can extract such a symbol using the other axioms.

But I now thing that's not necessarily the case.

I will have to think more carefully before I edit my post to fix the error. I had tried to present an equivalent set of axioms to the one in the paper, but it appears I have made the above mistake. Thank you for making me think about it.

Anonymous I

Wow I'm 6 hours behind on your conversation. I started from the beginning of the explanation. It's very interesting. @user21820

user21820

@LeakyNun: Argh. I also found another error, in (4). To make everything precise, here are axioms that will suffice in symbolic form:
(1) ∃e ∀x ( x+e = x = e+x ).
(2) ∀x,y,z ( (x+y)+z = x+(y+z) ).
(3) ∃x,y ( x≠y ∧ ¬∃u,v ( u≠e ∧ v≠e ∧ ( x=u+v ∨ y=u+v ) ) ).
(4) ∀a,b,c,d ( a+b = c+d ⇒ ∃x ( a+x=c ∧ b=x+d ∨ a=c+x ∧ x+b=d ) ).

I might as well just put these into that post.

@AnonymousI: I will go off in a few minutes so have fun reading and feel free to ask anything to clarify. I will definitely respond next time.

@LeakyNun: Sorry to go. See you next time! =)

Leaky Nun

16:14

see you

is concatenation cancellative?

Anonymous I

16:43

@LeakyNun How did you get establish your maths foundation so well. I mean you know techniques that professors teach students in the 1st year at university like propositional logic, Lambert W function?

Is the Chinese or Hongkong educational system that far progressed in teaching maths? Because in Europe students need to know much less (relatively) to enter university. Some students who perform well on olympiads know some university level stuff but the regular ones don't know anything on that matter. I wanted to know that for a long time. Sorry if I'm off-topic.

Leaky Nun

17:03

@AnonymousI no it’s just me, nothing to do with where i’m from / my educational system

I just like maths a lot

Mathmore

@LeakyNun nevertheless where are you from? :D

Leaky Nun

Hong Kong

user21820

@LeakyNun Strangely enough, cancellation cannot be proven from these axioms of TC. It took me quite a while to find a model that satisfies the axioms but doesn't satisfy cancellation "∀x,y,c ( x+c = y+c ⇒ x=y )". Let L be the set of all linear orders with each item labelled by 0 or 1, with + on L still being concatenation, modulo isomorphism. (1) is true in L because there is the empty linear order. (2) is true trivially. (3) is true because of the 2 singleton linear orders. (4) is true too.

But cancellation fails because of infinite linear orders... (0)+(0,0,0,...) = ()+(0,0,0,...) but (0) ≠ ().

Same for cancellation on the other side. Once you add induction you can prove cancellation on both sides.

Leaky Nun

you lost me at the definition of L

Mathmore

Good night @LeakyNun @user21820!

user21820

17:16

@AnonymousI As I told @LeakyNun just a while back, I knew almost no logic when I entered university.

@Mathmore Haha I got nerd-sniped by @LeakyNun's question...

@LeakyNun You know what are linear orders?

Leaky Nun

sure i do

user21820

Instead of just having an ordering on a set of items, also label each item.

Each label is either 0 or 1.

Leaky Nun

what set?

Mathmore

I didn't get the meaning of "nerd-sniped"

@user21820

user21820

@Mathmore explainxkcd.com/wiki/index.php/356:_Nerd_Sniping

I'm at home safe on a chair though.

@LeakyNun A linear order comprises a binary predicate on a set satisfying reflexivity, transitivity and anti-symmetry.

Now instead of just having an unlabelled set, you have a labelling, which is simply a function that maps each item in the linear order to its label.

Mathmore

17:21

@user21820 awesome xkcd!

linear order is just a total order

user21820

(0,1) is hence not isomorphic to (1,0).

Mathmore

total order relation is a partial order relation on a set in which all elements are comparable.

user21820

So distinct finite binary strings correspond to non-isomorphic members of L.

Mathmore

by comparable it means that either x "less than or equal to" y or y is "less than or equal to" x.

user21820

There are also infinite members of L such as (0,0,0,...) and (...,0,0,0) and (0,0...,)+(...,1,1)+(...,1,1)+...

@Mathmore: If you can understand why L is a model of those axioms, you can explain to @LeakyNun. If not, I'll explain next time. See you both! =)

Leaky Nun

17:31

@user21820 of course I know what linear order is

I just got lost when you represented them with symbols

so are we dealing with countable sets here?

Leaky Nun

17:44

i just mean there’s no way you write down linear orders like this

and why do you never mix 0 and 1 lol

@user21820 never mind you did

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic