June 5th, 2017, 04:24 PM  #1 
Newbie Joined: Mar 2016 From: Alabama Posts: 18 Thanks: 0  Foundations questions
1. Would an axiomatic theory of algorithms that transform any given input set to any arbitrary output set ("arbitrary" in the sense of "need not satisfy any particular criteria", not "arrived at by a nondeterministic process") be equivalent to a theory of universal computation? 2. In what way is a foundational theory of computation different from a foundational theory of mathematics? In particular, is either reducible to the other by reasonable standards of judgment? 
June 5th, 2017, 04:40 PM  #2  
Senior Member Joined: Aug 2012 Posts: 1,620 Thanks: 411  Quote:
Quote:
Quote:
Last edited by Maschke; June 5th, 2017 at 04:48 PM.  
June 5th, 2017, 05:28 PM  #3  
Newbie Joined: Mar 2016 From: Alabama Posts: 18 Thanks: 0  Quote:
Last edited by zambod; June 5th, 2017 at 05:47 PM.  
June 5th, 2017, 05:48 PM  #4  
Senior Member Joined: Aug 2012 Posts: 1,620 Thanks: 411  Quote:
As far as the halting problem, its importance is that it's the standard example of an easily stated problem that can not possibly be solved by an algorithm. Your question, "why is halting central to the definition of algorithms," does not seem to make sense. Halting has nothing to do with the definition of algorithms. Once you define an algorithm, the halting problem pops up as a problem that can't be solved by an algorithm. Can you say more about where your questions are coming from? Are you taking a class, are you the author of the paper you linked, are you pushing an agenda, trying to learn CS? I must say I was put off by the linked paper since in its very first paragraph it veers off into its own world. If nothing else (and there's plenty more else) take the statement, "... classical logic is a systematic tool for telling what is true." Since classical logic can never tell us what is true, what am I supposed to make of the rest of the paper? Are there translation errors involved that make this paper seem crankier than it is? Last edited by Maschke; June 5th, 2017 at 05:52 PM.  
June 5th, 2017, 06:04 PM  #5 
Senior Member Joined: Aug 2012 Posts: 1,620 Thanks: 411 
Are you the author of the paper? There is an article on CoL on Wiki https://en.wikipedia.org/wiki/Computability_logic It reads like an outline of the paper. Most of the references are to works by the same author. In the Talk page (click on Talk at the top of the Wiki page) I found the following comment: This entry strikes me as selfadvertising by Mr. Japaridze. There are quite a few "computational logics" like this one; an expert should decide whether Mr Japaridze's theory is such a breakthrough as to deserve a single entry to itself. This is my impression too. The author has a Ph.D. and is serious about his research project, but now he seems to have written his own Wiki page (against Wiki rules) to promote his ideas. And someone else on the Talk page noted, as I did, that calling classical logic a theory of truth is flat out wrong. If you're the author, I'm in no position to debate your ideas. But if you're just someone trying to learn computability theory, I'd stay stick to the standard sources and don't worry too much about CoL. My two cents on that. 
June 5th, 2017, 06:10 PM  #6  
Newbie Joined: Mar 2016 From: Alabama Posts: 18 Thanks: 0  Quote:
I'm a student. It's possible I gave the paper too much credit because it comes from a scholarly source.  
June 5th, 2017, 06:19 PM  #7  
Senior Member Joined: Aug 2012 Posts: 1,620 Thanks: 411  Quote:
I'm sure the paper is valid but it doesn't seem to bear on anything elementary. If he's trying to develop a logic for computable game theory that's way beyond my expertise. Last edited by Maschke; June 5th, 2017 at 06:22 PM.  
June 6th, 2017, 05:58 AM  #8  
Newbie Joined: Mar 2016 From: Alabama Posts: 18 Thanks: 0  Quote:
Mathematically, is there any reason to think we can't find structural regularities in the execution of a nonhalting procedure? Theoretically, in the Hoare logic model of imperative languages, "termination must be proved separately" as Wikipedia puts it: https://en.wikipedia.org/wiki/Hoare_logic In practice, loops that are not guaranteed to terminate have real world applications in programs that are supposed to run until the user quits, to give one example. Are such programs not "algorithms" if we can't prove that the user will quit? These are my grounds for thinking that computer science can be more classical than constructive if we put effort into discovering such a theory. Quote:
Trying to answer this question runs into a couple of snags. To be brutally honest, at its current stage of development, it looks like a bunch of completely unrelated minilogics to me. For comparison, this is what a successful 'Gametheoretic Model of Computation' looks like: https://arxiv.org/abs/1702.05073 Can you haul scrap metal from a junkyard onto your lawn and call it a "future car"? It's not easy to enumerate the properties of objects that we're not sure can "exist", as it were, in principle. That's the reason I gave for why "algorithms" are required to halt in all cases, but classical mathematics is on surer footing than some unknown "Computability logic" that may or may not exist in some unknown corner in the space of consistent concepts. Since classical mathematics analyzes functions that are not guaranteed to halt, it follows that the reason I gave falls short of being a sufficient deterrent. Last edited by zambod; June 6th, 2017 at 06:53 AM.  
June 6th, 2017, 02:51 PM  #9  
Senior Member Joined: Aug 2012 Posts: 1,620 Thanks: 411 
I wish I could respond to this at the level of knowledge it requires. I have only tangential knowledge of computer science and not all that much math either. You might consider clarifying your question down to something specific and answerable, and posting it on cs.stackexchange or else any of the Reddit groups for CS, algorithms, etc. That said, I found your post interesting and I have some comments that might be of interest. Quote:
On the other hand, computation is inherently constructive. It's exactly the study of everything we can construct using algorithms. So I am arguing that the link between computation and constructive math is more circumstantial than philosophical. In other words computation just happens to be about recipes, and constructivists like recipes. But I think the study of computation is itself agnostic to the philosophy. If computation turned out to involve nonconstructive elements then the computer scientists would just do that. They wouldn't be bothered by using nonconstructive math if that's what they needed to do to study computation. Whereas the constructivists would be annoyed. Does that make sense? I have a datapoint to support this opinion later. Quote:
Quote:
First, I was going to say that if we forget procedures and talk about bitstrings instead, then there are uncountably many bitstrings and only countably many procedures so almost all bitstrings have no "structural regularities." So that's a blunt force way to look at the problem. But it occurs to me that you're talking about something more subtle. Procedures that don't halt. I don't know anything about those. So maybe this is something people study. I do know that there is a concept in math called "definable but not computable." A number is computable if there is an algorithm that cranks out its decimal (or binary) digits. A number is definable if it can be uniquely characterized in the language of firstorder Peano arithmetic (or some other system, which may give you a different notion of definability). It's not hard to whip up a real number that is definable but not computable. One such is Chaitin's $\Omega$. https://en.wikipedia.org/wiki/Chaitin%27s_constant This number is essentially a bitstring where the nth bit tells you whether or not the nth Turing machine (in some particular encoding) halts. This number can not be computable else we'd solve the halting problem. But it's perfectly well definable, I just defined it. (Exercise for the reader to figure out how what I said makes it "definable in firstorder Peano arithmetic." That's beyond the limits of my knowlege). Now what's interesting is that Chaitin used his ideas to prove Gödel's incompleteness theorems in purely informationtheoretic terms. So we're actually in the realm of Gödelean incompleteness here. And here is something not too well known. Say you have an axiom system for arithmetic (theory of the natural numbers). We know it's incomplete, so there's some statement we can neither prove nor disprove. So we pick a truth value arbitrarily and add that as a new axiom. Now we have a NEW axiom system (the original one plus the independent statement or its negation). But this new system must ALSO be incomplete ... so we can add another axiom ... You can see that we are going to get an infinite hierarchy of axiom system that kind of branch out in all directions. And do you who studied this? None other than Turing. His doctoral dissertation was about "Ordinal models of computation," in which he used the mathematical theory of the ordinal numbers to keep track of the structures you get when you keep extending axiom systems. https://en.wikipedia.org/wiki/System...ed_on_Ordinals This is related to oracles. You assume you have a magic box that computes something noncomputable, and you see what you get. So Gödel, Turing, and Chaitin are all over this mysterious realm of extensions beyond what's computable. And I believe this is what you are talking about. Tell me if anything I've written is on target. Quote:
Quote:
So is a web browser not a computation in the sense of computer science? In which case, what is it? It's sort of like in math, if you define "proof" the way they do in logic, no working mathematician has ever seen a proof. If you define program as a computer scientist does, once you get beyond "hello world" no working programmer has ever seen a program! Small exaggeration but you get the idea. I have wondered about this for a long time. Quote:
But in math, we have a LOT of uncomputable things. Uncountably many. Too many to be accounted for in ANY possible formal system of symbol manipulation. Those kinds of systems are inherently countable. So there's three levels: * Computable. * Definable but not computable. Extending axiom systems one new statement at a time. Chaitin's ideas. Oracles. * Full mathematical ontology. Uncountably many real numbers, existence without recipes. The CoL thing? I confess that all I got out of it was that it is advanced and esoteric, not really bearing on the things I'm talking about at all. But I could be wrong. On a pragmatic basis I think you'd be much better off reading Chaitin (who writes pretty clearly) than this other guy who seems to be working in a very small area consisting mostly of himself and a couple of others. Just my impression. Quote:
Quote:
Quote:
Here's a lighthearted philosophical question. If people come by and take parts off the old car on my lawn, one piece at a time, and put them in their cars; and eventually every single part of my old car is now driving around in thousands of different cars; can we say that my car is still on the road? Quote:
Am I understanding you right? What things exist in principle, maybe I lost your meaning here. Quote:
Last edited by Maschke; June 6th, 2017 at 03:11 PM.  
June 8th, 2017, 11:33 AM  #10 
Newbie Joined: Mar 2016 From: Alabama Posts: 18 Thanks: 0 
I've been trying to think about why you find game semantics so exotic when researchers working on it intend it to be a more intuitive model for computation than Turing Machines. Have you studied programming computable functions (PCF), Martin Lof's type theory, linear logic and the early literature on game semantics? The first three are each a set of rules that can be listed on a single page. You can find basic texts on these subjects by Googling: <subject name> pdf


Tags 
foundations, questions 
Thread Tools  
Display Modes  

Similar Threads  
Thread  Thread Starter  Forum  Replies  Last Post 
Need recommendations for a good foundations of mathematics b  vindy  Math Books  1  February 22nd, 2014 09:07 AM 
Calculus Foundations (Leibniz and Berkeley)  bt359  Calculus  1  November 15th, 2013 12:39 PM 
Foundations of Geometry  carl1234  Math Books  3  February 21st, 2010 02:44 PM 
Foundations of Mathematics  CRGreathouse  Applied Math  10  July 26th, 2008 09:26 PM 