You can't reduce TM to propositional logic, which is essentially what you're proposing.

You'd need either to add recursion or a jump instruction with variables and sequences of formulae. See: http://math.stackexchange.com/questions/348379/why-is-propositional-logic-not-turing-complete

However, such a definition has been given by Bruno Poizat in his book called "Les petits cailloux - un approche model-theorique a l'algorithmie" (in french), which is the "bible" of the unit-cost complexity theory. Poizat makes a definition of P vs NP for all algebraic structures, and proves that for the structure ({0,1}, V, /\, -) one gets back the classical P vs NP problem. The problem is as follows: is there a polynomial p(n) such that, given a boolean circuit C(x*, y*) of size n (here x* and y* are tuples of boolean variables) there is a boolean circuit S(x*) of size bounded by p(n) such that 

"exists y* C(x*, y*) = 1 " S(x*) = 1

If for all C one has an S with |S| < p(|C|) with this property, then P = NP in a non-uniform way. If moreover, one has an algorithm to construct such an S given any C, then P = NP.

Well, Poizat has written much more in model theory and has an own philosophy to always write in french. This makes him less known in complexity. However, all statements made before are rigorously proven in his book, and much more. The book is easy to read and I recommend it. See here:

http://www.decitre.fr/livres/les-petits-cailloux-9782908016581.html

Explanation: "Nur al-Mantiq wal-Ma'rifah" is the own collection of books of the author. Other books by him, like "Course in Model Theory" and "Les groups stables" appeared also in this collection. The guy has been professor at the university Lyon 1.

Consider a SAT formula in CNF form (conjunction of distinctions) , i.e. (x1 OR x2 OR ...  OR xk ) AND  ... AND (  xl OR xl+1 OR ... OR xm ) . 

As you mention, due to the NAND gate universality, we can use De Morgan's law to convert OR to NAND gates ( x1 OR x2 ) = NOT(x1) NAND NOT(x2) and any negations of literals can be dealt as usual in the NAND case: NOT(x) = x NAND x . This is a polynomial time algorithm in the size of the formula, thus a reduction to a new problem, let's call it NAND-SAT, which is also NP-complete.

Now, you mention you require this to count cycles, I suppose from the context to calculate the unit-cost complexity of an algorithm that solves this problem. However, the above simply rewrote the problem in a different way, not achieving much or giving us new tools that we couldn't use before. Furthermore, as you mention, at least from a non-asymptotic point of view, counting unit steps is irrelevant: To compare P and NP, polynomial time reductions suffice since they are weaker than the smaller class (P). Thus, if an algorithm exists that solves SAT in polynomial unit cost, there is one that also solves SAT in polynomial time in the usual asymptotic model, perhaps with a small loss in the precision of measurement that is insignificant. Furthermore, it is likely that this gain would be only asymptotical in nature, thus we can use standard techniques summarized in the speedup theorem (http://en.wikipedia.org/wiki/Linear_speedup_theorem), which allows to bring the complexity from O(nk) to c nk + n + 2. for any c.

For the reasons above and given the restrictions imposed to the algorithm design of such an algorithm but not to its complexity (since it is poly-time equivalent to the usual case), complexity theorists do not usually use such a form when dealing with SAT.

