User lucas k. - MathOverflow

Can invariant of transitive reflexive closure in FOL+PA always been proven?

2010-10-28T19:54:45Z

I am trying to understand FOL + PA, better.

With FOL + PA I mean, first order logic, with addition and multiplication predicate and induction axiom scheme.

The book I am reading explains how to construct transitive reflexive closure with these predicates. By encoding the sequence using a prime number, that is larger than any of the numbers in the sequence.

However, it is not directly clear to me, that the invariant of this closure can be derived from the induction axiom scheme (it is also not explained in the book). If there is a predicate R(x,y), one wants to be able to prove that for any $\phi$:

$(\forall x,y:(\phi(x) ∧ R(x,y)) \to \phi(y)) \to (\forall x,y:(\phi(x) ∧ R^*(x,y)) \to \phi(y))$

It is not obvious to me that this is possible. For using induction, you need to number the values in the sequence. However, I doubt if there is already enough prove power to do so.

Does any have resources where this is detailed out? If such invariant is not possible, then FOL + PA constructed this way is crippled.

Lucas

Edit, here the definition as in the book of John Harrison:

$R^*(x,y) ::= \exists m, p, Q: primepow(p,Q) ∧ x < p ∧ y < p ∧$ $(\exists s: m = x + ps) ∧$

$(\exists r: r < Q ∧ m = r + Qy) ∧$

$\forall q: q < Q \to primepow(p,q) \to \exists r, a, b, s: m = r + q(a + p(b + ps)) ∧ r < q ∧ a < p ∧ b < p ∧ R(a,b)$

Answer by Lucas K. for Can invariant of transitive reflexive closure in FOL+PA always been proven?

2012-12-30T14:25:01Z

The answer can be found here:

http://www.staff.science.uu.nl/~ooste110/syllabi/peanomoeder.pdf

Most important part, theorem 1.9 ii.

With this theorem you can have some kind of sequence for which you can prove that the sequence can be extended. This proof is given in PA. With the sequences the remaining part is trivial.

The suggested book Shoenfield's "Mathematical Logic", doesn't provide the answer. It only gives the proof in informal mathematics, but not in PA. Which is required here. The informal mathematics assumes sequences you haven't available yet.

Is there a natural example of a second order proof that does not reduce to a first order proof in a straight forward way, if all variables are filled in?

2012-04-08T18:25:09Z

Dear all,

This is a retry of question Would Wiles proof of Fermat theorem reduce if you fill in the variables?. I stated that question badly, but my intention are genuine and hope do to a better job here.

First of all, with proof reduction I mean that there is a set of reduction rules (algorithm) that simplifies or alters a proof written in a formal logic. In such way, that the adapted proof will have a certain property after executing, for instance no higher order theorems, or no induction.

A normal mathematical proof is not likely to be reduced, because the mathematician did his best to have a minimum proof. However, if certain variables of the end theorem of the proof are replaced by constants, and this is substituted back over the proof, then a reduction algorithm may simplify such proof. Still, there is no guarantee that significant simplification can be performed on the proof.

Things get a little different when all variables of the end theorem are instantiated to constants, such that the end theorem is a quantifier free theorem. In that situation, ones hopes that the proof collapses and reduces to a trivial proof. This gives the mathematician confidence, that the end theorem is indeed correct (paradoxes have the property that they do not reduce).

If you do such reduction manually, then it often turns out not to be difficult. In case of induction, it can be unrolled if the n is known. However, to do this automated with an algorithm, is far from trivial. There is sequent calculus and cut-elimination and this is not simple.

Suppose there is a second order logic proof and the variables of the end theorem are replaced by constants and substituted back over the proof. For that, it would be nice to have an algorithm that reduces to proof to a trivial first order logic (+PA) proof.

However, it is impossible that we can prove in second order logic that such algorithm is guaranteed to give result. Because, falsum is a quantifier free formula, and by proving that the algorithm halts and gives result, we actually proof the relative consistency of second order logic to first order logic. Since, second order logic can prove the consistency of first order logic, it would mean that second order logic would prove its own consistency, which is not possible, unless it is inconsistent.

Still, the algorithm could exist (and in fact, if second order logic is consistent, it exists, by just searching for the theorem in first order logic), but you need a logic stronger than second order logic, to prove that the algorithm actually works.

Given above I expect (and maybe I am wrong here), that there are second order logical proof that do not reduce straight forward in a first order trivial proof, if all variables are filled in.

I am curious how those proofs look like and if there is a simple natural example (so, that is my question). Also if there is any literature in this area (in case I see it all wrong :-)

Regards,

Lucas

Would Wiles proof of Fermat's theorem reduce, if you fill in the variables?

2012-04-07T20:44:34Z

Hello all,

I have an interest in proof reduction. If in the final theorem of a proof, some variables are filled in, then the proof might be reduced to a simpler proof. If all variables are filled, then (often) the proof can fully reduced. I am interested in examples were proof reduction is not possible.

Suppose we would encode Wiles proof in a formal logic. Does the proof reduce if you fill in the values for $a$, $b$, $c$ and $n$?

Suppose we take $a = 11$, $b = 14$, $c = 16$, $n = 3$, then a fully reduced proof would look like this:

$0 \neq 21 \Rightarrow 4075 \neq 4096 \Rightarrow 11^3 + 13^3 \neq 16^3$

If it is not possible to reduce Wiles proof step by step with filled in values, why not?

I don't know much about Wiles proof, but my question is about logic and proof reduction. If you take the Four Color Theorem, then if you a particular planar graph, then you will end up with a graph that is colored with 4 colors.

Regards,

Lucas

How do you restrict the induction axiom in second (or higher) order logic?

2012-03-26T21:59:01Z

Dear all,

I am interested in reverse mathematics. The theory is that most of mathematics can be expressed and proven in ACA0, that is second order logic, with the induction axiom restricted.

However, maybe a stupid question, but how do you restrict the induction axiom in second order logic? If you have the successor function, then the natural numbers can be defined as the closure on that functions. From that definition, if I am not mistaken, the induction axiom follows. So, in fact you do not really have an induction axiom, but you just derive it.

But if it is not an axiom, how do you restrict it?

Regards,

Lucas

Is there any literature about inner-replacement rule?

2011-12-29T23:53:23Z

Hello all,

If you have a theorem $\vdash \alpha \rightarrow \beta$ and a theorem $\vdash \gamma$ then if $\alpha$ is a sub-expression of $\gamma$, and this sub-expression has an even number of negations within $\gamma$ (and it is not within a xor or boolean equality), then a new theorem can be obtained by replacing $\alpha$ with $\beta$ in $\vdash \gamma$.

Similar, if $\beta$ is a sub-expression of $\gamma$, and this has a odd number of negations, then a new theorem can be obtained by replacing $\beta$ with $\alpha$.

It is not so difficult to see that this is true, but has this rule a name? And is there any literature about it? If you introduce this rule, you can probably skip some axioms. Also, it is a more general form of modus pones.

The background of this question is, that one of my interests is how to do real mathematics in a formal logic. My opinion is that both sides should make steps to come closer to each other. Logicians should make logics that are more practical to use, and mathematicians should make proofs that are easier to formalize. I think above rule is quite natural for mathematicians, and can be verified by computer. At least when I am doing mathematics, I am well aware if a certain sub-expression is in a position that it can be weakened or strengthened. And I think that counts for all mathematicians.

With this rule you don't need the low-level proving with shifting assumptions in front of the $\vdash$ sign, to weaken or strengthen the sub-expression. This low-level shifting is a practice that in general can not be found in books of mathematics that do not deal with logic.

Regards,

Lucas

Program transformation as alternative for Hoare logic or temporal logic

2011-07-09T22:27:38Z

When trying to prove something about a program, the known techniques are Hoare logic and temporal logics.

An alternative is to transform a program in a mathematical (logical) expression. So, rather that mathematics is used to prove some properties of the program, the program itself is a piece of mathematics.

Loops become transitive reflexive closures. Example, if one has a program that calculates a Fibonacci number. If the program keeps the last two numbers of the Fibonacci sequence in variables, then this be converted by taking the transitive reflexive closure of the relation P, that is true (and only true) for the following situation:

$$ P((x,\space y, \space z), \space (x+1, \space z, \space y+z)) $$

In the original program, the right value is chosen within the loop. In the transitive reflexive closure, the right value must be selected outside the closure (loop). The transformed program is more like a non-deterministic program.

The transformation of a program in a logical expression, can be done automatically.

Although, this is not rocket science, I can not find any reference for this approach. I am busy with writing an article, where this is a part of (it is not the main subject). But I want to refer to the right articles and look if there is interesting material.

Does someone has interesting references?

Many thanks,

Lucas

Edit: Given the comment of Andreas, some clarification. The goal is to make formal reasoning about the program possible. So, transforming the program in a declarative language is insufficient, because the declarative language may not have means to make conclusions about a program, although the language itself might precisely defined. I was thinking in transforming the program in a FOL + PA expression. After such transformation, formal (that is why I tagged with lo.logic) reasoning can be done about the program. As far to my knowledge, I haven't seen this approach (the methods are always more in the direction of Hoare and temporal logics), although it is not very complicated. In my question I didn't want to restrict to FOL + PA.

Answer by Lucas K. for Are any natural examples of Gödel speed-up known?

2011-05-18T11:11:45Z

