What is partial fixed point logic?
---

Partial fixed point logic is a first order logic.  First order logic is also known as predicate calculus with a flow like "if x..then y..." or "There exists x such that x is Socrates and X is a man".  First order logic is very similar to propositional logic but has the addition of a quantifier.  Partial fixed point rewards TML with the benefits of being both sound and compete.

> Soundness is among the most fundamental properties of mathematical logic. The soundness property provides the initial reason for counting a logical system as desirable. The completeness property means that every validity (truth) is provable. Together they imply that all and only validities are provable.

**Clarification**

First order logic is typically [undecidable](http://kilby.stanford.edu/~rvg/154/handouts/fol.html), so the validity of my previous statement cannot be guaranteed. For the clearest possible understanding, watch this lecture by professor Dawar: 

https://www.youtube.com/watch?v=taUMcGbO4Oo

Decidable Fragments of First-Order and Fixed-Point Logic discusses this and we also know from Church and Turing that first order logic is undecidable. 

Datalog as an example of a programming language using first order logic
----

If we take a look at datalog we can get an idea of what capabilities Tau Meta Language under partial fixed point logic must have. Datalog is a deductive database language which is a synatic subset of Prolog. Datalog which is based on least fixed point logic is considered a [domain specific language](https://en.wikipedia.org/wiki/Domain-specific_language) because it is NOT Turing Complete. It is a language used primarily for Query Resolution purposes. Yet Query Evaluation is sound and complete with Datalog, and so we can at least get a good idea of what that means by looking at Datalog even though TML takes things a step further.

Conclusion
----
- Partial fixed point logic is first order logic. 
- This logic is similar to what we see from logic behind the language called Datalog. 
- In that using this logic we can create a language which on finite rather than infinite sets is guaranteed to terminate (no halting problem) on finite machines.
 - Not Turing complete. 
- Due to it being based on first order logic and specifically if based on partial fixed point first order logic, then we get the rewards of having soundness and completeness.

So we now know the features Tau Meta Language using partial fixed point logic will have. We know that this TML being multi-logic can give us the security guarantees not available anywhere else (not Ethereum, Tezos, or EOS). We know also that partial fixed point logic is P-SPACE based on an understanding of "descriptive complexity".  In specific, FO is the complexity class associated with formulas of first order logic and so this complexity class is relevant to Tau Meta Language utilizing partial fixed point logic.

> Restricting predicates to be from a set X yields a smaller class FO[X]. For instance, FO[<] is the set of star-free languages. The two different definitions of FO[<], in terms of logic and in terms of regular expressions, suggests that this class may be mathematically interesting beyond its role in computational complexity, and that methods from both logic and regular expressions may be useful in its study.



Datalog seems to be an example of this as it fits this profile. TauML seems to be going down this path. Finite model theory connects all the dots for those who want to aggressively dig deep into this subject because TML utilizing pfp is first order logic and finite model theory addresses this precisely.



References
----
1. https://en.wikipedia.org/wiki/Soundness#Logical_systems
2. [https://en.wikipedia.org/wiki/FO_(complexity)#Partial_fixed_point_is_PSPACE](https://en.wikipedia.org/wiki/FO_(complexity)#Partial_fixed_point_is_PSPACE)
3. https://en.wikipedia.org/wiki/PSPACE
4. https://github.com/idni/tau
5. https://en.wikipedia.org/wiki/Datalog
6. https://en.wikipedia.org/wiki/Trakhtenbrot%27s_theorem