Logic - 2018-09-17

12:34 AM

@user21820 so my proof on recursion was legit, I have found it in this paper so this means that this way of construction either forces us to have some logical inconsistency or to think that uniqueness is not always logically independent from existence, I don't know

David Reed

12:46 AM

I'm not certain about your last statement. What I can say is the recursion theorem basically says that a recursively defined function is in fact a function. That is, there exists a function that satisfies the constraints you have placed on it recursively

Basically it amounts to a proof that recursively defined functions are "allowed"

famesyasd

@DavidReed what I'm concerned about is that when I proved the "uniqueness" part of it being a fucntion I have used the "existence" function part there also, but I have always thought that uniqueness and existence parts should be logically independent

David Reed

Not certain I follow regarding "logically independent" here either unfortunately. If you are saying that in the course of the proof, you have used the fact that the function exists to conclude its unique I see no reason why that would be forbidden

There are certainly times where you can prove that something is unique without having proven that it exists.

That is you can prove "if it exists, then it must be unique" and have absolutely zero knowledge of its existence

MP inverse is a good example

Define it to be the unique matrix X such that (XAX) = X , AXA = A , (AX)*=AX, (XA)*=XA

You can show that IF such an X exists satisfying those 4 questions, then it will be the only one that does (uniqueness)

You can show that having absolutely zero knowledge of whether such an X satisfying those equations does in fact exist

famesyasd

No, in my proof it seems that existence is absolutely essential it's not about paraphrasing or something. To be precise, let's call the set that I want to prove is a function being recursively defined as 'h'. So in my proof, I have proved that forall x in N exists y (x,y) in h. But to prove that forall x in N forall y_1, y_2 if (x,y_1) in h and (x,y_2) in h I have used that previous fact that forall x in N exists y (x,y) in h!

David Reed

Yes recursion theorem needs to hit both existence and uniqueness

my point is you can use knowledge of its existence in proving its uniqueness--they don't have to be completely independent

Is that thing typed up there your proof?

famesyasd

@DavidReed sorry, I did not understand last sentence

David Reed

1:01 AM

The proof you are talking about, it that the image you posted up there?

famesyasd

yes, look at the second part

David Reed

ok one moment

famesyasd

where they show that S is an inductive set

David Reed

Ok So what specific line are you taking issue with

famesyasd

"Suppose now n in S. Then where exists a unique x in X such that (n,x) in u"

David Reed

1:08 AM

So you are wondering based off of everything previously said how you can conclude the x is unique?

If so the answer is because it is built into the definition of S

famesyasd

I don't know, I'm starting to think that your trick works now, lol. Okay so even if it works is there always a way to reconstruct a proof in a way that doesn't use this trick and derives uniqueness directly?

Like in your example with matrices

I mean to do it in a way without assuming existence at all

David Reed

That is to prove something along the lines of "if it exists, then it is unique"

is that what you're after? You can prove something will be unique without having any knowledge of its existence.

famesyasd

to prove uniqueness without saying that "if it exists..."

David Reed

that's a tricky proposistion

Here's the MP way. You say, suppose X and Y both satisfy all 4 of those equations

We then prove X = Y as follows

X = XAX = X(AX)* = XXA*=XX*(AYA)*=XXAYA*=X(AX)*(AY)*=XAXAY=XAY = XAYAY = (XA)*(YA)*Y = AXAYY = (AXA)*YY=AY*Y = (YA)*Y = YAY = Y

So I've shown that any two solutions to that system must be identical. (i.e. the solution to those 4 axioms, if it exists, will be unique

You then show existence by taking a full rank factorization of A, say A = FG, and define A+ = G*(GG*)^-1(FF)^-1F and show that it does in fact satisfy all the equations

so here in this approach we proved uniqueness before proving existence

but we HAD to assume existence in order to prove the uniqueness part

famesyasd

1:33 AM

where

David Reed

Well we effectively said "Suppose X and Y are solutions to this system. From that we deduced X=Y

famesyasd

oh, okay, but in my proof you'd also need to assume the existence of x, not only S(x) that's the problem

I mean, given (S(x), y_1) in h, (S(x), y_2) in h to also be able to conclude (x,y) in h for some y

David Reed

Are you saying you are stuck on the sentence "so there exists a unique x..."

famesyasd

yes

this is where we use external existence

David Reed

and you are stuck on wondering why it exists at all or you see that it exists and are wondering why it is unique

famesyasd

1:40 AM

it exists because I proved beforehand that it should exist, imagine if I did not do that in advance then I would not be able to complete the uniqueness part if I wanted to prove uniqueness part first

David Reed

Um heres the best I can, this is totally a consequence of the definition of S and the statement "Suppose n $\in$S

famesyasd

Oh, I did not notice that he mixed existence and uniqueness in one part lol, that's totally cheating

ehhh

David Reed

;)

famesyasd

I shall just go to sleep

user21820

4:28 AM

@famesyasd As I told you before, it should be trivial to translate your proof to 'separate' the existence and uniqueness part of your proof. Until you write it out formally in Fitch-style or sequent-style, I am unable to comment on it except to say that you are most probably wrong that it cannot be separated.

Sep 10 at 8:51, by user21820

> exists x ( Q(x) and forall y ( Q(y) implies x=y ) ) iff exists x ( Q(x) ) and forall x,y ( Q(x) and Q(y) implies x=y ).

Sep 10 at 9:22, by user21820