Take Goodstein's theorem for a particular n. The general case is not provable in PA. So, in higher order logic, the proof is of same length for every n. In PA the proof length grows when n becomes larger.

Can transfinite induction be defined as axiom scheme in FOL on bin-tree structures?

2010-08-11T18:21:52Z

Transfinite induction requires a second order induction hypothesis. So, that can not be defined as axiom scheme in FOL.

However, if I look to Goodstein's theorem en the Hydra games, then they have to do with tree structures.

Suppose we have in FOL a binary tree. This has an element 0 and a predicate that makes a pair P(x,y). We have the expected definitions on these tree like structures.

Now, is it possible to define an axiom scheme on this binary tree structure, that is strong enough for transfinite induction (to proof Goodstein's theorem)? Or, is a second order induction hypothesis always necessary, even when when we start to make schemes on tree structures? And why?

Lucas

Edit: I think my question was not fully clear yet.

If you have the natural numbers with the ordinals, you can make an axiom scheme as schoppenhauer suggests in the answer.

However, this requires definitions of ordinal. If you encode the ordinals in the natural numbers (using FOL + PA + addition and multiplication), you can not proof that these numbers are well ordered (I assume this base on the results of reverse mathematics). You need second order logic for that. So, the only option here is to define the ordinals as is and not base it on PA.

If we do so, we have defined the ordinals and the axiom scheme of transfinite induction and with that we should be able to prove Goodstein's theorem.

But, I am not so font on ordinals. So, my question is if it is possible to make a kind of induction axiom scheme on binary trees (instead of ordinal numbers), that is stronger than normal induction. FOL + these binary trees + binary tree induction axiom scheme, should be capable of proving Goodstein theorem.

I would like this, because I consider a binary tree as a much more simpler concept than ordinals.

I think this should be possible, based on the observation of the Hydra games which are based on Goodstein.

Answer by Lucas K. for "Simpler" statements equivalent to Con(PA) or Con(ZFC)?

2011-04-28T19:41:32Z

Maybe I understand the question wrong, but I think you should specify the logic in which the equivalence is proven. This is a little bit similar to relative consistency. Then you have three logics. The two logics that you compare and the logic in which you prove the relative consistency.

If your logic that proves the equivalence, can prove Con(PA), then the equivalent Turing machine is quite simple. Just a Turing machine that runs forever.

About the question itself. One reason why making a program that enumerates the theorems is hard, is because a logic is non-deterministic (you have choices in the axioms and inference rules you use) and a programming language (and a Turing machine) is deterministic. The task becomes much easier if you take a non-deterministic language.

To show that with a simple example. Take the last theorem of Fermat. To encode that as a halting problem, you have to diagonalize over a, b, c and n. This require some amount of coding. However, in a non-deterministic language, you just take a, b, c and n non-deterministic. A much simpler program.

Finally, the tricky part of programming the axioms and inference rules of a logic, is the variable substitution and the problem when variables are used multiple times. I think it should be possible to get fully rid of variables, which makes it easier to program, but less readable for humans.

Lucas

Answer by Lucas K. for Ask for recommendations for textbook on mathematical logic

2011-04-15T18:25:27Z

For really learning how to do mathematics in a formal logic, I suggest to look at one of the theorem provers and read their manual or tutorial. For instance, you can take a look at HOL-light.

My experience is that books about logic, fall short if it comes to the art of really doing mathematics in logic. You asked about examples. If you take a book about logic, you will probably not find an example of a proof of a well known theorem in a formal logic. However, you will find it in the manuals of the theorem provers.

For me, some things got a place, when I studied HOL-light.

Regards,

Lucas

Answer by Lucas K. for Writing "Semi-Formal" Proofs

2011-02-14T22:51:39Z

I suggest you take a look at the site of Freek Wiedijk:

http://www.cs.ru.nl/~freek/

He is a lot of papers about different formalizations. Also, some talks about 'proof sketches'. Set theory, is not the only formalization.

Also take a look at HOL light:

http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html

This formal logic, but not set theory, it is typed lambda calculus. It may inspire you for other ways of formalization than set theory.

Lucas

Reducing ACA₀ proof to First Order PA

2010-05-06T21:39:01Z

According to the Wikipedia ACA₀ is a conservative extension of First Order logic + PA.

http://en.wikipedia.org/wiki/Reverse_Mathematics

First of all I have a few questions about the proof:
a - What is the general sketch of this proof, is it based on models?
b - Consider the theorem that ACA₀ is a conservative extension of First Order + PA, and the proof of that theorem is proven in a formal system, what kind of logic is needed? If the proof is based on models, then it requires second order logic. However, the theorem itself is a ∏⁰₂ question as far as I understand, and can be expressed in First Order logic + PA. Is there also a proof in First Order logic + PA?

Then I am interested in the following:
c - Given an ACA₀ formal proof that ends in a theorem that is part of First Order logic + PA, is there an algorithm that reduces the ACA₀ proof to First Order + PA proof?

One could just do a breath first search on First Order logic + PA and given the fact that ACA₀ is a conservative extension, it is guaranteed to end. So, the answer to question c is definitely "yes", but I am looking for something more clever.

I am struggling with this algorithm for months. In general an ACA₀ proof, with a First Order + PA end theorem reduces rather easier. However, there are some non-trivial cases. If the answer to question b is "yes", then that proof might give hints for constructing the algorithm.

I want to use this algorithm to reduce proofs of full second order, such that the reduced proof is First Order logic + PA, or contains the use of the induction scheme with a second order induction hypothesis.

In many cases the use of second order induction hypothesis, can be reduced by using the "Constructive Omega Rule". I want to understand the limitations of this (if any).

Thanks in advance,

Lucas

Answer by Lucas K. for Are there any very hard unknots?

2011-01-27T22:50:15Z

The unknot on the Wikipedia doesn't seem trivial:

http://en.wikipedia.org/wiki/File:Thistlethwaite_unknot.svg

Lucas

Single logic foundation vs. multi-logic foundation

2011-01-24T20:43:42Z

Dear all,

I have always wondered why I have never read anything about this topic. My question is, are there are any books or articles covering this subject?

With this topic I mean the philosophical question, whether the foundation of mathematics consists of a single logic, or that it consists of multiple coexisting logics. If we compare it with programming languages, we see that multiple languages co-exist. One language is better in a certain domain than another, while this may not be true for another domain. There is no programming language that takes away the need of all others.

One could ask if this is the same with logics. That multiple logics co-exists. However, if you look at ZFC, then it is more an attempt to capture all in one logic. So, pursuing the idea of single logic foundation. While, more in the style of Hilbert's program, one starts with a simple logic (assembly) and then tries to build up other logics from there, so pursuing a multi-logic foundation.

Has there any serious discussion about this subject?

Regards,

Lucas

Is finitism an extreme form of constructivism?

2011-01-10T20:57:52Z

I hope this question is not too soft for MO.

The Wikipedia says about finitism that it is an extreme form of constructivism. See http://en.wikipedia.org/wiki/Finitism. I doubt that this is correct.

As I understand, there were different approaches to solve the crisis of the foundation of mathematics. One was constructivism, where there must be a witness of an object. Finitism was another approach were one (Hilbert) tried to give existing mathematics a foundation in finitism. But it was not a rejection of certain mathematical methods, just finding a foundation. Finally, the third approach was just adapting the logics, which led to ZFC and type-theory.

Hilbert opposed the intuitionism of Brouwer. So, it is a little bit strange to count them to the same family.

In more modern finitism, related to reverse mathematics, one tries to prove that a finitism result obtained by infinitism methods, has a finitism proof. This has many successes and it has been shown that this is at least true for large parts of mathematics. Again, this is not a rejection of infinitism methods, but just an attempt to find a better foundation. While, constructivism is really a rejection of certain arguments.

So, based on above arguments, I believe the statement in the Wikipedia is totally wrong.

Maybe someone has more historical knowledge than me? If I am right, I can try to correct the article.

Regards,

Lucas

Edit: Thanks for the answers. I agree with Mike Schulman that both can mean a variety of things. I do think that the article in the Wikipedia needs some rewriting. It might be the case that finitism is more strict, however, I think it is not a subset of constructivism by definition (after lots of reasoning, one might conclude that).

Answer by Lucas K. for What would you want to see at the Museum of Mathematics?

2010-12-26T16:40:36Z

Nothing. In a museum you put thing that are obsolete now. In mathematics nothing is obsolete (yet).

Answer by Lucas K. for How to prove Con(PA) in ZFC?

2010-12-22T18:26:28Z

You can also prove the consistency of PA with second order logic.

The key thing is that you need a higher order induction hypothesis. In first order logic + PA, the induction hypothesis are limited to first order expressions.

The strength of a logic is often determined by what you allow in the induction hypothesis.

logics restricted in arithmetic hierarchy

2010-11-23T21:42:13Z

Hello, I would like to know if this already has been researched.

There has been lot of research done, where logics are limited. They are often limited in the axioms or inference rules, which makes them weaker.

However, I am interested if someone has researched logics that are limited in arithmetic hierarchy. I am interested in a system that has only sentences of $\Pi^0_2$ .

Has someone worked that out?

Lucas

Answer by Lucas K. for Arguments against large cardinals

2010-10-29T20:04:09Z

Erinna, in your question you use the word 'exist'. In the philosophy of mathematics, that is a word that is part of discussion. If you follow a Plato philosophy, then there is a perfect mathematical universe, were all the objects 'exists'. Then you can talk about the existence of large cardinals. If you remove those objects from that universe, then that is probably considered a loss by many.

However, such philosophy has problems. The main problem is how this mathematical universe interacts with our daily world. Without such interaction, we can not access such universe. Of course, I have some personal opinions here, and one can have a long discussion.

In some philosophies one tries to have a more limited mathematics, with only mathematical objects with a clear meaning. In such philosophy, (large) cardinals are not part of that limited mathematics. However, that does not mean that other constructs are entirely rejected. They can still be mental constructs, or meta-mathematics. Constructs that can be used to do mathematics that has more clear meaning.

As said, with philosophy you can have lot of discussion and there are many views.

I think a better question is whether '(large) cardinals must be part of the fundamentals of mathematics'. I strongly say no to that question, although I do not object against (large) cardinals as mental construct.

Lucas

Answer by Lucas K. for What is Realistic Mathematics?

2010-08-10T22:18:50Z

This is more a philosophical question, and therefore hasn't a definite answer.

But if you want to make plausible that AC isn't realistic mathematics, you might reason something like the following:

There is a set of mathematical sentences, that has a direct (so, not indirect yet) relation with physics. Call this set B (of Basic). Personally, I think they are in the following four areas:

Computation
Probability
Geometry
Topology

Note, I count arithmetic as part of computation, since numbers are not a physical entity, but computation is. But, likely many people will disagree.

Also note, that the sentences in B, might be far simpler than the mathematical sentences suggested in your question or in one of the answers.

Now, we have more complex mathematical sentences, that are still "realistic", if they can be converted or "instantiated" to sentences of B. Call this extended set be E. These more complex sentences capture a higher principle, which can be powerful in the science of physics. Still, there is no direct link with physics, the mathematic sentence first needs to be instantiated, to make a direct link with physics. Example, any sentence with a real number, is not be part of B, because we can not observe real numbers in physics, but they can be part of E.

Consider that there is a sentence s1 ∈ E and s2 ∈ E. Furthermore, that s2 follows from s1, but with a rather difficult proof. Suppose there is a proposed axiom a, such that s1 + a leads more directly to s2 (a simpler proof). However, a ∉ E. So, axiom a is independent from sentences in B.

From above concept it follows that axioms can exist that are "useful", because they make proofs shorter, but have nevertheless no "meaning". I do believe that AC is such axiom.

About CH, I think it is not useful and not having a meaning.

But again, this is more an opinion.

Answer by Lucas K. for A decision problem in graph coloring

2010-07-09T23:43:30Z

Some thoughts.

I like the idea of inverting the graph. I think the problem can be converted, to coloring the (inverted) graph for which each color appears exactly twice, or just once but then only on selected vertices (a joker vertex).

If the original inverted graph contains a 3-clique, then one of the vertices of the clique can be selected and be allowed (but not necessarily) to be colored with a color not appearing anywhere else in the graph. You can repeat this step, until the graph does not contain any 3-clique anymore, that does not have a selected vertex. I think it is not difficult to prove that a coloring in the converted problem can be used to construct a coloring in the original problem and vice versa.

With the converted problem, you eliminate any vertex that has 1 or 2 edges. In case of 1 edge, you remove the vertex and its neighbor. In case of 2 edges, you contract. By contraction, you can create a new 3-clique. However, in the converted problem, you are not allowed to color that with one color (that is why the conversion is necessary, because it allows the contraction).

A cycle with an odd number of vertices, will end up in a single vertex, in which it becomes clear that a coloring is not possible. But not all impossible colorings will end up like that.

Finally, you can do a BFS. For the search-border, you have a set of possibilities. Each element of the set, specifies for every vertex on the border, whether it needs another vertex of the same color or not. You want the keep the search border small.

It might be NPC. For that, consider the vertices on the search-border as propositional variables and prove that any propositional expression can expressed as such graph (I don't know if that is possible).

Lucas

Answer by Lucas K. for What's your favorite equation, formula, identity or inequality?

2010-06-02T19:47:53Z

Bayes equations:

P(A|B) = P(A∩B)/P(B)

It is the basis of conditional probability.

Answer by Lucas K. for Can we color Z^+ with n colors such that a, 2a, ..., na all have different colors for all a?

2010-05-30T10:43:59Z

I suggested in a comment, to look for colorings that are the same for each a, except for a fixed permutation.

Suppose the colors are given by function c(x), for x ≥ 1. And a permutation function p(i,j), where i,j ∈ [1..n]. Where i is the index of the permutation, and j the index of the permutation of the color.

If n = 4 and the coloring starts with abcd, then p(1,1) = a, p(1,2) = b, p(1,3) = c, p(1,4) = d, p(2,1) = b, p(2,2) = d.

If the coloring is the same for each a, then we get the following equation:

c(an) = p(c(a),c(n))

It is more important to give a condition when the above condition is met.

Lemma 1: If p(x,y) is reflexive (p(x,y)=p(y,x)) and associative (p(x,p(y,z))=p(p(x,y),z)) and p(x,y)=p(1,xy) for xy ≤ n, then a coloring can be constructed.

Lemma 2: For each n a permutation exists such that it reflexive and associative and for p(x,y)=p(1,xy) for xy ≤ n.

To see how this works, for n = 4, we start the following permutation matrix:
abcd
bd..
c...
d...

Fill in the second row:
abcd
bdac
ca..
dc..

And complete it:
abcd
bdac
cadb
dcba

From this construct the coloring: abcdxaxcdxxbxxxa

By each prime number a > n (the x values in the coloring), you can choose a color for c(a), but you have to continue with the permutation of that color for c(ma).

Lemma 1 is trivial to prove, because the associative and reflexive conditions makes that reaching a number by different values of a, factoring the number and re-arranging makes that it must have the same value. For the values xy ≤ n, you can't factor anymore, and the condition must just met.

I haven't proven lemma 2 fully. A permutation matrix with reflexive and associative conditions, can be constructed by starting with 1 permutation that has a single cycle. The full matrix can be constructed by applying this permutation multiple times, up to n. It can be proven, that such matrix has the reflexive and associative condition, but not necessary the condition that p(x,y)=p(1,xy) for xy ≤ n;

The solution of François as matrix looks like this:
abcdef
bdface
cfbead
daebfc
ecafdb
fedcba

The permutation from first row to second row is not a permutation with a single cycle. It brings you from row 1, to row 2 to row 4, back to row 1. However, this can still be categorized as 1 cycle permutation, because the permutation from first row to third row, is a permutation with a single cycle.

Instead of looking at the permutation per color, it is better to look which colors are passed, when the permutation is applied multiple times. In above example the cycle is (first row to third row) a->c->b->f->d->e->a.

If we just make the second row a permutation with one cycle, then the cycle starts with: 1->2->4->8->16->32->64 etc. Then we can add 3 and the other primes.

For n = 27 we can get:
1->2->4->8->16->3->6->12->24->x->9->18->5->10->20->27->x->15->7->14->11->22->x->21->25->13->26->1

In above sequence, multiplications with 2, have 1 step, multiplication with 3, 5 steps, multiplications with 5 have 12 steps. The remaining primes 17, 19, 23 can be placed on any of the x values. The short parts 11->22 and 13->26 can easily be exchanged. From this cycle, you can make a permutation and permutation matrix that has the condition that p(x,y) = p(1,xy) for xy ≤ n. From that permutation the coloring can be constructed.

As you can see, it is not very difficult to construct a coloring this way. But, the sequence is also rather crowded. It is not a prove yet that it is always possible.

Answer by Lucas K. for What are the most attractive Turing undecidable problems in mathematics?

2010-05-25T20:33:08Z

Not mentioned yet, that any computer language extended with non-deterministic features is also Turing computable.

This is interesting, because it allows the language to be simplified. If the programs operate on objects that are nil or a pair. Then you only need five instructions:

The constant nil
A pair operator
A sequence operator, that executes one code fragment after another
An inverse operator
A closure operator, which repeats a code fragment zero or multiple times

If you want to construct a piece code of that adds the two values of a pair, then first make something that construct (a - 1, b + 1) from (a, b). Then take the closure. This will generate (a - n, b + n). Finally, pick the value (0, c) and output c. This can be done by using the inverse operator on the pair and nil.

So, programming is a little bit odd, because you select the right value outside the loop (closure), rather than inside the loop, as in deterministic languages. The advantages is the much more simpler structure. No variables, no recursion, no matching operators (just use the inverse) and no control-structures, except closure.

This makes it a little bit between programming and mathematics. The simpler structure, allows easier mathematical reasoning. So, it might be an idea to convert a program in a deterministic language, to a program of a simplified non-deterministic language, before doing any mathematics on the program.

Lucas

Answer by Lucas K. for What are the most attractive Turing undecidable problems in mathematics?

2010-05-24T19:59:16Z

The rule 110 is also a cute one.

Can Goodstein's theorem been proven with first order PA + Constructive Omega Rule?

2010-05-20T21:43:24Z

I am trying to understand transfinite induction and Gentzen's theories.

But I was wondering, if there is any connection with the Constructive Omega Rule (COR).

With COR I mean that if you can proof:

φ(x)

for every x in fully axiomatized system defined within your PA + COR system, then you may conclude:

∀ x.φ(x)

My question: Is it possible to prove Goodstein's theorem with PA + COR?

Or in general, has COR the same strength as transfinite induction or is it something entirely different (then I want to understand the difference).

Regards,

Lucas

Given the responses, some clarification of the rule is necessary. The referred article gives a rather good description of the rule I mean.

However, I do mean a rule that can actually be implemented. So, if there is a computable function that generates a PA proof A(n) for each n, then it is necessary to show in the meta-system (PA + COR), that this function terminates for each n.

Only then, the constructive omega rule (at least my variant), as additional inference rule, can be used to conclude ∀ n.A(n) in the PA + COR system.

Some second order proofs, with a first order final theorem can also be proven with first order PA + COR. Since, the Goodstein theorem is a second order proof with first order final theorem, I was curious of it is one of them.

Answer by Lucas K. for Remove unnecessary dependencies in a task graph?

2010-05-18T22:26:40Z

For each vertex x, make a set that contain each vertex y that can reach x. This sets also includes x.

If you have two edges b -> a and c -> a, then if the set associated with b is a subset of the set associated with c, then the edge b -> a can be removed.

Example:

a -> b
b -> c
a -> c

The set are:
a: { a }
b: { a, b } // Can be reached from a and b
c: { a, b, c}

If you look at the edges:
b -> c
a -> c

Then you see that the set of a is a subset of b. So, the edge a -> c can be removed.

Lucas

Answer by Lucas K. for What is the reverse mathematics of first-order logic and propositional logic?

2010-05-16T11:03:06Z

First of all, there is a difference between 'strength' and 'expressiveness'. This is not always unambiguous used in articles and literature.

With 'strength' is usually meant the possibility of a system to proof certain sentences. When comparing two systems for strength, one can limit the comparison to a certain subset of sentences.

Considering your question, I do think that you mean 'expressiveness'.

If you have first order logic + induction scheme + definitions for addition and multiplication, you can express any problem of discrete mathematics.

You need to build a 'pairing' construction and a 'transitive reflexive closure' construction. With those two, you can do anything. With some tricks with addition and multiplication, you can construct both.

You can also opt to start with a pairing operator and closure, and construct addition and multiplication from that.

If you have higher order logic, you don't need the addition and multiplication, because higher order logic allows the construction of pairing and closure in a different way.

So, I think the answer to your question is that you can codify all logics (with finite sentences) with First Order PA (or the question is not clear).

When talking about strength. First order PA + addition + multiplication, can't prove the consistency of itself. You need second order logic, with the ability to have second order formulas as induction hypothesis to prove consistency of first order logic + PA.

Lucas

Answer by Lucas K. for Would Euler's proofs get published in a modern math Journal, especially considering his treatment of the Infinite?

2010-05-13T12:00:56Z

I learned in my science history lessons, that the standards for mathematics varied over time.

In the ancient Greek time (let say, the period of Archimedes), it was preferred that a theorem had more than one proof. At least, it was not uncommon to give more than one proof.

So, one can argue, that current math articles would not be accepted by the well respected Archimedes.

I don't know the details, but don't assume that the standards of rigour were monotonic increasing over time.

Lucas

Comment by Lucas K.

2013-01-20T19:53:22Z

Access to the book again. The problem is that the first lemma of 6.4 is a lemma that can not be expressed as a lemma in FOL+PA (therefore not formally proven). If you want something that can be expressed in FOL+PA, one should have a sequence like construction, where you prove that the sequence can be extended with a new element. Such as theorem 1.9ii of the piece of Jaap van Oosten. Consequence is that Shoenfield only proves informally that certain functions are recursive, but is insufficient shown that recursiveability is provable in PA. I don't know if any theorems in the book depend on it.

Comment by Lucas K.

2013-01-19T23:46:06Z

If the answer is yes, then the next question is if it is NPC.

Comment by Lucas K.

2013-01-19T23:28:51Z

I agree with you that a fully formal proof would make a book unreadable (although, in these times you can put it on the internet and give a reference in the book :-). However, one can adopt a style of writing, where it is very clear how theorems (so, not proofs) could be writtten formaly. The referenced piece of Jaap van Oosten follows this style, and leaves many proofs to the reader (which I consider okay). The Shoenfield book doesn't follow this style. The sequences pop up in informal mathematics, without proper link to the formal part.

Comment by Lucas K.

2013-01-19T23:15:56Z

Note, that the proof is not required for the remaining part of the book. It is necessary to show that you can do basic mathematics (whatever that is) in FOL+PA. The book only addresses that FOL+PA can define certain things, such as computable functions. Still, I consider it an omission. My question popped up, because I was looking at rather simple systems where you could do some real mathematics, without the complexity of ZFC or type theory. If you start with a closure operator and a successor operator, you don't need the + and x of PA and it is a better prequal to 2nd order logic.

Comment by Lucas K.

2013-01-19T23:08:41Z

Andreas, I don't have the book by hand, because I am typing from a different location. But I do not agree with you that the proof was designed to be easily formalizable. The informal proof starts with an sequence. In the formal part, you are just trying to prove the basic properties of sequence. So, that is a no go. If you look to the reference I gave of Jaap van Oosten, you will see that the proof contains several non trivial induction step. You need to prove that a sequence can be extended. This is not trivial, when it is encoded with prime number, because you need to choose a new one.

Comment by Lucas K.

2013-01-08T21:46:23Z

@Andrew, although it is often mentioned that PA or PRA suffices, it is very hard to find the right material that tells how. There are some tricks to go from numbers to more complex datastructures and proves of that. Loops in programs can be rather easily expressed in closures. But, then you need the basic properties of closures. See for a detailed build of theorems: staff.science.uu.nl/~ooste110/syllabi/…

Comment by Lucas K.

2012-12-30T14:36:01Z

There is always the problem with probabilistic or statistical methods, that you may not ignore knowledge. In mathematical proof you may ignore info, that you don't need. If value c is determined, but someone comes with a good argument that the c is incorrect in this particular case, then you may not ignore that argument. That makes any answer obtained by this method, instable due to future knowledge.

Comment by Lucas K.

2012-04-10T20:37:53Z

Henry, thanks for pointing this out. I mean second order logic as in reverse math. So, where functions and predicates are just objects and with full comprehension principle. For my question it is only relevant, that we have a stronger logic that FOL + PA, that is capable of proving the consistency of FOL + PA. As far I know (but I could be wrong), second order logic in the sense of reverse math, is capable of that. For any consistent system that is capable of proving consistency of FOL + PA, it is not possible to prove relative consistency in that system. So, why does that proof fail?

Comment by Lucas K.

2012-04-10T20:32:07Z

Schoppenhauer, thanks for the answer. But this is not exactly what I was looking for. You extend the second order logic with additional axioms. But, I just want, without extending the logic, a theorem in second order logic, for which the proof does not reduce to a trivial first order logic theorem, when all variables are filled in. As I explained in my question, I think such theorem must exists, because if it does not exist the logic could prove its own consistency.

Comment by Lucas K.

2012-04-08T21:18:11Z

Neil, thanks for answer. I have learned some HOL-light. HOL, Isabelle and Coq (I don't know Agda), are type theory, I thought it would be simpler to restrict it to second order logic. If I indeed want to make such algorithm, then you are right that I need to be more specific. However, in general I can say, that such algorithm won't work, because it would ultimo mean that the logic could prove it's own consistency if it can prove the termination of the algorithm. Since, I can do these things manually, I don't understand which cases are intrinsically hard. I think these cases are in all sys.

Comment by Lucas K.

2012-04-08T21:02:48Z

Noah, thanks for reading my question. With 'proof' I mean the whole derivation tree of a theorem. For second order logic, I mean a logic where I can quantify over functions or predicates. I don't know what you mean that second-order logic has no good proof system. At least I can say, in informal mathematics, a proof that requires quantification over functions or predicates. For the proof reduction, it is difficult to be more clear, because I failed to make the precise algorithm. It is an attempt to automate the things I can do manually, but I want to understand better, why I failed.

Comment by Lucas K.

2012-04-07T23:33:28Z

I think you are right. My question is to vague. Particular, I am interested in reducing second order logic proofs, to first order proofs (FOL + PA), if you fill in all variables of the last theorem and do that over the whole proof. So, I want to end up with a FOL + PA proof. In case not all variables are filled in, then it is clearly not possible (for instance with Goodstein's theorem). I want to better understand where reduction of a proof is problematic and not that trivial, such that we need a stronger system than second order logic, to prove that reduction is possible.

Comment by Lucas K.

2012-04-07T23:11:17Z

But if so, how can you be sure that the reduction of FLT would work, if we know that we can not prove that the reduction is guaranteed to be working? As said in an earlier posting, I am interested in a natural example where this reduction is not working, when filling in variable to eliminate all quantifiers? Maybe it was better not to start this with FLT.

Comment by Lucas K.

2012-04-07T22:42:16Z

Note, my question is not really about FLT, it is just an example. You answer my question with your last sentence. But are you sure it works like that? Because, suppoes you have a proof of falsum in second order logic. If we can proof that such proof can be reduced to a proof of falsum in first order logic, then we can proof the relative consistentcy of those systems. This however, would lead to a paradox. So, I am trying to understand where things goes wrong.

Comment by Lucas K.

2012-04-07T22:09:20Z

I am not talking about reducing the theorem, but the proof. You must fill in the variables over the whole proof. In sequent calculus, you can then reduce the proof. In case of induction, you can unroll the induction, if n is known. Still there are reason why reducing is not always possible, otherwise you would be able to proof relative consistentcy between first en second order logic, in a not higher order logic. But i can't see why it fails in practice.