[problem of axiomatic consistency] - A New Kind of Science: The NKS Forum

A New Kind of Science: The NKS Forum

Pages:1

problem of axiomatic consistency
(Click here to view the original thread with full colors/images)

Posted by: Philip Ronald Dutton

The classical solution to consistency problems in axiomatic systems was to "encapsulate" the system in a finite model. Of couse, also, Hilbert's absolute proof method preferred to side step any association with infinity notions-- analysis which utilizes no infinite # of structural properties of formulas and no infinite # of operations with formulas. All this for fear of various problems down the road with contradictions of sorts.

Does not an algorithm, such as a simple looping program, tame the beast of infinity? Recast the classical method of model usage for the solving of axiomatic consistency using the model of a simple program rather than the finitistic models.

Even if the suggestion is ridiculous my idea should remain of interest in the following manner:

An NKS simple program is simple and therefore should somehow be an acceptable model on which certain structures and etc. could be cast (structures which need infinity encapsulated within the finite, the algorithm... or more precisely: the looping algorithm).

I have only read the intro chapter of NKS and remember therein was a mention of the Logics and how they might possibly benefit from NKS. Perhaps the idea in my head (which hopefully makes sense in writing) is related....

Hopefully, pro-NKS philosphers and logicians can understand my enthusiasm for such an experiment...

PS: I have not yet read for myself GODEL's proof. I have only read chapter's of background material. Therefore, I wonder, prematurely, if using an NKS simple program as a model would provide unexpected consequences... or rather, I should hope, fruitful insights.

Posted by: Gunnar Tomasson

Re. the following:

Does not an algorithm, such as a simple looping program, tame the beast of infinity? Recast the classical method of model usage for the solving of axiomatic consistency using the model of a simple program rather than the finitistic models.

Comment:

Perhaps I misunderstand the point at issue - but, it seems to me that there cannot in principle be ANY problem of "solving of axiomatic consistency".

For to speak of an axiomatic structure - for example, Euclidean geometry - is to speak of some given set of consistent axiomatic propositions.

Absemt such consistency, there is no axiomatic structure in the first place.

Gunnar

Posted by: Philip Ronald Dutton

I was thinking along these lines: pretend GODEL's proof had yet been written. Now, there must be only a few ways to tackle that problem of consistency. One of them is to "cast" onto the finite models while staying away from infinite models. Well, is not the non-terminating looping algorithm something that is finite but it has the power of the infinite? What would happen if a simple program had been used as the model?

Interesting, I think.

Of course my second point (within the original thread post) is perhaps of greater interest.

Thanks.

Posted by: Philip Ronald Dutton

If someone figured out some basic "properties" of some simple program (one that captures infinity via the common program loop), then perhaps some kind of axiomatic system could be built which "encapsulates" arithmetic using programs as a base structure.

If this was ever possible then would GODEL's proof apply?

Perhaps there is some intrinsic properties of simple non-terminating, looping programs which, if taken advantage of, would nullify GODEL's proof in relation to this particular axiomatic system.

What makes GODEL's proof hold water? Axiomatic systems in general OR the core elements on which they are founded?

If the latter, then how do we know that, by using simple programs as the core element, Godel's proof would no longer apply?

(obviously our generation of saavy computer users are more comfortable with programs... perhaps there is still something to be learned by using them as core elements instead of all the things that the pre-computer generation thinkers used in their axiomatic systems)

PS: Perhaps the rules of inference could be thought of as a simple program? If not then can we recast inference rules onto a simple nonterminating looping program?

Posted by: Jason Cawley

Arithmetic is already universal. That is what allows the metamathematical construction that encodes any proposition into some proposition of arithmetic. The axiom of arithmetic that corresponds to looping in programs is induction. Logic is not universal because it does not have such an axiom, making it strictly finite. Note that set theory differs from arithmetic because it allows transfinite induction - induction on arbitrary sets. So the cardinalities reached by logic, arithmetic, and set theory differ. The main point is that one already has enough potential complexity to encounter all the problems of irreducibility that universality entails, with just the axioms of arithmetic.

The section dealing most directly with these matters in the NKS book is called "Implications for Mathematics and Its Foundations", and starts on page 772, running to page 821. There is extensive supporting material in the notes, both technical and historical. The notes from that section, and from the preceding section are also relevant. Those notes run from page 1136 to 1177.

http://www.wolframscience.com/nksonline/page-772
http://www.wolframscience.com/nksonline/page-1136d-text

