Logic - 2018-02-15

« first day (547 days earlier) ← previous day next day → last day (2565 days later) »

user21820

05:16

@MatheinBoulomenos I see.

@MatheinBoulomenos This was one approach I took earlier, yes. However, it's not the one I take today (in my more recent post), which is what I sketched above:

13 hours ago, by user21820

After I construct the complex exponential, for complex parameter x and constant c we have d(exp(x)·exp(−x))/dx = 0 and hence Rolle's theorem extended to complex differentiable functions gives exp(x)·exp(−x) = exp(0)^2 = 1. Similarly d(exp(x+c)·exp(−x))/dx = 0 so exp(x+c)·exp(−x) = exp(c) and hence exp(x+c) = exp(x)·exp(c).

This is indeed a "uniqueness argument", but in my opinion a much simpler and also more elegant one. =)

About multiplying power series, I agree with you that it's usually not done right. Rigorously, one would have to do partial sums, and it is not intuitive why one should do it at all, nor why one should expect it to be true. In my approach, however, it is algebraically clear why it must work.

@MatheinBoulomenos Nice.

@MatheinBoulomenos I think then the main difference between your preferred approach and mine is that yours obtains all the results for the real exponential/trigonometric functions, but you still have to motivate a definition for the complex one. Do you have any motivating reason to consider the complex exponential? According to popular accounts, Euler simply took the power series for exp and plugged in complex numbers...

In contrast, I go straight to the complex exponential, and the motivation for wanting it is using it one can solve any homogenous linear ODE by proving that it can be expressed as a solution to a polynomial of the differential operator D, which splits completely over C, and so we need a complex-differentiable solution to the differential equation exp' = exp.

@LeakyNun I was a bit sleepy yesterday so I only noticed later that I got confused by your question... You say that ( nat → bool ) is undecidable, but what exactly does that mean? I got confused because it's similar to saying that it is not a class (in my type theory), which is easily proven via the undecidability theorem.

For completeness, here is the proof in my type theory, so you can see what you agree with and whether you like it:

user21820

05:41

Let t = ( nat n -> true ).
Let f = ( nat n -> null ).
If func(nat,bool) in class:
	t in func(nat,bool).
	If f in func(nat,bool):
		f(0) in bool.
		null in bool.
		null.
		null = true.
		false.
	not f in func(nat,bool).
	Let S = ( obj x -> ( ( nat y -> x in func(obj,proc(nat,obj)) ? x(x)(y) ) in func(nat,bool) ? f : t ) ).
	S in func(obj,proc(nat,obj)).
	S(S) == ( ( nat y -> S in func(obj,proc(nat,obj)) ? S(S)(y) ) in func(nat,bool) ? f : t ).
	== ( ( nat y -> true ? S(S)(y) ) in func(nat,bool) ? f : t ).

Here, "x == y" means "x and y are equivalent expressions". (It may be that both x and y are null.)

It's a necessary distinction so that we can expand procedure definitions without having to prove that the output is an object. Otherwise we cannot expand when the output is null, which defeats the whole point of having procedures with possibly null output.

In the above proof, though, the "==" are all between objects, because it's such a weak construction. So you don't even need the power of my type theory in reasoning about potentially null expressions. All we need is the ability to reason that ( nat n -> null ) is not a func(nat,bool). This is the shortest proof in my system, but in fact we don't even need this! We can replace it with first proving that there are distinct objects p,q,r and then defining f = ( nat n -> s ) such that not s in bool.

user21820

06:25

To get distinct objects p,q,r is trivial using inbuilt naturals 0 < 1 < 2. But if you want we can get by with the pure type theory fragment of my system. Namely, we prove "not obj in bool or not type in bool or not class in bool":

bool in class.
If obj,type,class in bool:
	obj = type or obj = class or type = class.
	Let R = { x : x in type ? not x in x }.
	If R in class:
		R in R == not R in R.
		false.
	If obj = type:
		R = { x : x in obj ? not x in x }.
		R in class.
		false.
	If obj = class:
		R in class.
		false.
	If type = class:
		R in class.
		false.
	false.
not obj in bool or not type in bool or not class in bool.

@LeakyNun: I'd be interested to know if you find any step in my deductions to be unsatisfactory. =)

user21820

06:42

As for the related question of proving the halting problem unsolvability, which is not the same as talking about ( nat → bool ), one would have to build the notion of programs in the system anyway; you can't get away from that. I've not tried to do it in my type theory, yet.

user21820

07:05

@LeakyNun: I think it's best if you have a type theory with inbuilt tuples, so that you can consider natural tuples, say ntuples, and consider a program as an ntuple that can be interpreted as proc(ntuple,ntuple). So you would have to construct that interpreter. Then you can talk about program behaviour.

3 hours later…