I love the comments on SAT (they're really informative), but we must remember that SAT is a problem, not an algorithm.  The question pertains to models of computation, and Pedro did a sufficient job answering the question in an informative manner.  I also think Peter also did a good job on emphasizing the differences between TMs, DFAs, and circuits.  The answers are all informative, but I just wanted to emphasize the first answer seeing as it is fundamental to understand the TMs can't be reduced to PL.  On a somewhat unrelated note, TMs are far more interesting to compare with 2nd order predicate calculus (seeing as the incompleteness results are analogous to the undecidability results for TMs), but it is important to distinguish though their logical limitations are both the same, one is a model of computation that underpins how we understand the computability of problems.  It would be fascinating if you could get TMs down to PL (but that just doesn't work as emphasized before).  

I emphasize that in Poizat proof a polynomial time decision TM is not equivalent to a circuit, but to a (recursive) sequence of circuits n --> C_n such that size (C_n) grows polynomially. There is a(nother) TM computing the circuit C_n (better said, the recursive mapping n ---> C_n). There is no reason to down-vote. (if this has been the reason, over all).

To add to Peter's answer, remember that this is a Q&A area.  People post questions and people are answering them.  Some may downvote (like myself, in all honesty) because somebody already answered the question and others have done a decent job of supplementing that answer.  I apologize if you feel offended by people down-voting your comments.  It is not against your research at all.  Since this is a Q&A area, I would love to see it be easier to access for other researchers so they get the answer the OP wants.  That is more than a sound reason to down-vote a response in such an area.  For example, me wasting answer space by acknowledging this could be down-voted since it is not relevant to the thread (just me pointing out things).

I hope this helps!  I greatly apologize.

@ Peter

Nothing about potential infinite memory in Poizat's unit-cost model. The sequence of circuits I was speaking about represent only the way a decision TM works. Inputs of length n go into the circuit C_n, which is of polynomial size, | C_n | < p(n). The sequence of circuits is computed in polynomial time by another  (finite, clasical) Turing machine. Nothing about infinite memory. It is a normation of the problem: read the length of the input, create the polynomial size decision circuit for this length, and handle the input using the circuit. by the way, those "circuits" are acyclic directed graphs, and the nodes are gates which perform operations. "Decision" means that here is only one output gate, which is boolean.

It is possible that you think, Poizat was working with RAM's. (random access machines) with infinite memory. No, he is not. 

If you think, Poizat needs infinite memory to save a real number: no, he does't. Unit cost means that the real number take only one memory position and is handled in a unit of time. This is the convention.

@ Daniel

I was not offended that someone came and downvoted all the answers. I have just supposed that the person did it without completely understanding the positions and answers he was downvoting. Fairly, the initial question was not really clear and there were some different ways to understand it. Don't you think? 

@ Peter

Right, TM has a potentially infinite memory. But if it is a polynomial time machine, for inputs of length n (n cells, say at the begining) it makes at most p(n) steps so it uses at most p(n) many cells, to finally arrive in an accepting or rejecting final state (or to stop after writing an accepting or a rejecting character...). The normation in (1) machine constructing a circuit of polynomial size in n with n input gates and one output gate (one and the same for all inputs of length n) and (2) the circuit handling the input - has been done in order to generalize the P vs NP problem for arbitrary algebraic structures. In this model, the original machine is a many-tape machine able to keep in cells name of elements of the given algebraic structure (for example real numbers...), every tape has a read-write head, and the operations are like "if x_i = x_k and you are in state r, let x_j = x_u + x_v, go in state q, and move all the heads a step to the right", etc. So the machine can verify relations in the algebraic structure, can perform operations in the algebraic structures, can be deterministic or not. There are two ways of being non-determinist: to go in a state from a finite set, or to guess an element of the algebraic structure... However, the normation in the two steps (construct the circuit for inputs of given length with a classical TM and then perform operations of the structure using the circuit) was a good prerequisite in handling the general setting described above. The surprize was that this setting, applied to the boolean algebra with two elements, gives much insight even in the classical P vs NP problem. I hope that these explanations were better than those given before... 

Why is "polynomial time" being used to describe cycles?  I thought the basis of PvNP was in cycles, not time.

Peter,

Thanks.  Do you follow Stephen Wolfram on a NKS?

Also, for the Traveller in the Twin Paradox, he comes back to his computer after a high speed flight and sees: little time = many cycles.  That would seem to make number of cycles more basic than time.

In other words, one can use Relativity to shorten time, but cycles are constant.

So, using the Lorentz Factor, I can make P = NP (in time) by travelling at a Relativistic velocity which yields a gamma that is the ratio of the number of cycles for the NP-scaling algorithm versus the short cut, hypothetical, and ingenious P-scaling  algorithm.  That method works in time but not in cycles.

See: http://youvan.com/Genetic%20Coding%20Algorithms%20for%20Engineering%20Membrane%20Proteins/Genetic%20Coding%20Algorithms%20for%20Engineering%20Membrane%20Proteins.docx

The joke is on me!

Doug