A decent entry point might be Hilbert's tenth problem and the construction of universal diophantine equations. See the historical note on page 1161 -

http://www.wolframscience.com/nksonline/page-1161a-text

And the preceding section in the main text, particularly the specific equation on page 786, that emulates rule 110.

http://www.wolframscience.com/nksonline/page-786

See also the note on page 1160 that explains the construction -

http://www.wolframscience.com/nksonline/page-1160b-text

I hope this helps.

Posted by: Philip Ronald Dutton

Jason,

Thanks for keeping me on track.
You mentioned in your previous reply that, "The axiom of arithmetic that corresponds to looping in programs is induction. Logic is not universal because it does not have such an axiom, making it strictly finite."

My ambitious intuition compels me to explore how simple programs (algorithms) can augment the structure of Logic.

It just seems very natural. I know I have not read enough about Logic, formal systems, etc. But, surely, somehow, an algorithm fits right into Logic?

Or, maybe, Logic rests in the nest of algorithmic __ether___?
Not sure the proper word!

Finally,
Okay so there is nothing in the core of Logic which resembles an algorithm but we use algorithms to compute Logic conclusions? If some kind of simple program (algorithm) was used to augment the core elements of Logic then would there be the associated risks of some kind of self-reference? (self reference because an algorithm would be a new core foundation but logical deductions and etc. would still require algorithmic process?).

I think the fruits of Logical conclusions can not exist without the algorithm process.

Thanks for putting up with my stubborn explorative mistakes!

Posted by: Jason Cawley

Logic is a particular case of an axiom system. Axiom systems are not directly equivalent to algorithms, but there are considerable cross relations between them. An algorithm typically tells you exactly what to do next. In an axiom system, there are a set of rules, and one asks e.g. whether a given statement can be traced to some subset of those rules using only those rules. In common speech we ask whether it "follows from" the axioms or rules. Which means, is there a path of steps allowed by the rules, from any of the rules, to the statement in question? This can be examined as a kind of multiway system.

For where universality comes in, see page 784 -

http://www.wolframscience.com/nksonline/page-784

Also relevant are the notes starting at "Axiom systems" on page 1150, and the following notes on Basic Logic and Predicate Logic. The next note covers Arithmetic. Just start on 1150 and read through them.

http://www.wolframscience.com/nksonline/page-1150

The NKS book eventually gets some impressive results on logic, including the shortest axiom for basic logic (given on page 808, with the proof it implies all of logic on pages 810-811), and enumerated logical theorems with those well enough known to have acquired names and receive textbook attention picked out (on page 817)

http://www.wolframscience.com/nksonline/page-808

http://www.wolframscience.com/nksonline/page-810

http://www.wolframscience.com/nksonline/page-817

Basic logic is in a sense fundamentally simpler than general recursive algorithms. You can put in all possible true and false values for all variables in a given expression, and just work out whether the proposition is always true or depends on some of those truth values. To be a theorem in logic, it has to always be true - a provable tautology. If instead it depends on some of the truth values, it counts as an "empirical" proposition or a claim about some state of affairs.

The ability to apply this finite, if sometimes involved, procedure, means that the particular sort of intractability that arises in more complicated systems does not yet appear. But proofs even in basic logic can get pretty involved. As the example on pages 810-811 (above) shows. In practice, it takes automated theorem proving software to handle such things.

Godel proved the consistency of pure predicate logic - a generalization of basic logic in which terms like "for every" and "there exists" are allowed - in 1930, in what is usually called his completeness theorem. Everyone has heard of his incompleteness theorem, which is about arithmetic. The preceding paper showed the same is not true in just pure predicate logic i.e. if a statement in pure predicate logic is true for all possible truth values of its variables, and all possible forms of predicates, then it can always be proved that it follows from the axioms of pure predicate logic. Thus, it is either a tautology, or there are possible values of its variables for which it isn't true.

When you go up to Peano arithmetic instead, as the axiom system used, this is no longer true, and instead there are propositions that can't be proven or disproven just from the axioms. Arithmetic is across the threshold of universality. Cardinality issues can still come up (continuum infinities and set theory are "bigger", if you like), but complexity is already there, undecidability, etc.

I should probably also say that one can of course look at the evolution of a CA or other such algorithm, as a sequence of logical expressions, showing the dependency of the later steps on the previous ones. Any deterministic rule has this character - the next state has to be "deducible" from the preceding one. That is what we mean by it following a rule. So one can e.g. write out boolean logic expressions for the 1st, 2nd, 3rd, etc steps in the evolution of a given CA rule from a given initial condition.

