gusl: (Default)
[FOM] The Myth of Hypercomputation
One argument against hypercomputation
is that even if someone hands me a hypercomputer (that solves the halting
problem, say), I cannot verify that it really works as advertised from a
finite set of finite measurements. Without the ability to make a finite
verification, I can never really "know" that the hypercomputer is "really
solving" the halting problem.

This is good stuff. I'll have to look at it later.


Héctor Zenil & Francisco Hernández-Quiroz - How might the human mind be computationally more powerful than Turing machines?

Finally, there are several arguments by Bringsjord.

I get the impression that all these arguments for hypercomputing minds are made in order to justify "romantic intuitions", i.e. they are not exploratory discoveries, which is what you would expect from unbiased scientists. I confess that I suffer from the symmetrical problem: always trying to justify my computationalist intuitions. (never mind that I may actually be a dualist in philosophy of mind)
gusl: (Default)
Videos from the Conference on Computing and Philosophy 2003

I can't see them yet, but will when I get home.

Tim Van Gelder's "Reason!Able: Computer Assisted Critical Thinking" looks particularly interesting.
Here is his project's website.
gusl: (Default)
It's impossible to prove Pi_1 statements without axioms that talk about infinity.

If it were possible, I would like to do it right now with Lisp. I have implemented a refuter for general Pi_1 statements, but even though implementing a verifier would never be successful, I still firmly believe in some proofs of Pi_1 statements. That means that I must implicitly accept axioms about infinity, much as I'd like not to.

Here's a nice theorem:
;;;All numbers with an odd number of divisors are perfect squares:
(forall #'(lambda (n) (implies (not (perfect-square-p n)) (evenp (n-divisors n)))))

And here's a nice proof:

(Lemma 1) Forall n in N, n is a perfect square IFF its prime factorization has an even power at all the primes.
(Lemma 2) Forall n in N, n-divisors(n) = PRODUCT (power(p_i,n) + 1) for each prime p_i in the factorization of n

Suppose n is not a perfect square (1)
Then there is a prime p in the prime factorization of n such that its power is odd. (by 1, L1)(2)
Since power(p,n) is odd, then power(p,n) + 1 is even. (3)
Then n-divisors(n) is even. (by 3, L2) (4)

But which axioms am I using in this proof? Are they too hard to dig out of the lemmas? My justification for the lemmas is my visual intuitions. Somewhere in proving them in any kind of system, you would need an axiom about infinity, right?

in case you want the rest of the Lisp code:
Read more... )
gusl: (Default)
In the philosophy of mathematics...

I am a formalist...

but let me tell you a story.

The characters are:

* Strawman Platonist
* We(1) is a mathematician who believes that if mathematical objects exist at all, then infinite-information mathematical objects exist too.
* We(2) takes a computer scientists' view. He's a total reductionist and in particular, believes in digital physics.

We(2) subscribes to an ontology of mathematics which says that only recursive objects exist:
* Infinite things do not really exist. We can talk about them as what would happen in the limit.
e.g. The set of natural numbers does not exist. What does exist is an algorithm which generates "them".

We(2) believes that the reason We(1) talks about infinite things is because it is simpler to talk about them as if they existed. The set N is a convenient fiction. Talking about algorithms just makes life more complicated. We(2) says that if We(1) were right, then We(1)'s access to it would be mediated through an oracle. Like most normal mathematicians, We(1) normally talks about mathematics as if oracles existed.

We(2) believes that oracles don't exist.

We(2) believes that the set N is an idealization of the algorithm which produces 0, S0, SS0, SSS0, etc. All sets are lists, and thus well-ordered.


* Recursive objects. The algorithm producing it terminates.
* r.e. objects, which are the limit of what the algorithm would produce.
* co-r.e. objects, which are the same, since in the limit, a set can defined by its elements as well as by its non-elements.

While recursive objects really exist (or can be directly perceived by mathematical cognition), r.e. and co-r.e. objects live in the Platonic realm.

We(2) has read his Kevin Kelly and believes that the channel through which we communicate with the Platonic realm is restricted by computability. (Kelly talks about the scientific process as a channel between the scientist and nature... here we talk about the channel between mathematician and *** THE PLATONIC REALM ***)

BUT, since We(2) thinks it doesn't make sense to talk about unknowable things (especially in mathematics!), then the only mathematical objects that it makes sense to say exist are the ones which are somehow knowable (i.e. through this channel)!

In We(2)'s ontology, is pi recursive or r.e.?

In a sense, pi is r.e.... pi is an algorithm which successively approximates the Platonic pi.
However, proofs about pi are recursive. (proofs are always recursive!)
So, we could say that proofs about pi only make reference to Pi.
But do proofs ever do anything other than refer? Sure, when are objects are computable: e.g. a proof that 2 + 3 = 5 in PA uses the senses of 2, 3 and 5. (at least, a formalist would agree that "SS0" is the sense of 2)

So We(2) makes a distinction between sense and reference for all mathematical objects. While some references can be reduced to their senses (e.g. any finite number or any finite set), some references have senses that are "transcendental" and can only be accessed through an oracle (e.g. any infinite set)

While pi's reference is recursive, pi itself (i.e. its sense) is r.e.
All mathematical objects have recursive reference (at least I've never seen a non-recursive reference printed anywhere ;-) ). Just like you're sending me an email this very moment... I've never been contradicted on this either! (stolen from [ profile] fare)

A little dialogue

Gustavo: Isn't it paradoxical that R has finite information (afterall it's easy to check whether something is in R), and yet some elements in it have infinite information? All objects used in mathematical discourse, even Platonic discourse, have finite information.

Henrik: No, we can reference R in a finite way, but R itself has infinite information.