Every proof that you have which proves uniqueness by proving one side can be easily transformed into a proof that goes by proving the other side.

Sep 10 at 9:24, by user21820

Instead of using the x that you proved existed to prove "forall y ( Q(y) implies x=y )" (to obtain the left-hand side), use the y given to you in the condition "Q(x) and Q(y)" to prove "x=y" (to obtain the right-hand side).

And there would be no logical inconsistency; don't get too excited about it! =)

@famesyasd: After you write your proof out in Fitch-style, I will transform it for you to one that 'separates' the existence and uniqueness parts. Then you will see why it is not as strange as you thought.

famesyasd

9:30 AM

@user21820 okay, I can see that by proving the left part the uniqueness follows and this is what's done in the proof above and this is what I can do in my proof. However, in the left hand side uniqueness and existence are mixed so I don't see how that helps with proving them separately. I mean I should be able to deduce the second half whenever, without using the left hand side.

user21820

@famesyasd Which is precisely what I am saying is trivial to achieve. If you can prove the left-hand side directly, you can also prove the right-hand side directly by using the proof of the logical equivalence to transform your original proof mechanically.

It seems to me that you are unable to perform that mechanical translation, and hence I would actually need to see and transform your formal proof for you.

famesyasd

9:50 AM

@user21820 Okay, suppose we have a function F: A -> A, a in A, and we take h such that forall x x in h iff forall b if [(0,a) in b and forall s in N, t in A if {(s,t) in b then (S(s), F(t)) in b}] then x in b. And suppose that we have proven already that h subset N times A and also that forall x in N exists y in A (x,y) in h.
Now we want to prove that forall x in N forall y1,y2 if (x,y1) in h and (x,y2) in h then y1=y2.
Let's take a set M subset N such that forall x x in M iff forall y1,y2 if (x,y1) in h and (x,y2) in h then y1=y2.

user21820

That is what I really dislike about prose proofs. I cannot do the translation mechanically because all the logical structure is obscured.

famesyasd

you can look at the proof I linked in the picture

it's literally the same

last ident

after words 0 in S.

user21820

All prose proofs have the same problem. That is why I said I wanted a Fitch-style proof, so that I can concretely show you that it is a mechanical translation.

famesyasd

It's gonna take forever writing it out here fully, can you show some toy example?

user21820

Let me think about a good toy example. I don't mean that you have to write out every detail, by the way. Just the contexts and the claims within them must be 100% clear, and all intermediate deductions can be left out.

famesyasd

9:56 AM

okay

user21820

Also, I can do the proof myself, but I was hoping to show you that I can mechanically transform any proof without even understanding it.

After you're done (or if you don't want to do it) you can take a look at my Fitch-style proof of uniqueness (with no proof of existence):

Given A in type and F in func(A,A) and c in A:
	Let Q = ( func(nat,A) f -> f(0) = c and forall k in nat ( f(k+1) = F(f(k)) ) ).
	Given g,h in func(nat,A) such that Q(g) and Q(h):
		g(0) = c = h(0).
		forall k in nat ( g(k+1) = F(g(k)) ).
		forall k in nat ( h(k+1) = F(h(k)) ).
		Given k in nat such that g(k) = h(k):
			g(k+1) = F(g(k)) = F(h(k)) = h(k+1).
		forall k in nat ( g(k) = h(k) ).	// by induction
		g = h.

famesyasd

This is not the same uniqueness I was talking about!!!

ahhhhhhhhhh

user21820

I think I have forgotten. So you want the internal uniqueness of the output given an input?

famesyasd

Yus!!!

user21820

(Of course, that problem only arises in a cumbersome foundation like ZFC.) Give me a while.

famesyasd

1:56 PM

@user21820 so is it possible to rewrite it or is there indeed some problem?

user21820

2:57 PM

@famesyasd I was busy with some other things just now.

famesyasd

3:49 PM

oh, okay

user21820

4:56 PM

Let rel = ( type S , type T -> func([S,T],bool) ).
Given A in type and F in func(A,A) and c in A:
	Let G = ( rel(nat,A) R -> R(0,c) and forall k in nat ( forall x in A ( R(k,x) implies R(k+1,F(x)) ) ) ).
	Let S = ( nat k , A x -> forall R in rel(nat,A) ( G(R) implies R(k,x) ) ).	// intersection of all relations satisfying G
	Let Q = ( nat k -> forall x,y in A ( S(k,x) and S(k,y) implies x=y ) ).	// uniqueness of mappings of k in S
	// Proof that S satisfies G //
	Given R in rel(nat,A) such that G(R):

@famesyasd: I've posted more or less a full sketch of the proof of the uniqueness of the mappings in the constructed relation (the intersection of all relations 'closed' under the recursion) with completely no proof of existence of any mapping except for the initial mapping.

user21820

5:57 PM

I should have said that I left out two small portions that you definitely can fill in. Also, this has made me curious about this method. It is more different from the one where you just build approximations (functions on {0..n} that satisfy the recursion) and take their union after proving that any two approximations agree, than I thought.

Note also that I did not use contradiction anywhere; my proof is completely constructive except for the quantifying over rel(nat,A) in the definition of S.

Anyway I got to go now. Feel free to ask if any step is unclear.

famesyasd

@user21820 how were you able to conclude that x = c and y = c?

I don't follow through half of the notation :(

to be precise I don't understand the first string, what is rel

to be very precise I think that you omitted the proof that G(R0)

Transcript for

♦ Logic

♦ $Mathematics$ Logic