What one sees in the case of the complicated ones, is that such logical expressions blow up very fast. This just shows the dependence of later site values on "a lot", or track how much is going on, or how interconnected the behavior is. As an example of this, see the diagram on page 618, showing what happens to these boolean expressions in just five steps of CA evolution, for a simple or nested rule (the upper 2 cases) or for a class 3 rule like rule 30 (the bottom one). In the top cases you might say logical analysis gets us somewhere. Not so in the bottom case. We are much better off just simulating the rule i.e. using formal experiment.

http://www.wolframscience.com/nksonline/page-618

I hope this helps. It is a large topic, and there is nothing wrong with dipping a toe into it at a time. You don't have anything to apologize for, in other words.

Posted by: Philip Ronald Dutton

A large topic indeed!
(shame on my early education system
for not having introduced more logic,
axiom systems, etc.)

Jason,
You said previously the following:
"I should probably also say that one can of course look at the evolution of a CA or other such algorithm, as a sequence of logical expressions, showing the dependency of the later steps on the previous ones. Any deterministic rule has this character - the next state has to be "deducible" from the preceding one. That is what we mean by it following a rule. "

If an algorithm can be recast into a sequence of logical expressions then can a sequence of logical expressions be recast into an algorithm? I am sure the answer is yes. I have difficulty with this recasting process because you can not seperate the two completely. Or in other words: you can not recast for the sake of a particular analysis and then expect not to have to use that one (which you just dropped) within the analysis.

For example, if someone recasts an algorithm into logical sequences, then, the very act of proof analysis requires the logician to use or follow algorithms.

It seems like self-reference or inseperability. However, I can not understand the implications and I do not know if my thoughts were constructed correctly. Either way, it sounds like it relates to NKS and so I wanted to ask. Thanks!

Posted by: Jason Cawley

"If an algorithm can be recast into a sequence of logical expressions then can a sequence of logical expressions be recast into an algorithm? I am sure the answer is yes."

In a general enough sense of "algorithm", sure. A sequence of logical expressions is a piece of logic if each step is related to the preceding, by use of one of the axioms, or some result previously proved to be consistent with the axioms. Otherwise, it can still be a sequence of logical expressions, but it is not a valid piece of logical reasoning. It may e.g. introduce a new fact, though, that is allowed, but isn't logical reasoning per se.

Let's restrict ourselves away from the generality "sequence of logical expressions", to the case where the sequence really is a piece of logical reasoning. Then each subsequent step is an application of one of the axioms of logic to the prior expression - or the application of a logical theorem already established (we say, "a lemma").

Lemmas can in turn be reduced to applications of the axioms. But any number of them, in any order. Lemmas complicate the issue, because in effect they increase the number of allowed transformations. Those are reducible to allowed transformations of the axioms, but not to just one of them. They "compress".

One can consider a piece of "primitive" logical reasoning, X. Define that as one in which each step is taken directly according to one of the original axioms - which we will purposefully "decompactify", trying to make each as simple an operation as possible. (From a compact axiom we would have to use lots of lemmas to prove anything. I mean, starting from those you'd have to deduce things you use all the time, like associativity etc).

When otherwise you'd use a lemma, you just do each step used in the lemma to each relevant part of the expression, in sequence. Then we are considering a sequence of logical expressions with the additional characteristic, that each subsequent step is an application of one and only one of the original axoims. (X is a piece of valid logic. Not all pieces of valid logic are like X).

Ok, all those distractions cleared away, we can see the basic issue, what is basically different than the usual algorithm case. At each step we have a choice of which axiom to apply. Application of any axiom to a logical expression will generate a new logical expression. Each one different, in general. From logical expression A0, we can apply the first axiom and go to A1, or the second and go to A2, or the third and go to A3, etc. Then at the next step we have the same sort of choice. So there are A11, A12, A13, A21, A22, A23, etc. Lots of possible sequences of application. Some of them will come to the same proposition, the same logical expression. Others will generate new ones not hit along any of the other lines.

So it is like a multiway system. But the sequence of logical expressions we are initially given, is just one of them. It is one possible path through a multiway system, algorithmically speaking. A multiway system "goes to" "all of them", so it is not quite the same. When on the other hand we have a typical "one valued" algorithm, like a CA, the next step is fully specified by the first. There isn't a choice of which rule to apply at each step. There is only one. (One can relax this and get something besides a classic CA - as was looked at in the thread, "CAs with global control").

So that handles the logic to algorithm relation.

But let's look at the more general case a second, where all we have is a sequence of logical expressions. The point is to see that both saying something is a piece of logic, and saying it comes from an algorithm, are saying something, that they don't need to be true.

Can any sequence of logical expressions be considered an algorithm, ignoring the rules of logic, just looking at the sequence as an explicit set of transformation rules? One step can be. That is, one can say

(a.b)v(c.d) -> (c)v(b)

without reading in any meaning to the symbols whatever. It is just a transformation rule. It says, "if you see this (lhs), replace it by this (rhs) at the next step". And one can look at any sequence of logical expressions as being a sequence of such transformation rules. But are they the same ones, or in any way related to each other, from one step to the next? If they aren't, then we wouldn't really call them an algorithm, taken together.

We might say each one was, a single step of a different one each time. If there is some sense in which they are a repeated application of the same transformation rule or rules, then we would typically call them an algorithm. But just an arbitrary table of arbitrary rules, "at step 1, do hhggjh->hjkekl, at step 2 do hjkekl->jeiuj, ..." we wouldn't call an "algorithm". It is just restating the sequence of logical expressions, itself.

A rule has to be used more than once, somewhere. A rule that only ever applies once, is only "sort of" a rule. The concept of a rule involves the idea of an invariable doing of something; there have to be varied things this invariable doing happens to, to consider it a rule, proper.

You might notice a set of rules being repeatedly applied, within the sequence of expressions, without being given that beforehand - but there is no assurance there is one, if all you are given is a sequence of logical expressions. They might have nothing to do with each other, and be a "sequence" in name only.

avb = ! c.d
j.h.t.r => o v h
...

Posted by: ahautot

[QUOTE]Originally posted by Jason Cawley
[B]Arithmetic is already universal. That is what allows the metamathematical construction that encodes any proposition into some proposition of arithmetic. The axiom of arithmetic that corresponds to looping in programs is induction. Logic is not universal because it does not have such an axiom, making it strictly finite.

Jason,
Two short correlated questions :
1) It is not immediately apparent (to me) where the induction axiom is hidden in the axioms list for group theory given page 773. Equivalently it is not evident how to emulate arithmetic in the frame of elementary group theory (including first order logic).

2) Universality (in the Godel sense) certainly implies undecidability and even Essentially syntactic incompleteness (which is stronger). What about the converse?

Connecting 1 & 2 the single thing I am sure to know is that Tarski has proved that group theory is undecidable.

Thanks for enlightenments.

Posted by: Jason Cawley

Yes, Tarski showed that group theory is universal, by the same reasoning and at the same time he showed it is undecidable. Both follow from his demonstration that any proposition in Peano arithmetic can be encoded as a proposition in group theory, which he showed in 1946, and is the basis of your correct statement that he showed group theory is undecidable.

The note entitled Algebraic Axioms starting on page 1159 discusses this in some detail, and how things differ in restrictions or special cases (like commutative group theory) rather than general group theory. (Note also that Tarski relied on having logic too - see the end of the note for the case of group theory without the logic axioms as well).

As for your second question, whether undecidability implies universality, in general it need not. Systems of so called "intermediate degree" are examples, and can exhibit formal undecidability without being themselves capable of universal computation. Wolfram discusses this briefly in the main text on page 734. The note entitled Intermediate Degrees on page 1130 discusses this is greater detail, and specifically credits a 1956 result by Friedberg and Muchnik for establishing this (by constructing a counterexample). Formally, universality implies undecidability but undecidability need not imply universality, or undecidability is a necessary but not a sufficient indicator of universality.

Wolfram argues in that note that essentially all known cases of intermediate degrees are based on some underlying universal system, with parts "turned off" or ignored externally to prove non-universality. But that is a debatable proposition. Just how important "intermediate degrees" might be for natural systems and the bearing of this on Wolfram's PCE conjecture, is an open question in NKS. Klaus Sutner has written a paper on intermediate degrees in CAs, and presented about the subject at the NKS 2004 conference. See the bibliography at wolframscience.com for details if you are interested.

Forum Sponsored by Wolfram Research

© 2004-2008 Wolfram Research, Inc. | Powered by vBulletin 2.3.0 © 2000-2002 Jelsoft Enterprises, Ltd. | Disclaimer
vB Easy Archive Final - Created by Xenon and modified/released by SkuZZy from the Job Openings