Gustavo: and, also, sometimes it may be very hard to check whether a number is in R... especially if the input is coded in terms of a difficult question (like the Riemann hypothesis)

Henrik: but in principle, even the Riemann hypothesis could be decidable axiomatically. O buraco é mais embaixo. (The real problem is worse than you think)

Gustavo is struggling with his intuitions about which mathematical statements are meaningful, and therefore should be provable. Gustavo is not comfortable with mathematics being semi-empirical. He wants an algorithmic way of coming up with new axioms.

Tentative definition: A statement is meaningful iff it is in principle verifiable or falsifiable. It would be nice to have a logic of which statements are meaningful:

"A /\ B" is meaningful iff "A" is meaningful and "B" is meaningful
"A \/ B" is meaningful iff "A" is meaningful and "B" is meaningful
"A -> B" is meaningful iff "A" is meaningful and "B" is meaningful
"~A" is meaningful iff "A" is meaningful
"forall x in X, phi(x)" is meaningful iff it is meaningful for each "phi(x)" for each x in X.

(is it not an accident that I had to bring the X outside of the quote for the definition of the universal, unlike all good definitions of semantics?)

Interlude: The diagonalization argument according to our view of infinite objects as non-terminating algorithms...

Given any algorithm producing infinitely-many infinite decimal expansions (each of which is really an algorithm) (i.e. given any infinite list of real numbers) (NB: lists are necessarily countable),

our construction algorithm outputs an algorithm which produces an infinite decimal expansion which differs from all decimal expansions above in at least one place (i.e. a real number which will never be produced by the algorithm above)

So the set R of all real numbers is not even r.e.

Let's look at the types of these algorithms, so that we may see something about the nature of R. (Can we talk about types when algorithms don't terminate?)

A number from 0-9 : D (e.g. 5 : D)
An infinite decimal expansion is of type A, (decimal expansion : list_of D) (e.g. pi : list_of D)
An algorithm producing decimal expansions : list_of (list_of D) (e.g. any list of real numbers)
Our diagonal construction algorithm returning a novel real number : (list_of (list_of D)) -> (list_of D)

list_of is a dependent type, taking a type as input.

Gustavo is hoping that we can somehow dismiss R as meaningless, using the fact that it's not r.e.

Reinterpreting the Quantifiers

forall is an infinite conjunction, e.g. forall x in N.phi(x) is actually phi(0) /\ phi(1) /\ phi(2) /\ ...
exists is an infinite disjunction, e.g. exists x in N.phi(x) is actually phi(0) \/ phi(1) \/ ...

so, "forall x in N. phi(x)" is not verifiable (it may be provable using axioms, but that's a different story)
likewise, "exists x in N. phi(x)" is not refutable.

To verify "forall x in N. phi(x)", we would need a machine that checks phi for all natural numbers.... such a machine requires an oracle. Remember: oracles don't exist!

Topological semantics

verifiable : open
refutable : closed
/\ : intersection
\/ : union
~ : complement

Suppose phi(x) is verifiable for all x. i.e. forall x, phi(x) is an open set.
Can we say that "forall x in N. phi(x)" is verifiable? No, because an infinite intersection of open sets is not necessarily open.
gusl: (Default)
I am a realist-in-truth-value for recursively-enumerable statements. i.e. I believe that statements for which counterexamples could be found if they existed must be either true or false.

For example, the Goldbach conjecture must be either true or false (since if it were false, you could find a number >4 which is not a sum of two primes). Also, whether any Turing Machine halts is a recursively-enumerable problem.

Basically, it seems to me that any meaningful problem is recursively-enumerable.

A consequence of Gödel's Incompleteness:
If a set of axioms expressing PA is recursively-enumerable, there will be statements which are undecidable.

I believe there should be an algorithmic way of deciding all recursively-enumerable statements, i.e. an algorithmic way of proceeding in making mathematics prove more true things whenever you run into undecidabilities (i.e. whenever you correctly prove, using a meta-method, that a sentence G is true but not provable in the original system). But this seems not to be possible, for if there were any such algorithm, we could construct its halting problem, and *that* problem would be undecidable in the new system.

So I do think that Gödel's theorem is significant for the philosophy of mathematics. And it seems like Chaitin is onto something when he says that mathematics must be semi-empirical.

Again, thanks to Benedikt Löwe for reciting me the theorem above.
gusl: (Default)
Bringsjord has worked out my Penrose-like idea, formalizing his argument in quantified modal logic.

So the Halting Problem, HP becomes: forall TMs x, there exists a TM y such that x does not decide y.

He shows that the assumptions:

(1) I!: There exists a Turing Machine M, such that no Turing machine can decide whether it halts. And *necessarily* so, since it's a mathematical theorem. (this seems wrong to me!)
(2) For every Turing Machine M, there is a person S such that it's logically possible for S to decide M.
(3) All people are machines.

lead to a contradiction. (the contradiction is trivial, but he goes through the formal steps of his modal logic)

Of course, (2) is controversial. If I am a computer (which I believe I am), I would like to see my "Goedel sentence": which Turing Machine can I in principle not decide?

The lesson from Goedel's incompleteness theorem is that you always need to pick more axioms.

Analogously, if you're a Turing Machine whose mission in life is to decide whether Turing Machines halt (my new favorite way for thinking about this stuff, thanks to [ profile] r6), you always need to change your Universal Turing Machine to one that decides more TMs.

Then the question becomes: "But how?". To me, the paradox remains, because if you have a systematic way of changing your Turing Machine simulator, then you're just using a meta-Turing Machine which is just as susceptible to undecidability: you'll never be able to decide whether the halting construction for meta-TM halts.

See Bringsjord - A Modal Disproof of "Strong" Artificial Intelligence (page 8)


gusl: (Default)

December 2016

18 192021222324


RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags