Lambda the Ultimate

I think this stuff fits pretty firmly within the bounds of LtU

It's not you that I was worried about...

"Anything knowable is computable"

So, there's "physical-C.T." and then "metaphysical-C.T.". :-). Oddly, that's relevant to current events (the "New Atheism" of Dawkins, et al.) and, yes, I think PL theory (particularly its ability to formulate questions about the semantics of source forms) is relevant to that debate but probably (hopefully!) it wanders afield of "Lambda the Ultimate".

-t

Another widespread foundational thesis: "Anything knowable is computable". You can prove anything entailed in a set of constraints, axioms, facts, etc. True by definition???

Second order logic is incomplete.

I have great respect for this kind of math but I don't think that we can settle the question this way. For instance we need a definition of knowledge. Knowledge is usually assumed to be unambiguous, concise and complete, if I remember correctly. This rules out incompleteness. Incompleteness is a problem of self reference (?) which is faulty knowledge construction. Anyway my thesis seems to be useful with a few qualifications perhaps.

I have great respect for this kind of math but I don't think that we can settle the question this way. For instance we need a definition of knowledge.

Do we, really? You framed your question in terms that did not appeal to "knowledge," but rather to proof and entailment ("You can prove anything entailed in a set of constraints, axioms, facts, etc."). The notion of incompleteness is stated precisely in those terms.

Knowledge is usually assumed to be unambiguous, concise and complete, if I remember correctly. This rules out incompleteness.

I don't know what you mean by "knowledge," but you don't seem to mean "justified true belief" or a variant thereof. Hmm, it's not even clear to me that you're talking about a relationship between a knower and a proposition.

In knowledge representation the goal is to avoid problems like incompleteness. This is done by being careful with the representation itself, and/or by using special logics that behave better such as Description Logics.

The thesis as I stated it can be made more clear: anything knowable is computable and vic versa; for descriptive logic this is certainly true. We also have in mind the Curry Howard isomorphism where a proof in descriptive logic is a program. Also we are talking about a "thesis" and not a theorem. Given proper restrictions the thesis approaches a theorem. Sorry about any misunderstanding. The thesis applied to second order logic might fail. We have knowable things that don't compute (ie run forever).

edit: We have all heard about true statements that can't be proven from Godel's theorem. There seem to be several ways to look at this. while they may be true they certainly arn't very useful and so don't count as part of a knowledge base. Another impression I have gotten is that these statements are actually incorrect because they involve self reference or are "inconsistent". Correct logic is paraconsistent. If anyone can clear this up I would be grateful.

Are you claiming that the theory of second-order logic is knowable?

Axiomatizations (i.e., "theories") of second order logic certainly do exist, and it is possible to "know" them. However, I suspect that's not what you mean by your question.

The logic most commonly known by the name "second-order logic" is not axiomatizable (the other logics are really multi-sorted first-order logic). If this isn't the logic you meant with your comment on Hank's mention of the "anything knowable is computable" thesis, then I'm at a loss with what you meant by it.

Let's try to concentrate on the technical and formal aspects of C-T. General discussions of atheism are certainly not on-topic for LtU, of course.

I reject any connection between logic, knowledge representation,

So, logic isn't about knowledge and knowledge doesn't need logic?
I'll be curious to understand what you mean by "logic" and by "knowledge".

Id say logis is correct reasoning from axioms, and knowledge is having good axioms.

You left out "and atheism", that is an answer to a previous post. The quote should be "I reject any connection between logic, knowledge representation and atheism".

You left out "and atheism",

Yes, just as Ehud Lamm I think this is irrelevant (though I am an atheist).
Does this means that without the reference to atheism your statement is incomplete (distorted or even meaningless)?
Weirder and weirder!
If you cannot make sense of the "shortened" quotation I am afraid we cannot discuss anything.

It is a challenge to think of anything I could add to the large volume of literature that is almost as old as computer science. But basically I think of the relation between logic and knowledge as "commonsense". Common Sense may be common but that doesn't mean it is easy to understand. Like many issues involving cognition it is too close to home. We may use it but we don't have or easily form theories about what we are doing. John McCarthy first made this connection in "the paper that started it all": "Programs with Common Sense". The link between logic and knowledge is pervasive and shows up in any use of logic once you see the link. Predicate Calculus makes this link particularly clear and is of course a basic logic for knowledge representation. The same logic is also the basis of logic programming. The Curry-Howard isomorphism having nothing to do with knowledge links proofs and programs. It is so pervasive it is hard to argue with, but as we all know it is still controversial almost 50 years later.

Basically I agree with the commonsense theory but I think there is another explanation based on language theory. What if we equate "semantics" with "knowledge". When we expand semantics into a real, application domain we have a little bit of knowledge.

I don't think anything is bad about Cybernetics. It is just that the main insights from cybernetics became well known and are used in mnay different fields (I am thinking mainly about system-level thinking and feedback phenomena), and people became discouraged of Cybernetics as a separate and independent field. Many areas of research these days (from complex systems theory to sytems biology) are related to cybernetics, and carry the torch. To this list of fields one is tempeted to add the work on coalgebras, the various calculi for distributed and concurrent systems etc.

One thing that did happen is that the term Cybernetics itself went out of fashion, so people don't often refer to themselves as Cyberneticians...

So can we think of Church's thesis as proven, based on a systems theory argument?

Lately I have been rereading a little book: An Introduction to Automata Theory by M. W. Shields. I have noticed some parallels with more familiar computer science such as lambda calculus (with and without types). Basically if we reduce a system (an input/output automata) to single state partitions we get a pure functional system. You can take this with a "grain of salt", since I am not a certified mathematician. Also most of the results in Shields seem to propagate into category theory and coalgebra.

Perhaps C-T will always be a thesis and not a theorem because we are interested in practical cases. Is this algorithm computable, is this class of algorithms computable, etc. This is the problem that Church and people of that era were dealing with. Basically "what is a computer?" Is an electronic, analog system a computer for solving differential equations? This seems to be the significance of "systems theory" which I mentioned above. It provides a way to individually state and answer these questions.

It looks to me like what they've done is reduce one informal thesis (Church-Turing) to four informal postulates.

That's exactly right, and it's exactly what they set out to do. The title claims the paper will provide an "axiomatization of Church's thesis." What they mean is something like this: Church's thesis is not, by itself, obviously true. We claim to come with a minimal set of 'obviously true' axioms from which we can prove Church's thesis (and hopefully other non-obvious results). So yes, it is a proof of the thesis, a proof with respect to some axioms. The whole point of axiomatics is that the axioms are simple, independent and self-evident.

So there are a couple of different ways to judge this work. On the one hand, we can ask whether CT actually follows from their axioms, and on the other hand, we can ask whether their axioms are the right ones. Finally, we can also ask whether an axiomatic theory of computation is useful or even possible.