Online research in philosophy

This paper surveys the various forms of Deduction Theorem for a broad range of relevant logics. The logics range from the basic system B of Routley-Meyer through to the system R of relevant implication, and the forms of Deduction Theorem are characterized by the various formula representations of rules that are either unrestricted or restricted in certain ways. The formula representations cover the iterated form,A 1 .A 2 . ... .A n B, the conjunctive form,A 1&A 2 & ...A n B, the combined conjunctive and iterated form, enthymematic version of these three forms, and the classical implicational form,A 1&A 2& ...A n B. The concept of general enthymeme is introduced and the Deduction Theorem is shown to apply for rules essentially derived using Modus Ponens and Adjunction only, with logics containing either (A B)&(B C) .A C orA B .B C .A C.

whole numbers that manages to assert that it itself is unprovable (from a given finite set F of axioms using formal logic). (Gödel's paper is included in the well-known anthology [1].) GF : ``GF cannot be proved from the finite set of axioms F.'' This assertion GF is therefore true if and only if it is unprovable, and the formal axiomatic system F in question either proves falsehoods (because it enables us to prove GF) or fails to prove a true assertion (because it does not enable us to prove GF). If we assume that the former situation is impossible, we conclude that F is necessarily incomplete since it does not permit us to establish the true statement GF.

Gödel's Theorem is often used in arguments against machine intelligence, suggesting humans are not bound by the rules of any formal system. However, Gödelian arguments can be used to support AI, provided we extend our notion of computation to include devices incorporating random number generators. A complete description scheme can be given for integer functions, by which nonalgorithmic functions are shown to be partly random. Not being restricted to algorithms can be accounted for by the availability of an arbitrary random function. Humans, then, might not be rule-bound, but Gödelian arguments also suggest how the relevant sort of nonalgorithmicity may be trivially made available to machines.

The Barcan formula made its first appearance in [1] as ♦(∃x)Φ 3 (∃x)♦Φ, in the logic S2. This logic, S2, despite interesting properties, is not much seen these days, and the Barcan formula itself has been simplified to ♦(∃x)Φ ⊃ (∃x)♦Φ. The paper [1] was one of the earliest serious investigations of first-order modal logic and, of necessity, it was axiomatic since a first-order modal semantics was still some years away. In the system as formulated, the converse of the Barcan formula was provable, but the Barcan formula itself was not. Consequently the Barcan formula was added as an axiom schema because it enabled an interesting development that otherwise seemed impossible.

In classical and intuitionistic arithmetics, any formula implies a true equation, and a false equation implies anything. In weaker logics fewer implications hold. In this paper we rehearse known results about the relevant arithmetic R, and we show that in linear arithmetic LL by contrast false equations never imply true ones. As a result, linear arithmetic is desecsed. A formula A which entails 0 = 0 is a secondary equation; one entailed by 0 6= 0 is a secondary unequation. A system of formal arithmetic is secsed if every extensional formula is either a secondary equation or a secondary unequation. We are indebted to the program MaGIC for the simple countermodel SZ7, on which 0 = 1 is not a secondary formula. This is a small but signi cant success for automated reasoning.

Gödel began his 1951 Gibbs Lecture by stating: “Research in the foundations of mathematics during the past few decades has produced some results which seem to me of interest, not only in themselves, but also with regard to their implications for the traditional philosophical problems about the nature of mathematics.” (Gödel 1951) Gödel is referring here especially to his own incompleteness theorems (Gödel 1931). Gödel’s first incompleteness theorem (as improved by Rosser (1936)) says that for any consistent formalized system F, which contains elementary arithmetic, there exists a sentence GF of the language of the system which is true but unprovable in that system. Gödel’s second incompleteness theorem states that no consistent formal system can prove its own consistency.

I must start with an apologia. My original paper, ``Minds, Machines and Gödel'', was written in the wake of Turing's 1950 paper in Mind, and was intended to show that minds were not Turing machines. Why, then, didn't I couch the argument in terms of Turing's theorem, which is easyish to prove and applies directly to Turing machines, instead of Gödel's theorem, which is horrendously difficult to prove, and doesn't so naturally or obviously apply to machines? The reason was that Gödel's theorem gave me something more: it raises questions of truth which evidently bear on the nature of mind, whereas Turing's theorem does not; it shows not only that the Gödelian well-formed formula is unprovable-in-the-system, but that it is true. It shows something about reasoning, that it is not completely rule-bound, so that we, who are rational, can transcend the rules of any particular logistic system, and construe the Gödelian well-formed formula not just as a string of symbols but as a proposition which is true. Turing's theorem might well be applied to a computer which someone claimed to represent a human mind, but it is not so obvious that what the computer could not do, the mind could. But it is very obvious that we have a concept of truth. Even if, as was claimed in a previous paper, it is not the summum bonum, it is a bonum, and one it is characteristic of minds to value. A representation of the human mind which could take no account of truth would be inherently implausible. Turing's theorem, though making the same negative point as Gödel's theorem, that some things cannot be done by even idealised computers, does not make the further positive point that we, in as much as we are rational agents, can do that very thing that the computer cannot. I have however, sometimes wondered whether I could not construct a parallel argument based on Turing's theorem, and have toyed with the idea of a von Neumann machine. A von Neumann machine was a black box, inside which was housed John von Neumann..

Mechanism is the thesis that men can be considered as machines, that there is no essential difference between minds and machines.John Lucas has argued that it is a consequence of Gödel's theorem that mechanism is false. Men cannot be considered as machines, because the intellectual capacities of men are superior to that of any machine. Lucas claims that we can do something that no machine can do-namely to produce as true the Gödel-formula of any given machine. But no machine can prove its own Gödel-formula.